Skip to content

Commit e098f86

Browse files
committed
Full slicing: fix bugs in handling array_equal
This statement has three operands, where the third holds the comparison result. Make sure value sets know about this statement.
1 parent 31f1b59 commit e098f86

File tree

4 files changed

+33
-10
lines changed

4 files changed

+33
-10
lines changed
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
main.c
3+
--full-slice
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^\[test_copy\.assertion\.4\] .* expected to fail: FAILURE$
7+
^\[test_unequal\.assertion\.1\] .* different sizes arrays are unequal: SUCCESS
8+
^\[test_unequal\.assertion\.2\] .* expected to fail: FAILURE
9+
^\[test_unequal\.assertion\.3\] .* different typed arrays are unequal: SUCCESS
10+
^\[test_unequal\.assertion\.4\] .* expected to fail: FAILURE
11+
^\[test_unequal\.assertion\.5\] .* expected to fail: FAILURE
12+
^\[test_unequal\.assertion\.6\] .* expected to fail: FAILURE
13+
^\*\* 5 of 14 failed
14+
^VERIFICATION FAILED$
15+
--
16+
^warning: ignoring
17+
--
18+
Verify the properties of various cprover array primitves

src/analyses/goto_rw.cpp

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -772,11 +772,14 @@ static void goto_rw_other(
772772
else if(statement == ID_array_equal)
773773
{
774774
// mark the dereferenced operands as being read
775-
for(const auto &op : code.operands())
776-
{
777-
rw_set.get_array_objects(
778-
function, target, rw_range_sett::get_modet::READ, op);
779-
}
775+
PRECONDITION(code.operands().size() == 3);
776+
rw_set.get_array_objects(
777+
function, target, rw_range_sett::get_modet::READ, code.op0());
778+
rw_set.get_array_objects(
779+
function, target, rw_range_sett::get_modet::READ, code.op1());
780+
// the third operand is the result
781+
rw_set.get_objects_rec(
782+
function, target, rw_range_sett::get_modet::LHS_W, code.op2());
780783
}
781784
else if(statement == ID_array_set)
782785
{

src/pointer-analysis/value_set.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1613,8 +1613,7 @@ void value_sett::apply_code_rec(
16131613
{
16141614
// can be ignored, we don't expect side effects here
16151615
}
1616-
else if(statement=="cpp_delete" ||
1617-
statement=="cpp_delete[]")
1616+
else if(statement == ID_cpp_delete || statement == ID_cpp_delete_array)
16181617
{
16191618
// does nothing
16201619
}
@@ -1651,6 +1650,9 @@ void value_sett::apply_code_rec(
16511650
else if(statement==ID_array_replace)
16521651
{
16531652
}
1653+
else if(statement == ID_array_equal)
1654+
{
1655+
}
16541656
else if(statement==ID_assume)
16551657
{
16561658
guard(to_code_assume(code).assumption(), ns);

src/pointer-analysis/value_set_fi.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1390,9 +1390,9 @@ void value_set_fit::apply_code(const codet &code, const namespacet &ns)
13901390
else if(statement==ID_fence)
13911391
{
13921392
}
1393-
else if(statement==ID_array_copy ||
1394-
statement==ID_array_replace ||
1395-
statement==ID_array_set)
1393+
else if(
1394+
statement == ID_array_copy || statement == ID_array_replace ||
1395+
statement == ID_array_set || statement == ID_array_equal)
13961396
{
13971397
}
13981398
else if(can_cast_expr<code_inputt>(code) || can_cast_expr<code_outputt>(code))

0 commit comments

Comments
 (0)