cprover
|
#include "nondet_static.h"
#include <goto-programs/goto_model.h>
#include <linking/static_lifetime_init.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, 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) |
Main entry point of the module. 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.cpp.
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 31 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 118 of file nondet_static.cpp.
void nondet_static | ( | const namespacet & | ns, |
goto_functionst & | goto_functions, | ||
const irep_idt & | fct_name | ||
) |
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.
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 71 of file nondet_static.cpp.
void nondet_static | ( | goto_modelt & | goto_model | ) |
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 133 of file nondet_static.cpp.