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"))
363  void make_location(const source_locationt &l)
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 
373  SINCE(2019, 2, 13, "use goto_programt::make_assertion() instead"))
374  void make_assertion(const exprt &g) { clear(ASSERT); guard=g; }
375 
377  SINCE(2019, 2, 13, "use goto_programt::make_assumption() instead"))
378  void make_assumption(const exprt &g) { clear(ASSUME); guard=g; }
379 
381  SINCE(2019, 2, 13, "use goto_programt::make_assignment() instead"))
382  void make_assignment() { clear(ASSIGN); }
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 
394  SINCE(2019, 2, 13, "use goto_programt::make_atomic_begin() instead"))
396 
398  SINCE(2019, 2, 13, "use goto_programt::make_atomic_end() instead"))
399  void make_atomic_end() { clear(ATOMIC_END); }
400 
402  SINCE(2019, 2, 13, "use goto_programt::make_end_function() instead"))
404 
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);
425  }
426 
427  void complete_goto(targett _target)
428  {
430  code.make_nil();
431  targets.push_back(_target);
432  type = GOTO;
433  }
434 
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 
451  SINCE(2019, 2, 13, "use goto_programt::make_function_call() instead"))
452  void make_function_call(const code_function_callt &_code)
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 
981  const code_gotot &_code,
983  {
984  return instructiont(_code, l, INCOMPLETE_GOTO, true_exprt(), {});
985  }
986 
988  targett _target,
990  {
991  return instructiont(
992  static_cast<const codet &>(get_nil_irep()),
993  l,
994  GOTO,
995  true_exprt(),
996  {_target});
997  }
998 
1000  targett _target,
1001  const exprt &g,
1003  {
1004  return instructiont(
1005  static_cast<const codet &>(get_nil_irep()),
1006  l,
1007  GOTO,
1008  g,
1009  {_target});
1010  }
1011 
1014  const code_assignt &_code,
1016  {
1017  return instructiont(_code, l, ASSIGN, nil_exprt(), {});
1018  }
1019 
1022  exprt lhs,
1023  exprt rhs,
1025  {
1026  return instructiont(
1027  code_assignt(std::move(lhs), std::move(rhs)), l, ASSIGN, nil_exprt(), {});
1028  }
1029 
1031  const code_declt &_code,
1033  {
1034  return instructiont(_code, l, DECL, nil_exprt(), {});
1035  }
1036 
1039  const code_function_callt &_code,
1041  {
1042  return instructiont(_code, l, FUNCTION_CALL, nil_exprt(), {});
1043  }
1044 
1047  exprt function,
1050  {
1051  return instructiont(
1052  code_function_callt(std::move(function), std::move(arguments)),
1053  l,
1054  FUNCTION_CALL,
1055  nil_exprt(),
1056  {});
1057  }
1058 };
1059 
1072 template <typename Target>
1074  Target target) const
1075 {
1076  if(target==instructions.end())
1077  return std::list<Target>();
1078 
1079  const auto next=std::next(target);
1080 
1081  const instructiont &i=*target;
1082 
1083  if(i.is_goto())
1084  {
1085  std::list<Target> successors(i.targets.begin(), i.targets.end());
1086 
1087  if(!i.get_condition().is_true() && next != instructions.end())
1088  successors.push_back(next);
1089 
1090  return successors;
1091  }
1092 
1093  if(i.is_start_thread())
1094  {
1095  std::list<Target> successors(i.targets.begin(), i.targets.end());
1096 
1097  if(next!=instructions.end())
1098  successors.push_back(next);
1099 
1100  return successors;
1101  }
1102 
1103  if(i.is_end_thread())
1104  {
1105  // no successors
1106  return std::list<Target>();
1107  }
1108 
1109  if(i.is_throw())
1110  {
1111  // the successors are non-obvious
1112  return std::list<Target>();
1113  }
1114 
1115  if(i.is_assume())
1116  {
1117  return !i.get_condition().is_false() && next != instructions.end()
1118  ? std::list<Target>{next}
1119  : std::list<Target>();
1120  }
1121 
1122  if(next!=instructions.end())
1123  {
1124  return std::list<Target>{next};
1125  }
1126 
1127  return std::list<Target>();
1128 }
1129 
1133 {
1134  const goto_programt::instructiont &_i1=*i1;
1135  const goto_programt::instructiont &_i2=*i2;
1136  return &_i1<&_i2;
1137 }
1138 
1139 // NOLINTNEXTLINE(readability/identifiers)
1141 {
1142  std::size_t operator()(
1143  const goto_programt::const_targett t) const
1144  {
1145  using hash_typet = decltype(&(*t));
1146  return std::hash<hash_typet>{}(&(*t));
1147  }
1148 };
1149 
1153 {
1154  template <class A, class B>
1155  bool operator()(const A &a, const B &b) const
1156  {
1157  return &(*a) == &(*b);
1158  }
1159 };
1160 
1161 #define forall_goto_program_instructions(it, program) \
1162  for(goto_programt::instructionst::const_iterator \
1163  it=(program).instructions.begin(); \
1164  it!=(program).instructions.end(); it++)
1165 
1166 #define Forall_goto_program_instructions(it, program) \
1167  for(goto_programt::instructionst::iterator \
1168  it=(program).instructions.begin(); \
1169  it!=(program).instructions.end(); it++)
1170 
1171 inline bool operator<(
1172  const goto_programt::const_targett &i1,
1173  const goto_programt::const_targett &i2)
1174 {
1175  return order_const_target(i1, i2);
1176 }
1177 
1178 inline bool operator<(
1179  const goto_programt::targett &i1,
1180  const goto_programt::targett &i2)
1181 {
1182  return &(*i1)<&(*i2);
1183 }
1184 
1185 std::list<exprt> objects_read(const goto_programt::instructiont &);
1186 std::list<exprt> objects_written(const goto_programt::instructiont &);
1187 
1188 std::list<exprt> expressions_read(const goto_programt::instructiont &);
1189 std::list<exprt> expressions_written(const goto_programt::instructiont &);
1190 
1191 std::string as_string(
1192  const namespacet &ns,
1193  const irep_idt &function,
1194  const goto_programt::instructiont &);
1195 
1196 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
const irept & get_nil_irep()
Definition: irep.cpp:26
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
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_return() instead")) void make_return()
Definition: goto_program.h:356
void update()
Update all indices.
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_other() instead")) void make_other(const codet &_code)
Definition: goto_program.h:384
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:448
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:967
static instructiont make_incomplete_goto(const code_gotot &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:980
targett add_instruction(goto_program_instruction_typet type)
Adds an instruction of given type at the end.
Definition: goto_program.h:701
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:606
std::list< targett > targetst
Definition: goto_program.h:581
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:639
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:549
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_decl() instead")) void make_decl(const code_declt &_code)
Definition: goto_program.h:443
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_goto() instead")) void make_goto(targett _target)
Definition: goto_program.h:413
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:517
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:527
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:920
static const source_locationt & nil()
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:927
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())
Definition: goto_program.h:999
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:729
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.
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_skip() instead")) void make_skip()
Definition: goto_program.h:359
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:669
const_targett const_cast_target(const_targett t) const
Dummy for templates with possible const contexts.
Definition: goto_program.h:595
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
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:1033
typet & type()
Return the type of the expression.
Definition: expr.h:81
exprt::operandst argumentst
Definition: std_code.h:1099
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:935
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:521
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
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:537
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_throw() instead")) void make_throw()
Definition: goto_program.h:366
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:851
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.
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_atomic_end() instead")) void make_atomic_end()
Definition: goto_program.h:397
targetst targets
The list of successor instructions.
Definition: goto_program.h:306
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_assignment() instead")) void make_assignment(const code_assignt &_code)
Definition: goto_program.h:435
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:783
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:946
std::list< instructiont > instructionst
Definition: goto_program.h:577
std::list< exprt > expressions_read(const goto_programt::instructiont &)
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:534
std::list< instructiont >::const_iterator const_targett
Definition: goto_program.h:301
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_catch() instead")) void make_catch()
Definition: goto_program.h:369
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:582
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:381
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:816
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_dead() instead")) void make_dead()
Definition: goto_program.h:390
const irep_idt & id() const
Definition: irep.h:418
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
unsigned loop_number
Number unique per function to identify loops.
Definition: goto_program.h:530
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:4107
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:957
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:755
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
instructionst::iterator targett
Definition: goto_program.h:579
A codet representing the declaration of a local variable.
Definition: std_code.h:399
void complete_goto(targett _target)
Definition: goto_program.h:427
The NIL expression.
Definition: std_expr.h:4125
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:585
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
Definition: goto_program.h:292
API to expression classes.
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_function_call() instead")) void make_function_call(const code_function_callt &_code)
Definition: goto_program.h:450
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:580
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:829
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
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:655
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1266
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:677
codet representation of a function call statement.
Definition: std_code.h:1089
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:285
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_location() instead")) void make_location(const source_locationt &l)
Definition: goto_program.h:362
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
void insert_before_swap(targett target, goto_programt &p)
Insertion that preserves jumps to "target".
Definition: goto_program.h:623
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:838
void compute_location_numbers()
Compute location numbers.
Definition: goto_program.h:741
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:777
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:615
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_assumption() instead")) void make_assumption(const exprt &g)
Definition: goto_program.h:376
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())
Definition: goto_program.h:987
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:647
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:495
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:694
Base class for all expressions.
Definition: expr.h:52
goto_programt()
Constructor.
Definition: goto_program.h:768
void set_return(code_returnt c)
Set the return statement for READ.
Definition: goto_program.h:234
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_end_function() instead")) void make_end_function()
Definition: goto_program.h:401
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:790
static instructiont make_location(const source_locationt &l)
Definition: goto_program.h:861
bool empty() const
Is the program empty?
Definition: goto_program.h:762
void compute_target_numbers()
Compute the target numbers.
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:510
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:464
void make_nil()
Definition: irep.h:475
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
validation_modet
Expression to hold a symbol (variable)
Definition: std_expr.h:88
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
void transform(std::function< optionalt< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
dstringt irep_idt
Definition: irep.h:32
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:1216
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_atomic_begin() instead")) void make_atomic_begin()
Definition: goto_program.h:393
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:511
goto_programt & operator=(const goto_programt &)=delete
std::string as_string(const namespacet &ns, const irep_idt &function, const goto_programt::instructiont &)
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_assignment() instead")) void make_assignment()
Definition: goto_program.h:380
instructiont(goto_program_instruction_typet _type)
Definition: goto_program.h:486
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_assertion() instead")) void make_assertion(const exprt &g)
Definition: goto_program.h:372
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_decl() instead")) void make_decl()
Definition: goto_program.h:387
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:337
static instructiont make_catch(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:883
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:913
A codet representing an assignment in the program.
Definition: std_code.h:292
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:843
std::ostream & output(std::ostream &out) const
Output goto-program to given stream.
Definition: goto_program.h:713
static instructiont make_throw(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:872
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1201
const codet & get_other() const
Get the statement for OTHER.
Definition: goto_program.h:255
DEPRECATED(SINCE(2019, 2, 13, "use goto_programt::make_incomplete_goto() instead")) void make_incomplete_goto(const code_gotot &_code)
Definition: goto_program.h:405