code_with_references.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Java bytecode
 
Author: Romain Brenguier, romain.brenguier@diffblue.com
 
\*******************************************************************/
 
#ifndef CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H
#define CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H
 
#include <memory>
#include <util/std_code.h>

codet allocate_array(
  const exprt &expr,
  const exprt &array_length_expr,
  const source_locationt &loc);

struct object_creation_referencet
{
  exprt expr;

  std::optional<exprt> array_length;
};

class code_with_referencest
{
public:
  using reference_substitutiont =
    std::function<const object_creation_referencet &(const std::string &)>;
 
  virtual code_blockt to_code(reference_substitutiont &) const = 0;
 
  virtual ~code_with_referencest() = default;
};

class code_without_referencest : public code_with_referencest
{
public:
  codet code;
 
  explicit code_without_referencest(codet code) : code(std::move(code))
  {
  }
 
  code_blockt to_code(reference_substitutiont &) const override
  {
    return code_blockt({code});
  }
};

class reference_allocationt : public code_with_referencest
{
public:
  std::string reference_id;
  source_locationt loc;
 
  reference_allocationt(std::string reference_id, source_locationt loc)
    : reference_id(std::move(reference_id)), loc(std::move(loc))
  {
  }
 
  code_blockt to_code(reference_substitutiont &references) const override;
};

class code_with_references_listt
{
public:
  std::list<std::shared_ptr<code_with_referencest>> list;
 
  void add(code_without_referencest code);
 
  void add(codet code);
 
  void add(reference_allocationt ref);
 
  void append(code_with_references_listt &&other);
 
  void add_to_front(code_without_referencest code);
};
 
#endif // CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H