Skip to content

Commit e606e4f

Browse files
committed
Fix for structs and nondet initialisation of pointers
1 parent 673e789 commit e606e4f

File tree

2 files changed

+6
-4
lines changed

2 files changed

+6
-4
lines changed

regression/cbmc/Initialization7/test.desc

Lines changed: 1 addition & 1 deletion
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

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -389,7 +389,9 @@ void value_sett::get_value_set_rec(
389389

390390
const typet &expr_type=ns.follow(expr.type());
391391

392-
if(expr.id()==ID_unknown || expr.id()==ID_invalid)
392+
if(
393+
expr.id() == ID_unknown || expr.id() == ID_invalid ||
394+
expr.id() == ID_nondet_symbol)
393395
{
394396
insert(dest, exprt(ID_unknown, original_type));
395397
}
@@ -1195,9 +1197,9 @@ void value_sett::assign(
11951197
"type:\n"+type.pretty();
11961198

11971199
rhs_member=make_member(rhs, name, ns);
1198-
1199-
assign(lhs_member, rhs_member, ns, false, add_to_sets);
12001200
}
1201+
1202+
assign(lhs_member, rhs_member, ns, false, add_to_sets);
12011203
}
12021204
}
12031205
else if(type.id()==ID_array)

0 commit comments

Comments
 (0)