cprover
Loading...
Searching...
No Matches
code_with_references.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Java bytecode
4
5Author: Romain Brenguier, romain.brenguier@diffblue.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H
10#define CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H
11
12#include <memory>
13#include <util/std_code.h>
14
18 const exprt &expr,
19 const exprt &array_length_expr,
20 const source_locationt &loc);
21
35
41{
42public:
44 std::function<const object_creation_referencet &(const std::string &)>;
45
47
48 virtual ~code_with_referencest() = default;
49};
50
53{
54public:
56
58 {
59 }
60
62 {
63 return code_blockt({code});
64 }
65};
66
77{
78public:
79 std::string reference_id;
81
86
87 code_blockt to_code(reference_substitutiont &references) const override;
88};
89
93{
94public:
95 std::list<std::shared_ptr<code_with_referencest>> list;
96
98
99 void add(codet code);
100
101 void add(reference_allocationt ref);
102
104
106};
107
108#endif // CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H
A codet representing sequential composition of program statements.
Definition std_code.h:130
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)
Base class for code which can contain references which can get replaced before generating actual code...
virtual ~code_with_referencest()=default
virtual code_blockt to_code(reference_substitutiont &) const =0
std::function< const object_creation_referencet &(const std::string &)> reference_substitutiont
Code that should not contain reference.
code_blockt to_code(reference_substitutiont &) const override
Data structure for representing an arbitrary statement in a program.
Base class for all expressions.
Definition expr.h:56
Allocation code which contains a reference.
reference_allocationt(std::string reference_id, source_locationt loc)
code_blockt to_code(reference_substitutiont &references) const override
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.
STL namespace.
nonstd::optional< T > optionalt
Definition optional.h:35
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.