Go to the source code of this file.
|
symbol_exprt | generate_nondet_int (const mp_integer &min_value, const mp_integer &max_value, const std::string &name_prefix, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table, 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...
|
|
◆ alternate_casest
◆ generate_nondet_int()
Gets a fresh nondet choice in range (min_value, max_value).
GOTO generated resembles:
- Parameters
-
min_value | Minimum value (inclusive) of returned int. |
max_value | Maximum value (inclusive) of returned int. |
name_prefix | Prefix for the fresh symbol name generated (should be function id) |
int_type | The type of the int used to non-deterministically choose one of the switch cases. |
mode | Mode (language) of the symbol to be generated. |
source_location | The location to mark the generated int with. |
symbol_table | The global symbol table. |
instructions | [out]: Output 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 36 of file nondet.cpp.
◆ generate_nondet_switch()
Pick nondeterministically between imperative actions 'switch_cases'.
- Parameters
-
name_prefix | Name prefix for fresh symbols (should be function id) |
switch_cases | List of codet objects to execute in each switch case. |
int_type | The type of the int used to non-deterministically choose one of the switch cases. |
mode | Mode (language) of the symbol to be generated. |
source_location | The location to mark the generated int with. |
symbol_table | The global symbol table. |
- Returns
- Returns a nondet-switch choosing between switch_cases. The resulting switch block has no default case.
Definition at line 87 of file nondet.cpp.