cprover
Loading...
Searching...
No Matches
nondet.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Non-deterministic object init and choice for JBMC
4
5Author: 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
16
18 std::function<symbol_exprt(const typet &type, std::string)>;
19
31 const exprt &min_value_expr,
32 const exprt &max_value_expr,
33 const std::string &basename_prefix,
34 const source_locationt &source_location,
35 allocate_objectst &allocate_objects,
36 code_blockt &instructions);
37
39 const exprt &min_value_expr,
40 const exprt &max_value_expr,
41 const std::string &basename_prefix,
42 const source_locationt &source_location,
43 const allocate_local_symbolt &alocate_local_symbol,
44 code_blockt &instructions);
45
65 const mp_integer &min_value,
66 const mp_integer &max_value,
67 const std::string &basename_prefix,
68 const typet &int_type,
69 const source_locationt &source_location,
70 allocate_objectst &allocate_objects,
71 code_blockt &instructions);
72
73typedef std::vector<codet> alternate_casest;
74
86 const irep_idt &name_prefix,
87 const alternate_casest &switch_cases,
88 const typet &int_type,
89 const irep_idt &mode,
90 const source_locationt &source_location,
91 symbol_table_baset &symbol_table);
92
93#endif // CPROVER_JAVA_BYTECODE_NONDET_H
A codet representing sequential composition of program statements.
Definition: std_code.h:130
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table base class interface.
The type of an expression, extends irept.
Definition: type.h:29
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
std::vector< codet > alternate_casest
Definition: nondet.h:73
std::function< symbol_exprt(const typet &type, std::string)> allocate_local_symbolt
Definition: nondet.h:18
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
BigInt mp_integer
Definition: smt_terms.h:12