replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #2658 from svorenova/bugfix_tg4365 

[TG-2755] Add nondet-static option to JBMC and fix it for static initializers
This commit is contained in:
svorenova 2018-08-23 15:51:24 +01:00 committed by GitHub
parent 6749aaf1d8 e37d051c22
commit d68708f00e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
15 changed files with 446 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
jbmc/regression/jbmc/nondet-static/My$PInner.class Normal file
View File

Binary file not shown.

BIN
jbmc/regression/jbmc/nondet-static/My$PSInner.class Normal file
View File

Binary file not shown.

BIN
jbmc/regression/jbmc/nondet-static/My$PrInner.class Normal file
View File

Binary file not shown.

BIN
jbmc/regression/jbmc/nondet-static/My$PrSInner.class Normal file
View File

Binary file not shown.

BIN
jbmc/regression/jbmc/nondet-static/My.class Normal file
View File

Binary file not shown.

238
jbmc/regression/jbmc/nondet-static/My.java Normal file
View File

@ -0,0 +1,238 @@
public class My {
public static int val() { return 3; }
public static int p1;
public static int p2 = 1;
public static int p3;
static { p3 = 2; }
public static int p4 = val();
public static Integer p5 = new Integer(5);
public static final int pf1 = 1;
public static final int pf2;
static { pf2 = 2; }
public static final int pf3 = val();
public static final Integer pf4 = new Integer(4);
private static int pr1;
private static int pr2 = 1;
private static int pr3;
static { pr3 = 2; }
private static int pr4 = val();
private static Integer pr5 = new Integer(5);
private static final int prf1 = 1;
private static final int prf2;
static { prf2 = 2; }
private static final int prf3 = val();
private static final Integer prf4 = new Integer(4);
// for inner classes, the missing cases of the above fields do not compile
public class PInner {
public static final int pf1 = 1;
private static final int prf1 = 1;
}
public static class PSInner {
public static int p1;
public static int p2 = 1;
public static int p3;
static { p3 = 2; }
public static int p4 = val();
public static Integer p5 = new Integer(5);
public static final int pf1 = 1;
public static final int pf2;
static { pf2 = 2; }
public static final int pf3 = val();
public static final Integer pf4 = new Integer(4);
private static int pr1;
private static int pr2 = 1;
private static int pr3;
static { pr3 = 2; }
private static int pr4 = val();
private static Integer pr5 = new Integer(5);
private static final int prf1 = 1;
private static final int prf2;
static { prf2 = 2; }
private static final int prf3 = val();
private static final Integer prf4 = new Integer(4);
}
private class PrInner {
public static final int pf1 = 1;
private static final int prf1 = 1;
}
private static class PrSInner {
public static int p1;
public static int p2 = 1;
public static int p3;
static { p3 = 2; }
public static int p4 = val();
public static Integer p5 = new Integer(5);
public static final int pf1 = 1;
public static final int pf2;
static { pf2 = 2; }
public static final int pf3 = val();
public static final Integer pf4 = new Integer(4);
private static int pr1;
private static int pr2 = 1;
private static int pr3;
static { pr3 = 2; }
private static int pr4 = val();
private static Integer pr5 = new Integer(5);
private static final int prf1 = 1;
private static final int prf2;
static { prf2 = 2; }
private static final int prf3 = val();
private static final Integer prf4 = new Integer(4);
}
public int field;
public My(int i) {
String s = "bla";
field = i;
if (p1 != 0)
field = 108; // this line can only be covered with nondet-static
if (p2 != 1)
field = 108; // this line can only be covered with nondet-static
if (p3 != 2)
field = 108; // this line can only be covered with nondet-static
if (p4 != 3)
field = 108; // this line can only be covered with nondet-static
if (!p5.equals(5))
field = 108; // this line can only be covered with nondet-static
if (pf1 != 1)
field = 108; // this line cannot be covered even with nondet-static
if (pf2 != 2)
field = 108; // this line cannot be covered even with nondet-static
if (pf3 != 3)
field = 108; // this line cannot be covered even with nondet-static
if (!pf4.equals(4))
field = 108; // this line cannot be covered even with nondet-static
if (pr1 != 0)
field = 108; // this line can only be covered with nondet-static
if (pr2 != 1)
field = 108; // this line can only be covered with nondet-static
if (pr3 != 2)
field = 108; // this line can only be covered with nondet-static
if (pr4 != 3)
field = 108; // this line can only be covered with nondet-static
if (!pr5.equals(5))
field = 108; // this line can only be covered with nondet-static
if (prf1 != 1)
field = 108; // this line cannot be covered even with nondet-static
if (prf2 != 2)
field = 108; // this line cannot be covered even with nondet-static
if (prf3 != 3)
field = 108; // this line cannot be covered even with nondet-static
if (!prf4.equals(4))
field = 108; // this line cannot be covered even with nondet-static
if (PInner.pf1 != 1)
field = 108; // this line cannot be covered even with nondet-static
if (PInner.prf1 != 1)
field = 108; // this line cannot be covered even with nondet-static
if (PSInner.p1 != 0)
field = 108; // this line can only be covered with nondet-static
if (PSInner.p2 != 1)
field = 108; // this line can only be covered with nondet-static
if (PSInner.p3 != 2)
field = 108; // this line can only be covered with nondet-static
if (PSInner.p4 != 3)
field = 108; // this line can only be covered with nondet-static
if (!PSInner.p5.equals(5))
field = 108; // this line can only be covered with nondet-static
if (PSInner.pf1 != 1)
field = 108; // this line cannot be covered even with nondet-static
if (PSInner.pf2 != 2)
field = 108; // this line cannot be covered even with nondet-static
if (PSInner.pf3 != 3)
field = 108; // this line cannot be covered even with nondet-static
if (!PSInner.pf4.equals(4))
field = 108; // this line cannot be covered even with nondet-static
if (PSInner.pr1 != 0)
field = 108; // this line can only be covered with nondet-static
if (PSInner.pr2 != 1)
field = 108; // this line can only be covered with nondet-static
if (PSInner.pr3 != 2)
field = 108; // this line can only be covered with nondet-static
if (PSInner.pr4 != 3)
field = 108; // this line can only be covered with nondet-static
if (!PSInner.pr5.equals(5))
field = 108; // this line can only be covered with nondet-static
if (PSInner.prf1 != 1)
field = 108; // this line cannot be covered even with nondet-static
if (PSInner.prf2 != 2)
field = 108; // this line cannot be covered even with nondet-static
if (PSInner.prf3 != 3)
field = 108; // this line cannot be covered even with nondet-static
if (!PSInner.prf4.equals(4))
field = 108; // this line cannot be covered even with nondet-static
if (PrInner.pf1 != 1)
field = 108; // this line cannot be covered even with nondet-static
if (PrInner.prf1 != 1)
field = 108; // this line cannot be covered even with nondet-static
if (PrSInner.p1 != 0)
field = 108; // this line can only be covered with nondet-static
if (PrSInner.p2 != 1)
field = 108; // this line can only be covered with nondet-static
if (PrSInner.p3 != 2)
field = 108; // this line can only be covered with nondet-static
if (PrSInner.p4 != 3)
field = 108; // this line can only be covered with nondet-static
if (!PrSInner.p5.equals(5))
field = 108; // this line can only be covered with nondet-static
if (PrSInner.pf1 != 1)
field = 108; // this line cannot be covered even with nondet-static
if (PrSInner.pf2 != 2)
field = 108; // this line cannot be covered even with nondet-static
if (PrSInner.pf3 != 3)
field = 108; // this line cannot be covered even with nondet-static
if (!PrSInner.pf4.equals(4))
field = 108; // this line cannot be covered even with nondet-static
if (PrSInner.pr1 != 0)
field = 108; // this line can only be covered with nondet-static
if (PrSInner.pr2 != 1)
field = 108; // this line can only be covered with nondet-static
if (PrSInner.pr3 != 2)
field = 108; // this line can only be covered with nondet-static
if (PrSInner.pr4 != 3)
field = 108; // this line can only be covered with nondet-static
if (!PrSInner.pr5.equals(5))
field = 108; // this line can only be covered with nondet-static
if (PrSInner.prf1 != 1)
field = 108; // this line cannot be covered even with nondet-static
if (PrSInner.prf2 != 2)
field = 108; // this line cannot be covered even with nondet-static
if (PrSInner.prf3 != 3)
field = 108; // this line cannot be covered even with nondet-static
if (!PSInner.prf4.equals(4))
field = 108; // this line cannot be covered even with nondet-static
if (s != "bla")
field = 108; // this line cannot be covered even with nondet-static
}
}

