nondet_static.h File Reference

#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 (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 std::set< std::string > &)
	Second 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.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_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 34 of file nondet_static.cpp.

nondet_static() [1/3]

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

nondet_static() [2/3]

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

nondet_static() [3/3]

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