cprover
Loading...
Searching...
No Matches
code_with_references.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Java bytecode
4
5Author: Romain Brenguier, romain.brenguier@diffblue.com
6
7\*******************************************************************/
8
10#include "java_types.h"
11
12#include <util/arith_tools.h>
13
27
30{
31 const object_creation_referencet &reference = references(reference_id);
32 INVARIANT(reference.array_length, "Length of reference array must be known");
34 {
35 return code_blockt(
36 {allocate_array(reference.expr, *reference.array_length, loc)});
37 }
38 // Fallback in case the array definition has not been seen yet, this can
39 // happen if `to_code` is called before the whole json file has been processed
40 // or the "@id" json field corresponding to `reference_id` doesn't appear in
41 // the file.
42 code_blockt code;
46 *reference.array_length, ID_ge, from_integer(0, java_int_type())}});
47 code.add(allocate_array(reference.expr, *reference.array_length, loc));
48 return code;
49}
50
52{
53 auto ptr = std::make_shared<code_without_referencest>(std::move(code));
54 list.emplace_back(std::move(ptr));
55}
56
58{
59 add(code_without_referencest{std::move(code)});
60}
61
63{
64 auto ptr = std::make_shared<reference_allocationt>(std::move(ref));
65 list.emplace_back(std::move(ptr));
66}
67
69{
70 list.splice(list.end(), other.list);
71}
72
74{
75 auto ptr = std::make_shared<code_without_referencest>(std::move(code));
76 list.emplace_front(std::move(ptr));
77}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:676
An assumption, which must hold in subsequent code.
Definition std_code.h:217
A codet representing sequential composition of program statements.
Definition std_code.h:130
void add(const codet &code)
Definition std_code.h:168
A codet representing an assignment in the program.
Definition std_code.h:24
Wrapper around a list of shared pointer to code_with_referencest objects, which provides a nicer inte...
void add_to_front(code_without_referencest code)
std::list< std::shared_ptr< code_with_referencest > > list
void append(code_with_references_listt &&other)
void add(code_without_referencest code)
std::function< const object_creation_referencet &(const std::string &)> reference_substitutiont
Code that should not contain reference.
Data structure for representing an arbitrary statement in a program.
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
Allocation code which contains a reference.
code_blockt to_code(reference_substitutiont &references) const override
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
An expression containing a side effect.
Definition std_code.h:1450
codet allocate_array(const exprt &expr, const exprt &array_length_expr, const source_locationt &loc)
Allocate a fresh array of length array_length_expr and assigns expr to it.
codet allocate_array(const exprt &expr, const exprt &array_length_expr, const source_locationt &loc)
Allocate a fresh array of length array_length_expr and assigns expr to it.
signedbv_typet java_int_type()
const typet & java_array_element_type(const struct_tag_typet &array_symbol)
Return a const reference to the element type of a given java array type.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474
Information to store when several references point to the same Java object.
exprt expr
Expression for the symbol that stores the value that may be reference equal to other values.
optionalt< exprt > array_length
If symbol is an array, this expression stores its length.