cprover
Loading...
Searching...
No Matches
goto_program.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Concrete Goto Program
4
5Author: 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
16
17#include <iosfwd>
18#include <set>
19#include <limits>
20#include <string>
21
22#include <util/deprecate.h>
23#include <util/invariant.h>
24#include <util/namespace.h>
26
27class code_gotot;
28enum 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 SET_RETURN_VALUE = 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
55std::ostream &operator<<(std::ostream &, goto_program_instruction_typet);
56
73{
74public:
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
179 class instructiont final
180 {
181 protected:
184
185 public:
187 const codet &get_code() const
188 {
189 return code;
190 }
191
194 {
195 return code;
196 }
197
199 const exprt &assign_lhs() const
200 {
202 return to_code_assign(code).lhs();
203 }
204
211
213 const exprt &assign_rhs() const
214 {
216 return to_code_assign(code).rhs();
217 }
218
225
228 {
231 return decl.symbol();
232 }
233
236 {
239 return decl.symbol();
240 }
241
244 {
246 return to_code_dead(code).symbol();
247 }
248
251 {
253 return to_code_dead(code).symbol();
254 }
255
257 const exprt &return_value() const
258 {
261 }
262
269
271 const exprt &call_function() const
272 {
275 }
276
283
285 const exprt &call_lhs() const
286 {
289 }
290
297
304
311
313 const codet &get_other() const
314 {
316 return code;
317 }
318
321 {
323 code = std::move(c);
324 }
325
328 protected:
330
331 public:
333 {
334 return _source_location;
335 }
336
341
344 {
345 return _type;
346 }
347
348 protected:
349 // Use type() to access. To prevent malformed instructions, no non-const
350 // access method is provided.
352
353 public:
358
360 bool has_condition() const
361 {
362 return is_goto() || is_incomplete_goto() || is_assume() || is_assert();
363 }
364
366 DEPRECATED(SINCE(2021, 10, 12, "Use condition() instead"))
367 const exprt &get_condition() const
368 {
370 return guard;
371 }
372
374 DEPRECATED(SINCE(2021, 10, 12, "Use condition_nonconst() instead"))
376 {
378 guard = std::move(c);
379 }
380
382 const exprt &condition() const
383 {
385 return guard;
386 }
387
390 {
392 return guard;
393 }
394
395 // The below will eventually become a single target only.
397 typedef std::list<instructiont>::iterator targett;
398 typedef std::list<instructiont>::const_iterator const_targett;
399 typedef std::list<targett> targetst;
400 typedef std::list<const_targett> const_targetst;
401
404
408 {
409 PRECONDITION(targets.size()==1);
410 return targets.front();
411 }
412
416 {
417 targets.clear();
418 targets.push_back(t);
419 }
420
421 bool has_target() const
422 {
423 return !targets.empty();
424 }
425
427 typedef std::list<irep_idt> labelst;
429
430 // will go away
431 std::set<targett> incoming_edges;
432
434 bool is_target() const
435 { return target_number!=nil_target; }
436
445
449 {
450 clear(SKIP);
451 }
452
456 {
458 _type = ASSUME;
459 targets.clear();
460 code.make_nil();
461 }
462
464 {
466 code.make_nil();
467 targets.push_back(_target);
468 _type = GOTO;
469 }
470
471 // clang-format off
472 bool is_goto () const { return _type == GOTO; }
473 bool is_set_return_value() const { return _type == SET_RETURN_VALUE; }
474 bool is_assign () const { return _type == ASSIGN; }
475 bool is_function_call () const { return _type == FUNCTION_CALL; }
476 bool is_throw () const { return _type == THROW; }
477 bool is_catch () const { return _type == CATCH; }
478 bool is_skip () const { return _type == SKIP; }
479 bool is_location () const { return _type == LOCATION; }
480 bool is_other () const { return _type == OTHER; }
481 bool is_decl () const { return _type == DECL; }
482 bool is_dead () const { return _type == DEAD; }
483 bool is_assume () const { return _type == ASSUME; }
484 bool is_assert () const { return _type == ASSERT; }
485 bool is_atomic_begin () const { return _type == ATOMIC_BEGIN; }
486 bool is_atomic_end () const { return _type == ATOMIC_END; }
487 bool is_start_thread () const { return _type == START_THREAD; }
488 bool is_end_thread () const { return _type == END_THREAD; }
489 bool is_end_function () const { return _type == END_FUNCTION; }
490 bool is_incomplete_goto () const { return _type == INCOMPLETE_GOTO; }
491 // clang-format on
492
494 instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit)
495 {
496 }
497
505
520
522 void swap(instructiont &instruction)
523 {
524 using std::swap;
525 swap(instruction.code, code);
527 swap(instruction._type, _type);
528 swap(instruction.guard, guard);
529 swap(instruction.targets, targets);
530 swap(instruction.labels, labels);
531 }
532
534 static const unsigned nil_target=
535 std::numeric_limits<unsigned>::max();
536
540 unsigned location_number = 0;
541
543 unsigned loop_number = 0;
544
548
550 bool is_backwards_goto() const
551 {
552 if(!is_goto())
553 return false;
554
555 for(const auto &t : targets)
556 if(t->location_number<=location_number)
557 return true;
558
559 return false;
560 }
561
562 std::string to_string() const
563 {
564 std::ostringstream instruction_id_builder;
566 return instruction_id_builder.str();
567 }
568
573 bool equals(const instructiont &other) const;
574
579 void validate(const namespacet &ns, const validation_modet vm) const;
580
583 void transform(std::function<optionalt<exprt>(exprt)>);
584
586 void apply(std::function<void(const exprt &)>) const;
587 };
588
589 // Never try to change this to vector-we mutate the list while iterating
590 typedef std::list<instructiont> instructionst;
591
592 typedef instructionst::iterator targett;
593 typedef instructionst::const_iterator const_targett;
594 typedef std::list<targett> targetst;
595 typedef std::list<const_targett> const_targetst;
596
599
603 {
604 return instructions.erase(t, t);
605 }
606
609 {
610 return t;
611 }
612
613 template <typename Target>
614 std::list<Target> get_successors(Target target) const;
615
617
620 {
621 PRECONDITION(target!=instructions.end());
622 const auto next=std::next(target);
623 instructions.insert(next, instructiont())->swap(*target);
624 }
625
644 void insert_before_swap(targett target, instructiont &instruction)
645 {
646 insert_before_swap(target);
647 target->swap(instruction);
648 }
649
653 targett target,
654 goto_programt &p)
655 {
656 PRECONDITION(target!=instructions.end());
657 if(p.instructions.empty())
658 return;
659 insert_before_swap(target, p.instructions.front());
660 auto next=std::next(target);
661 p.instructions.erase(p.instructions.begin());
662 instructions.splice(next, p.instructions);
663 }
664
669 {
670 return instructions.insert(target, instructiont());
671 }
672
677 {
678 return instructions.insert(target, i);
679 }
680
685 {
686 return instructions.insert(std::next(target), instructiont());
687 }
688
693 {
694 return instructions.insert(std::next(target), i);
695 }
696
699 {
700 instructions.splice(instructions.end(),
701 p.instructions);
702 }
703
707 const_targett target,
708 goto_programt &p)
709 {
710 instructions.splice(target, p.instructions);
711 }
712
715 targett add(instructiont &&instruction)
716 {
717 instructions.push_back(std::move(instruction));
718 return --instructions.end();
719 }
720
724 {
725 return add(instructiont());
726 }
727
734
736 std::ostream &output(
737 const namespacet &ns,
738 const irep_idt &identifier,
739 std::ostream &out) const;
740
742 std::ostream &output(std::ostream &out) const;
743
745 std::ostream &output_instruction(
746 const namespacet &ns,
747 const irep_idt &identifier,
748 std::ostream &out,
749 const instructionst::value_type &instruction) const;
750
753
756 {
757 for(auto &i : instructions)
758 {
759 INVARIANT(
760 nr != std::numeric_limits<unsigned>::max(),
761 "Too many location numbers assigned");
762 i.location_number=nr++;
763 }
764 }
765
768 {
769 unsigned nr=0;
771 }
772
775
777 void update();
778
780 static irep_idt
781 loop_id(const irep_idt &function_id, const instructiont &instruction)
782 {
783 return id2string(function_id) + "." +
784 std::to_string(instruction.loop_number);
785 }
786
788 bool empty() const
789 {
790 return instructions.empty();
791 }
792
795 {
796 }
797
799 {
800 }
801
803 void swap(goto_programt &program)
804 {
805 program.instructions.swap(instructions);
806 }
807
809 void clear()
810 {
812 }
813
817 {
818 PRECONDITION(!instructions.empty());
819 const auto end_function=std::prev(instructions.end());
820 DATA_INVARIANT(end_function->is_end_function(),
821 "goto program ends on END_FUNCTION");
822 return end_function;
823 }
824
828 {
829 PRECONDITION(!instructions.empty());
830 const auto end_function=std::prev(instructions.end());
831 DATA_INVARIANT(end_function->is_end_function(),
832 "goto program ends on END_FUNCTION");
833 return end_function;
834 }
835
837 void copy_from(const goto_programt &src);
838
840 bool has_assertion() const;
841
842 typedef std::set<irep_idt> decl_identifierst;
845
849 bool equals(const goto_programt &other) const;
850
855 void validate(const namespacet &ns, const validation_modet vm) const
856 {
857 for(const instructiont &ins : instructions)
858 {
859 ins.validate(ns, vm);
860 }
861 }
862
864 exprt return_value,
866 {
867 return instructiont(
868 code_returnt(std::move(return_value)),
869 l,
871 nil_exprt(),
872 {});
873 }
874
876 const code_returnt &code,
877 const source_locationt &l = source_locationt::nil()) = delete;
878
879 static instructiont
881 {
882 return instructiont(
883 static_cast<const codet &>(get_nil_irep()),
884 l,
885 SKIP,
886 nil_exprt(),
887 {});
888 }
889
891 {
892 return instructiont(
893 static_cast<const codet &>(get_nil_irep()),
894 l,
895 LOCATION,
896 nil_exprt(),
897 {});
898 }
899
900 static instructiont
902 {
903 return instructiont(
904 static_cast<const codet &>(get_nil_irep()),
905 l,
906 THROW,
907 nil_exprt(),
908 {});
909 }
910
911 static instructiont
913 {
914 return instructiont(
915 static_cast<const codet &>(get_nil_irep()),
916 l,
917 CATCH,
918 nil_exprt(),
919 {});
920 }
921
923 const exprt &g,
925 {
926 return instructiont(
927 static_cast<const codet &>(get_nil_irep()),
928 l,
929 ASSERT,
930 exprt(g),
931 {});
932 }
933
935 const exprt &g,
937 {
938 return instructiont(
939 static_cast<const codet &>(get_nil_irep()), l, ASSUME, g, {});
940 }
941
943 const codet &_code,
945 {
946 return instructiont(_code, l, OTHER, nil_exprt(), {});
947 }
948
950 const symbol_exprt &symbol,
952 {
953 return instructiont(code_declt(symbol), l, DECL, nil_exprt(), {});
954 }
955
957 const symbol_exprt &symbol,
959 {
960 return instructiont(code_deadt(symbol), l, DEAD, nil_exprt(), {});
961 }
962
963 static instructiont
965 {
966 return instructiont(
967 static_cast<const codet &>(get_nil_irep()),
968 l,
970 nil_exprt(),
971 {});
972 }
973
974 static instructiont
976 {
977 return instructiont(
978 static_cast<const codet &>(get_nil_irep()),
979 l,
981 nil_exprt(),
982 {});
983 }
984
985 static instructiont
987 {
988 return instructiont(
989 static_cast<const codet &>(get_nil_irep()),
990 l,
992 nil_exprt(),
993 {});
994 }
995
997 const exprt &_cond,
999 {
1000 PRECONDITION(_cond.type().id() == ID_bool);
1001 return instructiont(
1002 static_cast<const codet &>(get_nil_irep()),
1003 l,
1005 _cond,
1006 {});
1007 }
1008
1009 static instructiont
1011 {
1012 return instructiont(
1013 static_cast<const codet &>(get_nil_irep()),
1014 l,
1016 true_exprt(),
1017 {});
1018 }
1019
1020 static instructiont make_incomplete_goto(
1021 const code_gotot &,
1023
1027 {
1028 return instructiont(
1029 static_cast<const codet &>(get_nil_irep()),
1030 l,
1031 GOTO,
1032 true_exprt(),
1033 {_target});
1034 }
1035
1038 const exprt &g,
1040 {
1041 return instructiont(
1042 static_cast<const codet &>(get_nil_irep()),
1043 l,
1044 GOTO,
1045 g,
1046 {_target});
1047 }
1048
1051 const code_assignt &_code,
1053 {
1054 return instructiont(_code, l, ASSIGN, nil_exprt(), {});
1055 }
1056
1059 exprt lhs,
1060 exprt rhs,
1062 {
1063 return instructiont(
1064 code_assignt(std::move(lhs), std::move(rhs)), l, ASSIGN, nil_exprt(), {});
1065 }
1066
1068 const code_declt &_code,
1070 {
1071 return instructiont(_code, l, DECL, nil_exprt(), {});
1072 }
1073
1078 {
1079 return instructiont(_code, l, FUNCTION_CALL, nil_exprt(), {});
1080 }
1081
1084 exprt lhs,
1085 exprt function,
1088 {
1089 return instructiont(
1090 code_function_callt(lhs, std::move(function), std::move(arguments)),
1091 l,
1093 nil_exprt(),
1094 {});
1095 }
1096};
1097
1110template <typename Target>
1112 Target target) const
1113{
1114 if(target==instructions.end())
1115 return std::list<Target>();
1116
1117 const auto next=std::next(target);
1118
1119 const instructiont &i=*target;
1120
1121 if(i.is_goto())
1122 {
1123 std::list<Target> successors(i.targets.begin(), i.targets.end());
1124
1125 if(!i.get_condition().is_true() && next != instructions.end())
1126 successors.push_back(next);
1127
1128 return successors;
1129 }
1130
1131 if(i.is_start_thread())
1132 {
1133 std::list<Target> successors(i.targets.begin(), i.targets.end());
1134
1135 if(next!=instructions.end())
1136 successors.push_back(next);
1137
1138 return successors;
1139 }
1140
1141 if(i.is_end_thread())
1142 {
1143 // no successors
1144 return std::list<Target>();
1145 }
1146
1147 if(i.is_throw())
1148 {
1149 // the successors are non-obvious
1150 return std::list<Target>();
1151 }
1152
1153 if(i.is_assume())
1154 {
1155 return !i.get_condition().is_false() && next != instructions.end()
1156 ? std::list<Target>{next}
1157 : std::list<Target>();
1158 }
1159
1160 if(next!=instructions.end())
1161 {
1162 return std::list<Target>{next};
1163 }
1164
1165 return std::list<Target>();
1166}
1167
1171{
1174 return &_i1<&_i2;
1175}
1176
1177// NOLINTNEXTLINE(readability/identifiers)
1179{
1180 std::size_t operator()(
1181 const goto_programt::const_targett t) const
1182 {
1183 using hash_typet = decltype(&(*t));
1184 return std::hash<hash_typet>{}(&(*t));
1185 }
1186};
1187
1191{
1192 template <class A, class B>
1193 bool operator()(const A &a, const B &b) const
1194 {
1195 return &(*a) == &(*b);
1196 }
1197};
1198
1199template <typename GotoFunctionT, typename PredicateT, typename HandlerT>
1201 GotoFunctionT &&goto_function,
1204{
1205 auto &&instructions = goto_function.body.instructions;
1206 for(auto it = instructions.begin(); it != instructions.end(); ++it)
1207 {
1208 if(predicate(it))
1209 {
1210 handler(it);
1211 }
1212 }
1213}
1214
1215template <typename GotoFunctionT, typename HandlerT>
1217{
1218 using iterator_t = decltype(goto_function.body.instructions.begin());
1220 goto_function, [](const iterator_t &) { return true; }, handler);
1221}
1222
1223#define forall_goto_program_instructions(it, program) \
1224 for(goto_programt::instructionst::const_iterator \
1225 it=(program).instructions.begin(); \
1226 it!=(program).instructions.end(); it++)
1227
1228#define Forall_goto_program_instructions(it, program) \
1229 for(goto_programt::instructionst::iterator \
1230 it=(program).instructions.begin(); \
1231 it!=(program).instructions.end(); it++)
1232
1233inline bool operator<(
1236{
1237 return order_const_target(i1, i2);
1238}
1239
1240inline bool operator<(
1243{
1244 return &(*i1)<&(*i2);
1245}
1246
1247std::list<exprt> objects_read(const goto_programt::instructiont &);
1248std::list<exprt> objects_written(const goto_programt::instructiont &);
1249
1250std::list<exprt> expressions_read(const goto_programt::instructiont &);
1251std::list<exprt> expressions_written(const goto_programt::instructiont &);
1252
1253std::string as_string(
1254 const namespacet &ns,
1255 const irep_idt &function,
1257
1258#endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
A codet representing an assignment in the program.
A codet representing the removal of a local variable going out of scope.
symbol_exprt & symbol()
A codet representing the declaration of a local variable.
codet representation of a function call statement.
codet representation of a goto statement.
Definition std_code.h:841
codet representation of a "return from a function" statement.
const exprt & return_value() const
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
This class represents an instruction in the GOTO intermediate representation.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
unsigned target_number
A number to identify branch targets.
void transform(std::function< optionalt< exprt >(exprt)>)
Apply given transformer to all expressions; no return value means no change needed.
void turn_into_skip()
Transforms an existing instruction into a skip, retaining the source_location.
exprt & call_lhs()
Get the lhs of a FUNCTION_CALL (may be nil)
void complete_goto(targett _target)
bool is_target() const
Is this node a branch target?
codet code
Do not read or modify directly – use get_X() instead.
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
std::list< targett > targetst
std::set< targett > incoming_edges
const codet & get_code() const
Get the code represented by this instruction.
bool has_condition() const
Does this instruction have a condition?
codet & code_nonconst()
Set the code represented by this instruction.
void apply(std::function< void(const exprt &)>) const
Apply given function to all expressions.
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
targetst targets
The list of successor instructions.
const codet & get_other() const
Get the statement for OTHER.
symbol_exprt & dead_symbol()
Get the symbol for DEAD.
exprt & assign_lhs_nonconst()
Get the lhs of the assignment for ASSIGN.
unsigned loop_number
Number unique per function to identify loops.
exprt::operandst & call_arguments()
Get the arguments of a FUNCTION_CALL.
void turn_into_assume()
Transforms either an assertion or a GOTO instruction into an assumption, with the same condition.
goto_program_instruction_typet _type
bool equals(const instructiont &other) const
Syntactic equality: two instructiont are equal if they have the same type, code, guard,...
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
std::string to_string() const
const exprt::operandst & call_arguments() const
Get the arguments of a FUNCTION_CALL.
unsigned location_number
A globally unique number to identify a program location.
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
source_locationt _source_location
The location of the instruction in the source file.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
std::list< instructiont >::const_iterator const_targett
static const unsigned nil_target
Uniquely identify an invalid target or location.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
const exprt & call_function() const
Get the function that is called for FUNCTION_CALL.
std::list< const_targett > const_targetst
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.
void clear(goto_program_instruction_typet __type)
Clear the node.
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
void set_condition(exprt c)
Set the condition of gotos, assume, assert.
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
exprt guard
Guard for gotos, assume, assert Use condition() method to access.
const exprt & condition() const
Get the condition of gotos, assume, assert.
instructiont(goto_program_instruction_typet __type)
void swap(instructiont &instruction)
Swap two instructions.
exprt & condition_nonconst()
Get the condition of gotos, assume, assert.
std::list< irep_idt > labelst
Goto target labels.
source_locationt & source_location_nonconst()
exprt & return_value()
Get the return value of a SET_RETURN_VALUE instruction.
exprt & call_function()
Get the function that is called for FUNCTION_CALL.
exprt & assign_rhs_nonconst()
Get the rhs of the assignment for ASSIGN.
void set_other(codet &c)
Set the statement for OTHER.
const source_locationt & source_location() const
goto_program_instruction_typet type() const
What kind of instruction?
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
symbol_exprt & decl_symbol()
Get the declared symbol for DECL.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
void clear()
Clear the goto program.
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
static instructiont make_decl(const code_declt &_code, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const source_locationt &l=source_locationt::nil())
targett insert_after(const_targett target, const instructiont &i)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void update()
Update all indices.
goto_programt & operator=(goto_programt &&other)
targett const_cast_target(const_targett t)
Convert a const_targett to a targett - use with care and avoid whenever possible.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
bool has_assertion() const
Does the goto program have an assertion?
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
goto_programt & operator=(const goto_programt &)=delete
targett insert_before(const_targett target, const instructiont &i)
Insertion before the instruction pointed-to by the given instruction iterator target.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
instructionst::const_iterator const_targett
static instructiont make_set_return_value(const code_returnt &code, const source_locationt &l=source_locationt::nil())=delete
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
targett add_instruction(goto_program_instruction_typet type)
Adds an instruction of given type at the end.
targett add_instruction()
Adds an instruction at the end.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_goto(targett _target, const exprt &g, const source_locationt &l=source_locationt::nil())
void insert_before_swap(targett target, goto_programt &p)
Insertion that preserves jumps to "target".
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
goto_programt()
Constructor.
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
std::list< instructiont > instructionst
std::set< irep_idt > decl_identifierst
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
std::list< const_targett > const_targetst
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
goto_programt(const goto_programt &)=delete
Copying is deleted as this class contains pointers that cannot be copied.
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_throw(const source_locationt &l=source_locationt::nil())
const_targett const_cast_target(const_targett t) const
Dummy for templates with possible const contexts.
void compute_location_numbers(unsigned &nr)
Compute location numbers.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
const_targett get_end_function() const
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
static instructiont make_catch(const source_locationt &l=source_locationt::nil())
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
goto_programt(goto_programt &&other)
void compute_location_numbers()
Compute location numbers.
void swap(goto_programt &program)
Swap the goto program.
static instructiont make_location(const source_locationt &l)
void compute_target_numbers()
Compute the target numbers.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
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...
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.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
static instructiont make_assignment(exprt lhs, exprt rhs, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
void compute_loop_numbers()
Compute loop numbers.
std::list< targett > targetst
void make_nil()
Definition irep.h:454
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:2874
static const source_locationt & nil()
Expression to hold a symbol (variable)
Definition std_expr.h:80
The Boolean constant true.
Definition std_expr.h:2856
#define SINCE(year, month, day, msg)
Definition deprecate.h:26
#define DEPRECATED(msg)
Definition deprecate.h:23
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
const code_returnt & to_code_return(const codet &code)
const code_deadt & to_code_dead(const codet &code)
bool order_const_target(const goto_programt::const_targett i1, const goto_programt::const_targett i2)
void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler)
bool operator<(const goto_programt::const_targett &i1, const goto_programt::const_targett &i2)
std::list< exprt > expressions_read(const goto_programt::instructiont &)
std::list< exprt > objects_written(const goto_programt::instructiont &)
std::ostream & operator<<(std::ostream &, goto_program_instruction_typet)
Outputs a string representation of a goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
@ FUNCTION_CALL
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
std::string as_string(const namespacet &ns, const irep_idt &function, const goto_programt::instructiont &)
std::list< exprt > expressions_written(const goto_programt::instructiont &)
void for_each_instruction_if(GotoFunctionT &&goto_function, PredicateT predicate, HandlerT handler)
std::list< exprt > objects_read(const goto_programt::instructiont &)
const irept & get_nil_irep()
Definition irep.cpp:20
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
STL namespace.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
std::size_t operator()(const goto_programt::const_targett t) const
Functor to check whether iterators from different collections point at the same object.
bool operator()(const A &a, const B &b) const
validation_modet