loopst.h

Go to the documentation of this file.

#ifndef GOTO_PROGRAMS_LOOPST_H_
#define GOTO_PROGRAMS_LOOPST_H_
 
#include <goto-programs/goto_functions.h>
#include <unordered_set>
 
class loopst
{
public:
  loopst() : size(0)
  {
  }
 
  typedef std::unordered_set<expr2tc, irep2_hash> loop_varst;
 
  const loop_varst &get_modified_loop_vars() const;
  const loop_varst &get_unmodified_loop_vars() const;
 
  const goto_programt::targett get_original_loop_exit() const;
  void set_original_loop_exit(goto_programt::targett _loop_exit);
 
  const goto_programt::targett get_original_loop_head() const;
  void set_original_loop_head(goto_programt::targett _loop_head);

  goto_programt::targett effective_loop_head() const;
 
  void add_modified_var_to_loop(const expr2tc &expr);
  void add_unmodified_var_to_loop(const expr2tc &expr);

  void add_pointer_array_write_ptr(const expr2tc &ptr)
  {
    pointer_array_write_ptrs_.insert(ptr);
  }
 
  const loop_varst &get_pointer_array_write_ptrs() const
  {
    return pointer_array_write_ptrs_;
  }

  void set_pointer_array_write_unresolvable()
  {
    pointer_array_write_unresolvable_ = true;
  }
 
  bool pointer_array_write_unresolvable() const
  {
    return pointer_array_write_unresolvable_;
  }

  void set_writes_through_pointer()
  {
    writes_through_pointer_ = true;
  }
 
  bool writes_through_pointer() const
  {
    return writes_through_pointer_;
  }

  void add_written_pointer(const expr2tc &ptr)
  {
    written_pointers_.insert(ptr);
  }
 
  const loop_varst &get_written_pointers() const
  {
    return written_pointers_;
  }

  void add_written_pointee(const expr2tc &pointee)
  {
    written_pointees_.insert(pointee);
  }
 
  const loop_varst &get_written_pointees() const
  {
    return written_pointees_;
  }

  void set_unnamed_pointer_write()
  {
    unnamed_pointer_write_ = true;
  }
 
  bool unnamed_pointer_write() const
  {
    return unnamed_pointer_write_;
  }
 
  void dump() const;
  void dump_loop_vars() const;
  void output_to(std::ostream &oss) const;
  void output_loop_vars_to(std::ostream &oss) const;
 
  void set_size(std::size_t size)
  {
    this->size = size;
  }
 
protected:
  loop_varst modified_loop_vars;
  loop_varst unmodified_loop_vars;
 
  goto_programt::targett original_loop_head;
  goto_programt::targett original_loop_exit;
 
  std::size_t size;
  bool pointer_array_write_unresolvable_ = false;
  bool writes_through_pointer_ = false;
  loop_varst pointer_array_write_ptrs_;
  loop_varst written_pointers_;
  loop_varst written_pointees_;
  bool unnamed_pointer_write_ = false;
};
 
#endif /* GOTO_PROGRAMS_LOOPST_H_ */