goto_state.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Symbolic Execution
 
Author: Romain Brenguier, romain.brenguier@diffblue.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_GOTO_SYMEX_GOTO_STATE_H
#define CPROVER_GOTO_SYMEX_GOTO_STATE_H
 
#include <util/sharing_map.h>
 
#include <analyses/guard.h>
 
#include <pointer-analysis/value_set.h>
 
#include "renaming_level.h"
 
// Forward declaration required since subclass is used explicitly
// by the parent class.
class goto_symex_statet;
 
class goto_statet
{
public:
  unsigned depth = 0;
 
protected:
  symex_level2t level2;
 
public:
  sharing_mapt<exprt, symbol_exprt, false, irep_hash> dereference_cache;
 
  const symex_level2t &get_level2() const
  {
    return level2;
  }
  const symex_level2t &get_level2() const {…}
 
  value_sett value_set;
 
  // A guard is a particular condition that has to pass for an instruction
  // to be executed. The easiest example is an if/else: each instruction along
  // the if branch will be guarded by the condition of the if (and if there
  // is an else branch then instructions on it will be guarded by the negation
  // of the condition of the if).
  guardt guard;
 
  bool reachable;
 
  // Map L1 names to (L2) constants. Values will be evicted from this map
  // when they become non-constant. This is used to propagate values that have
  // been worked out to only have one possible value.
  //
  // "constants" can include symbols, but only in the context of an address-of
  // op (i.e. &x can be propagated), and an address-taken thing should only be
  // L1.
  sharing_mapt<irep_idt, exprt> propagation;
 
  void output_propagation_map(std::ostream &);
 
  unsigned atomic_section_id = 0;
 
  goto_statet() = delete;
  goto_statet &operator=(const goto_statet &other) = delete;
  goto_statet &operator=(goto_statet &&other) = default;
  goto_statet(const goto_statet &other) = default;
  goto_statet(goto_statet &&other) = default;
 
  explicit goto_statet(guard_managert &guard_manager)
    : guard(true_exprt(), guard_manager), reachable(true)
  {
  }
  explicit goto_statet(guard_managert &guard_manager) {…}
 
  void apply_condition(
    const exprt &condition, // L2
    const goto_symex_statet &previous_state,
    const namespacet &ns);
};
class goto_statet {…};
 
#endif // CPROVER_GOTO_SYMEX_GOTO_STATE_H