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 "nondet_static.h"#include <util/prefix.h>#include <util/std_code.h>#include <goto-programs/goto_model.h>#include <linking/static_lifetime_init.h>#include <regex>
Include dependency graph for nondet_static.cpp: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... | |
| static void | nondet_static (const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name) |
| Nondeterministically initializes global scope variables in a goto-function. 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 &goto_model) |
| First main entry point of the module. More... | |
| void | nondet_static (goto_modelt &goto_model, const std::set< std::string > &except_values) |
| Second main entry point of the module. More... | |
| void | nondet_static_matching (goto_modelt &goto_model, const std::string ®ex) |
| Nondeterministically initializes global scope variables that match the given regex. More... | |
Detailed Description
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.cpp.
Function Documentation
◆ is_nondet_initializable_static()
| bool is_nondet_initializable_static | ( | const symbol_exprt & | symbol_expr, |
| const namespacet & | ns | ||
| ) |
See the return.
- Parameters
-
symbol_expr The symbol expression to analyze. ns Namespace for resolving type information
- Returns
- True if the symbol expression holds a static symbol which can be nondeterministically initialized, false otherwise.
Definition at line 36 of file nondet_static.cpp.
◆ nondet_static() [1/4]
| void nondet_static | ( | const namespacet & | ns, |
| goto_functionst & | goto_functions | ||
| ) |
Nondeterministically initializes global scope variables in CPROVER_initialize function.
- Parameters
-
ns Namespace for resolving type information. [out] goto_functions Existing goto-functions to be updated.
Definition at line 129 of file nondet_static.cpp.
◆ nondet_static() [2/4]
|
static |
Nondeterministically initializes global scope variables in a goto-function.
Iterates over instructions in the specified function and replaces all values assigned to nondet-initializable static variables with nondeterministic values.
- Parameters
-
ns Namespace for resolving type information. [out] goto_functions Existing goto-functions to be updated. fct_name Name of the goto-function to be updated.
Definition at line 82 of file nondet_static.cpp.
◆ nondet_static() [3/4]
| 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).
- Parameters
-
[out] goto_model Existing goto-model to be updated.
Definition at line 139 of file nondet_static.cpp.
◆ nondet_static() [4/4]
| 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.
- Parameters
-
[out] goto_model Existing goto-model to be updated. except_values list of symbol names that should not be updated.
Definition at line 151 of file nondet_static.cpp.
◆ nondet_static_matching()
| void nondet_static_matching | ( | goto_modelt & | goto_model, |
| const std::string & | regex | ||
| ) |
Nondeterministically initializes global scope variables that match the given regex.
- Parameters
-
[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 211 of file nondet_static.cpp.
