CBMC
nondet.cpp File Reference
+ Include dependency graph for nondet.cpp:

Go to the source code of this file.

Functions

symbol_exprt generate_nondet_int (const exprt &min_value_expr, const exprt &max_value_expr, const std::string &basename_prefix, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions)
 Same as generate_nondet_int( const mp_integer &min_value, const mp_integer &max_value, const std::string &name_prefix, const typet &int_type, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions) except the minimum and maximum values are represented as exprts. More...
 
symbol_exprt generate_nondet_int (const exprt &min_value_expr, const exprt &max_value_expr, const std::string &basename_prefix, const source_locationt &source_location, const allocate_local_symbolt &alocate_local_symbol, code_blockt &instructions)
 Same as generate_nondet_int( const mp_integer &min_value, const mp_integer &max_value, const std::string &name_prefix, const typet &int_type, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions) except the minimum and maximum values are represented as exprts, and symbols are allocated using allocate_local_symbolt. More...
 
symbol_exprt generate_nondet_int (const mp_integer &min_value, const mp_integer &max_value, const std::string &basename_prefix, const typet &int_type, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions)
 Gets a fresh nondet choice in range (min_value, max_value). More...
 
code_blockt generate_nondet_switch (const irep_idt &name_prefix, const alternate_casest &switch_cases, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table)
 Pick nondeterministically between imperative actions 'switch_cases'. More...
 

Function Documentation

◆ generate_nondet_int() [1/3]

symbol_exprt generate_nondet_int ( const exprt min_value_expr,
const exprt max_value_expr,
const std::string &  basename_prefix,
const source_locationt source_location,
allocate_objectst allocate_objects,
code_blockt instructions 
)

Same as generate_nondet_int( const mp_integer &min_value, const mp_integer &max_value, const std::string &name_prefix, const typet &int_type, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions) except the minimum and maximum values are represented as exprts.

Definition at line 15 of file nondet.cpp.

◆ generate_nondet_int() [2/3]

symbol_exprt generate_nondet_int ( const exprt min_value_expr,
const exprt max_value_expr,
const std::string &  basename_prefix,
const source_locationt source_location,
const allocate_local_symbolt alocate_local_symbol,
code_blockt instructions 
)

Same as generate_nondet_int( const mp_integer &min_value, const mp_integer &max_value, const std::string &name_prefix, const typet &int_type, const source_locationt &source_location, allocate_objectst &allocate_objects, code_blockt &instructions) except the minimum and maximum values are represented as exprts, and symbols are allocated using allocate_local_symbolt.

Definition at line 38 of file nondet.cpp.

◆ generate_nondet_int() [3/3]

symbol_exprt generate_nondet_int ( const mp_integer min_value,
const mp_integer max_value,
const std::string &  basename_prefix,
const typet int_type,
const source_locationt source_location,
allocate_objectst allocate_objects,
code_blockt instructions 
)

Gets a fresh nondet choice in range (min_value, max_value).

GOTO generated resembles:

int_type name_prefix::nondet_int = NONDET(int_type)
ASSUME(name_prefix::nondet_int >= min_value)
ASSUME(name_prefix::nondet_int <= max_value)
@ ASSUME
Definition: goto_program.h:35
Parameters
min_valueMinimum value (inclusive) of returned int.
max_valueMaximum value (inclusive) of returned int.
basename_prefixBasename prefix for the fresh symbol name generated.
int_typeThe type of the int used to non-deterministically choose one of the switch cases.
allocate_objectsHandles allocation of new objects.
source_locationThe location to mark the generated int with.
[out]instructionsOutput instructions are written to 'instructions'. These declare, nondet-initialise and range-constrain (with assume statements) a fresh integer.
Returns
Returns a symbol expression for the resulting integer.

Definition at line 72 of file nondet.cpp.

◆ generate_nondet_switch()

code_blockt generate_nondet_switch ( const irep_idt name_prefix,
const alternate_casest switch_cases,
const typet int_type,
const irep_idt mode,
const source_locationt source_location,
symbol_table_baset symbol_table 
)

Pick nondeterministically between imperative actions 'switch_cases'.

Parameters
name_prefixName prefix for fresh symbols (should be function id)
switch_casesList of codet objects to execute in each switch case.
int_typeThe type of the int used to non-deterministically choose one of the switch cases.
modeMode (language) of the symbol to be generated.
source_locationThe location to mark the generated int with.
symbol_tableThe global symbol table.
Returns
Returns a nondet-switch choosing between switch_cases. The resulting switch block has no default case.

Definition at line 91 of file nondet.cpp.