File tree Expand file tree Collapse file tree 2 files changed +8
-2
lines changed
src/goto-instrument/contracts Expand file tree Collapse file tree 2 files changed +8
-2
lines changed Original file line number Diff line number Diff line change @@ -26,7 +26,8 @@ assigns_clause_targett::assigns_clause_targett(
26
26
contract(contract),
27
27
init_block(),
28
28
log(log_parameter),
29
- local_target(typet())
29
+ local_target(typet()),
30
+ target_id(object_ptr.id())
30
31
{
31
32
INVARIANT (
32
33
pointer_object.type ().id () == ID_pointer,
@@ -74,6 +75,11 @@ exprt assigns_clause_targett::alias_expression(const exprt &lhs)
74
75
return conjunction (condition);
75
76
}
76
77
78
+ if (target_id == ID_dereference)
79
+ {
80
+ return conjunction (condition);
81
+ }
82
+
77
83
const exprt lhs_offset = pointer_offset (lhs_ptr);
78
84
const exprt target_offset = pointer_offset (target);
79
85
Original file line number Diff line number Diff line change @@ -16,7 +16,6 @@ Date: July 2021
16
16
17
17
#include " contracts.h"
18
18
19
- #include < ansi-c/expr2c.h>
20
19
#include < util/pointer_offset_size.h>
21
20
22
21
// / \brief A base class for assigns clause targets
@@ -48,6 +47,7 @@ class assigns_clause_targett
48
47
goto_programt init_block;
49
48
messaget &log;
50
49
symbol_exprt local_target;
50
+ const irep_idt &target_id;
51
51
};
52
52
53
53
class assigns_clauset
You can’t perform that action at this time.
0 commit comments