cprover
code_with_references.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java bytecode
4 
5 Author: 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 
24 {
28 
34 };
35 
41 {
42 public:
44  std::function<const object_creation_referencet &(const std::string &)>;
45 
47 
48  virtual ~code_with_referencest() = default;
49 };
50 
53 {
54 public:
56 
57  explicit code_without_referencest(codet code) : code(std::move(code))
58  {
59  }
60 
62  {
63  return code_blockt({code});
64  }
65 };
66 
77 {
78 public:
79  std::string reference_id;
81 
83  : reference_id(std::move(reference_id)), loc(std::move(loc))
84  {
85  }
86 
87  code_blockt to_code(reference_substitutiont &references) const override;
88 };
89 
93 {
94 public:
95  std::list<std::shared_ptr<code_with_referencest>> list;
96 
97  void add(code_without_referencest code);
98 
99  void add(codet code);
100 
101  void add(reference_allocationt ref);
102 
103  void append(code_with_references_listt &&other);
104 
106 };
107 
108 #endif // CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H
A codet representing sequential composition of program statements.
Definition: std_code.h:168
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
std::function< const object_creation_referencet &(const std::string &)> reference_substitutiont
virtual code_blockt to_code(reference_substitutiont &) const =0
Code that should not contain reference.
code_blockt to_code(reference_substitutiont &) const override
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
Base class for all expressions.
Definition: expr.h:54
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.
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.