Skip to content

Commit a44e6ea

Browse files
author
svorenova
committed
Make nondet-static check for ID_C_no_nondet_initialization_allowed
1 parent 7c0f770 commit a44e6ea

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

src/goto-instrument/nondet_static.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,12 @@ 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+
continue;
54+
4955
// constant?
5056
if(is_constant_or_has_constant_components(sym.type(), ns))
5157
continue;

0 commit comments

Comments
 (0)