Skip to content

Commit 2262960

Browse files
committed
Fix for structs and nondet initialisation of pointers
1 parent c445f51 commit 2262960

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
@@ -487,7 +487,9 @@ void value_sett::get_value_set_rec(
487487

488488
const typet &expr_type=ns.follow(expr.type());
489489

490-
if(expr.id()==ID_unknown || expr.id()==ID_invalid)
490+
if(expr.id()==ID_unknown ||
491+
expr.id()==ID_invalid ||
492+
expr.id()==ID_nondet_symbol)
491493
{
492494
insert(dest, exprt(ID_unknown, original_type));
493495
}
@@ -1294,9 +1296,9 @@ void value_sett::assign(
12941296
"type:\n"+type.pretty();
12951297

12961298
rhs_member=make_member(rhs, name, ns);
1297-
1298-
assign(lhs_member, rhs_member, ns, is_simplified, add_to_sets);
12991299
}
1300+
1301+
assign(lhs_member, rhs_member, ns, is_simplified, add_to_sets);
13001302
}
13011303
}
13021304
else if(type.id()==ID_array)

0 commit comments

Comments
 (0)