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 <iosfwd>
16 #include <set>
17 #include <limits>
18 #include <sstream>
19 #include <string>
20 
21 #include <util/deprecate.h>
22 #include <util/invariant.h>
23 #include <util/namespace.h>
24 #include <util/source_location.h>
25 #include <util/std_code.h>
26 #include <util/std_expr.h>
27 #include <util/symbol_table.h>
28 
29 enum class validation_modet;
30 
33 {
35  GOTO = 1, // branch, possibly guarded
36  ASSUME = 2, // non-failing guarded self loop
37  ASSERT = 3, // assertions
38  OTHER = 4, // anything else
39  SKIP = 5, // just advance the PC
40  START_THREAD = 6, // spawns an asynchronous thread
41  END_THREAD = 7, // end the current thread
42  LOCATION = 8, // semantically like SKIP
43  END_FUNCTION = 9, // exit point of a function
44  ATOMIC_BEGIN = 10, // marks a block without interleavings
45  ATOMIC_END = 11, // end of a block without interleavings
46  RETURN = 12, // set function return value (no control-flow change)
47  ASSIGN = 13, // assignment lhs:=rhs
48  DECL = 14, // declare a local variable
49  DEAD = 15, // marks the end-of-live of a local variable
50  FUNCTION_CALL = 16, // call a function
51  THROW = 17, // throw an exception
52  CATCH = 18, // push, pop or enter an exception handler
53  INCOMPLETE_GOTO = 19 // goto where target is yet to be determined
54 };
55 
56 std::ostream &operator<<(std::ostream &, goto_program_instruction_typet);
57 
74 {
75 public:
77  goto_programt(const goto_programt &)=delete;
79 
80  // Move operations need to be explicitly enabled as they are deleted with the
81  // copy operations
82  // default for move operations isn't available on Windows yet, so define
83  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
84  // under "Defaulted and Deleted Functions")
85 
87  instructions(std::move(other.instructions))
88  {
89  }
90 
92  {
93  instructions=std::move(other.instructions);
94  return *this;
95  }
96 
179  class instructiont final
180  {
181  public:
184 
186  const code_assignt &get_assign() const
187  {
189  return to_code_assign(code);
190  }
191 
194  {
196  code = std::move(c);
197  }
198 
200  DEPRECATED(SINCE(2021, 2, 24, "Use decl_symbol instead"))
201  const code_declt &get_decl() const
202  {
204  const auto &decl = expr_checked_cast<code_declt>(code);
205  INVARIANT(
206  !decl.initial_value(),
207  "code_declt in goto program may not contain initialization.");
208  return decl;
209  }
210 
212  const symbol_exprt &decl_symbol() const
213  {
215  auto &decl = expr_checked_cast<code_declt>(code);
216  INVARIANT(
217  !decl.initial_value(),
218  "code_declt in goto program may not contain initialization.");
219  return decl.symbol();
220  }
221 
224  {
226  auto &decl = expr_checked_cast<code_declt>(code);
227  INVARIANT(
228  !decl.initial_value(),
229  "code_declt in goto program may not contain initialization.");
230  return decl.symbol();
231  }
232 
234  DEPRECATED(SINCE(2021, 2, 24, "Use decl_symbol instead"))
236  {
238  INVARIANT(
239  !c.initial_value(),
240  "Initialization must be separated from code_declt before adding to "
241  "goto_instructiont.");
242  code = std::move(c);
243  }
244 
246  DEPRECATED(SINCE(2021, 2, 24, "Use dead_symbol instead"))
247  const code_deadt &get_dead() const
248  {
250  return to_code_dead(code);
251  }
252 
254  const symbol_exprt &dead_symbol() const
255  {
257  return to_code_dead(code).symbol();
258  }
259 
262  {
264  return to_code_dead(code).symbol();
265  }
266 
268  DEPRECATED(SINCE(2021, 2, 24, "Use dead_symbol instead"))
270  {
272  code = std::move(c);
273  }
274 
276  DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead"))
277  const code_returnt &get_return() const
278  {
280  return to_code_return(code);
281  }
282 
284  const exprt &return_value() const
285  {
287  return to_code_return(code).return_value();
288  }
289 
292  {
294  return to_code_return(code).return_value();
295  }
296 
298  DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead"))
300  {
302  code = std::move(c);
303  }
304 
307  {
309  return to_code_function_call(code);
310  }
311 
314  {
316  code = std::move(c);
317  }
318 
320  const codet &get_other() const
321  {
323  return code;
324  }
325 
327  void set_other(codet &c)
328  {
330  code = std::move(c);
331  }
332 
335 
338 
342 
344  bool has_condition() const
345  {
346  return is_goto() || is_incomplete_goto() || is_assume() || is_assert();
347  }
348 
350  const exprt &get_condition() const
351  {
353  return guard;
354  }
355 
358  {
360  guard = std::move(c);
361  }
362 
363  // The below will eventually become a single target only.
365  typedef std::list<instructiont>::iterator targett;
366  typedef std::list<instructiont>::const_iterator const_targett;
367  typedef std::list<targett> targetst;
368  typedef std::list<const_targett> const_targetst;
369 
372 
376  {
377  PRECONDITION(targets.size()==1);
378  return targets.front();
379  }
380 
384  {
385  targets.clear();
386  targets.push_back(t);
387  }
388 
389  bool has_target() const
390  {
391  return !targets.empty();
392  }
393 
395  typedef std::list<irep_idt> labelst;
397 
398  // will go away
399  std::set<targett> incoming_edges;
400 
402  bool is_target() const
403  { return target_number!=nil_target; }
404 
407  {
408  type=_type;
409  targets.clear();
410  guard=true_exprt();
411  code.make_nil();
412  }
413 
417  {
418  clear(SKIP);
419  }
420 
421  void complete_goto(targett _target)
422  {
424  code.make_nil();
425  targets.push_back(_target);
426  type = GOTO;
427  }
428 
429  bool is_goto () const { return type==GOTO; }
430  bool is_return () const { return type==RETURN; }
431  bool is_assign () const { return type==ASSIGN; }
432  bool is_function_call() const { return type==FUNCTION_CALL; }
433  bool is_throw () const { return type==THROW; }
434  bool is_catch () const { return type==CATCH; }
435  bool is_skip () const { return type==SKIP; }
436  bool is_location () const { return type==LOCATION; }
437  bool is_other () const { return type==OTHER; }
438  bool is_decl () const { return type==DECL; }
439  bool is_dead () const { return type==DEAD; }
440  bool is_assume () const { return type==ASSUME; }
441  bool is_assert () const { return type==ASSERT; }
442  bool is_atomic_begin () const { return type==ATOMIC_BEGIN; }
443  bool is_atomic_end () const { return type==ATOMIC_END; }
444  bool is_start_thread () const { return type==START_THREAD; }
445  bool is_end_thread () const { return type==END_THREAD; }
446  bool is_end_function () const { return type==END_FUNCTION; }
447  bool is_incomplete_goto() const
448  {
449  return type == INCOMPLETE_GOTO;
450  }
451 
453  instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit)
454  {
455  }
456 
458  : code(static_cast<const codet &>(get_nil_irep())),
459  source_location(static_cast<const source_locationt &>(get_nil_irep())),
460  type(_type),
461  guard(true_exprt())
462  {
463  }
464 
467  codet _code,
468  source_locationt _source_location,
470  exprt _guard,
471  targetst _targets)
472  : code(std::move(_code)),
473  source_location(std::move(_source_location)),
474  type(_type),
475  guard(std::move(_guard)),
476  targets(std::move(_targets))
477  {
478  }
479 
481  void swap(instructiont &instruction)
482  {
483  using std::swap;
484  swap(instruction.code, code);
485  swap(instruction.source_location, source_location);
486  swap(instruction.type, type);
487  swap(instruction.guard, guard);
488  swap(instruction.targets, targets);
489  }
490 
492  static const unsigned nil_target=
493  std::numeric_limits<unsigned>::max();
494 
498  unsigned location_number = 0;
499 
501  unsigned loop_number = 0;
502 
506 
508  bool is_backwards_goto() const
509  {
510  if(!is_goto())
511  return false;
512 
513  for(const auto &t : targets)
514  if(t->location_number<=location_number)
515  return true;
516 
517  return false;
518  }
519 
520  std::string to_string() const
521  {
522  std::ostringstream instruction_id_builder;
523  instruction_id_builder << type;
524  return instruction_id_builder.str();
525  }
526 
531  bool equals(const instructiont &other) const;
532 
537  void validate(const namespacet &ns, const validation_modet vm) const;
538 
541  void transform(std::function<optionalt<exprt>(exprt)>);
542 
544  void apply(std::function<void(const exprt &)>) const;
545  };
546 
547  // Never try to change this to vector-we mutate the list while iterating
548  typedef std::list<instructiont> instructionst;
549 
550  typedef instructionst::iterator targett;
551  typedef instructionst::const_iterator const_targett;
552  typedef std::list<targett> targetst;
553  typedef std::list<const_targett> const_targetst;
554 
557 
561  {
562  return instructions.erase(t, t);
563  }
564 
567  {
568  return t;
569  }
570 
571  template <typename Target>
572  std::list<Target> get_successors(Target target) const;
573 
574  void compute_incoming_edges();
575 
578  {
579  PRECONDITION(target!=instructions.end());
580  const auto next=std::next(target);
581  instructions.insert(next, instructiont())->swap(*target);
582  }
583 
586  void insert_before_swap(targett target, instructiont &instruction)
587  {
588  insert_before_swap(target);
589  target->swap(instruction);
590  }
591 
595  targett target,
596  goto_programt &p)
597  {
598  PRECONDITION(target!=instructions.end());
599  if(p.instructions.empty())
600  return;
601  insert_before_swap(target, p.instructions.front());
602  auto next=std::next(target);
603  p.instructions.erase(p.instructions.begin());
604  instructions.splice(next, p.instructions);
605  }
606 
611  {
612  return instructions.insert(target, instructiont());
613  }
614 
619  {
620  return instructions.insert(target, i);
621  }
622 
627  {
628  return instructions.insert(std::next(target), instructiont());
629  }
630 
635  {
636  return instructions.insert(std::next(target), i);
637  }
638 
641  {
642  instructions.splice(instructions.end(),
643  p.instructions);
644  }
645 
649  const_targett target,
650  goto_programt &p)
651  {
652  instructions.splice(target, p.instructions);
653  }
654 
657  targett add(instructiont &&instruction)
658  {
659  instructions.push_back(std::move(instruction));
660  return --instructions.end();
661  }
662 
666  {
667  return add(instructiont());
668  }
669 
673  {
674  return add(instructiont(type));
675  }
676 
678  std::ostream &output(
679  const namespacet &ns,
680  const irep_idt &identifier,
681  std::ostream &out) const;
682 
684  std::ostream &output(std::ostream &out) const
685  {
686  return output(namespacet(symbol_tablet()), irep_idt(), out);
687  }
688 
690  std::ostream &output_instruction(
691  const namespacet &ns,
692  const irep_idt &identifier,
693  std::ostream &out,
694  const instructionst::value_type &instruction) const;
695 
697  void compute_target_numbers();
698 
700  void compute_location_numbers(unsigned &nr)
701  {
702  for(auto &i : instructions)
703  {
704  INVARIANT(
705  nr != std::numeric_limits<unsigned>::max(),
706  "Too many location numbers assigned");
707  i.location_number=nr++;
708  }
709  }
710 
713  {
714  unsigned nr=0;
716  }
717 
719  void compute_loop_numbers();
720 
722  void update();
723 
725  static irep_idt
726  loop_id(const irep_idt &function_id, const instructiont &instruction)
727  {
728  return id2string(function_id) + "." +
729  std::to_string(instruction.loop_number);
730  }
731 
733  bool empty() const
734  {
735  return instructions.empty();
736  }
737 
740  {
741  }
742 
744  {
745  }
746 
748  void swap(goto_programt &program)
749  {
750  program.instructions.swap(instructions);
751  }
752 
754  void clear()
755  {
756  instructions.clear();
757  }
758 
762  {
763  PRECONDITION(!instructions.empty());
764  const auto end_function=std::prev(instructions.end());
765  DATA_INVARIANT(end_function->is_end_function(),
766  "goto program ends on END_FUNCTION");
767  return end_function;
768  }
769 
773  {
774  PRECONDITION(!instructions.empty());
775  const auto end_function=std::prev(instructions.end());
776  DATA_INVARIANT(end_function->is_end_function(),
777  "goto program ends on END_FUNCTION");
778  return end_function;
779  }
780 
782  void copy_from(const goto_programt &src);
783 
785  bool has_assertion() const;
786 
787  typedef std::set<irep_idt> decl_identifierst;
789  void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
790 
794  bool equals(const goto_programt &other) const;
795 
800  void validate(const namespacet &ns, const validation_modet vm) const
801  {
802  for(const instructiont &ins : instructions)
803  {
804  ins.validate(ns, vm);
805  }
806  }
807 
808  static instructiont
810  {
811  return instructiont(code_returnt(), l, RETURN, nil_exprt(), {});
812  }
813 
815  code_returnt c,
817  {
818  return instructiont(std::move(c), l, RETURN, nil_exprt(), {});
819  }
820 
821  static instructiont
823  {
824  return instructiont(
825  static_cast<const codet &>(get_nil_irep()),
826  l,
827  SKIP,
828  nil_exprt(),
829  {});
830  }
831 
833  {
834  return instructiont(
835  static_cast<const codet &>(get_nil_irep()),
836  l,
837  LOCATION,
838  nil_exprt(),
839  {});
840  }
841 
842  static instructiont
844  {
845  return instructiont(
846  static_cast<const codet &>(get_nil_irep()),
847  l,
848  THROW,
849  nil_exprt(),
850  {});
851  }
852 
853  static instructiont
855  {
856  return instructiont(
857  static_cast<const codet &>(get_nil_irep()),
858  l,
859  CATCH,
860  nil_exprt(),
861  {});
862  }
863 
865  const exprt &g,
867  {
868  return instructiont(
869  static_cast<const codet &>(get_nil_irep()),
870  l,
871  ASSERT,
872  exprt(g),
873  {});
874  }
875 
877  const exprt &g,
879  {
880  return instructiont(
881  static_cast<const codet &>(get_nil_irep()), l, ASSUME, g, {});
882  }
883 
885  const codet &_code,
887  {
888  return instructiont(_code, l, OTHER, nil_exprt(), {});
889  }
890 
892  const symbol_exprt &symbol,
894  {
895  return instructiont(code_declt(symbol), l, DECL, nil_exprt(), {});
896  }
897 
899  const symbol_exprt &symbol,
901  {
902  return instructiont(code_deadt(symbol), l, DEAD, nil_exprt(), {});
903  }
904 
905  static instructiont
907  {
908  return instructiont(
909  static_cast<const codet &>(get_nil_irep()),
910  l,
911  ATOMIC_BEGIN,
912  nil_exprt(),
913  {});
914  }
915 
916  static instructiont
918  {
919  return instructiont(
920  static_cast<const codet &>(get_nil_irep()),
921  l,
922  ATOMIC_END,
923  nil_exprt(),
924  {});
925  }
926 
927  static instructiont
929  {
930  return instructiont(
931  static_cast<const codet &>(get_nil_irep()),
932  l,
933  END_FUNCTION,
934  nil_exprt(),
935  {});
936  }
937 
939  const exprt &_cond,
941  {
942  PRECONDITION(_cond.type().id() == ID_bool);
943  return instructiont(
944  static_cast<const codet &>(get_nil_irep()),
945  l,
947  _cond,
948  {});
949  }
950 
951  static instructiont
953  {
954  return instructiont(
955  static_cast<const codet &>(get_nil_irep()),
956  l,
958  true_exprt(),
959  {});
960  }
961 
963  const code_gotot &_code,
965  {
966  return instructiont(_code, l, INCOMPLETE_GOTO, true_exprt(), {});
967  }
968 
970  targett _target,
972  {
973  return instructiont(
974  static_cast<const codet &>(get_nil_irep()),
975  l,
976  GOTO,
977  true_exprt(),
978  {_target});
979  }
980 
982  targett _target,
983  const exprt &g,
985  {
986  return instructiont(
987  static_cast<const codet &>(get_nil_irep()),
988  l,
989  GOTO,
990  g,
991  {_target});
992  }
993 
996  const code_assignt &_code,
998  {
999  return instructiont(_code, l, ASSIGN, nil_exprt(), {});
1000  }
1001 
1004  exprt lhs,
1005  exprt rhs,
1007  {
1008  return instructiont(
1009  code_assignt(std::move(lhs), std::move(rhs)), l, ASSIGN, nil_exprt(), {});
1010  }
1011 
1013  const code_declt &_code,
1015  {
1016  return instructiont(_code, l, DECL, nil_exprt(), {});
1017  }
1018 
1021  const code_function_callt &_code,
1023  {
1024  return instructiont(_code, l, FUNCTION_CALL, nil_exprt(), {});
1025  }
1026 
1029  exprt function,
1032  {
1033  return instructiont(
1034  code_function_callt(std::move(function), std::move(arguments)),
1035  l,
1036  FUNCTION_CALL,
1037  nil_exprt(),
1038  {});
1039  }
1040 };
1041 
1054 template <typename Target>
1056  Target target) const
1057 {
1058  if(target==instructions.end())
1059  return std::list<Target>();
1060 
1061  const auto next=std::next(target);
1062 
1063  const instructiont &i=*target;
1064 
1065  if(i.is_goto())
1066  {
1067  std::list<Target> successors(i.targets.begin(), i.targets.end());
1068 
1069  if(!i.get_condition().is_true() && next != instructions.end())
1070  successors.push_back(next);
1071 
1072  return successors;
1073  }
1074 
1075  if(i.is_start_thread())
1076  {
1077  std::list<Target> successors(i.targets.begin(), i.targets.end());
1078 
1079  if(next!=instructions.end())
1080  successors.push_back(next);
1081 
1082  return successors;
1083  }
1084 
1085  if(i.is_end_thread())
1086  {
1087  // no successors
1088  return std::list<Target>();
1089  }
1090 
1091  if(i.is_throw())
1092  {
1093  // the successors are non-obvious
1094  return std::list<Target>();
1095  }
1096 
1097  if(i.is_assume())
1098  {
1099  return !i.get_condition().is_false() && next != instructions.end()
1100  ? std::list<Target>{next}
1101  : std::list<Target>();
1102  }
1103 
1104  if(next!=instructions.end())
1105  {
1106  return std::list<Target>{next};
1107  }
1108 
1109  return std::list<Target>();
1110 }
1111 
1115 {
1116  const goto_programt::instructiont &_i1=*i1;
1117  const goto_programt::instructiont &_i2=*i2;
1118  return &_i1<&_i2;
1119 }
1120 
1121 // NOLINTNEXTLINE(readability/identifiers)
1123 {
1124  std::size_t operator()(
1125  const goto_programt::const_targett t) const
1126  {
1127  using hash_typet = decltype(&(*t));
1128  return std::hash<hash_typet>{}(&(*t));
1129  }
1130 };
1131 
1135 {
1136  template <class A, class B>
1137  bool operator()(const A &a, const B &b) const
1138  {
1139  return &(*a) == &(*b);
1140  }
1141 };
1142 
1143 template <typename GotoFunctionT, typename PredicateT, typename HandlerT>
1145  GotoFunctionT &&goto_function,
1146  PredicateT predicate,
1147  HandlerT handler)
1148 {
1149  auto &&instructions = goto_function.body.instructions;
1150  for(auto it = instructions.begin(); it != instructions.end(); ++it)
1151  {
1152  if(predicate(it))
1153  {
1154  handler(it);
1155  }
1156  }
1157 }
1158 
1159 template <typename GotoFunctionT, typename HandlerT>
1160 void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
1161 {
1162  using iterator_t = decltype(goto_function.body.instructions.begin());
1164  goto_function, [](const iterator_t &) { return true; }, handler);
1165 }
1166 
1167 #define forall_goto_program_instructions(it, program) \
1168  for(goto_programt::instructionst::const_iterator \
1169  it=(program).instructions.begin(); \
1170  it!=(program).instructions.end(); it++)
1171 
1172 #define Forall_goto_program_instructions(it, program) \
1173  for(goto_programt::instructionst::iterator \
1174  it=(program).instructions.begin(); \
1175  it!=(program).instructions.end(); it++)
1176 
1177 inline bool operator<(
1178  const goto_programt::const_targett &i1,
1179  const goto_programt::const_targett &i2)
1180 {
1181  return order_const_target(i1, i2);
1182 }
1183 
1184 inline bool operator<(
1185  const goto_programt::targett &i1,
1186  const goto_programt::targett &i2)
1187 {
1188  return &(*i1)<&(*i2);
1189 }
1190 
1191 std::list<exprt> objects_read(const goto_programt::instructiont &);
1192 std::list<exprt> objects_written(const goto_programt::instructiont &);
1193 
1194 std::list<exprt> expressions_read(const goto_programt::instructiont &);
1195 std::list<exprt> expressions_written(const goto_programt::instructiont &);
1196 
1197 std::string as_string(
1198  const namespacet &ns,
1199  const irep_idt &function,
1200  const goto_programt::instructiont &);
1201 
1202 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
goto_programt::instructiont::is_skip
bool is_skip() const
Definition: goto_program.h:435
goto_programt::instructiont::get_dead
const code_deadt & get_dead() const
Get the dead statement for DEAD.
Definition: goto_program.h:247
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_programt::instructiont::is_throw
bool is_throw() const
Definition: goto_program.h:433
goto_programt::instructiont::has_target
bool has_target() const
Definition: goto_program.h:389
goto_programt::instructiont::set_other
void set_other(codet &c)
Set the statement for OTHER.
Definition: goto_program.h:327
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
goto_programt::~goto_programt
~goto_programt()
Definition: goto_program.h:743
operator<
bool operator<(const goto_programt::const_targett &i1, const goto_programt::const_targett &i2)
Definition: goto_program.h:1177
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:334
goto_programt::instructiont::labelst
std::list< irep_idt > labelst
Goto target labels.
Definition: goto_program.h:395
goto_programt::instructiont::complete_goto
void complete_goto(targett _target)
Definition: goto_program.h:421
goto_programt::insert_after
targett insert_after(const_targett target, const instructiont &i)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:634
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:898
goto_programt::instructiont::set_assign
void set_assign(code_assignt c)
Set the assignment for ASSIGN.
Definition: goto_program.h:193
goto_programt::instructiont::to_string
std::string to_string() const
Definition: goto_program.h:520
goto_programt::instructiont::is_other
bool is_other() const
Definition: goto_program.h:437
irept::make_nil
void make_nil()
Definition: irep.h:464
goto_programt::instructiont::swap
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:481
goto_programt::const_cast_target
const_targett const_cast_target(const_targett t) const
Dummy for templates with possible const contexts.
Definition: goto_program.h:566
goto_programt::instructiont::clear
void clear(goto_program_instruction_typet _type)
Clear the node.
Definition: goto_program.h:406
goto_programt::compute_loop_numbers
void compute_loop_numbers()
Compute loop numbers.
Definition: goto_program.cpp:532
goto_programt::const_targetst
std::list< const_targett > const_targetst
Definition: goto_program.h:553
goto_programt::instructiont::get_return
const code_returnt & get_return() const
Get the return statement for READ.
Definition: goto_program.h:277
goto_programt::goto_programt
goto_programt(const goto_programt &)=delete
Copying is deleted as this class contains pointers that cannot be copied.
goto_programt::instructiont::set_return
void set_return(code_returnt c)
Set the return statement for READ.
Definition: goto_program.h:299
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:548
for_each_instruction_if
void for_each_instruction_if(GotoFunctionT &&goto_function, PredicateT predicate, HandlerT handler)
Definition: goto_program.h:1144
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:337
goto_programt::instructiont::is_dead
bool is_dead() const
Definition: goto_program.h:439
source_locationt::nil
static const source_locationt & nil()
Definition: source_location.h:188
expressions_read
std::list< exprt > expressions_read(const goto_programt::instructiont &)
Definition: goto_program.cpp:273
goto_programt::instructiont::decl_symbol
symbol_exprt & decl_symbol()
Get the declared symbol for DECL.
Definition: goto_program.h:223
goto_programt::instructiont::is_catch
bool is_catch() const
Definition: goto_program.h:434
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:540
goto_programt::copy_from
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
Definition: goto_program.cpp:625
goto_programt::instructiont::apply
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
Definition: goto_program.cpp:1015
invariant.h
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:928
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:657
goto_programt::instructiont::transform
void transform(std::function< optionalt< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
Definition: goto_program.cpp:909
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:733
exprt
Base class for all expressions.
Definition: expr.h:54
pointee_address_equalt
Functor to check whether iterators from different collections point at the same object.
Definition: goto_program.h:1135
goto_programt::insert_before_swap
void insert_before_swap(targett target, goto_programt &p)
Insertion that preserves jumps to "target".
Definition: goto_program.h:594
goto_programt::instructiont::set_decl
void set_decl(code_declt c)
Set the declaration for DECL.
Definition: goto_program.h:235
goto_programt::get_decl_identifiers
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
Definition: goto_program.cpp:230
objects_written
std::list< exprt > objects_written(const goto_programt::instructiont &)
Definition: goto_program.cpp:423
goto_programt::has_assertion
bool has_assertion() const
Does the goto program have an assertion?
Definition: goto_program.cpp:666
irep_idt
dstringt irep_idt
Definition: irep.h:37
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
goto_programt::instructiont::targets
targetst targets
The list of successor instructions.
Definition: goto_program.h:371
goto_programt::instructiont::is_incomplete_goto
bool is_incomplete_goto() const
Definition: goto_program.h:447
goto_programt::make_return
static instructiont make_return(code_returnt c, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:814
goto_programt::get_successors
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition: goto_program.h:1055
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
goto_programt::insert_before_swap
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
Definition: goto_program.h:586
goto_programt::instructiont::is_end_thread
bool is_end_thread() const
Definition: goto_program.h:445
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:891
namespace.h
goto_programt::instructiont::decl_symbol
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:212
goto_programt::instructiont::is_atomic_end
bool is_atomic_end() const
Definition: goto_program.h:443
goto_programt::instructiont::instructiont
instructiont()
Definition: goto_program.h:452
goto_programt::instructiont::get_assign
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
Definition: goto_program.h:186
objects_read
std::list< exprt > objects_read(const goto_programt::instructiont &)
Definition: goto_program.cpp:396
goto_programt::get_end_function
const_targett get_end_function() const
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:772
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:995
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:969
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
goto_programt::instructiont::get_other
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:320
goto_programt::instructiont::const_targett
std::list< instructiont >::const_iterator const_targett
Definition: goto_program.h:366
goto_programt::loop_id
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:726
goto_programt::instructiont::is_atomic_begin
bool is_atomic_begin() const
Definition: goto_program.h:442
goto_programt::instructiont::set_function_call
void set_function_call(code_function_callt c)
Set the function call for FUNCTION_CALL.
Definition: goto_program.h:313
goto_programt::targetst
std::list< targett > targetst
Definition: goto_program.h:552
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_programt::make_function_call
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1020
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:665
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
THROW
@ THROW
Definition: goto_program.h:51
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
goto_programt::insert_before
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:610
GOTO
@ GOTO
Definition: goto_program.h:35
goto_programt::equals
bool equals(const goto_programt &other) const
Syntactic equality: two goto_programt are equal if, and only if, they have the same number of instruc...
Definition: goto_program.cpp:1070
goto_programt::instructiont::validate
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
Definition: goto_program.cpp:708
goto_programt::instructiont::turn_into_skip
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
Definition: goto_program.h:416
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:864
goto_programt::compute_target_numbers
void compute_target_numbers()
Compute the target numbers.
Definition: goto_program.cpp:571
goto_programt::make_decl
static instructiont make_decl(const code_declt &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1012
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:648
goto_programt::instructiont::dead_symbol
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:254
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
deprecate.h
goto_programt::goto_programt
goto_programt(goto_programt &&other)
Definition: goto_program.h:86
goto_programt::output_instruction
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Definition: goto_program.cpp:42
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:183
goto_programt::output
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
Definition: goto_program.cpp:548
goto_programt::instructiont::targett
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
Definition: goto_program.h:365
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:822
goto_programt::instructiont::is_decl
bool is_decl() const
Definition: goto_program.h:438
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1159
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
goto_programt::compute_location_numbers
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:700
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:551
nil_exprt
The NIL expression.
Definition: std_expr.h:2735
goto_programt::instructiont::is_backwards_goto
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:508
goto_programt::instructiont::is_location
bool is_location() const
Definition: goto_program.h:436
pointee_address_equalt::operator()
bool operator()(const A &a, const B &b) const
Definition: goto_program.h:1137
goto_programt::instructiont::labels
labelst labels
Definition: goto_program.h:396
goto_programt::instructiont::get_function_call
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
Definition: goto_program.h:306
goto_programt::instructiont::equals
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard,...
Definition: goto_program.cpp:696
expressions_written
std::list< exprt > expressions_written(const goto_programt::instructiont &)
Definition: goto_program.cpp:328
source_location.h
goto_programt::instructiont::has_condition
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:344
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:34
goto_programt::make_atomic_begin
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:906
OTHER
@ OTHER
Definition: goto_program.h:38
goto_programt::goto_programt
goto_programt()
Constructor.
Definition: goto_program.h:739
validation_modet
validation_modet
Definition: validation_mode.h:13
code_deadt::symbol
symbol_exprt & symbol()
Definition: std_code.h:505
irept::id
const irep_idt & id() const
Definition: irep.h:407
goto_programt::instructiont::is_end_function
bool is_end_function() const
Definition: goto_program.h:446
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
goto_programt::validate
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
Definition: goto_program.h:800
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1224
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1391
const_target_hash
Definition: goto_program.h:1123
goto_programt::add_instruction
targett add_instruction(goto_program_instruction_typet type)
Adds an instruction of given type at the end.
Definition: goto_program.h:672
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:43
SKIP
@ SKIP
Definition: goto_program.h:39
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:499
goto_programt::instructiont::set_target
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:383
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
goto_programt::instructiont::return_value
exprt & return_value()
Get the return value of a RETURN instruction.
Definition: goto_program.h:291
goto_programt::compute_incoming_edges
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
Definition: goto_program.cpp:676
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_programt::instructiont::targetst
std::list< targett > targetst
Definition: goto_program.h:367
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:754
goto_programt::instructiont::return_value
const exprt & return_value() const
Get the return value of a RETURN instruction.
Definition: goto_program.h:284
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:640
goto_programt::output
std::ostream & output(std::ostream &out) const
Output goto-program to given stream.
Definition: goto_program.h:684
goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:33
goto_programt::instructiont::is_goto
bool is_goto() const
Definition: goto_program.h:429
goto_programt::make_return
static instructiont make_return(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:809
source_locationt
Definition: source_location.h:20
goto_programt::instructiont::get_decl
const code_declt & get_decl() const
Get the declaration for DECL.
Definition: goto_program.h:201
RETURN
@ RETURN
Definition: goto_program.h:46
goto_programt::get_end_function
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:761
goto_programt::compute_location_numbers
void compute_location_numbers()
Compute location numbers.
Definition: goto_program.h:712
goto_programt::make_goto
static instructiont make_goto(targett _target, const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:981
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
ASSIGN
@ ASSIGN
Definition: goto_program.h:47
goto_programt::instructiont::is_assert
bool is_assert() const
Definition: goto_program.h:441
goto_programt::instructiont::target_number
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:505
goto_programt::operator=
goto_programt & operator=(goto_programt &&other)
Definition: goto_program.h:91
CATCH
@ CATCH
Definition: goto_program.h:52
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1342
DECL
@ DECL
Definition: goto_program.h:48
goto_programt::instructiont::incoming_edges
std::set< targett > incoming_edges
Definition: goto_program.h:399
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
goto_programt::make_function_call
static instructiont make_function_call(exprt function, code_function_callt::argumentst arguments, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1028
goto_programt::instructiont::location_number
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:498
goto_programt::insert_before
targett insert_before(const_targett target, const instructiont &i)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:618
goto_programt::const_cast_target
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible.
Definition: goto_program.h:560
as_string
std::string as_string(const namespacet &ns, const irep_idt &function, const goto_programt::instructiont &)
goto_programt::instructiont::dead_symbol
symbol_exprt & dead_symbol()
Get the symbol for DEAD.
Definition: goto_program.h:261
ASSUME
@ ASSUME
Definition: goto_program.h:36
goto_programt::make_other
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:884
goto_programt::make_incomplete_goto
static instructiont make_incomplete_goto(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:952
goto_programt::instructiont::guard
exprt guard
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write.
Definition: goto_program.h:341
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:431
order_const_target
bool order_const_target(const goto_programt::const_targett i1, const goto_programt::const_targett i2)
Definition: goto_program.h:1112
goto_programt::instructiont::loop_number
unsigned loop_number
Number unique per function to identify loops.
Definition: goto_program.h:501
START_THREAD
@ START_THREAD
Definition: goto_program.h:40
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:50
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
operator<<
std::ostream & operator<<(std::ostream &, goto_program_instruction_typet)
Outputs a string representation of a goto_program_instruction_typet
Definition: goto_program.cpp:1102
goto_programt::insert_after
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:626
goto_programt::instructiont::set_condition
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:357
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:45
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:551
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:876
DEAD
@ DEAD
Definition: goto_program.h:49
goto_programt::instructiont::const_targetst
std::list< const_targett > const_targetst
Definition: goto_program.h:368
goto_programt::operator=
goto_programt & operator=(const goto_programt &)=delete
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:44
goto_programt::make_incomplete_goto
static instructiont make_incomplete_goto(const code_gotot &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:962
goto_programt::instructiont::is_assume
bool is_assume() const
Definition: goto_program.h:440
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
goto_programt::instructiont::set_dead
void set_dead(code_deadt c)
Set the dead statement for DEAD.
Definition: goto_program.h:269
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:577
symbol_table.h
Author: Diffblue Ltd.
goto_programt::make_throw
static instructiont make_throw(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:843
for_each_instruction
void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
Definition: goto_program.h:1160
code_returnt::return_value
const exprt & return_value() const
Definition: std_code.h:1352
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
goto_programt::instructiont::is_start_thread
bool is_start_thread() const
Definition: goto_program.h:444
true_exprt
The Boolean constant true.
Definition: std_expr.h:2717
goto_programt::instructiont::get_condition
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:350
LOCATION
@ LOCATION
Definition: goto_program.h:42
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:432
ASSERT
@ ASSERT
Definition: goto_program.h:37
goto_programt::decl_identifierst
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:787
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
std_expr.h
API to expression classes.
goto_programt::instructiont::is_target
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:402
goto_programt::instructiont::instructiont
instructiont(codet _code, source_locationt _source_location, goto_program_instruction_typet _type, exprt _guard, targetst _targets)
Constructor that can set all members, passed by value.
Definition: goto_program.h:466
goto_programt::instructiont::nil_target
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:492
goto_programt::make_location
static instructiont make_location(const source_locationt &l)
Definition: goto_program.h:832
goto_programt::instructiont::get_target
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:375
END_THREAD
@ END_THREAD
Definition: goto_program.h:41
goto_programt::swap
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:748
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:53
goto_programt::make_assignment
static instructiont make_assignment(exprt lhs, exprt rhs, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1003
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:550
goto_programt::instructiont::instructiont
instructiont(goto_program_instruction_typet _type)
Definition: goto_program.h:457
goto_programt::make_incomplete_goto
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:938
const_target_hash::operator()
std::size_t operator()(const goto_programt::const_targett t) const
Definition: goto_program.h:1124
goto_programt::make_catch
static instructiont make_catch(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:854
goto_programt::instructiont::is_return
bool is_return() const
Definition: goto_program.h:430
goto_programt::make_atomic_end
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:917
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35