CBMC
nondet_static.h 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 <set>
#include <string>
+ Include dependency graph for nondet_static.h:
+ This graph shows which files directly or indirectly include this file:

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

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

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 36 of file nondet_static.cpp.

◆ nondet_static() [1/2]

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
[in,out]goto_modelExisting goto-model to be updated.

Definition at line 131 of file nondet_static.cpp.

◆ nondet_static() [2/2]

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_modelExisting goto-model to be updated.
except_valueslist of symbol names that should not be updated.

Definition at line 143 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_modelExisting goto-model to be updated.
regexregex 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.