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 "std_code.h"
13 #include "std_expr.h"
14 
15 class allocate_objectst;
16 class symbol_table_baset;
17 
19  std::function<symbol_exprt(const typet &type, std::string)>;
20 
32  const exprt &min_value_expr,
33  const exprt &max_value_expr,
34  const std::string &basename_prefix,
35  const source_locationt &source_location,
36  allocate_objectst &allocate_objects,
37  code_blockt &instructions);
38 
40  const exprt &min_value_expr,
41  const exprt &max_value_expr,
42  const std::string &basename_prefix,
43  const source_locationt &source_location,
44  const allocate_local_symbolt &alocate_local_symbol,
45  code_blockt &instructions);
46 
66  const mp_integer &min_value,
67  const mp_integer &max_value,
68  const std::string &basename_prefix,
69  const typet &int_type,
70  const source_locationt &source_location,
71  allocate_objectst &allocate_objects,
72  code_blockt &instructions);
73 
74 typedef std::vector<codet> alternate_casest;
75 
87  const irep_idt &name_prefix,
88  const alternate_casest &switch_cases,
89  const typet &int_type,
90  const irep_idt &mode,
91  const source_locationt &source_location,
92  symbol_table_baset &symbol_table);
93 
94 #endif // CPROVER_JAVA_BYTECODE_NONDET_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
typet
The type of an expression, extends irept.
Definition: type.h:29
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
exprt
Base class for all expressions.
Definition: expr.h:53
generate_nondet_int
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,...
Definition: nondet.cpp:17
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
alternate_casest
std::vector< codet > alternate_casest
Definition: nondet.h:74
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
std_code.h
source_locationt
Definition: source_location.h:20
allocate_local_symbolt
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
Definition: nondet.h:19
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'.
Definition: nondet.cpp:93
allocate_objectst
Definition: allocate_objects.h:31
std_expr.h
API to expression classes.