Skip to content

Commit 7882421

Browse files
author
svorenova
committed
Make nondet-static check for ID_C_no_nondet_initialization_allowed
1 parent cac4945 commit 7882421

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

src/goto-instrument/nondet_static.cpp

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,14 @@ void nondet_static(
4646
if(!ns.lookup(sym.get_identifier()).is_static_lifetime)
4747
continue;
4848

49+
// should not be nondet-initialized, e.g., proprietary variables?
50+
if(
51+
ns.lookup(sym.get_identifier())
52+
.type.get_bool(ID_C_no_nondet_initialization_allowed))
53+
{
54+
continue;
55+
}
56+
4957
// constant?
5058
if(is_constant_or_has_constant_components(sym.type(), ns))
5159
continue;

0 commit comments

Comments
 (0)