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:
182 
184  irep_idt function;
185 
188 
191 
194 
195  // The below will eventually become a single target only.
197  typedef std::list<instructiont>::iterator targett;
198  typedef std::list<instructiont>::const_iterator const_targett;
199  typedef std::list<targett> targetst;
200  typedef std::list<const_targett> const_targetst;
201 
204 
208  {
209  PRECONDITION(targets.size()==1);
210  return targets.front();
211  }
212 
216  {
217  targets.clear();
218  targets.push_back(t);
219  }
220 
221  bool has_target() const
222  {
223  return !targets.empty();
224  }
225 
227  typedef std::list<irep_idt> labelst;
229 
230  // will go away
231  std::set<targett> incoming_edges;
232 
234  bool is_target() const
235  { return target_number!=nil_target; }
236 
239  {
240  type=_type;
241  targets.clear();
242  guard=true_exprt();
243  code.make_nil();
244  }
245 
246  void make_return() { clear(RETURN); }
247  void make_skip() { clear(SKIP); }
250  void make_throw() { clear(THROW); }
251  void make_catch() { clear(CATCH); }
252  void make_assertion(const exprt &g) { clear(ASSERT); guard=g; }
253  void make_assumption(const exprt &g) { clear(ASSUME); guard=g; }
255  void make_other(const codet &_code) { clear(OTHER); code=_code; }
256  void make_decl() { clear(DECL); }
257  void make_dead() { clear(DEAD); }
261 
262  void make_incomplete_goto(const code_gotot &_code)
263  {
265  code = _code;
266  }
267 
268  void make_goto(targett _target)
269  {
270  clear(GOTO);
271  targets.push_back(_target);
272  }
273 
274  void make_goto(targett _target, const exprt &g)
275  {
276  make_goto(_target);
277  guard=g;
278  }
279 
280  void complete_goto(targett _target)
281  {
283  targets.push_back(_target);
284  type = GOTO;
285  }
286 
287  void make_assignment(const codet &_code)
288  {
289  clear(ASSIGN);
290  code=_code;
291  }
292 
293  void make_decl(const codet &_code)
294  {
295  clear(DECL);
296  code=_code;
297  }
298 
299  void make_function_call(const codet &_code)
300  {
302  code=_code;
303  }
304 
305  bool is_goto () const { return type==GOTO; }
306  bool is_return () const { return type==RETURN; }
307  bool is_assign () const { return type==ASSIGN; }
308  bool is_function_call() const { return type==FUNCTION_CALL; }
309  bool is_throw () const { return type==THROW; }
310  bool is_catch () const { return type==CATCH; }
311  bool is_skip () const { return type==SKIP; }
312  bool is_location () const { return type==LOCATION; }
313  bool is_other () const { return type==OTHER; }
314  bool is_decl () const { return type==DECL; }
315  bool is_dead () const { return type==DEAD; }
316  bool is_assume () const { return type==ASSUME; }
317  bool is_assert () const { return type==ASSERT; }
318  bool is_atomic_begin () const { return type==ATOMIC_BEGIN; }
319  bool is_atomic_end () const { return type==ATOMIC_END; }
320  bool is_start_thread () const { return type==START_THREAD; }
321  bool is_end_thread () const { return type==END_THREAD; }
322  bool is_end_function () const { return type==END_FUNCTION; }
323  bool is_incomplete_goto() const
324  {
325  return type == INCOMPLETE_GOTO;
326  }
327 
329  instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit)
330  {
331  }
332 
334  source_location(static_cast<const source_locationt &>(get_nil_irep())),
335  type(_type),
336  guard(true_exprt()),
337  location_number(0),
338  loop_number(0),
340  {
341  }
342 
344  void swap(instructiont &instruction)
345  {
346  using std::swap;
347  swap(instruction.code, code);
348  swap(instruction.source_location, source_location);
349  swap(instruction.type, type);
350  swap(instruction.guard, guard);
351  swap(instruction.targets, targets);
352  swap(instruction.function, function);
353  }
354 
355  #if (defined _MSC_VER && _MSC_VER <= 1800)
356  // Visual Studio <= 2013 does not support constexpr, making
357  // numeric_limits::max() unviable for a static const member
358  static const unsigned nil_target=
359  static_cast<unsigned>(-1);
360  #else
361  static const unsigned nil_target=
363  std::numeric_limits<unsigned>::max();
364  #endif
365 
369  unsigned location_number;
370 
372  unsigned loop_number;
373 
376  unsigned target_number;
377 
379  bool is_backwards_goto() const
380  {
381  if(!is_goto())
382  return false;
383 
384  for(const auto &t : targets)
385  if(t->location_number<=location_number)
386  return true;
387 
388  return false;
389  }
390 
391  std::string to_string() const
392  {
393  std::ostringstream instruction_id_builder;
394  instruction_id_builder << type;
395  return instruction_id_builder.str();
396  }
397 
402  bool equals(const instructiont &other) const;
403 
408  void validate(const namespacet &ns, const validation_modet vm) const;
409  };
410 
411  // Never try to change this to vector-we mutate the list while iterating
412  typedef std::list<instructiont> instructionst;
413 
414  typedef instructionst::iterator targett;
415  typedef instructionst::const_iterator const_targett;
416  typedef std::list<targett> targetst;
417  typedef std::list<const_targett> const_targetst;
418 
421 
425  {
426  return instructions.erase(t, t);
427  }
428 
431  {
432  return t;
433  }
434 
440  static const irep_idt get_function_id(
441  const_targett l)
442  {
443  // The field `function` of an instruction may not always contain the id of
444  // the function it is currently in, due to goto program modifications such
445  // as inlining. For example, if an instruction in a function `f` is inlined
446  // into a function `g`, the instruction may, depending on the arguments to
447  // the inliner, retain the original value of `f` in the function field.
448  // However, instructions of type END_FUNCTION are never inlined into other
449  // functions, hence they contain the id of the function they are in. Thus,
450  // this function takes the END_FUNCTION instruction of the goto program and
451  // returns the value of its function field.
452 
453  while(!l->is_end_function())
454  ++l;
455 
456  return l->function;
457  }
458 
463  static const irep_idt get_function_id(
464  const goto_programt &p)
465  {
466  PRECONDITION(!p.empty());
467 
468  return get_function_id(--p.instructions.end());
469  }
470 
471  template <typename Target>
472  std::list<Target> get_successors(Target target) const;
473 
474  void compute_incoming_edges();
475 
478  {
479  PRECONDITION(target!=instructions.end());
480  const auto next=std::next(target);
481  instructions.insert(next, instructiont())->swap(*target);
482  }
483 
486  void insert_before_swap(targett target, instructiont &instruction)
487  {
488  insert_before_swap(target);
489  target->swap(instruction);
490  }
491 
495  targett target,
496  goto_programt &p)
497  {
498  PRECONDITION(target!=instructions.end());
499  if(p.instructions.empty())
500  return;
501  insert_before_swap(target, p.instructions.front());
502  auto next=std::next(target);
503  p.instructions.erase(p.instructions.begin());
504  instructions.splice(next, p.instructions);
505  }
506 
511  {
512  return instructions.insert(target, instructiont());
513  }
514 
519  {
520  return instructions.insert(std::next(target), instructiont());
521  }
522 
525  {
526  instructions.splice(instructions.end(),
527  p.instructions);
528  }
529 
533  const_targett target,
534  goto_programt &p)
535  {
536  instructions.splice(target, p.instructions);
537  }
538 
542  {
543  instructions.push_back(instructiont());
544  return --instructions.end();
545  }
546 
550  {
551  instructions.push_back(instructiont(type));
552  return --instructions.end();
553  }
554 
556  std::ostream &output(
557  const namespacet &ns,
558  const irep_idt &identifier,
559  std::ostream &out) const;
560 
562  std::ostream &output(std::ostream &out) const
563  {
564  return output(namespacet(symbol_tablet()), "", out);
565  }
566 
568  std::ostream &output_instruction(
569  const namespacet &ns,
570  const irep_idt &identifier,
571  std::ostream &out,
572  const instructionst::value_type &instruction) const;
573 
575  void compute_target_numbers();
576 
578  void compute_location_numbers(unsigned &nr)
579  {
580  for(auto &i : instructions)
581  {
582  INVARIANT(
583  nr != std::numeric_limits<unsigned>::max(),
584  "Too many location numbers assigned");
585  i.location_number=nr++;
586  }
587  }
588 
594  void update_instructions_function(const irep_idt &function_id)
595  {
596  for(auto &instruction : instructions)
597  {
598  if(instruction.function.empty())
599  {
600  instruction.function = function_id;
601  }
602  }
603  }
604 
607  {
608  unsigned nr=0;
610  }
611 
613  void compute_loop_numbers();
614 
616  void update();
617 
619  static irep_idt loop_id(const instructiont &instruction)
620  {
621  return id2string(instruction.function)+"."+
622  std::to_string(instruction.loop_number);
623  }
624 
626  bool empty() const
627  {
628  return instructions.empty();
629  }
630 
633  {
634  }
635 
637  {
638  }
639 
641  void swap(goto_programt &program)
642  {
643  program.instructions.swap(instructions);
644  }
645 
647  void clear()
648  {
649  instructions.clear();
650  }
651 
655  {
656  PRECONDITION(!instructions.empty());
657  const auto end_function=std::prev(instructions.end());
658  DATA_INVARIANT(end_function->is_end_function(),
659  "goto program ends on END_FUNCTION");
660  return end_function;
661  }
662 
666  {
667  PRECONDITION(!instructions.empty());
668  const auto end_function=std::prev(instructions.end());
669  DATA_INVARIANT(end_function->is_end_function(),
670  "goto program ends on END_FUNCTION");
671  return end_function;
672  }
673 
675  void copy_from(const goto_programt &src);
676 
678  bool has_assertion() const;
679 
680  typedef std::set<irep_idt> decl_identifierst;
682  void get_decl_identifiers(decl_identifierst &decl_identifiers) const;
683 
687  bool equals(const goto_programt &other) const;
688 
693  void validate(const namespacet &ns, const validation_modet vm) const
694  {
695  for(const instructiont &ins : instructions)
696  {
697  ins.validate(ns, vm);
698  }
699  }
700 };
701 
714 template <typename Target>
716  Target target) const
717 {
718  if(target==instructions.end())
719  return std::list<Target>();
720 
721  const auto next=std::next(target);
722 
723  const instructiont &i=*target;
724 
725  if(i.is_goto())
726  {
727  std::list<Target> successors(i.targets.begin(), i.targets.end());
728 
729  if(!i.guard.is_true() && next!=instructions.end())
730  successors.push_back(next);
731 
732  return successors;
733  }
734 
735  if(i.is_start_thread())
736  {
737  std::list<Target> successors(i.targets.begin(), i.targets.end());
738 
739  if(next!=instructions.end())
740  successors.push_back(next);
741 
742  return successors;
743  }
744 
745  if(i.is_end_thread())
746  {
747  // no successors
748  return std::list<Target>();
749  }
750 
751  if(i.is_throw())
752  {
753  // the successors are non-obvious
754  return std::list<Target>();
755  }
756 
757  if(i.is_assume())
758  {
759  return
760  !i.guard.is_false() && next!=instructions.end() ?
761  std::list<Target>{next} :
762  std::list<Target>();
763  }
764 
765  if(next!=instructions.end())
766  {
767  return std::list<Target>{next};
768  }
769 
770  return std::list<Target>();
771 }
772 
773 inline bool order_const_target(
776 {
777  const goto_programt::instructiont &_i1=*i1;
778  const goto_programt::instructiont &_i2=*i2;
779  return &_i1<&_i2;
780 }
781 
782 // NOLINTNEXTLINE(readability/identifiers)
784 {
785  std::size_t operator()(
786  const goto_programt::const_targett t) const
787  {
788  using hash_typet = decltype(&(*t));
789  return std::hash<hash_typet>{}(&(*t));
790  }
791 };
792 
796 {
797  template <class A, class B>
798  bool operator()(const A &a, const B &b) const
799  {
800  return &(*a) == &(*b);
801  }
802 };
803 
804 #define forall_goto_program_instructions(it, program) \
805  for(goto_programt::instructionst::const_iterator \
806  it=(program).instructions.begin(); \
807  it!=(program).instructions.end(); it++)
808 
809 #define Forall_goto_program_instructions(it, program) \
810  for(goto_programt::instructionst::iterator \
811  it=(program).instructions.begin(); \
812  it!=(program).instructions.end(); it++)
813 
814 inline bool operator<(
817 {
818  return order_const_target(i1, i2);
819 }
820 
821 inline bool operator<(
822  const goto_programt::targett &i1,
823  const goto_programt::targett &i2)
824 {
825  return &(*i1)<&(*i2);
826 }
827 
828 std::list<exprt> objects_read(const goto_programt::instructiont &);
829 std::list<exprt> objects_written(const goto_programt::instructiont &);
830 
831 std::list<exprt> expressions_read(const goto_programt::instructiont &);
832 std::list<exprt> expressions_written(const goto_programt::instructiont &);
833 
834 std::string as_string(
835  const namespacet &ns,
837 
838 #endif // CPROVER_GOTO_PROGRAMS_GOTO_PROGRAM_H
const irept & get_nil_irep()
Definition: irep.cpp:55
goto_programt(goto_programt &&other)
Definition: goto_program.h:85
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:184
void update()
Update all indices.
targett add_instruction(goto_program_instruction_typet type)
Adds an instruction of given type at the end.
Definition: goto_program.h:549
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:477
std::list< targett > targetst
Definition: goto_program.h:416
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:510
void compute_loop_numbers()
Compute loop numbers.
std::set< targett > incoming_edges
Definition: goto_program.h:231
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:391
void make_assumption(const exprt &g)
Definition: goto_program.h:253
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:369
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:190
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void compute_location_numbers(unsigned &nr)
Compute location numbers.
Definition: goto_program.h:578
std::size_t operator()(const goto_programt::const_targett t) const
Definition: goto_program.h:785
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:131
bool has_assertion() const
Does the goto program have an assertion?
std::list< exprt > objects_written(const goto_programt::instructiont &)
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:524
const_targett const_cast_target(const_targett t) const
Dummy for templates with possible const contexts.
Definition: goto_program.h:430
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:424
bool operator<(const goto_programt::const_targett &i1, const goto_programt::const_targett &i2)
Definition: goto_program.h:814
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:122
codet representation of a goto statement.
Definition: std_code.h:913
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 const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:362
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void make_assignment(const codet &_code)
Definition: goto_program.h:287
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:207
bool operator()(const A &a, const B &b) const
Definition: goto_program.h:798
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
Definition: goto_program.h:379
void make_function_call(const codet &_code)
Definition: goto_program.h:299
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.
targetst targets
The list of successor instructions.
Definition: goto_program.h:203
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:647
static const irep_idt get_function_id(const goto_programt &p)
Get the id of the function that contains the given goto program.
Definition: goto_program.h:463
std::list< instructiont > instructionst
Definition: goto_program.h:412
std::list< exprt > expressions_read(const goto_programt::instructiont &)
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:376
std::list< instructiont >::const_iterator const_targett
Definition: goto_program.h:198
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:417
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:680
const_targett get_end_function() const
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:665
unsigned loop_number
Number unique per function to identify loops.
Definition: goto_program.h:372
std::list< exprt > expressions_written(const goto_programt::instructiont &)
The Boolean constant true.
Definition: std_expr.h:4402
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
instructionst::iterator targett
Definition: goto_program.h:414
void complete_goto(targett _target)
Definition: goto_program.h:280
void make_location(const source_locationt &l)
Definition: goto_program.h:248
std::string as_string(const namespacet &ns, const goto_programt::instructiont &)
void make_other(const codet &_code)
Definition: goto_program.h:255
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:415
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition: goto_program.h:715
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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:693
static irep_idt loop_id(const instructiont &instruction)
Human-readable loop name.
Definition: goto_program.h:619
#define PRECONDITION(CONDITION)
Definition: invariant.h:427
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:31
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:518
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:532
void insert_before_swap(targett target, goto_programt &p)
Insertion that preserves jumps to "target".
Definition: goto_program.h:494
Functor to check whether iterators from different collections point at the same object.
Definition: goto_program.h:795
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Author: Diffblue Ltd.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
void compute_location_numbers()
Compute location numbers.
Definition: goto_program.h:606
bool order_const_target(const goto_programt::const_targett i1, const goto_programt::const_targett i2)
Definition: goto_program.h:773
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:641
void insert_before_swap(targett target, instructiont &instruction)
Insertion that preserves jumps to "target".
Definition: goto_program.h:486
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
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:199
std::list< irep_idt > labelst
Goto target labels.
Definition: goto_program.h:227
void update_instructions_function(const irep_idt &function_id)
Sets the function member of each instruction if not yet set Note that a goto program need not be a go...
Definition: goto_program.h:594
void make_decl(const codet &_code)
Definition: goto_program.h:293
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:187
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
Base class for all expressions.
Definition: expr.h:54
goto_programt()
Constructor.
Definition: goto_program.h:632
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:654
void make_goto(targett _target, const exprt &g)
Definition: goto_program.h:274
bool empty() const
Is the program empty?
Definition: goto_program.h:626
void compute_target_numbers()
Compute the target numbers.
void swap(instructiont &instruction)
Swap two instructions.
Definition: goto_program.h:344
std::list< const_targett > const_targetst
Definition: goto_program.h:200
void clear(goto_program_instruction_typet _type)
Clear the node.
Definition: goto_program.h:238
static const irep_idt get_function_id(const_targett l)
Get the id of the function that contains the instruction pointed-to by the given instruction iterator...
Definition: goto_program.h:440
void make_nil()
Definition: irep.h:315
void make_incomplete_goto(const code_gotot &_code)
Definition: goto_program.h:262
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
Definition: goto_program.h:197
void make_assertion(const exprt &g)
Definition: goto_program.h:252
validation_modet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
void set_target(targett t)
Sets the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:215
#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:474
goto_programt & operator=(const goto_programt &)=delete
instructiont(goto_program_instruction_typet _type)
Definition: goto_program.h:333
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:234
void make_goto(targett _target)
Definition: goto_program.h:268
std::ostream & output(std::ostream &out) const
Output goto-program to given stream.
Definition: goto_program.h:562