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("use goto_programt::make_return() instead")
357  void make_return() { clear(RETURN); }
358 
359  DEPRECATED("use goto_programt::make_skip() instead")
360  void make_skip() { clear(SKIP); }
361 
362  DEPRECATED("use goto_programt::make_location() instead")
365 
366  DEPRECATED("use goto_programt::make_throw() instead")
367  void make_throw() { clear(THROW); }
368 
369  DEPRECATED("use goto_programt::make_catch() instead")
370  void make_catch() { clear(CATCH); }
371 
372  DEPRECATED("use goto_programt::make_assertion() instead")
373  void make_assertion(const exprt &g) { clear(ASSERT); guard=g; }
374 
375  DEPRECATED("use goto_programt::make_assumption() instead")
376  void make_assumption(const exprt &g) { clear(ASSUME); guard=g; }
377 
378  DEPRECATED("use goto_programt::make_assignment() instead")
380 
381  DEPRECATED("use goto_programt::make_other() instead")
382  void make_other(const codet &_code) { clear(OTHER); code=_code; }
383 
384  DEPRECATED("use goto_programt::make_decl() instead")
385  void make_decl() { clear(DECL); }
386 
387  DEPRECATED("use goto_programt::make_dead() instead")
388  void make_dead() { clear(DEAD); }
389 
390  DEPRECATED("use goto_programt::make_atomic_begin() instead")
392 
393  DEPRECATED("use goto_programt::make_atomic_end() instead")
395 
396  DEPRECATED("use goto_programt::make_atomic_end_function() instead")
398 
399  DEPRECATED("use goto_programt::make_incomplete_goto() instead")
400  void make_incomplete_goto(const code_gotot &_code)
401  {
403  code = _code;
404  }
405 
406  DEPRECATED("use goto_programt::make_goto() instead")
407  void make_goto(targett _target)
408  {
409  clear(GOTO);
410  targets.push_back(_target);
411  }
412 
413  DEPRECATED("use goto_programt::make_goto() instead")
414  void make_goto(targett _target, const exprt &g)
415  {
416  make_goto(_target);
417  guard=g;
418  }
419 
420  void complete_goto(targett _target)
421  {
423  code.make_nil();
424  targets.push_back(_target);
425  type = GOTO;
426  }
427 
428  DEPRECATED("use goto_programt::make_assignment() instead")
429  void make_assignment(const code_assignt &_code)
430  {
431  clear(ASSIGN);
432  code=_code;
433  }
434 
435  DEPRECATED("use goto_programt::make_decl() instead")
436  void make_decl(const code_declt &_code)
437  {
438  clear(DECL);
439  code=_code;
440  }
441 
442  DEPRECATED("use goto_programt::make_function_call() instead")
444  {
446  code=_code;
447  }
448 
449  bool is_goto () const { return type==GOTO; }
450  bool is_return () const { return type==RETURN; }
451  bool is_assign () const { return type==ASSIGN; }
452  bool is_function_call() const { return type==FUNCTION_CALL; }
453  bool is_throw () const { return type==THROW; }
454  bool is_catch () const { return type==CATCH; }
455  bool is_skip () const { return type==SKIP; }
456  bool is_location () const { return type==LOCATION; }
457  bool is_other () const { return type==OTHER; }
458  bool is_decl () const { return type==DECL; }
459  bool is_dead () const { return type==DEAD; }
460  bool is_assume () const { return type==ASSUME; }
461  bool is_assert () const { return type==ASSERT; }
462  bool is_atomic_begin () const { return type==ATOMIC_BEGIN; }
463  bool is_atomic_end () const { return type==ATOMIC_END; }
464  bool is_start_thread () const { return type==START_THREAD; }
465  bool is_end_thread () const { return type==END_THREAD; }
466  bool is_end_function () const { return type==END_FUNCTION; }
467  bool is_incomplete_goto() const
468  {
469  return type == INCOMPLETE_GOTO;
470  }
471 
473  instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit)
474  {
475  }
476 
478  : code(static_cast<const codet &>(get_nil_irep())),
479  source_location(static_cast<const source_locationt &>(get_nil_irep())),
480  type(_type),
481  guard(true_exprt())
482  {
483  }
484 
487  codet _code,
488  source_locationt _source_location,
490  exprt _guard,
491  targetst _targets)
492  : code(std::move(_code)),
493  source_location(std::move(_source_location)),
494  type(_type),
495  guard(std::move(_guard)),
496  targets(std::move(_targets))
497  {
498  }
499 
501  void swap(instructiont &instruction)
502  {
503  using std::swap;
504  swap(instruction.code, code);
505  swap(instruction.source_location, source_location);
506  swap(instruction.type, type);
507  swap(instruction.guard, guard);
508  swap(instruction.targets, targets);
509  }
510 
512  static const unsigned nil_target=
513  std::numeric_limits<unsigned>::max();
514 
518  unsigned location_number = 0;
519 
521  unsigned loop_number = 0;
522 
526 
528  bool is_backwards_goto() const
529  {
530  if(!is_goto())
531  return false;
532 
533  for(const auto &t : targets)
534  if(t->location_number<=location_number)
535  return true;
536 
537  return false;
538  }
539 
540  std::string to_string() const
541  {
542  std::ostringstream instruction_id_builder;
543  instruction_id_builder << type;
544  return instruction_id_builder.str();
545  }
546 
551  bool equals(const instructiont &other) const;
552 
557  void validate(const namespacet &ns, const validation_modet vm) const;
558 
561  void transform(std::function<optionalt<exprt>(exprt)>);
562 
564  void apply(std::function<void(const exprt &)>) const;
565  };
566 
567  // Never try to change this to vector-we mutate the list while iterating
568  typedef std::list<instructiont> instructionst;
569 
570  typedef instructionst::iterator targett;
571  typedef instructionst::const_iterator const_targett;
572  typedef std::list<targett> targetst;
573  typedef std::list<const_targett> const_targetst;
574 
577 
581  {
582  return instructions.erase(t, t);
583  }
584 
587  {
588  return t;
589  }
590 
591  optionalt<const_targett> get_target(const unsigned location_number) const
592  {
593  PRECONDITION(!instructions.empty());
594 
595  const unsigned start_location_number = instructions.front().location_number;
596 
597  if(
598  location_number < start_location_number ||
599  location_number > instructions.back().location_number)
600  {
601  return nullopt;
602  }
603 
604  auto location_target =
605  std::next(instructions.begin(), location_number - start_location_number);
606 
607  // location numbers are contiguous unless new instructions are inserted
608  // here we check that nobody inserted any instruction into our function
609  CHECK_RETURN(location_target->location_number == location_number);
610  return location_target;
611  }
612 
613  template <typename Target>
614  std::list<Target> get_successors(Target target) const;
615 
616  void compute_incoming_edges();
617 
620  {
621  PRECONDITION(target!=instructions.end());
622  const auto next=std::next(target);
623  instructions.insert(next, instructiont())->swap(*target);
624  }
625 
628  void insert_before_swap(targett target, instructiont &instruction)
629  {
630  insert_before_swap(target);
631  target->swap(instruction);
632  }
633 
637  targett target,
638  goto_programt &p)
639  {
640  PRECONDITION(target!=instructions.end());
641  if(p.instructions.empty())
642  return;
643  insert_before_swap(target, p.instructions.front());
644  auto next=std::next(target);
645  p.instructions.erase(p.instructions.begin());
646  instructions.splice(next, p.instructions);
647  }
648 
653  {
654  return instructions.insert(target, instructiont());
655  }
656 
661  {
662  return instructions.insert(target, i);
663  }
664 
669  {
670  return instructions.insert(std::next(target), instructiont());
671  }
672 
677  {
678  return instructions.insert(std::next(target), i);
679  }
680 
683  {
684  instructions.splice(instructions.end(),
685  p.instructions);
686  }
687 
691  const_targett target,
692  goto_programt &p)
693  {
694  instructions.splice(target, p.instructions);
695  }
696 
699  targett add(instructiont &&instruction)
700  {
701  instructions.push_back(std::move(instruction));
702  return --instructions.end();
703  }
704 
708  {
709  return add(instructiont());
710  }
711 
715  {
716  return add(instructiont(type));
717  }
718 
720  std::ostream &output(
721  const namespacet &ns,
722  const irep_idt &identifier,
723  std::ostream &out) const;
724 
726  std::ostream &output(std::ostream &out) const
727  {
728  return output(namespacet(symbol_tablet()), "", out);
729  }
730 
732  std::ostream &output_instruction(
733  const namespacet &ns,
734  const irep_idt &identifier,
735  std::ostream &out,
736  const instructionst::value_type &instruction) const;
737 
739  void compute_target_numbers();
740 
742  void compute_location_numbers(unsigned &nr)
743  {
744  for(auto &i : instructions)
745  {
746  INVARIANT(
747  nr != std::numeric_limits<unsigned>::max(),
748  "Too many location numbers assigned");
749  i.location_number=nr++;
750  }
751  }
752 
755  {
756  unsigned nr=0;
758  }
759 
761  void compute_loop_numbers();
762 
764  void update();
765 
767  static irep_idt
768  loop_id(const irep_idt &function_id, const instructiont &instruction)
769  {
770  return id2string(function_id) + "." +
771  std::to_string(instruction.loop_number);
772  }
773 
775  bool empty() const
776  {
777  return instructions.empty();
778  }
779 
782  {
783  }
784 
786  {
787  }
788 
790  void swap(goto_programt &program)
791  {
792  program.instructions.swap(instructions);
793  }
794 
796  void clear()
797  {
798  instructions.clear();
799  }
800 
804  {
805  PRECONDITION(!instructions.empty());
806  const auto end_function=std::prev(instructions.end());
807  DATA_INVARIANT(end_function->is_end_function(),
808  "goto program ends on END_FUNCTION");
809  return end_function;
810  }
811 
815  {
816  PRECONDITION(!instructions.empty());
817  const auto end_function=std::prev(instructions.end());
818  DATA_INVARIANT(end_function->is_end_function(),
819  "goto program ends on END_FUNCTION");
820  return end_function;
821  }
822 
824  void copy_from(const goto_programt &src);
825 
827  bool has_assertion() const;
828 
829  typedef std::set<irep_idt> decl_identifierst;
831  void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
832 
836  bool equals(const goto_programt &other) const;
837 
842  void validate(const namespacet &ns, const validation_modet vm) const
843  {
844  for(const instructiont &ins : instructions)
845  {
846  ins.validate(ns, vm);
847  }
848  }
849 
850  static instructiont
852  {
853  return instructiont(code_returnt(), l, RETURN, nil_exprt(), {});
854  }
855 
857  code_returnt c,
859  {
860  return instructiont(std::move(c), l, RETURN, nil_exprt(), {});
861  }
862 
863  static instructiont
865  {
866  return instructiont(
867  static_cast<const codet &>(get_nil_irep()),
868  l,
869  SKIP,
870  nil_exprt(),
871  {});
872  }
873 
875  {
876  return instructiont(
877  static_cast<const codet &>(get_nil_irep()),
878  l,
879  LOCATION,
880  nil_exprt(),
881  {});
882  }
883 
884  static instructiont
886  {
887  return instructiont(
888  static_cast<const codet &>(get_nil_irep()),
889  l,
890  THROW,
891  nil_exprt(),
892  {});
893  }
894 
895  static instructiont
897  {
898  return instructiont(
899  static_cast<const codet &>(get_nil_irep()),
900  l,
901  CATCH,
902  nil_exprt(),
903  {});
904  }
905 
907  const exprt &g,
909  {
910  return instructiont(
911  static_cast<const codet &>(get_nil_irep()),
912  l,
913  ASSERT,
914  exprt(g),
915  {});
916  }
917 
919  const exprt &g,
921  {
922  return instructiont(
923  static_cast<const codet &>(get_nil_irep()), l, ASSUME, g, {});
924  }
925 
927  const codet &_code,
929  {
930  return instructiont(_code, l, OTHER, nil_exprt(), {});
931  }
932 
934  const symbol_exprt &symbol,
936  {
937  return instructiont(code_declt(symbol), l, DECL, nil_exprt(), {});
938  }
939 
941  const symbol_exprt &symbol,
943  {
944  return instructiont(code_deadt(symbol), l, DEAD, nil_exprt(), {});
945  }
946 
947  static instructiont
949  {
950  return instructiont(
951  static_cast<const codet &>(get_nil_irep()),
952  l,
953  ATOMIC_BEGIN,
954  nil_exprt(),
955  {});
956  }
957 
958  static instructiont
960  {
961  return instructiont(
962  static_cast<const codet &>(get_nil_irep()),
963  l,
964  ATOMIC_END,
965  nil_exprt(),
966  {});
967  }
968 
969  static instructiont
971  {
972  return instructiont(
973  static_cast<const codet &>(get_nil_irep()),
974  l,
975  END_FUNCTION,
976  nil_exprt(),
977  {});
978  }
979 
981  const exprt &_cond,
983  {
984  PRECONDITION(_cond.type().id() == ID_bool);
985  return instructiont(
986  static_cast<const codet &>(get_nil_irep()),
987  l,
989  _cond,
990  {});
991  }
992 
994  const code_gotot &_code,
996  {
997  return instructiont(_code, l, INCOMPLETE_GOTO, true_exprt(), {});
998  }
999 
1001  targett _target,
1003  {
1004  return instructiont(
1005  static_cast<const codet &>(get_nil_irep()),
1006  l,
1007  GOTO,
1008  true_exprt(),
1009  {_target});
1010  }
1011 
1013  targett _target,
1014  const exprt &g,
1016  {
1017  return instructiont(
1018  static_cast<const codet &>(get_nil_irep()),
1019  l,
1020  GOTO,
1021  g,
1022  {_target});
1023  }
1024 
1027  const code_assignt &_code,
1029  {
1030  return instructiont(_code, l, ASSIGN, nil_exprt(), {});
1031  }
1032 
1035  exprt lhs,
1036  exprt rhs,
1038  {
1039  return instructiont(
1040  code_assignt(std::move(lhs), std::move(rhs)), l, ASSIGN, nil_exprt(), {});
1041  }
1042 
1044  const code_declt &_code,
1046  {
1047  return instructiont(_code, l, DECL, nil_exprt(), {});
1048  }
1049 
1052  const code_function_callt &_code,
1054  {
1055  return instructiont(_code, l, FUNCTION_CALL, nil_exprt(), {});
1056  }
1057 
1060  exprt function,
1063  {
1064  return instructiont(
1065  code_function_callt(std::move(function), std::move(arguments)),
1066  l,
1067  FUNCTION_CALL,
1068  nil_exprt(),
1069  {});
1070  }
1071 };
1072 
1085 template <typename Target>
1087  Target target) const
1088 {
1089  if(target==instructions.end())
1090  return std::list<Target>();
1091 
1092  const auto next=std::next(target);
1093 
1094  const instructiont &i=*target;
1095 
1096  if(i.is_goto())
1097  {
1098  std::list<Target> successors(i.targets.begin(), i.targets.end());
1099 
1100  if(!i.get_condition().is_true() && next != instructions.end())
1101  successors.push_back(next);
1102 
1103  return successors;
1104  }
1105 
1106  if(i.is_start_thread())
1107  {
1108  std::list<Target> successors(i.targets.begin(), i.targets.end());
1109 
1110  if(next!=instructions.end())
1111  successors.push_back(next);
1112 
1113  return successors;
1114  }
1115 
1116  if(i.is_end_thread())
1117  {
1118  // no successors
1119  return std::list<Target>();
1120  }
1121 
1122  if(i.is_throw())
1123  {
1124  // the successors are non-obvious
1125  return std::list<Target>();
1126  }
1127 
1128  if(i.is_assume())
1129  {
1130  return !i.get_condition().is_false() && next != instructions.end()
1131  ? std::list<Target>{next}
1132  : std::list<Target>();
1133  }
1134 
1135  if(next!=instructions.end())
1136  {
1137  return std::list<Target>{next};
1138  }
1139 
1140  return std::list<Target>();
1141 }
1142 
1146 {
1147  const goto_programt::instructiont &_i1=*i1;
1148  const goto_programt::instructiont &_i2=*i2;
1149  return &_i1<&_i2;
1150 }
1151 
1152 // NOLINTNEXTLINE(readability/identifiers)
1154 {
1155  std::size_t operator()(
1156  const goto_programt::const_targett t) const
1157  {
1158  using hash_typet = decltype(&(*t));
1159  return std::hash<hash_typet>{}(&(*t));
1160  }
1161 };
1162 
1166 {
1167  template <class A, class B>
1168  bool operator()(const A &a, const B &b) const
1169  {
1170  return &(*a) == &(*b);
1171  }
1172 };
1173 
1174 #define forall_goto_program_instructions(it, program) \
1175  for(goto_programt::instructionst::const_iterator \
1176  it=(program).instructions.begin(); \
1177  it!=(program).instructions.end(); it++)
1178 
1179 #define Forall_goto_program_instructions(it, program) \
1180  for(goto_programt::instructionst::iterator \
1181  it=(program).instructions.begin(); \
1182  it!=(program).instructions.end(); it++)
1183 
1184 inline bool operator<(
1185  const goto_programt::const_targett &i1,
1186  const goto_programt::const_targett &i2)
1187 {
1188  return order_const_target(i1, i2);
1189 }
1190 
1191 inline bool operator<(
1192  const goto_programt::targett &i1,
1193  const goto_programt::targett &i2)
1194 {
1195  return &(*i1)<&(*i2);
1196 }
1197 
1198 std::list<exprt> objects_read(const goto_programt::instructiont &);
1199 std::list<exprt> objects_written(const goto_programt::instructiont &);
1200 
1201 std::list<exprt> expressions_read(const goto_programt::instructiont &);
1202 std::list<exprt> expressions_written(const goto_programt::instructiont &);
1203 
1204 std::string as_string(
1205  const namespacet &ns,
1206  const irep_idt &function,
1207  const goto_programt::instructiont &);
1208 
1209 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
const irept & get_nil_irep()
Definition: irep.cpp:51
goto_programt(goto_programt &&other)
Definition: goto_program.h:85
exprt guard
Guard for gotos, assume, assert Use get_condition() to read, and set_condition(c) to write...
Definition: goto_program.h:276
void set_function_call(code_function_callt c)
Set the function call for FUNCTION_CALL.
Definition: goto_program.h:248
void update()
Update all indices.
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:436
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:699
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:980
static instructiont make_incomplete_goto(const code_gotot &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:993
targett add_instruction(goto_program_instruction_typet type)
Adds an instruction of given type at the end.
Definition: goto_program.h:714
const std::string & id2string(const irep_idt &d)
Definition: irep.h:42
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
std::list< targett > targetst
Definition: goto_program.h:572
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:906
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:652
void compute_loop_numbers()
Compute loop numbers.
std::set< targett > incoming_edges
Definition: goto_program.h:334
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
std::string to_string() const
Definition: goto_program.h:540
void make_assumption(const exprt &g)
Definition: goto_program.h:376
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:505
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:518
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
static const source_locationt & nil()
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:940
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:272
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
static instructiont make_goto(targett _target, const exprt &g, const source_locationt &l=source_locationt::nil())
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:742
std::size_t operator()(const goto_programt::const_targett t) const
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:279
bool has_assertion() const
Does the goto program have an assertion?
const code_returnt & get_return() const
Get the return statement for READ.
Definition: goto_program.h:227
std::list< exprt > objects_written(const goto_programt::instructiont &)
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:682
const_targett const_cast_target(const_targett t) const
Dummy for templates with possible const contexts.
Definition: goto_program.h:586
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:580
bool operator<(const goto_programt::const_targett &i1, const goto_programt::const_targett &i2)
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
codet representation of a goto statement.
Definition: std_code.h:1046
typet & type()
Return the type of the expression.
Definition: expr.h:75
exprt::operandst argumentst
Definition: std_code.h:1125
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
STL namespace.
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:948
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:512
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:310
bool operator()(const A &a, const B &b) const
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:528
static instructiont make_function_call(exprt function, code_function_callt::argumentst arguments, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:864
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard, number of targets, and labels.
static instructiont make_assignment(exprt lhs, exprt rhs, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targetst targets
The list of successor instructions.
Definition: goto_program.h:306
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
void clear()
Clear the goto program.
Definition: goto_program.h:796
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:959
std::list< instructiont > instructionst
Definition: goto_program.h:568
std::list< exprt > expressions_read(const goto_programt::instructiont &)
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:525
std::list< instructiont >::const_iterator const_targett
Definition: goto_program.h:301
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...
std::list< const_targett > const_targetst
Definition: goto_program.h:573
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:369
static instructiont make_decl(const code_declt &_code, const source_locationt &l=source_locationt::nil())
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:829
const irep_idt & id() const
Definition: irep.h:413
const_targett get_end_function() const
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:814
unsigned loop_number
Number unique per function to identify loops.
Definition: goto_program.h:521
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
Definition: goto_program.h:185
std::list< exprt > expressions_written(const goto_programt::instructiont &)
const code_declt & get_decl() const
Get the declaration for DECL.
Definition: goto_program.h:199
The Boolean constant true.
Definition: std_expr.h:4326
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:970
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:768
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
instructionst::iterator targett
Definition: goto_program.h:570
A codet representing the declaration of a local variable.
Definition: std_code.h:387
void complete_goto(targett _target)
Definition: goto_program.h:420
The NIL expression.
Definition: std_expr.h:4344
void make_location(const source_locationt &l)
Definition: goto_program.h:363
void make_function_call(const code_function_callt &_code)
Definition: goto_program.h:443
void make_other(const codet &_code)
Definition: goto_program.h:382
nonstd::optional< T > optionalt
Definition: optional.h:35
void set_dead(code_deadt c)
Set the dead statement for DEAD.
Definition: goto_program.h:220
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:576
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:292
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:571
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
goto_programt & operator=(goto_programt &&other)
Definition: goto_program.h:90
std::list< exprt > objects_read(const goto_programt::instructiont &)
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
Definition: goto_program.h:842
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:31
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:668
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1292
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:690
codet representation of a function call statement.
Definition: std_code.h:1107
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:285
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:918
void insert_before_swap(targett target, goto_programt &p)
Insertion that preserves jumps to "target".
Definition: goto_program.h:636
Functor to check whether iterators from different collections point at the same object.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:36
Author: Diffblue Ltd.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
static instructiont make_return(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:851
void compute_location_numbers()
Compute location numbers.
Definition: goto_program.h:754
bool order_const_target(const goto_programt::const_targett i1, const goto_programt::const_targett i2)
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:790
const code_deadt & get_dead() const
Get the dead statement for DEAD.
Definition: goto_program.h:213
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
Definition: goto_program.h:628
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
#define DEPRECATED(msg)
Definition: deprecate.h:23
std::ostream & operator<<(std::ostream &, goto_program_instruction_typet)
Outputs a string representation of a goto_program_instruction_typet
std::list< targett > targetst
Definition: goto_program.h:302
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
void set_assign(code_assignt c)
Set the assignment for ASSIGN.
Definition: goto_program.h:192
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:660
std::list< irep_idt > labelst
Goto target labels.
Definition: goto_program.h:330
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:486
void set_other(codet &c)
Set the statement for OTHER.
Definition: goto_program.h:262
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
Definition: goto_program.h:351
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:269
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:707
Base class for all expressions.
Definition: expr.h:52
goto_programt()
Constructor.
Definition: goto_program.h:781
void set_return(code_returnt c)
Set the return statement for READ.
Definition: goto_program.h:234
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:803
static instructiont make_location(const source_locationt &l)
Definition: goto_program.h:874
bool empty() const
Is the program empty?
Definition: goto_program.h:775
void compute_target_numbers()
Compute the target numbers.
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:501
std::list< const_targett > const_targetst
Definition: goto_program.h:303
void clear(goto_program_instruction_typet _type)
Clear the node.
Definition: goto_program.h:341
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:452
void make_nil()
Definition: irep.h:470
void make_incomplete_goto(const code_gotot &_code)
Definition: goto_program.h:400
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
Definition: goto_program.h:300
const code_function_callt & get_function_call() const
Get the function call for FUNCTION_CALL.
Definition: goto_program.h:241
void make_assertion(const exprt &g)
Definition: goto_program.h:373
validation_modet
Expression to hold a symbol (variable)
Definition: std_expr.h:100
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:676
void transform(std::function< optionalt< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:182
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
codet representation of a "return from a function" statement.
Definition: std_code.h:1242
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:318
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
goto_programt & operator=(const goto_programt &)=delete
std::string as_string(const namespacet &ns, const irep_idt &function, const goto_programt::instructiont &)
instructiont(goto_program_instruction_typet _type)
Definition: goto_program.h:477
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:337
void make_goto(targett _target)
Definition: goto_program.h:407
static instructiont make_catch(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:896
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:926
A codet representing an assignment in the program.
Definition: std_code.h:285
void set_decl(code_declt c)
Set the declaration for DECL.
Definition: goto_program.h:206
static instructiont make_return(code_returnt c, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:856
std::ostream & output(std::ostream &out) const
Output goto-program to given stream.
Definition: goto_program.h:726
static instructiont make_throw(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:885
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1227
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:255
optionalt< const_targett > get_target(const unsigned location_number) const
Definition: goto_program.h:591