70
jbmc/regression/jbmc/nondet-static/test.desc Normal file
View File

@ -0,0 +1,70 @@
CORE symex-driven-lazy-loading-expected-failure
My.class
--function "My.<init>" --cover location --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
^EXIT=0$
^SIGNAL=0$
file My\.java line 104 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 106 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 108 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 110 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 112 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 117 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 119 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 121 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 124 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 126 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 128 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 130 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 132 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 137 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 139 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 141 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 150 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 152 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 154 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 156 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 158 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 163 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 165 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 167 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 170 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 172 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 174 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 176 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 178 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 183 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 185 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 187 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 196 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 198 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 200 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 202 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 204 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 209 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 211 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 213 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 216 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 218 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 220 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 222 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 224 function java::My\.\<init\>:\(I\)V.*SATISFIED$
file My\.java line 229 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 231 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 233 function java::My\.\<init\>:\(I\)V.*FAILED$
file My\.java line 236 function java::My\.\<init\>:\(I\)V.*FAILED$
--
file My\.java line 115 function java::My\.\<init\>:\(I\)V
file My\.java line 135 function java::My\.\<init\>:\(I\)V
file My\.java line 144 function java::My\.\<init\>:\(I\)V
file My\.java line 147 function java::My\.\<init\>:\(I\)V
file My\.java line 161 function java::My\.\<init\>:\(I\)V
file My\.java line 181 function java::My\.\<init\>:\(I\)V
file My\.java line 190 function java::My\.\<init\>:\(I\)V
file My\.java line 193 function java::My\.\<init\>:\(I\)V
file My\.java line 207 function java::My\.\<init\>:\(I\)V
file My\.java line 227 function java::My\.\<init\>:\(I\)V
--
This tests nondet-static option
This fails under symex-driven lazy loading because nondet-static cannot be used
with it

