Skip to content

Commit fd6154b

Browse files
committed
Use constant propagation to dereference left-hand sides
We still fall back to setting values to top if dereferencing fails.
1 parent 446cf4c commit fd6154b

File tree

3 files changed

+28
-4
lines changed

3 files changed

+28
-4
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int x;
6+
int *p = &x;
7+
*p = 42;
8+
assert(x == 42);
9+
return 0;
10+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--constants --verify
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.assertion.1\] file main.c line 8 function main, assertion x == 42: SUCCESS$
7+
--
8+
^warning: ignoring

src/analyses/constant_propagator.cpp

+10-4
Original file line numberDiff line numberDiff line change
@@ -38,12 +38,18 @@ void constant_propagator_domaint::assign_rec(
3838
{
3939
if(lhs.id() == ID_dereference)
4040
{
41-
const bool have_dirty = (cp != nullptr);
41+
exprt eval_lhs = lhs;
42+
if(partial_evaluate(dest_values, eval_lhs, ns))
43+
{
44+
const bool have_dirty = (cp != nullptr);
4245

43-
if(have_dirty)
44-
dest_values.set_dirty_to_top(cp->dirty, ns);
46+
if(have_dirty)
47+
dest_values.set_dirty_to_top(cp->dirty, ns);
48+
else
49+
dest_values.set_to_top();
50+
}
4551
else
46-
dest_values.set_to_top();
52+
assign_rec(dest_values, eval_lhs, rhs, ns, cp);
4753
}
4854
else if(lhs.id() == ID_index)
4955
{

0 commit comments

Comments
 (0)