1414#include < util/std_expr.h>
1515#include < util/std_types.h>
1616
17- // / Function: constant_pointer_abstract_objectt::constant_pointer_abstract_objectt
18- // /
1917// / \param type: the type the abstract_object is representing
2018constant_pointer_abstract_objectt::constant_pointer_abstract_objectt (
2119 const typet &t)
@@ -24,8 +22,6 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
2422 PRECONDITION (t.id () == ID_pointer);
2523}
2624
27- // / Function: constant_pointer_abstract_objectt::constant_pointer_abstract_objectt
28- // /
2925// / \param type: the type the abstract_object is representing
3026// / \param top: is the abstract_object starting as top
3127// / \param bottom: is the abstract_object starting as bottom
@@ -41,18 +37,15 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
4137 PRECONDITION (t.id () == ID_pointer);
4238}
4339
44- // / Function: constant_pointer_abstract_objectt::constant_pointer_abstract_objectt
45- // /
4640// / \param old: the abstract object to copy from
4741constant_pointer_abstract_objectt::constant_pointer_abstract_objectt (
4842 const constant_pointer_abstract_objectt &old)
4943 : pointer_abstract_objectt(old), value_stack(old.value_stack)
5044{
5145}
5246
53- // / Function: constant_pointer_abstract_objectt::constant_pointer_abstract_objectt
54- // /
55- // / \param expr: the expression to use as the starting pointer for an abstract object
47+ // / \param expr: the expression to use as the starting pointer for
48+ // / an abstract object
5649constant_pointer_abstract_objectt::constant_pointer_abstract_objectt (
5750 const exprt &e,
5851 const abstract_environmentt &environment,
@@ -70,17 +63,14 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
7063 clear_top ();
7164 }
7265}
73-
74- // / Function: constant_pointer_abstract_objectt::merge
75- // /
76- // / \param other: the pointer being merged
77- // /
78- // / \return Returns the result of the merge.
79- // /
8066// / Set this abstract object to be the result of merging this
8167// / abstract object. This calls the merge_constant_pointers if
8268// / we are trying to merge a constant pointer we use the constant pointer
8369// / constant pointer merge
70+ // /
71+ // / \param other: the pointer being merged
72+ // /
73+ // / \return Returns the result of the merge.
8474abstract_object_pointert
8575constant_pointer_abstract_objectt::merge (abstract_object_pointert other) const
8676{
@@ -97,16 +87,14 @@ constant_pointer_abstract_objectt::merge(abstract_object_pointert other) const
9787 }
9888}
9989
100- // / Function: constant_pointer_abstract_objectt::merge_constant_pointers
90+ // / Merges two constant pointers. If they are pointing at the same
91+ // / value, we merge, otherwise we set to top.
10192// /
10293// / \param other: the pointer being merged
10394// /
10495// / \return Returns a new abstract object that is the result of the merge
10596// / unless the merge is the same as this abstract object, in which
10697// / case it returns this.
107- // /
108- // / Merges two constant pointers. If they are pointing at the same
109- // / value, we merge, otherwise we set to top.
11098abstract_object_pointert
11199constant_pointer_abstract_objectt::merge_constant_pointers (
112100 const constant_pointer_abstract_pointert other) const
@@ -131,7 +119,7 @@ constant_pointer_abstract_objectt::merge_constant_pointers(
131119 }
132120}
133121
134- // / Function: constant_pointer_abstract_objectt::to_constant
122+ // / To try and find a constant expression for this abstract object
135123// /
136124// / \return Returns an expression representing the value if it can.
137125// / Returns a nil expression if it can be more than one value.
@@ -140,7 +128,6 @@ constant_pointer_abstract_objectt::merge_constant_pointers(
140128// / result of to_constant called on whatever abstract object this
141129// / pointer is pointing to.
142130// /
143- // / To try and find a constant expression for this abstract object
144131exprt constant_pointer_abstract_objectt::to_constant () const
145132{
146133 if (is_top () || is_bottom ())
@@ -155,14 +142,12 @@ exprt constant_pointer_abstract_objectt::to_constant() const
155142 }
156143}
157144
158- // / Function: constant_pointer_abstract_objectt::output
145+ // / Print the value of the pointer. Either NULL if nullpointer or
146+ // / ptr -> ( output of what the pointer is pointing to).
159147// /
160148// / \param out: the stream to write to
161149// / \param ai: ?
162150// / \param ns: ?
163- // /
164- // / Print the value of the pointer. Either NULL if nullpointer or
165- // / ptr -> ( output of what the pointer is pointing to).
166151void constant_pointer_abstract_objectt::output (
167152 std::ostream &out,
168153 const ai_baset &ai,
@@ -206,17 +191,15 @@ void constant_pointer_abstract_objectt::output(
206191 }
207192}
208193
209- // / Function: constant_pointer_abstract_objectt::read_dereference
194+ // / A helper function to dereference a value from a pointer. Providing
195+ // / the pointer can only be pointing at one thing, returns an abstract
196+ // / object representing that thing. If null or top will return top.
210197// /
211198// / \param env: the environment
212199// / \param ns: the namespace
213200// /
214201// / \return An abstract object representing the value this pointer is pointing
215202// / to
216- // /
217- // / A helper function to dereference a value from a pointer. Providing
218- // / the pointer can only be pointing at one thing, returns an abstract
219- // / object representing that thing. If null or top will return top.
220203abstract_object_pointert constant_pointer_abstract_objectt::read_dereference (
221204 const abstract_environmentt &env,
222205 const namespacet &ns) const
@@ -235,25 +218,23 @@ abstract_object_pointert constant_pointer_abstract_objectt::read_dereference(
235218 }
236219}
237220
238- // / Function: constant_pointer_abstract_objectt::write_dereference
221+ // / A helper function to evaluate writing to a pointers value.
222+ // / If the pointer can only be pointing to one element that it overwrites
223+ // / that element (or merges if merging_write) with the new value.
224+ // / If don't know what we are pointing to, we delegate to the parent.
239225// /
240226// / \param environment: the environment
241227// / \param ns: the namespace
242228// / \param stack: the remaining stack
243229// / \param new_value: the value to write to the dereferenced pointer
244230// / \param merging_write: is it a merging write (i.e. we aren't certain
245231// / we are writing to this particular pointer therefore
246- // / the value should be merged with whatever is already there
247- // / or we are certain we are writing to this pointer so
248- // / therefore the value can be replaced
232+ // / the value should be merged with whatever is already
233+ // / there or we are certain we are writing to this pointer
234+ // / so therefore the value can be replaced
249235// /
250236// / \return A modified abstract object representing this pointer after it
251237// / has been written to.
252- // /
253- // / A helper function to evaluate writing to a pointers value.
254- // / If the pointer can only be pointing to one element that it overwrites
255- // / that element (or merges if merging_write) with the new value.
256- // / If don't know what we are pointing to, we delegate to the parent.
257238sharing_ptrt<pointer_abstract_objectt>
258239constant_pointer_abstract_objectt::write_dereference (
259240 abstract_environmentt &environment,
0 commit comments