CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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:235
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:731
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:518
Information to store when several references point to the same Java object.
std::optional< exprt > array_length
If symbol is an array, this expression stores its length.
exprt expr
Expression for the symbol that stores the value that may be reference equal to other values.