cprover
nondet.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Non-deterministic object init and choice for JBMC
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_JAVA_BYTECODE_NONDET_H
10 #define CPROVER_JAVA_BYTECODE_NONDET_H
11 
12 #include <util/std_code.h>
13 #include <util/std_expr.h>
14 #include <util/symbol_table.h>
15 
17  const mp_integer &min_value,
18  const mp_integer &max_value,
19  const std::string &name_prefix,
20  const typet &int_type,
21  const irep_idt &mode,
22  const source_locationt &source_location,
23  symbol_table_baset &symbol_table,
24  code_blockt &instructions);
25 
26 typedef std::vector<codet> alternate_casest;
27 
29  const irep_idt &name_prefix,
30  const alternate_casest &switch_cases,
31  const typet &int_type,
32  const irep_idt &mode,
33  const source_locationt &source_location,
34  symbol_table_baset &symbol_table);
35 
36 #endif // CPROVER_JAVA_BYTECODE_NONDET_H
The type of an expression, extends irept.
Definition: type.h:27
BigInt mp_integer
Definition: mp_arith.h:22
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).
Definition: nondet.cpp:36
API to expression classes.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Author: Diffblue Ltd.
The symbol table base class interface.
static mp_integer max_value(const typet &type)
Get max value for an integer type.
A codet representing sequential composition of program statements.
Definition: std_code.h:150
Expression to hold a symbol (variable)
Definition: std_expr.h:143
std::vector< codet > alternate_casest
Definition: nondet.h:26
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 &#39;switch_cases&#39;.
Definition: nondet.cpp:87