2
jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
View File

@ -645,6 +645,8 @@ void java_bytecode_convert_classt::convert(
// link matches the method used by java_bytecode_convert_method::convert
// for methods.
new_symbol.type.set(ID_C_class, class_symbol.name);
new_symbol.type.set(ID_C_field, f.name);
new_symbol.type.set(ID_C_constant, f.is_final);
new_symbol.pretty_name=id2string(class_symbol.pretty_name)+
"."+id2string(f.name);
new_symbol.mode=ID_java;

15
jbmc/src/java_bytecode/java_bytecode_language.cpp
View File

@ -157,6 +157,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
else
java_cp_include_files=".*";
nondet_static = cmd.isset("nondet-static");
language_options_initialized=true;
}
@ -1039,9 +1041,18 @@ bool java_bytecode_languaget::convert_single_method(
case synthetic_method_typet::STATIC_INITIALIZER_WRAPPER:
if(threading_support)
symbol.value = get_thread_safe_clinit_wrapper_body(
function_id, symbol_table);
function_id,
symbol_table,
nondet_static,
object_factory_parameters,
get_pointer_type_selector());
else
symbol.value = get_clinit_wrapper_body(function_id, symbol_table);
symbol.value = get_clinit_wrapper_body(
function_id,
symbol_table,
nondet_static,
object_factory_parameters,
get_pointer_type_selector());
break;
case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:
symbol.value =

1
jbmc/src/java_bytecode/java_bytecode_language.h
View File

@ -193,6 +193,7 @@ protected:
bool throw_assertion_error;
java_string_library_preprocesst string_preprocess;
std::string java_cp_include_files;
bool nondet_static;
// list of classes to force load even without reference from the entry point
std::vector<irep_idt> java_load_classes;

120
jbmc/src/java_bytecode/java_static_initializers.cpp
View File

