shadow_memory_state.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symex Shadow Memory Instrumentation
 
Author: Peter Schrammel
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_SYMEX_SHADOW_MEMORY_STATE_H
#define CPROVER_GOTO_SYMEX_SHADOW_MEMORY_STATE_H
 
#include <util/std_expr.h>
 
#include "shadow_memory_field_definitions.h"
 
#include <map>
 
class address_of_exprt;
 
class shadow_memory_statet
{
public:
  shadow_memory_field_definitionst fields;
 
  struct shadowed_addresst
  {
    exprt address;
    symbol_exprt shadow;
  };
  struct shadowed_addresst {…};
 
  // addresses must remain in sequence
  std::map<irep_idt, std::vector<shadowed_addresst>> address_fields;
};
class shadow_memory_statet {…};
 
#endif // CPROVER_GOTO_SYMEX_SHADOW_MEMORY_STATE_H