11 #include <unordered_set> 34 const std::string &prefix=
"tmp_object_factory")
71 const typet &target_type,
72 bool create_dynamic_objects);
77 const exprt &max_length_expr,
78 const typet &element_type);
82 std::vector<const symbolt *> &_symbols_created,
84 bool _assume_non_null,
85 size_t _max_nondet_array_length,
99 bool create_dynamic_objects);
110 bool create_dynamic_objects,
119 bool create_dynamic_objects,
127 bool create_dynamic_objects,
138 const exprt &target_expr,
139 const typet &allocate_type,
140 bool create_dynamic_objects)
142 const typet &allocate_type_resolved=
ns.
follow(allocate_type);
144 bool cast_needed=allocate_type_resolved!=target_type;
145 if(!create_dynamic_objects)
155 code.add_source_location()=
loc;
164 if(allocate_type.
id()!=ID_empty)
171 malloc_expr.type()=result_type;
189 code.add_source_location()=
loc;
232 const typet &target_type,
233 bool create_dynamic_objects)
235 if(target_type.
id()==ID_struct &&
251 create_dynamic_objects);
253 if(target.
id()==ID_address_of)
254 init_expr=target.
op0();
263 create_dynamic_objects,
283 bool create_dynamic_objects,
288 if(subtype.
id()==ID_struct)
294 struct_tag==class_identifier)
307 create_dynamic_objects);
313 assignments.
append(non_null_inst);
333 assignments.
add(null_check);
355 bool create_dynamic_objects,
362 const componentst &components=struct_type.
components();
365 class_identifier=struct_tag;
369 for(
const auto &component : components)
371 const typet &component_type=component.type();
376 if(name==
"@class_identifier")
384 else if(name==
"@lock")
392 INVARIANT(!name.
empty(),
"Each component of a struct must have a name");
394 bool _is_sub=name[0]==
'@';
401 create_dynamic_objects);
423 bool create_dynamic_objects,
425 const typet &override_type)
430 if(type.
id()==ID_pointer)
438 create_dynamic_objects,
441 else if(type.
id()==ID_struct)
449 create_dynamic_objects,
454 exprt rhs=type.
id()==ID_c_bool?
476 const exprt &max_length_expr,
477 const typet &element_type)
483 "nondet_array_length");
485 const auto &length_sym_expr=length_sym.
symbol_expr();
494 assume2(length_sym_expr, ID_le, max_length_expr);
502 java_new_array.set(ID_length_upper_bound, max_length_expr);
503 java_new_array.type().subtype().set(ID_C_element_type, element_type);
515 assert(expr.
type().
id()==ID_pointer);
519 const typet &element_type=
544 init_array_expr.
type(),
547 const auto &array_init_symexpr=array_init_symbol.
symbol_expr();
590 plus_exprt(array_init_symexpr, counter_expr, array_init_symexpr.
type()),
616 size_t max_nondet_array_length,
623 main_symbol.
mode=ID_java;
625 main_symbol.
name=identifier;
627 main_symbol.
type=type;
633 bool moving_symbol_failed=symbol_table.
move(main_symbol, main_symbol_ptr);
634 assert(!moving_symbol_failed);
636 std::vector<const symbolt *> symbols_created;
637 symbols_created.push_back(main_symbol_ptr);
643 max_nondet_array_length,
655 for(
const symbolt *
const symbol_ptr : symbols_created)
662 init_code.
append(assignments);
The type of an expression.
irep_idt name
The unique identifier.
exprt size_of_expr(const typet &type, const namespacet &ns)
const codet & then_case() const
const typet & follow(const typet &src) const
Linking: Zero Initialization.
A generic base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
code_assignt get_null_assignment(const exprt &expr, const pointer_typet &ptr_type)
Adds an instruction to init_code null-initialising expr.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_tablet &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
irep_idt mode
Language mode.
const exprt & cond() const
exprt allocate_object(code_blockt &assignments, const exprt &, const typet &, bool create_dynamic_objects)
void copy_to_operands(const exprt &expr)
Goto Programs with Functions.
std::vector< componentt > componentst
void move_to_operands(exprt &expr)
Fresh auxiliary symbol creation.
The null pointer constant.
const componentst & components() const
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, bool allow_null, symbol_tablet &symbol_table, size_t max_nondet_array_length, const source_locationt &loc)
void gen_pointer_target_init(code_blockt &assignments, const exprt &expr, const typet &target_type, bool create_dynamic_objects)
Initialises an object tree rooted at expr, allocating child objects as necessary and nondet-initialis...
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
A constant literal expression.
void gen_nondet_array_init(code_blockt &assignments, const exprt &expr)
create code to initialize a Java array with size max_nondet_array_length, loop over elements and init...
std::unordered_set< irep_idt, irep_id_hash > recursion_set
#define INVARIANT(CONDITION, REASON)
Extract member of struct or union.
const char * as_string(coverage_criteriont c)
exprt object_size(const exprt &pointer)
const irep_idt & id() const
void add(const codet &code)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
A declaration of a local variable.
std::vector< const symbolt * > & symbols_created
Operator to dereference a pointer.
static irep_idt entry_point()
API to expression classes.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
A label for branch targets.
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
A side effect that returns a non-deterministically chosen value.
symbol_tablet & symbol_table
static exprt get_nondet_bool(const typet &type)
Operator to return the address of an object.
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
java_object_factoryt(std::vector< const symbolt *> &_symbols_created, const source_locationt &loc, bool _assume_non_null, size_t _max_nondet_array_length, symbol_tablet &_symbol_table)
bool has_prefix(const std::string &s, const std::string &prefix)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
static symbolt & new_tmp_symbol(symbol_tablet &symbol_table, const source_locationt &loc, const typet &type, const std::string &prefix="tmp_object_factory")
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
void gen_nondet_init(code_blockt &assignments, const exprt &expr, bool is_sub, irep_idt class_identifier, bool create_dynamic_objects, bool override=false, const typet &override_type=empty_typet())
Creates a nondet for expr, including calling itself recursively to make appropriate symbols to point ...
void gen_nondet_struct_init(code_blockt &assignments, const exprt &expr, bool is_sub, irep_idt class_identifier, bool create_dynamic_objects, const struct_typet &struct_type)
Initialises an object tree rooted at expr, allocating child objects as necessary and nondet-initialis...
Base class for all expressions.
size_t max_nondet_array_length
void gen_nondet_pointer_init(code_blockt &assignments, const exprt &expr, const irep_idt &class_identifier, bool create_dynamic_objects, const pointer_typet &pointer_type)
Initialises a primitive or object tree rooted at expr, of type pointer.
irep_idt base_name
Base (non-scoped) name.
void allocate_nondet_length_array(code_blockt &assignments, const exprt &lhs, const exprt &max_length_expr, const typet &element_type)
Allocates a fresh array.
source_locationt & add_source_location()
A statement in a programming language.
const typet & subtype() const
An expression containing a side effect.
const codet & else_case() const
const irept & find(const irep_namet &name) const
const source_locationt & loc