cprover
goto_program.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Concrete Goto Program
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
13 #define CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
14 
15 #include <set>
16 
17 #include <util/std_code.h>
18 
19 #include "goto_program_template.h"
20 
24 class goto_programt:public goto_program_templatet<codet, exprt>
25 {
26 public:
27  std::ostream &output_instruction(
28  const class namespacet &ns,
29  const irep_idt &identifier,
30  std::ostream &out,
31  instructionst::const_iterator it) const;
32 
33  std::ostream &output_instruction(
34  const class namespacet &ns,
35  const irep_idt &identifier,
36  std::ostream &out,
37  const instructiont &instruction) const;
38 
40 
41  // Copying is unavailable as base class copy is deleted
42  // MSVC is unable to automatically determine this
43  goto_programt(const goto_programt &)=delete;
44  goto_programt &operator=(const goto_programt &)=delete;
45 
46  // Move operations need to be explicitly enabled as they are deleted with the
47  // copy operations
48  // default for move operations isn't available on Windows yet, so define
49  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
50  // under "Defaulted and Deleted Functions")
51 
53  goto_program_templatet(std::move(other))
54  {
55  }
56 
58  {
59  goto_program_templatet::operator=(std::move(other));
60  return *this;
61  }
62 
63  // get the variables in decl statements
64  typedef std::set<irep_idt> decl_identifierst;
65  void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
66 };
67 
68 #define forall_goto_program_instructions(it, program) \
69  for(goto_programt::instructionst::const_iterator \
70  it=(program).instructions.begin(); \
71  it!=(program).instructions.end(); it++)
72 
73 #define Forall_goto_program_instructions(it, program) \
74  for(goto_programt::instructionst::iterator \
75  it=(program).instructions.begin(); \
76  it!=(program).instructions.end(); it++)
77 
78 inline bool operator<(
81 {
82  return order_const_target<codet, exprt>(i1, i2);
83 }
84 
85 // NOLINTNEXTLINE(readability/identifiers)
87 
88 std::list<exprt> objects_read(const goto_programt::instructiont &);
89 std::list<exprt> objects_written(const goto_programt::instructiont &);
90 
91 std::list<exprt> expressions_read(const goto_programt::instructiont &);
92 std::list<exprt> expressions_written(const goto_programt::instructiont &);
93 
94 std::string as_string(
95  const namespacet &ns,
96  const goto_programt::instructiont &);
97 
98 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
goto_programt(goto_programt &&other)
Definition: goto_program.h:52
std::list< exprt > objects_written(const goto_programt::instructiont &)
A generic container class for the GOTO intermediate representation of one function.
STL namespace.
std::list< exprt > expressions_read(const goto_programt::instructiont &)
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:64
bool operator<(const goto_programt::const_targett i1, const goto_programt::const_targett i2)
Definition: goto_program.h:78
std::list< exprt > expressions_written(const goto_programt::instructiont &)
instructionst::const_iterator const_targett
Goto Program Template.
std::string as_string(const namespacet &ns, const goto_programt::instructiont &)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
goto_programt & operator=(goto_programt &&other)
Definition: goto_program.h:57
std::list< exprt > objects_read(const goto_programt::instructiont &)
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
goto_program_templatet & operator=(const goto_program_templatet &)=delete
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Base class for all expressions.
Definition: expr.h:46
A statement in a programming language.
Definition: std_code.h:19
goto_programt & operator=(const goto_programt &)=delete
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.