cprover
|
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 <util/options.h>
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 (const namespacet &ns, goto_functionst &goto_functions) |
Nondeterministically initializes global scope variables in CPROVER_initialize function. More... | |
void | nondet_static (goto_modelt &) |
First main entry point of the module. More... | |
void | nondet_static (goto_modelt &, const optionst::value_listt &) |
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 33 of file nondet_static.cpp.
void nondet_static | ( | const namespacet & | ns, |
goto_functionst & | goto_functions | ||
) |
Nondeterministically initializes global scope variables in CPROVER_initialize function.
ns | Namespace for resolving type information. | |
[out] | goto_functions | Existing goto-functions to be updated. |
Definition at line 128 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).
[out] | goto_model | Existing goto-model to be updated. |
Definition at line 138 of file nondet_static.cpp.
void nondet_static | ( | goto_modelt & | , |
const optionst::value_listt & | |||
) |