read_cbmc_goto_object.h

Go to the documentation of this file.

#pragma once
 
#include <istream>
#include <map>
#include <string>
#include <vector>
#include <util/irep/irep.h>
 
class contextt;
class goto_functionst;

bool is_cbmc_goto_magic(const unsigned char header[4]);

class cbmc_irep_readert
{
public:
  explicit cbmc_irep_readert(std::istream &in) : in(in)
  {
  }

  unsigned read_word();

  std::string read_string();

  irep_idt read_string_ref();

  void read_reference(irept &dest);

  bool failed() const
  {
    return failed_;
  }
 
private:
  void read_irep(irept &dest);
 
  std::istream &in;
  bool failed_ = false;
  std::map<unsigned, irept> irep_cache;
  std::map<unsigned, irep_idt> string_cache;
};

struct cbmc_symbolt
{
  irept stype; // CBMC "type"; renamed to avoid the C++ keyword clash Rust hit
  irept value;
  irept location;
  std::string name;
  std::string module;
  std::string base_name;
  std::string mode;
  std::string pretty_name;
  unsigned flags = 0;
  bool is_type = false;
  bool is_weak = false;
  bool is_property = false;
  bool is_macro = false;
  bool is_exported = false;
  bool is_input = false;
  bool is_output = false;
  bool is_state_var = false;
  bool is_parameter = false;
  bool is_auxiliary = false;
  bool binding = false;
  bool is_lvalue = false;
  bool is_static_lifetime = false;
  bool is_thread_local = false;
  bool is_file_local = false;
  bool is_extern = false;
  bool is_volatile = false;
};

struct cbmc_instructiont
{
  irept code;
  irept source_location;
  irept guard;
  unsigned instr_type = 0;
  unsigned target_number = 0;
  std::vector<unsigned> targets;
  std::vector<std::string> labels;
};
 
struct cbmc_functiont
{
  std::string name;
  std::vector<cbmc_instructiont> instructions;
};
 
struct cbmc_parse_resultt
{
  std::vector<cbmc_symbolt> symbols;
  std::vector<cbmc_functiont> functions;
};

bool parse_cbmc_goto(
  std::istream &in,
  const std::string &filename,
  cbmc_parse_resultt &result);

bool read_cbmc_goto_object(
  std::istream &in,
  const std::string &filename,
  contextt &context,
  goto_functionst &goto_functions);