Skip to content

Commit b62bf01

Browse files
author
svorenova
committed
Make nondet-static check for ID_C_no_nondet_initialization
1 parent a50562e commit b62bf01

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
@@ -42,6 +42,14 @@ void nondet_static(
4242
if(has_prefix(id2string(sym.get_identifier()), CPROVER_PREFIX))
4343
continue;
4444

45+
// any other internal variable such as Java specific?
46+
if(
47+
ns.lookup(sym.get_identifier())
48+
.type.get_bool(ID_C_no_nondet_initialization))
49+
{
50+
continue;
51+
}
52+
4553
// static lifetime?
4654
if(!ns.lookup(sym.get_identifier()).is_static_lifetime)
4755
continue;

0 commit comments

Comments
 (0)