cprover
|
#include "nondet.h"
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/fresh_symbol.h>
#include <util/symbol.h>
Go to the source code of this file.
Functions | |
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... | |
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).
GOTO generated resembles:
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. |
Definition at line 36 of file nondet.cpp.
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'.
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. |
Definition at line 87 of file nondet.cpp.