cprover
nondet_static.cpp File Reference

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 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...
 
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...
 

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_exprThe symbol expression to analyze.
nsNamespace for resolving type information
Returns
True if the symbol expression holds a static symbol which can be nondeterministically initialized, false otherwise.

Definition at line 31 of file nondet_static.cpp.

◆ nondet_static() [1/3]

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.

Parameters
nsNamespace for resolving type information.
[out]goto_functionsExisting goto-functions to be updated.
fct_nameName of the goto-function to be updated.

Definition at line 71 of file nondet_static.cpp.

◆ nondet_static() [2/3]

void nondet_static ( const namespacet ns,
goto_functionst goto_functions 
)

Nondeterministically initializes global scope variables in CPROVER_initialize function.

Parameters
nsNamespace for resolving type information.
[out]goto_functionsExisting goto-functions to be updated.

Definition at line 118 of file nondet_static.cpp.

◆ nondet_static() [3/3]

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).

Parameters
[out]goto_modelExisting goto-model to be updated.

Definition at line 133 of file nondet_static.cpp.