Skip to content

Commit 2249288

Browse files
committed
Use extended interpretation of "is constant"
1 parent c23e8ee commit 2249288

File tree

5 files changed

+11
-13
lines changed

5 files changed

+11
-13
lines changed
Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,8 @@
1-
FUTURE
1+
KNOWNBUG
22
main.c
3-
--constants --simplify out.gb
3+
--constants --verify
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$
6+
^\[main.assertion.1\] line 9 assertion a\[(\(signed( long)? long int\))?0\] == 0: FAILURE \(if reachable\)$
87
--
98
^warning: ignoring
Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
FUTURE
1+
CORE
22
main.c
33
--constants --verify
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.assertion.1\] file main.c line 10 function main, assertion a\[(\(signed( long)? long int\))?0\] == 2: FAILURE$
6+
^\[main.assertion.1\] line 10 assertion a\[(\(signed( long)? long int\))?0\] == 2: FAILURE \(if reachable\)$
77
--
88
^warning: ignoring
Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,8 @@
1-
FUTURE
1+
KNOWNBUG
22
main.c
3-
--constants --simplify out.gb
3+
--constants --verify
44
^EXIT=0$
55
^SIGNAL=0$
6-
^Simplified: assert: 1, assume: 0, goto: 0, assigns: 0, function calls: 0$
7-
^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 0, function calls: 0$
6+
^\[main.assertion.1\] line 9 assertion a\[(\(signed( long)? long int\))?0\] == 1: SUCCESS$
87
--
98
^warning: ignoring
Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
FUTURE
1+
CORE
22
main.c
33
--constants --verify
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.assertion.1\] file main.c line 9 function main, assertion a\[(\(signed( long)? long int\))?0\] == 2: FAILURE$
6+
^\[main.assertion.1\] line 9 assertion a\[(\(signed( long)? long int\))?0\] == 2: FAILURE \(if reachable\)$
77
--
88
^warning: ignoring

src/analyses/constant_propagator.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ void constant_propagator_domaint::assign_rec(
4747
exprt tmp=rhs;
4848
partial_evaluate(dest_values, tmp, ns);
4949

50-
if(tmp.is_constant())
50+
if(dest_values.is_constant(tmp))
5151
{
5252
DATA_INVARIANT(
5353
base_type_eq(ns.lookup(s).type, tmp.type(), ns),

0 commit comments

Comments
 (0)