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/invariant.h>
22 #include <util/namespace.h>
23 #include <util/source_location.h>
24 #include <util/std_code.h>
25 #include <util/std_expr.h>
26 #include <util/symbol_table.h>
27 
28 enum class validation_modet;
29 
32 {
34  GOTO = 1, // branch, possibly guarded
35  ASSUME = 2, // non-failing guarded self loop
36  ASSERT = 3, // assertions
37  OTHER = 4, // anything else
38  SKIP = 5, // just advance the PC
39  START_THREAD = 6, // spawns an asynchronous thread
40  END_THREAD = 7, // end the current thread
41  LOCATION = 8, // semantically like SKIP
42  END_FUNCTION = 9, // exit point of a function
43  ATOMIC_BEGIN = 10, // marks a block without interleavings
44  ATOMIC_END = 11, // end of a block without interleavings
45  RETURN = 12, // set function return value (no control-flow change)
46  ASSIGN = 13, // assignment lhs:=rhs
47  DECL = 14, // declare a local variable
48  DEAD = 15, // marks the end-of-live of a local variable
49  FUNCTION_CALL = 16, // call a function
50  THROW = 17, // throw an exception
51  CATCH = 18, // push, pop or enter an exception handler
52  INCOMPLETE_GOTO = 19 // goto where target is yet to be determined
53 };
54 
55 std::ostream &operator<<(std::ostream &, goto_program_instruction_typet);
56 
73 {
74 public:
76  goto_programt(const goto_programt &)=delete;
77  goto_programt &operator=(const goto_programt &)=delete;
78 
79  // Move operations need to be explicitly enabled as they are deleted with the
80  // copy operations
81  // default for move operations isn't available on Windows yet, so define
82  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
83  // under "Defaulted and Deleted Functions")
84 
86  instructions(std::move(other.instructions))
87  {
88  }
89 
91  {
92  instructions=std::move(other.instructions);
93  return *this;
94  }
95 
178  class instructiont final
179  {
180  public:
183 
185  const code_assignt &get_assign() const
186  {
188  return to_code_assign(code);
189  }
190 
193  {
195  code = std::move(c);
196  }
197 
199  const code_declt &get_decl() const
200  {
202  return to_code_decl(code);
203  }
204 
207  {
209  code = std::move(c);
210  }
211 
213  const code_deadt &get_dead() const
214  {
216  return to_code_dead(code);
217  }
218 
221  {
223  code = std::move(c);
224  }
225 
227  const code_returnt &get_return() const
228  {
230  return to_code_return(code);
231  }
232 
235  {
237  code = std::move(c);
238  }
239 
242  {
244  return to_code_function_call(code);
245  }
246 
249  {
251  code = std::move(c);
252  }
253 
255  const codet &get_other() const
256  {
258  return code;
259  }
260 
262  void set_other(codet &c)
263  {
265  code = std::move(c);
266  }
267 
270 
273 
277 
279  bool has_condition() const
280  {
281  return is_goto() || is_incomplete_goto() || is_assume() || is_assert();
282  }
283 
285  const exprt &get_condition() const
286  {
288  return guard;
289  }
290 
293  {
295  guard = std::move(c);
296  }
297 
298  // The below will eventually become a single target only.
300  typedef std::list<instructiont>::iterator targett;
301  typedef std::list<instructiont>::const_iterator const_targett;
302  typedef std::list<targett> targetst;
303  typedef std::list<const_targett> const_targetst;
304 
307 
311  {
312  PRECONDITION(targets.size()==1);
313  return targets.front();
314  }
315 
319  {
320  targets.clear();
321  targets.push_back(t);
322  }
323 
324  bool has_target() const
325  {
326  return !targets.empty();
327  }
328 
330  typedef std::list<irep_idt> labelst;
332 
333  // will go away
334  std::set<targett> incoming_edges;
335 
337  bool is_target() const
338  { return target_number!=nil_target; }
339 
342  {
343  type=_type;
344  targets.clear();
345  guard=true_exprt();
346  code.make_nil();
347  }
348 
352  {
353  clear(SKIP);
354  }
355 
356  DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_return() instead"))
357  void make_return() { clear(RETURN); }
358 
359  DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_skip() instead"))
360  void make_skip() { clear(SKIP); }
361 
362  DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_location() instead"))
365 
366  DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_throw() instead"))
367  void make_throw() { clear(THROW); }
368 
369  DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_catch() instead"))
370  void make_catch() { clear(CATCH); }
371 
372  DEPRECATED(
373  SINCE(2019, 2, 13, "use goto_programt::make_assertion() instead"))
374  void make_assertion(const exprt &g) { clear(ASSERT); guard=g; }
375 
376  DEPRECATED(
377  SINCE(2019, 2, 13, "use goto_programt::make_assumption() instead"))
378  void make_assumption(const exprt &g) { clear(ASSUME); guard=g; }
379 
380  DEPRECATED(
381  SINCE(2019, 2, 13, "use goto_programt::make_assignment() instead"))
383 
384  DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_other() instead"))
385  void make_other(const codet &_code) { clear(OTHER); code=_code; }
386 
387  DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_decl() instead"))
388  void make_decl() { clear(DECL); }
389 
390  DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_dead() instead"))
391  void make_dead() { clear(DEAD); }
392 
393  DEPRECATED(
394  SINCE(2019, 2, 13, "use goto_programt::make_atomic_begin() instead"))
396 
397  DEPRECATED(
398  SINCE(2019, 2, 13, "use goto_programt::make_atomic_end() instead"))
400 
401  DEPRECATED(
402  SINCE(2019, 2, 13, "use goto_programt::make_end_function() instead"))
404 
405  DEPRECATED(
406  SINCE(2019, 2, 13, "use goto_programt::make_incomplete_goto() instead"))
407  void make_incomplete_goto(const code_gotot &_code)
408  {
410  code = _code;
411  }
412 
413  DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_goto() instead"))
414  void make_goto(targett _target)
415  {
416  clear(GOTO);
417  targets.push_back(_target);
418  }
419 
420  DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_goto() instead"))
421  void make_goto(targett _target, const exprt &g)
422  {
423  make_goto(_target);
424  guard=g;
425  }
426 
427  void complete_goto(targett _target)
428  {
430  code.make_nil();
431  targets.push_back(_target);
432  type = GOTO;
433  }
434 
435  DEPRECATED(
436  SINCE(2019, 2, 13, "use goto_programt::make_assignment() instead"))
437  void make_assignment(const code_assignt &_code)
438  {
439  clear(ASSIGN);
440  code=_code;
441  }
442 
443  DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_decl() instead"))
444  void make_decl(const code_declt &_code)
445  {
446  clear(DECL);
447  code=_code;
448  }
449 
450  DEPRECATED(
451  SINCE(2019, 2, 13, "use goto_programt::make_function_call() instead"))
453  {
455  code=_code;
456  }
457 
458  bool is_goto () const { return type==GOTO; }
459  bool is_return () const { return type==RETURN; }
460  bool is_assign () const { return type==ASSIGN; }
461  bool is_function_call() const { return type==FUNCTION_CALL; }
462  bool is_throw () const { return type==THROW; }
463  bool is_catch () const { return type==CATCH; }
464  bool is_skip () const { return type==SKIP; }
465  bool is_location () const { return type==LOCATION; }
466  bool is_other () const { return type==OTHER; }
467  bool is_decl () const { return type==DECL; }
468  bool is_dead () const { return type==DEAD; }
469  bool is_assume () const { return type==ASSUME; }
470  bool is_assert () const { return type==ASSERT; }
471  bool is_atomic_begin () const { return type==ATOMIC_BEGIN; }
472  bool is_atomic_end () const { return type==ATOMIC_END; }
473  bool is_start_thread () const { return type==START_THREAD; }
474  bool is_end_thread () const { return type==END_THREAD; }
475  bool is_end_function () const { return type==END_FUNCTION; }
476  bool is_incomplete_goto() const
477  {
478  return type == INCOMPLETE_GOTO;
479  }
480 
482  instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit)
483  {
484  }
485 
487  : code(static_cast<const codet &>(get_nil_irep())),
488  source_location(static_cast<const source_locationt &>(get_nil_irep())),
489  type(_type),
490  guard(true_exprt())
491  {
492  }
493 
496  codet _code,
497  source_locationt _source_location,
499  exprt _guard,
500  targetst _targets)
501  : code(std::move(_code)),
502  source_location(std::move(_source_location)),
503  type(_type),
504  guard(std::move(_guard)),
505  targets(std::move(_targets))
506  {
507  }
508 
510  void swap(instructiont &instruction)
511  {
512  using std::swap;
513  swap(instruction.code, code);
514  swap(instruction.source_location, source_location);
515  swap(instruction.type, type);
516  swap(instruction.guard, guard);
517  swap(instruction.targets, targets);
518  }
519 
521  static const unsigned nil_target=
522  std::numeric_limits<unsigned>::max();
523 
527  unsigned location_number = 0;
528 
530  unsigned loop_number = 0;
531 
535 
537  bool is_backwards_goto() const
538  {
539  if(!is_goto())
540  return false;
541 
542  for(const auto &t : targets)
543  if(t->location_number<=location_number)
544  return true;
545 
546  return false;
547  }
548 
549  std::string to_string() const
550  {
551  std::ostringstream instruction_id_builder;
552  instruction_id_builder << type;
553  return instruction_id_builder.str();
554  }
555 
560  bool equals(const instructiont &other) const;
561 
566  void validate(const namespacet &ns, const validation_modet vm) const;
567 
570  void transform(std::function<optionalt<exprt>(exprt)>);
571 
573  void apply(std::function<void(const exprt &)>) const;
574  };
575 
576  // Never try to change this to vector-we mutate the list while iterating
577  typedef std::list<instructiont> instructionst;
578 
579  typedef instructionst::iterator targett;
580  typedef instructionst::const_iterator const_targett;
581  typedef std::list<targett> targetst;
582  typedef std::list<const_targett> const_targetst;
583 
586 
590  {
591  return instructions.erase(t, t);
592  }
593 
596  {
597  return t;
598  }
599 
600  template <typename Target>
601  std::list<Target> get_successors(Target target) const;
602 
603  void compute_incoming_edges();
604 
607  {
608  PRECONDITION(target!=instructions.end());
609  const auto next=std::next(target);
610  instructions.insert(next, instructiont())->swap(*target);
611  }
612 
615  void insert_before_swap(targett target, instructiont &instruction)
616  {
617  insert_before_swap(target);
618  target->swap(instruction);
619  }
620 
624  targett target,
625  goto_programt &p)
626  {
627  PRECONDITION(target!=instructions.end());
628  if(p.instructions.empty())
629  return;
630  insert_before_swap(target, p.instructions.front());
631  auto next=std::next(target);
632  p.instructions.erase(p.instructions.begin());
633  instructions.splice(next, p.instructions);
634  }
635 
640  {
641  return instructions.insert(target, instructiont());
642  }
643 
648  {
649  return instructions.insert(target, i);
650  }
651 
656  {
657  return instructions.insert(std::next(target), instructiont());
658  }
659 
664  {
665  return instructions.insert(std::next(target), i);
666  }
667 
670  {
671  instructions.splice(instructions.end(),
672  p.instructions);
673  }
674 
678  const_targett target,
679  goto_programt &p)
680  {
681  instructions.splice(target, p.instructions);
682  }
683 
686  targett add(instructiont &&instruction)
687  {
688  instructions.push_back(std::move(instruction));
689  return --instructions.end();
690  }
691 
695  {
696  return add(instructiont());
697  }
698 
702  {
703  return add(instructiont(type));
704  }
705 
707  std::ostream &output(
708  const namespacet &ns,
709  const irep_idt &identifier,
710  std::ostream &out) const;
711 
713  std::ostream &output(std::ostream &out) const
714  {
715  return output(namespacet(symbol_tablet()), irep_idt(), out);
716  }
717 
719  std::ostream &output_instruction(
720  const namespacet &ns,
721  const irep_idt &identifier,
722  std::ostream &out,
723  const instructionst::value_type &instruction) const;
724 
726  void compute_target_numbers();
727 
729  void compute_location_numbers(unsigned &nr)
730  {
731  for(auto &i : instructions)
732  {
733  INVARIANT(
734  nr != std::numeric_limits<unsigned>::max(),
735  "Too many location numbers assigned");
736  i.location_number=nr++;
737  }
738  }
739 
742  {
743  unsigned nr=0;
745  }
746 
748  void compute_loop_numbers();
749 
751  void update();
752 
754  static irep_idt
755  loop_id(const irep_idt &function_id, const instructiont &instruction)
756  {
757  return id2string(function_id) + "." +
758  std::to_string(instruction.loop_number);
759  }
760 
762  bool empty() const
763  {
764  return instructions.empty();
765  }
766 
769  {
770  }
771 
773  {
774  }
775 
777  void swap(goto_programt &program)
778  {
779  program.instructions.swap(instructions);
780  }
781 
783  void clear()
784  {
785  instructions.clear();
786  }
787 
791  {
792  PRECONDITION(!instructions.empty());
793  const auto end_function=std::prev(instructions.end());
794  DATA_INVARIANT(end_function->is_end_function(),
795  "goto program ends on END_FUNCTION");
796  return end_function;
797  }
798 
802  {
803  PRECONDITION(!instructions.empty());
804  const auto end_function=std::prev(instructions.end());
805  DATA_INVARIANT(end_function->is_end_function(),
806  "goto program ends on END_FUNCTION");
807  return end_function;
808  }
809 
811  void copy_from(const goto_programt &src);
812 
814  bool has_assertion() const;
815 
816  typedef std::set<irep_idt> decl_identifierst;
818  void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
819 
823  bool equals(const goto_programt &other) const;
824 
829  void validate(const namespacet &ns, const validation_modet vm) const
830  {
831  for(const instructiont &ins : instructions)
832  {
833  ins.validate(ns, vm);
834  }
835  }
836 
837  static instructiont
839  {
840  return instructiont(code_returnt(), l, RETURN, nil_exprt(), {});
841  }
842 
844  code_returnt c,
846  {
847  return instructiont(std::move(c), l, RETURN, nil_exprt(), {});
848  }
849 
850  static instructiont
852  {
853  return instructiont(
854  static_cast<const codet &>(get_nil_irep()),
855  l,
856  SKIP,
857  nil_exprt(),
858  {});
859  }
860 
862  {
863  return instructiont(
864  static_cast<const codet &>(get_nil_irep()),
865  l,
866  LOCATION,
867  nil_exprt(),
868  {});
869  }
870 
871  static instructiont
873  {
874  return instructiont(
875  static_cast<const codet &>(get_nil_irep()),
876  l,
877  THROW,
878  nil_exprt(),
879  {});
880  }
881 
882  static instructiont
884  {
885  return instructiont(
886  static_cast<const codet &>(get_nil_irep()),
887  l,
888  CATCH,
889  nil_exprt(),
890  {});
891  }
892 
894  const exprt &g,
896  {
897  return instructiont(
898  static_cast<const codet &>(get_nil_irep()),
899  l,
900  ASSERT,
901  exprt(g),
902  {});
903  }
904 
906  const exprt &g,
908  {
909  return instructiont(
910  static_cast<const codet &>(get_nil_irep()), l, ASSUME, g, {});
911  }
912 
914  const codet &_code,
916  {
917  return instructiont(_code, l, OTHER, nil_exprt(), {});
918  }
919 
921  const symbol_exprt &symbol,
923  {
924  return instructiont(code_declt(symbol), l, DECL, nil_exprt(), {});
925  }
926 
928  const symbol_exprt &symbol,
930  {
931  return instructiont(code_deadt(symbol), l, DEAD, nil_exprt(), {});
932  }
933 
934  static instructiont
936  {
937  return instructiont(
938  static_cast<const codet &>(get_nil_irep()),
939  l,
940  ATOMIC_BEGIN,
941  nil_exprt(),
942  {});
943  }
944 
945  static instructiont
947  {
948  return instructiont(
949  static_cast<const codet &>(get_nil_irep()),
950  l,
951  ATOMIC_END,
952  nil_exprt(),
953  {});
954  }
955 
956  static instructiont
958  {
959  return instructiont(
960  static_cast<const codet &>(get_nil_irep()),
961  l,
962  END_FUNCTION,
963  nil_exprt(),
964  {});
965  }
966 
968  const exprt &_cond,
970  {
971  PRECONDITION(_cond.type().id() == ID_bool);
972  return instructiont(
973  static_cast<const codet &>(get_nil_irep()),
974  l,
976  _cond,
977  {});
978  }
979 
980  static instructiont
982  {
983  return instructiont(
984  static_cast<const codet &>(get_nil_irep()),
985  l,
987  true_exprt(),
988  {});
989  }
990 
992  const code_gotot &_code,
994  {
995  return instructiont(_code, l, INCOMPLETE_GOTO, true_exprt(), {});
996  }
997 
999  targett _target,
1001  {
1002  return instructiont(
1003  static_cast<const codet &>(get_nil_irep()),
1004  l,
1005  GOTO,
1006  true_exprt(),
1007  {_target});
1008  }
1009 
1011  targett _target,
1012  const exprt &g,
1014  {
1015  return instructiont(
1016  static_cast<const codet &>(get_nil_irep()),
1017  l,
1018  GOTO,
1019  g,
1020  {_target});
1021  }
1022 
1025  const code_assignt &_code,
1027  {
1028  return instructiont(_code, l, ASSIGN, nil_exprt(), {});
1029  }
1030 
1033  exprt lhs,
1034  exprt rhs,
1036  {
1037  return instructiont(
1038  code_assignt(std::move(lhs), std::move(rhs)), l, ASSIGN, nil_exprt(), {});
1039  }
1040 
1042  const code_declt &_code,
1044  {
1045  return instructiont(_code, l, DECL, nil_exprt(), {});
1046  }
1047 
1050  const code_function_callt &_code,
1052  {
1053  return instructiont(_code, l, FUNCTION_CALL, nil_exprt(), {});
1054  }
1055 
1058  exprt function,
1061  {
1062  return instructiont(
1063  code_function_callt(std::move(function), std::move(arguments)),
1064  l,
1065  FUNCTION_CALL,
1066  nil_exprt(),
1067  {});
1068  }
1069 };
1070 
1083 template <typename Target>
1085  Target target) const
1086 {
1087  if(target==instructions.end())
1088  return std::list<Target>();
1089 
1090  const auto next=std::next(target);
1091 
1092  const instructiont &i=*target;
1093 
1094  if(i.is_goto())
1095  {
1096  std::list<Target> successors(i.targets.begin(), i.targets.end());
1097 
1098  if(!i.get_condition().is_true() && next != instructions.end())
1099  successors.push_back(next);
1100 
1101  return successors;
1102  }
1103 
1104  if(i.is_start_thread())
1105  {
1106  std::list<Target> successors(i.targets.begin(), i.targets.end());
1107 
1108  if(next!=instructions.end())
1109  successors.push_back(next);
1110 
1111  return successors;
1112  }
1113 
1114  if(i.is_end_thread())
1115  {
1116  // no successors
1117  return std::list<Target>();
1118  }
1119 
1120  if(i.is_throw())
1121  {
1122  // the successors are non-obvious
1123  return std::list<Target>();
1124  }
1125 
1126  if(i.is_assume())
1127  {
1128  return !i.get_condition().is_false() && next != instructions.end()
1129  ? std::list<Target>{next}
1130  : std::list<Target>();
1131  }
1132 
1133  if(next!=instructions.end())
1134  {
1135  return std::list<Target>{next};
1136  }
1137 
1138  return std::list<Target>();
1139 }
1140 
1144 {
1145  const goto_programt::instructiont &_i1=*i1;
1146  const goto_programt::instructiont &_i2=*i2;
1147  return &_i1<&_i2;
1148 }
1149 
1150 // NOLINTNEXTLINE(readability/identifiers)
1152 {
1153  std::size_t operator()(
1154  const goto_programt::const_targett t) const
1155  {
1156  using hash_typet = decltype(&(*t));
1157  return std::hash<hash_typet>{}(&(*t));
1158  }
1159 };
1160 
1164 {
1165  template <class A, class B>
1166  bool operator()(const A &a, const B &b) const
1167  {
1168  return &(*a) == &(*b);
1169  }
1170 };
1171 
1172 #define forall_goto_program_instructions(it, program) \
1173  for(goto_programt::instructionst::const_iterator \
1174  it=(program).instructions.begin(); \
1175  it!=(program).instructions.end(); it++)
1176 
1177 #define Forall_goto_program_instructions(it, program) \
1178  for(goto_programt::instructionst::iterator \
1179  it=(program).instructions.begin(); \
1180  it!=(program).instructions.end(); it++)
1181 
1182 inline bool operator<(
1183  const goto_programt::const_targett &i1,
1184  const goto_programt::const_targett &i2)
1185 {
1186  return order_const_target(i1, i2);
1187 }
1188 
1189 inline bool operator<(
1190  const goto_programt::targett &i1,
1191  const goto_programt::targett &i2)
1192 {
1193  return &(*i1)<&(*i2);
1194 }
1195 
1196 std::list<exprt> objects_read(const goto_programt::instructiont &);
1197 std::list<exprt> objects_written(const goto_programt::instructiont &);
1198 
1199 std::list<exprt> expressions_read(const goto_programt::instructiont &);
1200 std::list<exprt> expressions_written(const goto_programt::instructiont &);
1201 
1202 std::string as_string(
1203  const namespacet &ns,
1204  const irep_idt &function,
1205  const goto_programt::instructiont &);
1206 
1207 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
goto_programt::instructiont::is_skip
bool is_skip() const
Definition: goto_program.h:464
goto_programt::instructiont::get_dead
const code_deadt & get_dead() const
Get the dead statement for DEAD.
Definition: goto_program.h:213
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
goto_programt::instructiont::is_throw
bool is_throw() const
Definition: goto_program.h:462
goto_programt::instructiont::has_target
bool has_target() const
Definition: goto_program.h:324
goto_programt::instructiont::set_other
void set_other(codet &c)
Set the statement for OTHER.
Definition: goto_program.h:262
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
goto_programt::~goto_programt
~goto_programt()
Definition: goto_program.h:772
operator<
bool operator<(const goto_programt::const_targett &i1, const goto_programt::const_targett &i2)
Definition: goto_program.h:1182
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:269
goto_programt::instructiont::labelst
std::list< irep_idt > labelst
Goto target labels.
Definition: goto_program.h:330
goto_programt::instructiont::complete_goto
void complete_goto(targett _target)
Definition: goto_program.h:427
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:663
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:927
goto_programt::instructiont::make_function_call
void make_function_call(const code_function_callt &_code)
Definition: goto_program.h:452
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:453
goto_programt::instructiont::set_assign
void set_assign(code_assignt c)
Set the assignment for ASSIGN.
Definition: goto_program.h:192
goto_programt::instructiont::to_string
std::string to_string() const
Definition: goto_program.h:549
goto_programt::instructiont::is_other
bool is_other() const
Definition: goto_program.h:466
goto_programt::instructiont::make_end_function
void make_end_function()
Definition: goto_program.h:403
irept::make_nil
void make_nil()
Definition: irep.h:475
goto_programt::instructiont::swap
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:510
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:595
goto_programt::instructiont::clear
void clear(goto_program_instruction_typet _type)
Clear the node.
Definition: goto_program.h:341
goto_programt::compute_loop_numbers
void compute_loop_numbers()
Compute loop numbers.
Definition: goto_program.cpp:533
goto_programt::const_targetst
std::list< const_targett > const_targetst
Definition: goto_program.h:582
goto_programt::instructiont::get_return
const code_returnt & get_return() const
Get the return statement for READ.
Definition: goto_program.h:227
goto_programt::instructiont::set_return
void set_return(code_returnt c)
Set the return statement for READ.
Definition: goto_program.h:234
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:577
goto_programt::instructiont::make_dead
void make_dead()
Definition: goto_program.h:391
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:272
goto_programt::instructiont::make_incomplete_goto
void make_incomplete_goto(const code_gotot &_code)
Definition: goto_program.h:407
goto_programt::instructiont::is_dead
bool is_dead() const
Definition: goto_program.h:468
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::is_catch
bool is_catch() const
Definition: goto_program.h:463
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:541
goto_programt::copy_from
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
Definition: goto_program.cpp:626
goto_programt::instructiont::apply
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
Definition: goto_program.cpp:1028
invariant.h
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:404
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:957
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
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:910
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:762
exprt
Base class for all expressions.
Definition: expr.h:52
pointee_address_equalt
Functor to check whether iterators from different collections point at the same object.
Definition: goto_program.h:1163
goto_programt::insert_before_swap
void insert_before_swap(targett target, goto_programt &p)
Insertion that preserves jumps to "target".
Definition: goto_program.h:623
goto_programt::instructiont::set_decl
void set_decl(code_declt c)
Set the declaration for DECL.
Definition: goto_program.h:206
goto_programt::get_decl_identifiers
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
Definition: goto_program.cpp:229
objects_written
std::list< exprt > objects_written(const goto_programt::instructiont &)
Definition: goto_program.cpp:424
goto_programt::has_assertion
bool has_assertion() const
Does the goto program have an assertion?
Definition: goto_program.cpp:667
irep_idt
dstringt irep_idt
Definition: irep.h:32
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:306
goto_programt::instructiont::is_incomplete_goto
bool is_incomplete_goto() const
Definition: goto_program.h:476
goto_programt::make_return
static instructiont make_return(code_returnt c, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:843
goto_programt::get_successors
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition: goto_program.h:1084
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
goto_programt::insert_before_swap
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
Definition: goto_program.h:615
goto_programt::instructiont::is_end_thread
bool is_end_thread() const
Definition: goto_program.h:474
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:88
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:920
namespace.h
goto_programt::instructiont::is_atomic_end
bool is_atomic_end() const
Definition: goto_program.h:472
goto_programt::instructiont::instructiont
instructiont()
Definition: goto_program.h:481
goto_programt::instructiont::get_assign
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
Definition: goto_program.h:185
objects_read
std::list< exprt > objects_read(const goto_programt::instructiont &)
Definition: goto_program.cpp:397
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:801
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:1024
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:998
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
goto_programt::instructiont::get_other
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:255
goto_programt::instructiont::const_targett
std::list< instructiont >::const_iterator const_targett
Definition: goto_program.h:301
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:755
goto_programt::instructiont::is_atomic_begin
bool is_atomic_begin() const
Definition: goto_program.h:471
goto_programt::instructiont::make_decl
void make_decl()
Definition: goto_program.h:388
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:248
goto_programt::targetst
std::list< targett > targetst
Definition: goto_program.h:581
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
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:1049
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:694
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
THROW
Definition: goto_program.h:50
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1204
coverage_criteriont::LOCATION
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:639
GOTO
Definition: goto_program.h:34
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:1083
goto_programt::instructiont::make_other
void make_other(const codet &_code)
Definition: goto_program.h:385
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:709
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:351
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
goto_programt::compute_target_numbers
void compute_target_numbers()
Compute the target numbers.
Definition: goto_program.cpp:572
goto_programt::make_decl
static instructiont make_decl(const code_declt &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1041
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:677
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
goto_programt::goto_programt
goto_programt(goto_programt &&other)
Definition: goto_program.h:85
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:41
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
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:549
goto_programt::instructiont::targett
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
Definition: goto_program.h:300
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:851
goto_programt::instructiont::is_decl
bool is_decl() const
Definition: goto_program.h:467
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1148
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:729
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:522
nil_exprt
The NIL expression.
Definition: std_expr.h:4162
goto_programt::instructiont::is_backwards_goto
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:537
goto_programt::instructiont::is_location
bool is_location() const
Definition: goto_program.h:465
pointee_address_equalt::operator()
bool operator()(const A &a, const B &b) const
Definition: goto_program.h:1166
goto_programt::instructiont::labels
labelst labels
Definition: goto_program.h:331
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:241
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:697
expressions_written
std::list< exprt > expressions_written(const goto_programt::instructiont &)
Definition: goto_program.cpp:329
source_location.h
goto_programt::instructiont::has_condition
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:279
NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
goto_programt::make_atomic_begin
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:935
OTHER
Definition: goto_program.h:37
goto_programt::goto_programt
goto_programt()
Constructor.
Definition: goto_program.h:768
validation_modet
validation_modet
Definition: validation_mode.h:12
irept::id
const irep_idt & id() const
Definition: irep.h:418
goto_programt::instructiont::is_end_function
bool is_end_function() const
Definition: goto_program.h:475
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1316
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:829
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1214
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1381
const_target_hash
Definition: goto_program.h:1151
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:701
END_FUNCTION
Definition: goto_program.h:42
SKIP
Definition: goto_program.h:38
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:469
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:318
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
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:677
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_programt::instructiont::make_goto
void make_goto(targett _target)
Definition: goto_program.h:414
goto_programt::instructiont::targetst
std::list< targett > targetst
Definition: goto_program.h:302
goto_programt::instructiont::make_assignment
void make_assignment()
Definition: goto_program.h:382
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:783
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:669
goto_programt::output
std::ostream & output(std::ostream &out) const
Output goto-program to given stream.
Definition: goto_program.h:713
goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:31
goto_programt::instructiont::is_goto
bool is_goto() const
Definition: goto_program.h:458
goto_programt::make_return
static instructiont make_return(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:838
source_locationt
Definition: source_location.h:19
goto_programt::instructiont::make_atomic_begin
void make_atomic_begin()
Definition: goto_program.h:395
goto_programt::instructiont::get_decl
const code_declt & get_decl() const
Get the declaration for DECL.
Definition: goto_program.h:199
RETURN
Definition: goto_program.h:45
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:790
goto_programt::compute_location_numbers
void compute_location_numbers()
Compute location numbers.
Definition: goto_program.h:741
goto_programt::make_goto
static instructiont make_goto(targett _target, const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1010
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
ASSIGN
Definition: goto_program.h:46
goto_programt::instructiont::is_assert
bool is_assert() const
Definition: goto_program.h:470
goto_programt::instructiont::target_number
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:534
goto_programt::operator=
goto_programt & operator=(goto_programt &&other)
Definition: goto_program.h:90
CATCH
Definition: goto_program.h:51
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1331
DECL
Definition: goto_program.h:47
goto_programt::instructiont::incoming_edges
std::set< targett > incoming_edges
Definition: goto_program.h:334
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:386
goto_programt::instructiont::make_assumption
void make_assumption(const exprt &g)
Definition: goto_program.h:378
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:1057
goto_programt::instructiont::location_number
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:527
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:647
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:589
as_string
std::string as_string(const namespacet &ns, const irep_idt &function, const goto_programt::instructiont &)
goto_programt::instructiont::make_return
void make_return()
Definition: goto_program.h:357
ASSUME
Definition: goto_program.h:35
goto_programt::make_other
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:913
goto_programt::make_incomplete_goto
static instructiont make_incomplete_goto(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:981
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:276
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:460
order_const_target
bool order_const_target(const goto_programt::const_targett i1, const goto_programt::const_targett i2)
Definition: goto_program.h:1141
goto_programt::instructiont::loop_number
unsigned loop_number
Number unique per function to identify loops.
Definition: goto_program.h:530
START_THREAD
Definition: goto_program.h:39
FUNCTION_CALL
Definition: goto_program.h:49
goto_programt::instructiont::make_location
void make_location(const source_locationt &l)
Definition: goto_program.h:363
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
operator<<
std::ostream & operator<<(std::ostream &, goto_program_instruction_typet)
Outputs a string representation of a goto_program_instruction_typet
Definition: goto_program.cpp:1115
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:655
goto_programt::instructiont::set_condition
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:292
goto_programt::instructiont::make_atomic_end
void make_atomic_end()
Definition: goto_program.h:399
ATOMIC_END
Definition: goto_program.h:44
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
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:905
DEAD
Definition: goto_program.h:48
goto_programt::instructiont::const_targetst
std::list< const_targett > const_targetst
Definition: goto_program.h:303
goto_programt::operator=
goto_programt & operator=(const goto_programt &)=delete
goto_programt::instructiont::make_throw
void make_throw()
Definition: goto_program.h:367
ATOMIC_BEGIN
Definition: goto_program.h:43
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:991
goto_programt::instructiont::is_assume
bool is_assume() const
Definition: goto_program.h:469
goto_programt::instructiont::set_dead
void set_dead(code_deadt c)
Set the dead statement for DEAD.
Definition: goto_program.h:220
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:606
symbol_table.h
Author: Diffblue Ltd.
goto_programt::instructiont::make_assertion
void make_assertion(const exprt &g)
Definition: goto_program.h:374
goto_programt::make_throw
static instructiont make_throw(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:872
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:297
goto_programt::instructiont::is_start_thread
bool is_start_thread() const
Definition: goto_program.h:473
true_exprt
The Boolean constant true.
Definition: std_expr.h:4144
goto_programt::instructiont::get_condition
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:285
goto_programt::instructiont::make_catch
void make_catch()
Definition: goto_program.h:370
LOCATION
Definition: goto_program.h:41
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:461
ASSERT
Definition: goto_program.h:36
goto_programt::decl_identifierst
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:816
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
std_expr.h
goto_programt::instructiont::is_target
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:337
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:495
goto_programt::instructiont::nil_target
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:521
goto_programt::make_location
static instructiont make_location(const source_locationt &l)
Definition: goto_program.h:861
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:310
END_THREAD
Definition: goto_program.h:40
goto_programt::swap
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:777
INCOMPLETE_GOTO
Definition: goto_program.h:52
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:1032
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
goto_programt::instructiont::instructiont
instructiont(goto_program_instruction_typet _type)
Definition: goto_program.h:486
goto_programt::make_incomplete_goto
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:967
validation_modet::INVARIANT
const_target_hash::operator()
std::size_t operator()(const goto_programt::const_targett t) const
Definition: goto_program.h:1153
goto_programt::make_catch
static instructiont make_catch(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:883
goto_programt::instructiont::is_return
bool is_return() const
Definition: goto_program.h:459
goto_programt::make_atomic_end
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:946
goto_programt::instructiont::make_skip
void make_skip()
Definition: goto_program.h:360
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34