File tree 1 file changed +8
-3
lines changed
1 file changed +8
-3
lines changed Original file line number Diff line number Diff line change 21
21
#include < util/pointer_offset_size.h>
22
22
#include < string.h>
23
23
24
- // / reads a memory address and loads it into the dest variable marks cell as
25
- // / read before written if cell has never been written
24
+ // / Reads a memory address and loads it into the ` dest` variable.
25
+ // / Marks cell as `READ_BEFORE_WRITTEN` if cell has never been written.
26
26
void interpretert::read (
27
27
const mp_integer &address,
28
28
mp_vectort &dest) const
@@ -102,7 +102,9 @@ void interpretert::clear_input_flags()
102
102
}
103
103
}
104
104
105
- // / \return Number of leaf primitive types; returns true on error
105
+ // / \param ty: a type
106
+ // / \param [out] result: Number of leaf primitive types in `ty`
107
+ // / \return returns true on error
106
108
bool interpretert::count_type_leaves (const typet &ty, mp_integer &result)
107
109
{
108
110
if (ty.id ()==ID_struct)
@@ -299,6 +301,9 @@ bool interpretert::memory_offset_to_byte_offset(
299
301
}
300
302
}
301
303
304
+ // / Evaluate an expression
305
+ // / \param expr: expression to evaluate
306
+ // / \param [out] dest: vector in which the result of the evaluation is stored
302
307
void interpretert::evaluate (
303
308
const exprt &expr,
304
309
mp_vectort &dest)
You can’t perform that action at this time.
0 commit comments