Skip to content

Commit 2775f9e

Browse files
committed
Fix for structs and nondet initialisation of pointers
1 parent abde3ee commit 2775f9e

File tree

2 files changed

+6
-4
lines changed

2 files changed

+6
-4
lines changed

regression/cbmc/Initialization7/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=10$

src/pointer-analysis/value_set.cpp

+5-3
Original file line numberDiff line numberDiff line change
@@ -358,7 +358,9 @@ void value_sett::get_value_set_rec(
358358

359359
const typet &expr_type=ns.follow(expr.type());
360360

361-
if(expr.id()==ID_unknown || expr.id()==ID_invalid)
361+
if(
362+
expr.id() == ID_unknown || expr.id() == ID_invalid ||
363+
expr.id() == ID_nondet_symbol)
362364
{
363365
insert(dest, exprt(ID_unknown, original_type));
364366
}
@@ -1138,9 +1140,9 @@ void value_sett::assign(
11381140
"type:\n"+type.pretty();
11391141

11401142
rhs_member=make_member(rhs, name, ns);
1141-
1142-
assign(lhs_member, rhs_member, ns, is_simplified, add_to_sets);
11431143
}
1144+
1145+
assign(lhs_member, rhs_member, ns, is_simplified, add_to_sets);
11441146
}
11451147
}
11461148
else if(type.id()==ID_array)

0 commit comments

Comments
 (0)