CBMC
|
Nondeterministically initializes global scope variables, except for constants (such as string literals, final fields) and internal variables (such as CPROVER and symex variables, language specific internal variables). More...
#include <set>
#include <string>
Go to the source code of this file.
Functions | |
bool | is_nondet_initializable_static (const symbol_exprt &symbol_expr, const namespacet &ns) |
See the return. More... | |
void | nondet_static (goto_modelt &) |
First main entry point of the module. More... | |
void | nondet_static (goto_modelt &, const std::set< std::string > &) |
Second main entry point of the module. More... | |
void | nondet_static_matching (goto_modelt &, const std::string &) |
Nondeterministically initializes global scope variables that match the given regex. More... | |
Nondeterministically initializes global scope variables, except for constants (such as string literals, final fields) and internal variables (such as CPROVER and symex variables, language specific internal variables).
Definition in file nondet_static.h.
bool is_nondet_initializable_static | ( | const symbol_exprt & | symbol_expr, |
const namespacet & | ns | ||
) |
See the return.
symbol_expr | The symbol expression to analyze. |
ns | Namespace for resolving type information |
Definition at line 36 of file nondet_static.cpp.
void nondet_static | ( | goto_modelt & | goto_model | ) |
First main entry point of the module.
Nondeterministically initializes global scope variables, except for constants (such as string literals, final fields) and internal variables (such as CPROVER and symex variables, language specific internal variables).
[in,out] | goto_model | Existing goto-model to be updated. |
Definition at line 131 of file nondet_static.cpp.
void nondet_static | ( | goto_modelt & | goto_model, |
const std::set< std::string > & | except_values | ||
) |
Second main entry point of the module.
Nondeterministically initializes global scope variables, except for constants (such as string literals, final fields), internal variables (such as CPROVER and symex variables, language specific internal variables) and variables passed to except_value.
[out] | goto_model | Existing goto-model to be updated. |
except_values | list of symbol names that should not be updated. |
Definition at line 143 of file nondet_static.cpp.
void nondet_static_matching | ( | goto_modelt & | goto_model, |
const std::string & | regex | ||
) |
Nondeterministically initializes global scope variables that match the given regex.
[out] | goto_model | Existing goto-model to be updated. |
regex | regex for matching variables in the format "filename:variable" (same format as those of except_values in nondet_static(goto_model, except_values) variant above). |
Definition at line 203 of file nondet_static.cpp.