@ -180,14 +180,25 @@ gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
/// Generates codet that iterates through the base types of the class specified
/// by class_name, C, and recursively adds calls to their clinit wrapper.
/// Finally a call to the clinint wrapper of C is made.
/// Finally a call to the clinit of C is made. If nondet-static option was
/// given then all static variables that are not constants (i.e. final) are
/// then re-assigned to a nondet value.
/// \param symbol_table: symbol table
/// \param class_name: name of the class to generate clinit wrapper calls for
/// \param [out] init_body: appended with calls to clinit wrapper
/// \param nondet_static: true if nondet-static option was given
/// \param object_factory_parameters: object factory parameters used to populate
/// nondet-initialized globals and objects reachable from them (only needed
/// if nondet-static is true)
/// \param pointer_type_selector: used to choose concrete types for abstract-
/// typed globals and fields (only needed if nondet-static is true)
static void clinit_wrapper_do_recursive_calls(
const symbol_tablet &symbol_table,
symbol_table_baset &symbol_table,
const irep_idt &class_name,
code_blockt &init_body)
code_blockt &init_body,
const bool nondet_static,
const object_factory_parameterst &object_factory_parameters,
const select_pointer_typet &pointer_type_selector)
{
const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
for(const auto &base : to_class_type(class_symbol.type).bases())
@ -210,6 +221,52 @@ static void clinit_wrapper_do_recursive_calls(
call_real_init.function() = find_sym_it->second.symbol_expr();
init_body.move_to_operands(call_real_init);
}
// If nondet-static option is given, add a standard nondet initialization for
// each non-final static field of this class. Note this is the same invocation
// used in get_stub_initializer_body and java_static_lifetime_init.
if(nondet_static)
{
object_factory_parameterst parameters = object_factory_parameters;
parameters.function_id = clinit_wrapper_name(class_name);
std::vector<irep_idt> nondet_ids;
std::for_each(
symbol_table.symbols.begin(),
symbol_table.symbols.end(),
[&](const std::pair<irep_idt, symbolt> &symbol) {
if(
symbol.second.type.get(ID_C_class) == class_name &&
symbol.second.is_static_lifetime &&
!symbol.second.type.get_bool(ID_C_constant))
{
nondet_ids.push_back(symbol.first);
}
});
for(const auto &id : nondet_ids)
{
const symbol_exprt new_global_symbol =
symbol_table.lookup_ref(id).symbol_expr();
parameters.max_nonnull_tree_depth =
is_non_null_library_global(id)
? std::max(
size_t(1), object_factory_parameters.max_nonnull_tree_depth)
: object_factory_parameters.max_nonnull_tree_depth;
gen_nondet_init(
new_global_symbol,
init_body,
symbol_table,
source_locationt(),
false,
allocation_typet::DYNAMIC,
parameters,
pointer_type_selector,
update_in_placet::NO_UPDATE_IN_PLACE);
}
}
}
/// Checks whether a static initializer wrapper is needed for a given class,
@ -316,9 +373,9 @@ static void create_clinit_wrapper_symbols(
"clinit wrapper");
}
/// Thread safe version of the static initialiser.
/// Thread safe version of the static initializer.
///
/// Produces the static initialiser wrapper body for the given function. This
/// Produces the static initializer wrapper body for the given function. This
/// static initializer implements (a simplification of) the algorithm defined
/// in Section 5.5 of the JVM Specs. This function, or wrapper, checks whether
/// static init has already taken place, calls the actual `<clinit>` method if
@ -365,7 +422,8 @@ static void create_clinit_wrapper_symbols(
/// // ...
/// java::In::clinit_wrapper();
///
/// java::C::<clinit>();
/// java::C::<clinit>(); // or nondet-initialization of all static
/// // variables of C if nondet-static is true
///
/// // Setting this variable to INIT_COMPLETE will let other threads "cross"
/// // beyond the assume() statement above in this function.
@ -382,10 +440,19 @@ static void create_clinit_wrapper_symbols(
/// \param function_id: clinit wrapper function id (the wrapper_method_symbol
/// name created by `create_clinit_wrapper_symbols`)
/// \param symbol_table: global symbol table
/// \return the body of the static initialiser wrapper
/// \param nondet_static: true if nondet-static option was given
/// \param object_factory_parameters: object factory parameters used to populate
/// nondet-initialized globals and objects reachable from them (only needed
/// if nondet-static is true)
/// \param pointer_type_selector: used to choose concrete types for abstract-
/// typed globals and fields (only needed if nondet-static is true)
/// \return the body of the static initializer wrapper
codet get_thread_safe_clinit_wrapper_body(
const irep_idt &function_id,
symbol_table_baset &symbol_table)
symbol_table_baset &symbol_table,
const bool nondet_static,
const object_factory_parameterst &object_factory_parameters,
const select_pointer_typet &pointer_type_selector)
{
const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
@ -532,11 +599,18 @@ codet get_thread_safe_clinit_wrapper_body(
// // ...
// java::In::clinit_wrapper();
//
// java::C::<clinit>();
// java::C::<clinit>(); // or nondet-initialization of all static
// // variables of C if nondet-static is true
//
{
code_blockt init_body;
clinit_wrapper_do_recursive_calls(symbol_table, class_name, init_body);
clinit_wrapper_do_recursive_calls(
symbol_table,
class_name,
init_body,
nondet_static,
object_factory_parameters,
pointer_type_selector);
function_body.append(init_body);
}
@ -557,15 +631,24 @@ codet get_thread_safe_clinit_wrapper_body(
return function_body;
}
/// Produces the static initialiser wrapper body for the given function.
/// Produces the static initializer wrapper body for the given function.
/// Note: this version of the clinit wrapper is not thread safe.
/// \param function_id: clinit wrapper function id (the wrapper_method_symbol
/// name created by `create_clinit_wrapper_symbols`)
/// \param symbol_table: global symbol table
/// \return the body of the static initialiser wrapper/
/// \param nondet_static: true if nondet-static option was given
/// \param object_factory_parameters: object factory parameters used to populate
/// nondet-initialized globals and objects reachable from them (only needed
/// if nondet-static is true)
/// \param pointer_type_selector: used to choose concrete types for abstract-
/// typed globals and fields (only needed if nondet-static is true)
/// \return the body of the static initializer wrapper
codet get_clinit_wrapper_body(
const irep_idt &function_id,
symbol_table_baset &symbol_table)
symbol_table_baset &symbol_table,
const bool nondet_static,
const object_factory_parameterst &object_factory_parameters,
const select_pointer_typet &pointer_type_selector)
{
// Assume that class C extends class C' and implements interfaces
// I1, ..., In. We now create the following function (possibly recursively
@ -583,7 +666,8 @@ codet get_clinit_wrapper_body(
// // ...
// java::In::clinit_wrapper();
//
// java::C::<clinit>();
// java::C::<clinit>(); // or nondet-initialization of all static
// // variables of C if nondet-static is true
// }
// }
const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
@ -609,7 +693,13 @@ codet get_clinit_wrapper_body(
code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
init_body.move_to_operands(set_already_run);
clinit_wrapper_do_recursive_calls(symbol_table, class_name, init_body);
clinit_wrapper_do_recursive_calls(
symbol_table,
class_name,
init_body,
nondet_static,
object_factory_parameters,
pointer_type_selector);
wrapper_body.then_case() = init_body;

10
jbmc/src/java_bytecode/java_static_initializers.h
View File

@ -29,11 +29,17 @@ void create_static_initializer_wrappers(
codet get_thread_safe_clinit_wrapper_body(
const irep_idt &function_id,
symbol_table_baset &symbol_table);
symbol_table_baset &symbol_table,
const bool nondet_static,
const object_factory_parameterst &object_factory_parameters,
const select_pointer_typet &pointer_type_selector);
codet get_clinit_wrapper_body(
const irep_idt &function_id,
symbol_table_baset &symbol_table);
symbol_table_baset &symbol_table,
const bool nondet_static,
const object_factory_parameterst &object_factory_parameters,
const select_pointer_typet &pointer_type_selector);
class stub_global_initializer_factoryt
{

7
jbmc/src/jbmc/jbmc_parse_options.cpp
View File

@ -124,6 +124,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
if(cmdline.isset("cover"))
parse_cover_options(cmdline, options);
if(cmdline.isset("nondet-static"))
options.set_option("nondet-static", true);
if(cmdline.isset("no-simplify"))
options.set_option("simplify", false);
@ -1095,6 +1098,10 @@ void jbmc_parse_optionst::help()
" will be restricted to loaded methods in this case,\n" // NOLINT(*)
" and only output after the symex phase.\n"
"\n"
"Semantic transformations:\n"
// NOLINTNEXTLINE(whitespace/line_length)
" --nondet-static add nondeterministic initialization of variables with static lifetime\n"
"\n"
"BMC options:\n"
HELP_BMC
"\n"

1
jbmc/src/jbmc/jbmc_parse_options.h
View File

@ -67,6 +67,7 @@ class optionst;
"(drop-unused-functions)" \
"(property):(stop-on-fail)(trace)" \
"(verbosity):" \
"(nondet-static)" \
"(version)" \
"(cover):(symex-coverage-report):" \
OPT_TIMESTAMP \

1
src/util/irep_ids.def
View File

@ -351,6 +351,7 @@ IREP_ID_TWO(power, **)
IREP_ID_ONE(factorial_power)
IREP_ID_ONE(pretty_name)
IREP_ID_TWO(C_class, #class)
IREP_ID_TWO(C_field, #field)
IREP_ID_TWO(C_interface, #interface)
IREP_ID_ONE(event)
IREP_ID_ONE(designated_initializer)