nondet_8h_source.html

 /*******************************************************************\


 Module: Non-deterministic object init and choice for JBMC


 Author: Diffblue Ltd.


 \*******************************************************************/


 #ifndef CPROVER_JAVA_BYTECODE_NONDET_H

 #define CPROVER_JAVA_BYTECODE_NONDET_H


 #include <util/std_code.h>


 class allocate_objectst;

 class symbol_table_baset;


 using allocate_local_symbolt =

   std::function<symbol_exprt(const typet &type, std::string)>;


 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);


 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);


 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);


 typedef std::vector<codet> alternate_casest;


 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);


 #endif // CPROVER_JAVA_BYTECODE_NONDET_H

allocate_objectst
Definition: allocate_objects.h:27

code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:130

dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38

exprt
Base class for all expressions.
Definition: expr.h:56

source_locationt
Definition: source_location.h:20

symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:131

symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:23

typet
The type of an expression, extends irept.
Definition: type.h:29

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:91

alternate_casest
std::vector< codet > alternate_casest
Definition: nondet.h:82

allocate_local_symbolt
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
Definition: nondet.h:18

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:15

mp_integer
BigInt mp_integer
Definition: smt_terms.h:17

std_code.h