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 <string>
19 
20 #include <util/deprecate.h>
21 #include <util/invariant.h>
22 #include <util/namespace.h>
23 #include <util/source_location.h>
24 #include <util/std_code.h>
25 
26 enum class validation_modet;
27 
30 {
32  GOTO = 1, // branch, possibly guarded
33  ASSUME = 2, // non-failing guarded self loop
34  ASSERT = 3, // assertions
35  OTHER = 4, // anything else
36  SKIP = 5, // just advance the PC
37  START_THREAD = 6, // spawns an asynchronous thread
38  END_THREAD = 7, // end the current thread
39  LOCATION = 8, // semantically like SKIP
40  END_FUNCTION = 9, // exit point of a function
41  ATOMIC_BEGIN = 10, // marks a block without interleavings
42  ATOMIC_END = 11, // end of a block without interleavings
43  SET_RETURN_VALUE = 12, // set function return value (no control-flow change)
44  ASSIGN = 13, // assignment lhs:=rhs
45  DECL = 14, // declare a local variable
46  DEAD = 15, // marks the end-of-live of a local variable
47  FUNCTION_CALL = 16, // call a function
48  THROW = 17, // throw an exception
49  CATCH = 18, // push, pop or enter an exception handler
50  INCOMPLETE_GOTO = 19 // goto where target is yet to be determined
51 };
52 
53 std::ostream &operator<<(std::ostream &, goto_program_instruction_typet);
54 
71 {
72 public:
74  goto_programt(const goto_programt &)=delete;
76 
77  // Move operations need to be explicitly enabled as they are deleted with the
78  // copy operations
79  // default for move operations isn't available on Windows yet, so define
80  // explicitly (see https://msdn.microsoft.com/en-us/library/hh567368.aspx
81  // under "Defaulted and Deleted Functions")
82 
84  instructions(std::move(other.instructions))
85  {
86  }
87 
89  {
90  instructions=std::move(other.instructions);
91  return *this;
92  }
93 
177  class instructiont final
178  {
179  protected:
182 
183  public:
185  const codet &get_code() const
186  {
187  return code;
188  }
189 
192  {
193  return code;
194  }
195 
197  DEPRECATED(SINCE(2021, 2, 24, "Use assign_lhs/rhs instead"))
198  const code_assignt &get_assign() const
199  {
201  return to_code_assign(code);
202  }
203 
205  const exprt &assign_lhs() const
206  {
208  return to_code_assign(code).lhs();
209  }
210 
213  {
215  return to_code_assign(code).lhs();
216  }
217 
219  const exprt &assign_rhs() const
220  {
222  return to_code_assign(code).rhs();
223  }
224 
227  {
229  return to_code_assign(code).rhs();
230  }
231 
233  DEPRECATED(SINCE(2021, 2, 24, "Use assign_lhs/rhs instead"))
235  {
237  code = std::move(c);
238  }
239 
241  DEPRECATED(SINCE(2021, 2, 24, "Use decl_symbol instead"))
242  const code_declt &get_decl() const
243  {
245  const auto &decl = expr_checked_cast<code_declt>(code);
246  INVARIANT(
247  !decl.initial_value(),
248  "code_declt in goto program may not contain initialization.");
249  return decl;
250  }
251 
253  const symbol_exprt &decl_symbol() const
254  {
256  auto &decl = expr_checked_cast<code_declt>(code);
257  INVARIANT(
258  !decl.initial_value(),
259  "code_declt in goto program may not contain initialization.");
260  return decl.symbol();
261  }
262 
265  {
267  auto &decl = expr_checked_cast<code_declt>(code);
268  INVARIANT(
269  !decl.initial_value(),
270  "code_declt in goto program may not contain initialization.");
271  return decl.symbol();
272  }
273 
275  DEPRECATED(SINCE(2021, 2, 24, "Use decl_symbol instead"))
277  {
279  INVARIANT(
280  !c.initial_value(),
281  "Initialization must be separated from code_declt before adding to "
282  "goto_instructiont.");
283  code = std::move(c);
284  }
285 
287  DEPRECATED(SINCE(2021, 2, 24, "Use dead_symbol instead"))
288  const code_deadt &get_dead() const
289  {
291  return to_code_dead(code);
292  }
293 
295  const symbol_exprt &dead_symbol() const
296  {
298  return to_code_dead(code).symbol();
299  }
300 
303  {
305  return to_code_dead(code).symbol();
306  }
307 
309  DEPRECATED(SINCE(2021, 2, 24, "Use dead_symbol instead"))
311  {
313  code = std::move(c);
314  }
315 
317  DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead"))
318  const code_returnt &get_return() const
319  {
321  return to_code_return(code);
322  }
323 
325  const exprt &return_value() const
326  {
328  return to_code_return(code).return_value();
329  }
330 
333  {
335  return to_code_return(code).return_value();
336  }
337 
339  DEPRECATED(SINCE(2021, 2, 24, "Use return_value instead"))
341  {
343  code = std::move(c);
344  }
345 
347 #if 1
349  2021,
350  2,
351  24,
352  "Use call_function(), call_lhs(), call_arguments() instead"))
354  {
356  return to_code_function_call(code);
357  }
358 #endif
359 
361  const exprt &call_function() const
362  {
365  }
366 
369  {
372  }
373 
375  const exprt &call_lhs() const
376  {
378  return to_code_function_call(code).lhs();
379  }
380 
383  {
385  return to_code_function_call(code).lhs();
386  }
387 
390  {
393  }
394 
397  {
400  }
401 
403 #if 1
405  2021,
406  2,
407  24,
408  "Use call_function(), call_lhs(), call_arguments() instead"))
410  {
412  code = std::move(c);
413  }
414 #endif
415 
417  const codet &get_other() const
418  {
420  return code;
421  }
422 
424  void set_other(codet &c)
425  {
427  code = std::move(c);
428  }
429 
432 
435 
439 
441  bool has_condition() const
442  {
443  return is_goto() || is_incomplete_goto() || is_assume() || is_assert();
444  }
445 
447  const exprt &get_condition() const
448  {
450  return guard;
451  }
452 
455  {
457  guard = std::move(c);
458  }
459 
460  // The below will eventually become a single target only.
462  typedef std::list<instructiont>::iterator targett;
463  typedef std::list<instructiont>::const_iterator const_targett;
464  typedef std::list<targett> targetst;
465  typedef std::list<const_targett> const_targetst;
466 
469 
473  {
474  PRECONDITION(targets.size()==1);
475  return targets.front();
476  }
477 
481  {
482  targets.clear();
483  targets.push_back(t);
484  }
485 
486  bool has_target() const
487  {
488  return !targets.empty();
489  }
490 
492  typedef std::list<irep_idt> labelst;
494 
495  // will go away
496  std::set<targett> incoming_edges;
497 
499  bool is_target() const
500  { return target_number!=nil_target; }
501 
504  {
505  type=_type;
506  targets.clear();
507  guard=true_exprt();
508  code.make_nil();
509  }
510 
514  {
515  clear(SKIP);
516  }
517 
518  void complete_goto(targett _target)
519  {
521  code.make_nil();
522  targets.push_back(_target);
523  type = GOTO;
524  }
525 
526  // clang-format off
527  bool is_goto () const { return type == GOTO; }
528  bool is_set_return_value() const { return type == SET_RETURN_VALUE; }
529  bool is_assign () const { return type == ASSIGN; }
530  bool is_function_call () const { return type == FUNCTION_CALL; }
531  bool is_throw () const { return type == THROW; }
532  bool is_catch () const { return type == CATCH; }
533  bool is_skip () const { return type == SKIP; }
534  bool is_location () const { return type == LOCATION; }
535  bool is_other () const { return type == OTHER; }
536  bool is_decl () const { return type == DECL; }
537  bool is_dead () const { return type == DEAD; }
538  bool is_assume () const { return type == ASSUME; }
539  bool is_assert () const { return type == ASSERT; }
540  bool is_atomic_begin () const { return type == ATOMIC_BEGIN; }
541  bool is_atomic_end () const { return type == ATOMIC_END; }
542  bool is_start_thread () const { return type == START_THREAD; }
543  bool is_end_thread () const { return type == END_THREAD; }
544  bool is_end_function () const { return type == END_FUNCTION; }
545  bool is_incomplete_goto () const { return type == INCOMPLETE_GOTO; }
546  // clang-format on
547 
549  instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit)
550  {
551  }
552 
554  : code(static_cast<const codet &>(get_nil_irep())),
555  source_location(static_cast<const source_locationt &>(get_nil_irep())),
556  type(_type),
557  guard(true_exprt())
558  {
559  }
560 
563  codet _code,
564  source_locationt _source_location,
566  exprt _guard,
567  targetst _targets)
568  : code(std::move(_code)),
569  source_location(std::move(_source_location)),
570  type(_type),
571  guard(std::move(_guard)),
572  targets(std::move(_targets))
573  {
574  }
575 
577  void swap(instructiont &instruction)
578  {
579  using std::swap;
580  swap(instruction.code, code);
581  swap(instruction.source_location, source_location);
582  swap(instruction.type, type);
583  swap(instruction.guard, guard);
584  swap(instruction.targets, targets);
585  }
586 
588  static const unsigned nil_target=
589  std::numeric_limits<unsigned>::max();
590 
594  unsigned location_number = 0;
595 
597  unsigned loop_number = 0;
598 
602 
604  bool is_backwards_goto() const
605  {
606  if(!is_goto())
607  return false;
608 
609  for(const auto &t : targets)
610  if(t->location_number<=location_number)
611  return true;
612 
613  return false;
614  }
615 
616  std::string to_string() const
617  {
618  std::ostringstream instruction_id_builder;
619  instruction_id_builder << type;
620  return instruction_id_builder.str();
621  }
622 
627  bool equals(const instructiont &other) const;
628 
633  void validate(const namespacet &ns, const validation_modet vm) const;
634 
637  void transform(std::function<optionalt<exprt>(exprt)>);
638 
640  void apply(std::function<void(const exprt &)>) const;
641  };
642 
643  // Never try to change this to vector-we mutate the list while iterating
644  typedef std::list<instructiont> instructionst;
645 
646  typedef instructionst::iterator targett;
647  typedef instructionst::const_iterator const_targett;
648  typedef std::list<targett> targetst;
649  typedef std::list<const_targett> const_targetst;
650 
653 
657  {
658  return instructions.erase(t, t);
659  }
660 
663  {
664  return t;
665  }
666 
667  template <typename Target>
668  std::list<Target> get_successors(Target target) const;
669 
670  void compute_incoming_edges();
671 
674  {
675  PRECONDITION(target!=instructions.end());
676  const auto next=std::next(target);
677  instructions.insert(next, instructiont())->swap(*target);
678  }
679 
682  void insert_before_swap(targett target, instructiont &instruction)
683  {
684  insert_before_swap(target);
685  target->swap(instruction);
686  }
687 
691  targett target,
692  goto_programt &p)
693  {
694  PRECONDITION(target!=instructions.end());
695  if(p.instructions.empty())
696  return;
697  insert_before_swap(target, p.instructions.front());
698  auto next=std::next(target);
699  p.instructions.erase(p.instructions.begin());
700  instructions.splice(next, p.instructions);
701  }
702 
707  {
708  return instructions.insert(target, instructiont());
709  }
710 
715  {
716  return instructions.insert(target, i);
717  }
718 
723  {
724  return instructions.insert(std::next(target), instructiont());
725  }
726 
731  {
732  return instructions.insert(std::next(target), i);
733  }
734 
737  {
738  instructions.splice(instructions.end(),
739  p.instructions);
740  }
741 
745  const_targett target,
746  goto_programt &p)
747  {
748  instructions.splice(target, p.instructions);
749  }
750 
753  targett add(instructiont &&instruction)
754  {
755  instructions.push_back(std::move(instruction));
756  return --instructions.end();
757  }
758 
762  {
763  return add(instructiont());
764  }
765 
769  {
770  return add(instructiont(type));
771  }
772 
774  std::ostream &output(
775  const namespacet &ns,
776  const irep_idt &identifier,
777  std::ostream &out) const;
778 
780  std::ostream &output(std::ostream &out) const;
781 
783  std::ostream &output_instruction(
784  const namespacet &ns,
785  const irep_idt &identifier,
786  std::ostream &out,
787  const instructionst::value_type &instruction) const;
788 
790  void compute_target_numbers();
791 
793  void compute_location_numbers(unsigned &nr)
794  {
795  for(auto &i : instructions)
796  {
797  INVARIANT(
798  nr != std::numeric_limits<unsigned>::max(),
799  "Too many location numbers assigned");
800  i.location_number=nr++;
801  }
802  }
803 
806  {
807  unsigned nr=0;
809  }
810 
812  void compute_loop_numbers();
813 
815  void update();
816 
818  static irep_idt
819  loop_id(const irep_idt &function_id, const instructiont &instruction)
820  {
821  return id2string(function_id) + "." +
822  std::to_string(instruction.loop_number);
823  }
824 
826  bool empty() const
827  {
828  return instructions.empty();
829  }
830 
833  {
834  }
835 
837  {
838  }
839 
841  void swap(goto_programt &program)
842  {
843  program.instructions.swap(instructions);
844  }
845 
847  void clear()
848  {
849  instructions.clear();
850  }
851 
855  {
856  PRECONDITION(!instructions.empty());
857  const auto end_function=std::prev(instructions.end());
858  DATA_INVARIANT(end_function->is_end_function(),
859  "goto program ends on END_FUNCTION");
860  return end_function;
861  }
862 
866  {
867  PRECONDITION(!instructions.empty());
868  const auto end_function=std::prev(instructions.end());
869  DATA_INVARIANT(end_function->is_end_function(),
870  "goto program ends on END_FUNCTION");
871  return end_function;
872  }
873 
875  void copy_from(const goto_programt &src);
876 
878  bool has_assertion() const;
879 
880  typedef std::set<irep_idt> decl_identifierst;
882  void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
883 
887  bool equals(const goto_programt &other) const;
888 
893  void validate(const namespacet &ns, const validation_modet vm) const
894  {
895  for(const instructiont &ins : instructions)
896  {
897  ins.validate(ns, vm);
898  }
899  }
900 
902  code_returnt c,
904  {
905  return instructiont(std::move(c), l, SET_RETURN_VALUE, nil_exprt(), {});
906  }
907 
908  static instructiont
910  {
911  return instructiont(
912  static_cast<const codet &>(get_nil_irep()),
913  l,
914  SKIP,
915  nil_exprt(),
916  {});
917  }
918 
920  {
921  return instructiont(
922  static_cast<const codet &>(get_nil_irep()),
923  l,
924  LOCATION,
925  nil_exprt(),
926  {});
927  }
928 
929  static instructiont
931  {
932  return instructiont(
933  static_cast<const codet &>(get_nil_irep()),
934  l,
935  THROW,
936  nil_exprt(),
937  {});
938  }
939 
940  static instructiont
942  {
943  return instructiont(
944  static_cast<const codet &>(get_nil_irep()),
945  l,
946  CATCH,
947  nil_exprt(),
948  {});
949  }
950 
952  const exprt &g,
954  {
955  return instructiont(
956  static_cast<const codet &>(get_nil_irep()),
957  l,
958  ASSERT,
959  exprt(g),
960  {});
961  }
962 
964  const exprt &g,
966  {
967  return instructiont(
968  static_cast<const codet &>(get_nil_irep()), l, ASSUME, g, {});
969  }
970 
972  const codet &_code,
974  {
975  return instructiont(_code, l, OTHER, nil_exprt(), {});
976  }
977 
979  const symbol_exprt &symbol,
981  {
982  return instructiont(code_declt(symbol), l, DECL, nil_exprt(), {});
983  }
984 
986  const symbol_exprt &symbol,
988  {
989  return instructiont(code_deadt(symbol), l, DEAD, nil_exprt(), {});
990  }
991 
992  static instructiont
994  {
995  return instructiont(
996  static_cast<const codet &>(get_nil_irep()),
997  l,
998  ATOMIC_BEGIN,
999  nil_exprt(),
1000  {});
1001  }
1002 
1003  static instructiont
1005  {
1006  return instructiont(
1007  static_cast<const codet &>(get_nil_irep()),
1008  l,
1009  ATOMIC_END,
1010  nil_exprt(),
1011  {});
1012  }
1013 
1014  static instructiont
1016  {
1017  return instructiont(
1018  static_cast<const codet &>(get_nil_irep()),
1019  l,
1020  END_FUNCTION,
1021  nil_exprt(),
1022  {});
1023  }
1024 
1026  const exprt &_cond,
1028  {
1029  PRECONDITION(_cond.type().id() == ID_bool);
1030  return instructiont(
1031  static_cast<const codet &>(get_nil_irep()),
1032  l,
1034  _cond,
1035  {});
1036  }
1037 
1038  static instructiont
1040  {
1041  return instructiont(
1042  static_cast<const codet &>(get_nil_irep()),
1043  l,
1045  true_exprt(),
1046  {});
1047  }
1048 
1050  const code_gotot &_code,
1052  {
1053  return instructiont(_code, l, INCOMPLETE_GOTO, true_exprt(), {});
1054  }
1055 
1057  targett _target,
1059  {
1060  return instructiont(
1061  static_cast<const codet &>(get_nil_irep()),
1062  l,
1063  GOTO,
1064  true_exprt(),
1065  {_target});
1066  }
1067 
1069  targett _target,
1070  const exprt &g,
1072  {
1073  return instructiont(
1074  static_cast<const codet &>(get_nil_irep()),
1075  l,
1076  GOTO,
1077  g,
1078  {_target});
1079  }
1080 
1083  const code_assignt &_code,
1085  {
1086  return instructiont(_code, l, ASSIGN, nil_exprt(), {});
1087  }
1088 
1091  exprt lhs,
1092  exprt rhs,
1094  {
1095  return instructiont(
1096  code_assignt(std::move(lhs), std::move(rhs)), l, ASSIGN, nil_exprt(), {});
1097  }
1098 
1100  const code_declt &_code,
1102  {
1103  return instructiont(_code, l, DECL, nil_exprt(), {});
1104  }
1105 
1108  const code_function_callt &_code,
1110  {
1111  return instructiont(_code, l, FUNCTION_CALL, nil_exprt(), {});
1112  }
1113 
1116  exprt lhs,
1117  exprt function,
1120  {
1121  return instructiont(
1122  code_function_callt(lhs, std::move(function), std::move(arguments)),
1123  l,
1124  FUNCTION_CALL,
1125  nil_exprt(),
1126  {});
1127  }
1128 };
1129 
1142 template <typename Target>
1144  Target target) const
1145 {
1146  if(target==instructions.end())
1147  return std::list<Target>();
1148 
1149  const auto next=std::next(target);
1150 
1151  const instructiont &i=*target;
1152 
1153  if(i.is_goto())
1154  {
1155  std::list<Target> successors(i.targets.begin(), i.targets.end());
1156 
1157  if(!i.get_condition().is_true() && next != instructions.end())
1158  successors.push_back(next);
1159 
1160  return successors;
1161  }
1162 
1163  if(i.is_start_thread())
1164  {
1165  std::list<Target> successors(i.targets.begin(), i.targets.end());
1166 
1167  if(next!=instructions.end())
1168  successors.push_back(next);
1169 
1170  return successors;
1171  }
1172 
1173  if(i.is_end_thread())
1174  {
1175  // no successors
1176  return std::list<Target>();
1177  }
1178 
1179  if(i.is_throw())
1180  {
1181  // the successors are non-obvious
1182  return std::list<Target>();
1183  }
1184 
1185  if(i.is_assume())
1186  {
1187  return !i.get_condition().is_false() && next != instructions.end()
1188  ? std::list<Target>{next}
1189  : std::list<Target>();
1190  }
1191 
1192  if(next!=instructions.end())
1193  {
1194  return std::list<Target>{next};
1195  }
1196 
1197  return std::list<Target>();
1198 }
1199 
1203 {
1204  const goto_programt::instructiont &_i1=*i1;
1205  const goto_programt::instructiont &_i2=*i2;
1206  return &_i1<&_i2;
1207 }
1208 
1209 // NOLINTNEXTLINE(readability/identifiers)
1211 {
1212  std::size_t operator()(
1213  const goto_programt::const_targett t) const
1214  {
1215  using hash_typet = decltype(&(*t));
1216  return std::hash<hash_typet>{}(&(*t));
1217  }
1218 };
1219 
1223 {
1224  template <class A, class B>
1225  bool operator()(const A &a, const B &b) const
1226  {
1227  return &(*a) == &(*b);
1228  }
1229 };
1230 
1231 template <typename GotoFunctionT, typename PredicateT, typename HandlerT>
1233  GotoFunctionT &&goto_function,
1234  PredicateT predicate,
1235  HandlerT handler)
1236 {
1237  auto &&instructions = goto_function.body.instructions;
1238  for(auto it = instructions.begin(); it != instructions.end(); ++it)
1239  {
1240  if(predicate(it))
1241  {
1242  handler(it);
1243  }
1244  }
1245 }
1246 
1247 template <typename GotoFunctionT, typename HandlerT>
1248 void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
1249 {
1250  using iterator_t = decltype(goto_function.body.instructions.begin());
1252  goto_function, [](const iterator_t &) { return true; }, handler);
1253 }
1254 
1255 #define forall_goto_program_instructions(it, program) \
1256  for(goto_programt::instructionst::const_iterator \
1257  it=(program).instructions.begin(); \
1258  it!=(program).instructions.end(); it++)
1259 
1260 #define Forall_goto_program_instructions(it, program) \
1261  for(goto_programt::instructionst::iterator \
1262  it=(program).instructions.begin(); \
1263  it!=(program).instructions.end(); it++)
1264 
1265 inline bool operator<(
1266  const goto_programt::const_targett &i1,
1267  const goto_programt::const_targett &i2)
1268 {
1269  return order_const_target(i1, i2);
1270 }
1271 
1272 inline bool operator<(
1273  const goto_programt::targett &i1,
1274  const goto_programt::targett &i2)
1275 {
1276  return &(*i1)<&(*i2);
1277 }
1278 
1279 std::list<exprt> objects_read(const goto_programt::instructiont &);
1280 std::list<exprt> objects_written(const goto_programt::instructiont &);
1281 
1282 std::list<exprt> expressions_read(const goto_programt::instructiont &);
1283 std::list<exprt> expressions_written(const goto_programt::instructiont &);
1284 
1285 std::string as_string(
1286  const namespacet &ns,
1287  const irep_idt &function,
1288  const goto_programt::instructiont &);
1289 
1290 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
goto_programt::instructiont::is_skip
bool is_skip() const
Definition: goto_program.h:533
goto_programt::instructiont::get_dead
const code_deadt & get_dead() const
Get the dead statement for DEAD.
Definition: goto_program.h:288
goto_programt::instructiont::call_arguments
exprt::operandst & call_arguments()
Get the arguments of a FUNCTION_CALL.
Definition: goto_program.h:396
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:531
goto_programt::instructiont::has_target
bool has_target() const
Definition: goto_program.h:486
goto_programt::instructiont::set_other
void set_other(codet &c)
Set the statement for OTHER.
Definition: goto_program.h:424
goto_programt::~goto_programt
~goto_programt()
Definition: goto_program.h:836
operator<
bool operator<(const goto_programt::const_targett &i1, const goto_programt::const_targett &i2)
Definition: goto_program.h:1265
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:431
goto_programt::instructiont::labelst
std::list< irep_idt > labelst
Goto target labels.
Definition: goto_program.h:492
goto_programt::instructiont::complete_goto
void complete_goto(targett _target)
Definition: goto_program.h:518
SET_RETURN_VALUE
@ SET_RETURN_VALUE
Definition: goto_program.h:43
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:730
goto_programt::make_dead
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:985
goto_programt::instructiont::set_assign
void set_assign(code_assignt c)
Set the assignment for ASSIGN.
Definition: goto_program.h:234
goto_programt::instructiont::to_string
std::string to_string() const
Definition: goto_program.h:616
goto_programt::instructiont::is_other
bool is_other() const
Definition: goto_program.h:535
irept::make_nil
void make_nil()
Definition: irep.h:465
goto_programt::instructiont::swap
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:577
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:662
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:315
goto_programt::instructiont::clear
void clear(goto_program_instruction_typet _type)
Clear the node.
Definition: goto_program.h:503
goto_programt::compute_loop_numbers
void compute_loop_numbers()
Compute loop numbers.
Definition: goto_program.cpp:568
goto_programt::const_targetst
std::list< const_targett > const_targetst
Definition: goto_program.h:649
goto_programt::instructiont::get_return
const code_returnt & get_return() const
Get the return statement for READ.
Definition: goto_program.h:318
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 SET_RETURN_VALUE.
Definition: goto_program.h:340
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:644
for_each_instruction_if
void for_each_instruction_if(GotoFunctionT &&goto_function, PredicateT predicate, HandlerT handler)
Definition: goto_program.h:1232
goto_programt::instructiont::type
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:434
goto_programt::instructiont::is_dead
bool is_dead() const
Definition: goto_program.h:537
goto_programt::instructiont::assign_lhs_nonconst
exprt & assign_lhs_nonconst()
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:212
source_locationt::nil
static const source_locationt & nil()
Definition: source_location.h:187
expressions_read
std::list< exprt > expressions_read(const goto_programt::instructiont &)
Definition: goto_program.cpp:319
goto_programt::instructiont::decl_symbol
symbol_exprt & decl_symbol()
Get the declared symbol for DECL.
Definition: goto_program.h:264
goto_programt::instructiont::is_catch
bool is_catch() const
Definition: goto_program.h:532
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:576
goto_programt::copy_from
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
Definition: goto_program.cpp:661
goto_programt::instructiont::apply
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
Definition: goto_program.cpp:1049
invariant.h
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:400
goto_programt::make_end_function
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1015
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
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:945
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:826
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:1223
goto_programt::insert_before_swap
void insert_before_swap(targett target, goto_programt &p)
Insertion that preserves jumps to "target".
Definition: goto_program.h:690
goto_programt::instructiont::set_decl
void set_decl(code_declt c)
Set the declaration for DECL.
Definition: goto_program.h:276
goto_programt::get_decl_identifiers
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
Definition: goto_program.cpp:276
objects_written
std::list< exprt > objects_written(const goto_programt::instructiont &)
Definition: goto_program.cpp:459
goto_programt::has_assertion
bool has_assertion() const
Does the goto program have an assertion?
Definition: goto_program.cpp:702
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
goto_programt::instructiont::targets
targetst targets
The list of successor instructions.
Definition: goto_program.h:468
goto_programt::instructiont::is_incomplete_goto
bool is_incomplete_goto() const
Definition: goto_program.h:545
goto_programt::make_return
static instructiont make_return(code_returnt c, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:901
goto_programt::get_successors
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition: goto_program.h:1143
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
goto_programt::insert_before_swap
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
Definition: goto_program.h:682
goto_programt::instructiont::is_end_thread
bool is_end_thread() const
Definition: goto_program.h:543
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:978
namespace.h
goto_programt::instructiont::decl_symbol
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:253
goto_programt::instructiont::is_atomic_end
bool is_atomic_end() const
Definition: goto_program.h:541
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1238
goto_programt::instructiont::call_arguments
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
Definition: goto_program.h:389
goto_programt::instructiont::instructiont
instructiont()
Definition: goto_program.h:548
goto_programt::instructiont::get_assign
const code_assignt & get_assign() const
Get the assignment for ASSIGN.
Definition: goto_program.h:198
objects_read
std::list< exprt > objects_read(const goto_programt::instructiont &)
Definition: goto_program.cpp:432
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:865
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:1082
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1056
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
goto_programt::instructiont::get_other
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:417
goto_programt::instructiont::get_code
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:185
goto_programt::instructiont::const_targett
std::list< instructiont >::const_iterator const_targett
Definition: goto_program.h:463
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:819
goto_programt::instructiont::is_atomic_begin
bool is_atomic_begin() const
Definition: goto_program.h:540
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:409
goto_programt::targetst
std::list< targett > targetst
Definition: goto_program.h:648
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:1107
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:761
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
THROW
@ THROW
Definition: goto_program.h:48
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1213
goto_programt::make_function_call
static instructiont make_function_call(exprt lhs, exprt function, code_function_callt::argumentst arguments, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1115
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:706
GOTO
@ GOTO
Definition: goto_program.h:32
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:1101
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:744
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:513
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:951
goto_programt::compute_target_numbers
void compute_target_numbers()
Compute the target numbers.
Definition: goto_program.cpp:607
goto_programt::make_decl
static instructiont make_decl(const code_declt &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1099
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:510
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:744
goto_programt::instructiont::dead_symbol
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:295
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:83
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:47
goto_programt::instructiont::code
codet code
Do not read or modify directly – use get_X() instead.
Definition: goto_program.h:181
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:584
goto_programt::instructiont::call_function
exprt & call_function()
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:368
goto_programt::instructiont::targett
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
Definition: goto_program.h:462
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:909
goto_programt::instructiont::is_decl
bool is_decl() const
Definition: goto_program.h:536
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1157
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
goto_programt::compute_location_numbers
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:793
to_code_dead
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:549
nil_exprt
The NIL expression.
Definition: std_expr.h:2820
goto_programt::instructiont::is_backwards_goto
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:604
goto_programt::instructiont::is_location
bool is_location() const
Definition: goto_program.h:534
pointee_address_equalt::operator()
bool operator()(const A &a, const B &b) const
Definition: goto_program.h:1225
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:310
goto_programt::instructiont::labels
labelst labels
Definition: goto_program.h:493
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:353
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:732
expressions_written
std::list< exprt > expressions_written(const goto_programt::instructiont &)
Definition: goto_program.cpp:368
source_location.h
goto_programt::instructiont::has_condition
bool has_condition() const
Does this instruction have a condition?
Definition: goto_program.h:441
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:31
goto_programt::instructiont::is_set_return_value
bool is_set_return_value() const
Definition: goto_program.h:528
goto_programt::make_atomic_begin
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:993
OTHER
@ OTHER
Definition: goto_program.h:35
goto_programt::goto_programt
goto_programt()
Constructor.
Definition: goto_program.h:832
validation_modet
validation_modet
Definition: validation_mode.h:13
code_deadt::symbol
symbol_exprt & symbol()
Definition: std_code.h:503
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:544
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1324
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:893
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1222
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1389
const_target_hash
Definition: goto_program.h:1211
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:768
goto_programt::instructiont::call_lhs
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:375
goto_programt::instructiont::assign_rhs
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:219
END_FUNCTION
@ END_FUNCTION
Definition: goto_program.h:40
SKIP
@ SKIP
Definition: goto_program.h:36
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:497
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:480
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 SET_RETURN_VALUE instruction.
Definition: goto_program.h:332
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:712
std_code.h
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1258
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_programt::instructiont::targetst
std::list< targett > targetst
Definition: goto_program.h:464
goto_programt::clear
void clear()
Clear the goto program.
Definition: goto_program.h:847
goto_programt::instructiont::return_value
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
Definition: goto_program.h:325
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:736
goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:30
goto_programt::instructiont::is_goto
bool is_goto() const
Definition: goto_program.h:527
source_locationt
Definition: source_location.h:19
goto_programt::instructiont::get_decl
const code_declt & get_decl() const
Get the declaration for DECL.
Definition: goto_program.h:242
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:854
goto_programt::compute_location_numbers
void compute_location_numbers()
Compute location numbers.
Definition: goto_program.h:805
goto_programt::make_goto
static instructiont make_goto(targett _target, const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1068
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
ASSIGN
@ ASSIGN
Definition: goto_program.h:44
goto_programt::instructiont::is_assert
bool is_assert() const
Definition: goto_program.h:539
goto_programt::instructiont::target_number
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:601
goto_programt::operator=
goto_programt & operator=(goto_programt &&other)
Definition: goto_program.h:88
CATCH
@ CATCH
Definition: goto_program.h:49
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
DECL
@ DECL
Definition: goto_program.h:45
goto_programt::instructiont::incoming_edges
std::set< targett > incoming_edges
Definition: goto_program.h:496
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:381
goto_programt::instructiont::assign_lhs
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:205
goto_programt::instructiont::location_number
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:594
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:714
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:656
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:302
goto_programt::instructiont::call_lhs
exprt & call_lhs()
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:382
ASSUME
@ ASSUME
Definition: goto_program.h:33
goto_programt::instructiont::assign_rhs_nonconst
exprt & assign_rhs_nonconst()
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:226
goto_programt::make_other
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:971
goto_programt::make_incomplete_goto
static instructiont make_incomplete_goto(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1039
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:438
goto_programt::instructiont::is_assign
bool is_assign() const
Definition: goto_program.h:529
order_const_target
bool order_const_target(const goto_programt::const_targett i1, const goto_programt::const_targett i2)
Definition: goto_program.h:1200
goto_programt::instructiont::loop_number
unsigned loop_number
Number unique per function to identify loops.
Definition: goto_program.h:597
START_THREAD
@ START_THREAD
Definition: goto_program.h:37
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:47
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
operator<<
std::ostream & operator<<(std::ostream &, goto_program_instruction_typet)
Outputs a string representation of a goto_program_instruction_typet
Definition: goto_program.cpp:1133
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:722
goto_programt::instructiont::set_condition
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:454
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:42
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:647
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:20
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:963
DEAD
@ DEAD
Definition: goto_program.h:46
goto_programt::instructiont::const_targetst
std::list< const_targett > const_targetst
Definition: goto_program.h:465
goto_programt::operator=
goto_programt & operator=(const goto_programt &)=delete
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:41
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:1049
goto_programt::instructiont::is_assume
bool is_assume() const
Definition: goto_program.h:538
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
goto_programt::instructiont::set_dead
void set_dead(code_deadt c)
Set the dead statement for DEAD.
Definition: goto_program.h:310
goto_programt::insert_before_swap
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:673
goto_programt::make_throw
static instructiont make_throw(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:930
for_each_instruction
void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
Definition: goto_program.h:1248
code_returnt::return_value
const exprt & return_value() const
Definition: std_code.h:1350
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
goto_programt::instructiont::is_start_thread
bool is_start_thread() const
Definition: goto_program.h:542
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
goto_programt::instructiont::get_condition
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:447
LOCATION
@ LOCATION
Definition: goto_program.h:39
goto_programt::instructiont::is_function_call
bool is_function_call() const
Definition: goto_program.h:530
ASSERT
@ ASSERT
Definition: goto_program.h:34
goto_programt::decl_identifierst
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:880
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
goto_programt::instructiont::is_target
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:499
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:562
goto_programt::instructiont::code_nonconst
codet & code_nonconst()
Set the code represented by this instruction.
Definition: goto_program.h:191
goto_programt::instructiont::nil_target
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:588
goto_programt::make_location
static instructiont make_location(const source_locationt &l)
Definition: goto_program.h:919
goto_programt::instructiont::call_function
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
Definition: goto_program.h:361
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:472
END_THREAD
@ END_THREAD
Definition: goto_program.h:38
goto_programt::swap
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:841
INCOMPLETE_GOTO
@ INCOMPLETE_GOTO
Definition: goto_program.h:50
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:1090
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:646
code_function_callt::function
exprt & function()
Definition: std_code.h:1248
goto_programt::instructiont::instructiont
instructiont(goto_program_instruction_typet _type)
Definition: goto_program.h:553
goto_programt::make_incomplete_goto
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1025
const_target_hash::operator()
std::size_t operator()(const goto_programt::const_targett t) const
Definition: goto_program.h:1212
goto_programt::make_catch
static instructiont make_catch(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:941
goto_programt::make_atomic_end
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:1004
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33