cprover
goto_program.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_program.h"
13 
14 #include <ostream>
15 #include <iomanip>
16 
17 #include <util/std_expr.h>
18 #include <util/validate.h>
19 
20 #include <langapi/language_util.h>
21 
36  const namespacet &ns,
37  const irep_idt &identifier,
38  std::ostream &out,
39  const instructiont &instruction) const
40 {
41  out << " // " << instruction.location_number << " ";
42 
43  if(!instruction.source_location.is_nil())
44  out << instruction.source_location.as_string();
45  else
46  out << "no location";
47 
48  out << "\n";
49 
50  if(!instruction.labels.empty())
51  {
52  out << " // Labels:";
53  for(const auto &label : instruction.labels)
54  out << " " << label;
55 
56  out << '\n';
57  }
58 
59  if(instruction.is_target())
60  out << std::setw(6) << instruction.target_number << ": ";
61  else
62  out << " ";
63 
64  switch(instruction.type)
65  {
67  out << "NO INSTRUCTION TYPE SET" << '\n';
68  break;
69 
70  case GOTO:
71  if(!instruction.guard.is_true())
72  {
73  out << "IF "
74  << from_expr(ns, identifier, instruction.guard)
75  << " THEN ";
76  }
77 
78  out << "GOTO ";
79 
80  for(instructiont::targetst::const_iterator
81  gt_it=instruction.targets.begin();
82  gt_it!=instruction.targets.end();
83  gt_it++)
84  {
85  if(gt_it!=instruction.targets.begin())
86  out << ", ";
87  out << (*gt_it)->target_number;
88  }
89 
90  out << '\n';
91  break;
92 
93  case RETURN:
94  case OTHER:
95  case DECL:
96  case DEAD:
97  case FUNCTION_CALL:
98  case ASSIGN:
99  out << from_expr(ns, identifier, instruction.code) << '\n';
100  break;
101 
102  case ASSUME:
103  case ASSERT:
104  if(instruction.is_assume())
105  out << "ASSUME ";
106  else
107  out << "ASSERT ";
108 
109  {
110  out << from_expr(ns, identifier, instruction.guard);
111 
112  const irep_idt &comment=instruction.source_location.get_comment();
113  if(comment!="")
114  out << " // " << comment;
115  }
116 
117  out << '\n';
118  break;
119 
120  case SKIP:
121  out << "SKIP" << '\n';
122  break;
123 
124  case END_FUNCTION:
125  out << "END_FUNCTION" << '\n';
126  break;
127 
128  case LOCATION:
129  out << "LOCATION" << '\n';
130  break;
131 
132  case THROW:
133  out << "THROW";
134 
135  {
136  const irept::subt &exception_list=
137  instruction.code.find(ID_exception_list).get_sub();
138 
139  for(const auto &ex : exception_list)
140  out << " " << ex.id();
141  }
142 
143  if(instruction.code.operands().size()==1)
144  out << ": " << from_expr(ns, identifier, instruction.code.op0());
145 
146  out << '\n';
147  break;
148 
149  case CATCH:
150  {
151  if(instruction.code.get_statement()==ID_exception_landingpad)
152  {
153  const auto &landingpad=to_code_landingpad(instruction.code);
154  out << "EXCEPTION LANDING PAD ("
155  << from_type(ns, identifier, landingpad.catch_expr().type())
156  << ' '
157  << from_expr(ns, identifier, landingpad.catch_expr())
158  << ")";
159  }
160  else if(instruction.code.get_statement()==ID_push_catch)
161  {
162  out << "CATCH-PUSH ";
163 
164  unsigned i=0;
165  const irept::subt &exception_list=
166  instruction.code.find(ID_exception_list).get_sub();
168  instruction.targets.size() == exception_list.size(),
169  "unexpected discrepancy between sizes of instruction"
170  "targets and exception list");
171  for(instructiont::targetst::const_iterator
172  gt_it=instruction.targets.begin();
173  gt_it!=instruction.targets.end();
174  gt_it++, i++)
175  {
176  if(gt_it!=instruction.targets.begin())
177  out << ", ";
178  out << exception_list[i].id() << "->"
179  << (*gt_it)->target_number;
180  }
181  }
182  else if(instruction.code.get_statement()==ID_pop_catch)
183  {
184  out << "CATCH-POP";
185  }
186  else
187  {
188  UNREACHABLE;
189  }
190 
191  out << '\n';
192  break;
193  }
194 
195  case ATOMIC_BEGIN:
196  out << "ATOMIC_BEGIN" << '\n';
197  break;
198 
199  case ATOMIC_END:
200  out << "ATOMIC_END" << '\n';
201  break;
202 
203  case START_THREAD:
204  out << "START THREAD "
205  << instruction.get_target()->target_number
206  << '\n';
207  break;
208 
209  case END_THREAD:
210  out << "END THREAD" << '\n';
211  break;
212 
213  default:
214  UNREACHABLE;
215  }
216 
217  return out;
218 }
219 
221  decl_identifierst &decl_identifiers) const
222 {
224  {
225  if(it->is_decl())
226  {
228  it->code.get_statement() == ID_decl,
229  "expected statement to be declaration statement");
231  it->code.operands().size() == 1,
232  "declaration statement expects one operand");
233  const symbol_exprt &symbol_expr=to_symbol_expr(it->code.op0());
234  decl_identifiers.insert(symbol_expr.get_identifier());
235  }
236  }
237 }
238 
239 void parse_lhs_read(const exprt &src, std::list<exprt> &dest)
240 {
241  if(src.id()==ID_dereference)
242  {
243  dest.push_back(to_dereference_expr(src).pointer());
244  }
245  else if(src.id()==ID_index)
246  {
247  auto &index_expr = to_index_expr(src);
248  dest.push_back(index_expr.index());
249  parse_lhs_read(index_expr.array(), dest);
250  }
251  else if(src.id()==ID_member)
252  {
253  parse_lhs_read(to_member_expr(src).compound(), dest);
254  }
255  else if(src.id()==ID_if)
256  {
257  auto &if_expr = to_if_expr(src);
258  dest.push_back(if_expr.cond());
259  parse_lhs_read(if_expr.true_case(), dest);
260  parse_lhs_read(if_expr.false_case(), dest);
261  }
262 }
263 
264 std::list<exprt> expressions_read(
265  const goto_programt::instructiont &instruction)
266 {
267  std::list<exprt> dest;
268 
269  switch(instruction.type)
270  {
271  case ASSUME:
272  case ASSERT:
273  case GOTO:
274  dest.push_back(instruction.guard);
275  break;
276 
277  case RETURN:
278  if(to_code_return(instruction.code).return_value().is_not_nil())
279  dest.push_back(to_code_return(instruction.code).return_value());
280  break;
281 
282  case FUNCTION_CALL:
283  {
284  const code_function_callt &function_call=
285  to_code_function_call(instruction.code);
286  forall_expr(it, function_call.arguments())
287  dest.push_back(*it);
288  if(function_call.lhs().is_not_nil())
289  parse_lhs_read(function_call.lhs(), dest);
290  }
291  break;
292 
293  case ASSIGN:
294  {
295  const code_assignt &assignment=to_code_assign(instruction.code);
296  dest.push_back(assignment.rhs());
297  parse_lhs_read(assignment.lhs(), dest);
298  }
299  break;
300 
301  default:
302  {
303  }
304  }
305 
306  return dest;
307 }
308 
309 std::list<exprt> expressions_written(
310  const goto_programt::instructiont &instruction)
311 {
312  std::list<exprt> dest;
313 
314  switch(instruction.type)
315  {
316  case FUNCTION_CALL:
317  {
318  const code_function_callt &function_call=
319  to_code_function_call(instruction.code);
320  if(function_call.lhs().is_not_nil())
321  dest.push_back(function_call.lhs());
322  }
323  break;
324 
325  case ASSIGN:
326  dest.push_back(to_code_assign(instruction.code).lhs());
327  break;
328 
329  default:
330  {
331  }
332  }
333 
334  return dest;
335 }
336 
338  const exprt &src,
339  std::list<exprt> &dest)
340 {
341  if(src.id()==ID_symbol)
342  dest.push_back(src);
343  else if(src.id()==ID_address_of)
344  {
345  // don't traverse!
346  }
347  else if(src.id()==ID_dereference)
348  {
349  // this reads what is pointed to plus the pointer
350  auto &deref = to_dereference_expr(src);
351  dest.push_back(deref);
352  objects_read(deref.pointer(), dest);
353  }
354  else
355  {
356  forall_operands(it, src)
357  objects_read(*it, dest);
358  }
359 }
360 
361 std::list<exprt> objects_read(
362  const goto_programt::instructiont &instruction)
363 {
364  std::list<exprt> expressions=expressions_read(instruction);
365 
366  std::list<exprt> dest;
367 
368  for(const auto &expr : expressions)
369  objects_read(expr, dest);
370 
371  return dest;
372 }
373 
375  const exprt &src,
376  std::list<exprt> &dest)
377 {
378  if(src.id()==ID_if)
379  {
380  auto &if_expr = to_if_expr(src);
381  objects_written(if_expr.true_case(), dest);
382  objects_written(if_expr.false_case(), dest);
383  }
384  else
385  dest.push_back(src);
386 }
387 
388 std::list<exprt> objects_written(
389  const goto_programt::instructiont &instruction)
390 {
391  std::list<exprt> expressions=expressions_written(instruction);
392 
393  std::list<exprt> dest;
394 
395  for(const auto &expr : expressions)
396  objects_written(expr, dest);
397 
398  return dest;
399 }
400 
401 std::string as_string(
402  const class namespacet &ns,
404 {
405  std::string result;
406 
407  switch(i.type)
408  {
409  case NO_INSTRUCTION_TYPE:
410  return "(NO INSTRUCTION TYPE)";
411 
412  case GOTO:
413  if(!i.guard.is_true())
414  {
415  result+="IF "
416  +from_expr(ns, i.function, i.guard)
417  +" THEN ";
418  }
419 
420  result+="GOTO ";
421 
422  for(goto_programt::instructiont::targetst::const_iterator
423  gt_it=i.targets.begin();
424  gt_it!=i.targets.end();
425  gt_it++)
426  {
427  if(gt_it!=i.targets.begin())
428  result+=", ";
429  result+=std::to_string((*gt_it)->target_number);
430  }
431  return result;
432 
433  case RETURN:
434  case OTHER:
435  case DECL:
436  case DEAD:
437  case FUNCTION_CALL:
438  case ASSIGN:
439  return from_expr(ns, i.function, i.code);
440 
441  case ASSUME:
442  case ASSERT:
443  if(i.is_assume())
444  result+="ASSUME ";
445  else
446  result+="ASSERT ";
447 
448  result+=from_expr(ns, i.function, i.guard);
449 
450  {
452  if(comment!="")
453  result+=" /* "+id2string(comment)+" */";
454  }
455  return result;
456 
457  case SKIP:
458  return "SKIP";
459 
460  case END_FUNCTION:
461  return "END_FUNCTION";
462 
463  case LOCATION:
464  return "LOCATION";
465 
466  case THROW:
467  return "THROW";
468 
469  case CATCH:
470  return "CATCH";
471 
472  case ATOMIC_BEGIN:
473  return "ATOMIC_BEGIN";
474 
475  case ATOMIC_END:
476  return "ATOMIC_END";
477 
478  case START_THREAD:
479  result+="START THREAD ";
480 
481  if(i.targets.size()==1)
482  result+=std::to_string(i.targets.front()->target_number);
483  return result;
484 
485  case END_THREAD:
486  return "END THREAD";
487 
488  default:
489  UNREACHABLE;
490  }
491 }
492 
497 {
498  unsigned nr=0;
499  for(auto &i : instructions)
500  if(i.is_backwards_goto())
501  i.loop_number=nr++;
502 }
503 
505 {
510 }
511 
512 std::ostream &goto_programt::output(
513  const namespacet &ns,
514  const irep_idt &identifier,
515  std::ostream &out) const
516 {
517  // output program
518 
519  for(const auto &instruction : instructions)
520  output_instruction(ns, identifier, out, instruction);
521 
522  return out;
523 }
524 
536 {
537  // reset marking
538 
539  for(auto &i : instructions)
540  i.target_number=instructiont::nil_target;
541 
542  // mark the goto targets
543 
544  for(const auto &i : instructions)
545  {
546  for(const auto &t : i.targets)
547  {
548  if(t!=instructions.end())
549  t->target_number=0;
550  }
551  }
552 
553  // number the targets properly
554  unsigned cnt=0;
555 
556  for(auto &i : instructions)
557  {
558  if(i.is_target())
559  {
560  i.target_number=++cnt;
562  i.target_number != 0, "GOTO instruction target cannot be zero");
563  }
564  }
565 
566  // check the targets!
567  // (this is a consistency check only)
568 
569  for(const auto &i : instructions)
570  {
571  for(const auto &t : i.targets)
572  {
573  if(t!=instructions.end())
574  {
576  t->target_number != 0, "instruction's number cannot be zero");
578  t->target_number != instructiont::nil_target,
579  "GOTO instruction target cannot be nil_target");
580  }
581  }
582  }
583 }
584 
590 {
591  // Definitions for mapping between the two programs
592  typedef std::map<const_targett, targett> targets_mappingt;
593  targets_mappingt targets_mapping;
594 
595  clear();
596 
597  // Loop over program - 1st time collects targets and copy
598 
599  for(instructionst::const_iterator
600  it=src.instructions.begin();
601  it!=src.instructions.end();
602  ++it)
603  {
604  auto new_instruction=add_instruction();
605  targets_mapping[it]=new_instruction;
606  *new_instruction=*it;
607  }
608 
609  // Loop over program - 2nd time updates targets
610 
611  for(auto &i : instructions)
612  {
613  for(auto &t : i.targets)
614  {
615  targets_mappingt::iterator
616  m_target_it=targets_mapping.find(t);
617 
618  CHECK_RETURN(m_target_it != targets_mapping.end());
619 
620  t=m_target_it->second;
621  }
622  }
623 
626 }
627 
631 {
632  for(const auto &i : instructions)
633  if(i.is_assert() && !i.guard.is_true())
634  return true;
635 
636  return false;
637 }
638 
641 {
642  for(auto &i : instructions)
643  {
644  i.incoming_edges.clear();
645  }
646 
647  for(instructionst::iterator
648  it=instructions.begin();
649  it!=instructions.end();
650  ++it)
651  {
652  for(const auto &s : get_successors(it))
653  {
654  if(s!=instructions.end())
655  s->incoming_edges.insert(it);
656  }
657  }
658 }
659 
661 {
662  // clang-format off
663  return
664  type == other.type &&
665  code == other.code &&
666  guard == other.guard &&
667  targets.size() == other.targets.size() &&
668  labels == other.labels;
669  // clang-format on
670 }
671 
673  const namespacet &ns,
674  const validation_modet vm) const
675 {
676  validate_full_code(code, ns, vm);
677  validate_full_expr(guard, ns, vm);
678 
679  switch(type)
680  {
681  case NO_INSTRUCTION_TYPE:
682  break;
683  case GOTO:
684  break;
685  case ASSUME:
686  break;
687  case ASSERT:
688  break;
689  case OTHER:
690  break;
691  case SKIP:
692  break;
693  case START_THREAD:
694  break;
695  case END_THREAD:
696  break;
697  case LOCATION:
698  break;
699  case END_FUNCTION:
700  break;
701  case ATOMIC_BEGIN:
702  break;
703  case ATOMIC_END:
704  break;
705  case RETURN:
706  break;
707  case ASSIGN:
708  DATA_CHECK(
709  code.get_statement() == ID_assign,
710  "assign instruction should contain an assign statement");
711  DATA_CHECK(targets.empty(), "assign instruction should not have a target");
712  break;
713  case DECL:
714  break;
715  case DEAD:
716  break;
717  case FUNCTION_CALL:
718  break;
719  case THROW:
720  break;
721  case CATCH:
722  break;
723  case INCOMPLETE_GOTO:
724  break;
725  }
726 }
727 
728 bool goto_programt::equals(const goto_programt &other) const
729 {
730  if(instructions.size() != other.instructions.size())
731  return false;
732 
733  goto_programt::const_targett other_it = other.instructions.begin();
734  for(const auto &ins : instructions)
735  {
736  if(!ins.equals(*other_it))
737  return false;
738 
739  // the number of targets is the same as instructiont::equals returned "true"
740  auto other_target_it = other_it->targets.begin();
741  for(const auto t : ins.targets)
742  {
743  if(
744  t->location_number - ins.location_number !=
745  (*other_target_it)->location_number - other_it->location_number)
746  {
747  return false;
748  }
749 
750  ++other_target_it;
751  }
752 
753  ++other_it;
754  }
755 
756  return true;
757 }
758 
760 std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t)
761 {
762  switch(t)
763  {
764  case NO_INSTRUCTION_TYPE:
765  out << "NO_INSTRUCTION_TYPE";
766  break;
767  case GOTO:
768  out << "GOTO";
769  break;
770  case ASSUME:
771  out << "ASSUME";
772  break;
773  case ASSERT:
774  out << "ASSERT";
775  break;
776  case OTHER:
777  out << "OTHER";
778  break;
779  case DECL:
780  out << "DECL";
781  break;
782  case DEAD:
783  out << "DEAD";
784  break;
785  case SKIP:
786  out << "SKIP";
787  break;
788  case START_THREAD:
789  out << "START_THREAD";
790  break;
791  case END_THREAD:
792  out << "END_THREAD";
793  break;
794  case LOCATION:
795  out << "LOCATION";
796  break;
797  case END_FUNCTION:
798  out << "END_FUNCTION";
799  break;
800  case ATOMIC_BEGIN:
801  out << "ATOMIC_BEGIN";
802  break;
803  case ATOMIC_END:
804  out << "ATOMIC_END";
805  break;
806  case RETURN:
807  out << "RETURN";
808  break;
809  case ASSIGN:
810  out << "ASSIGN";
811  break;
812  case FUNCTION_CALL:
813  out << "FUNCTION_CALL";
814  break;
815  default:
816  out << "?";
817  }
818 
819  return out;
820 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3449
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
const irep_idt & get_statement() const
Definition: std_code.h:56
irep_idt function
The function this instruction belongs to.
Definition: goto_program.h:184
void update()
Update all indices.
const exprt & return_value() const
Definition: std_code.h:1085
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
void compute_loop_numbers()
Compute loop numbers.
void validate(const namespacet &ns, const validation_modet vm) const
Check that the instruction is well-formed.
exprt & op0()
Definition: expr.h:84
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
std::vector< irept > subt
Definition: irep.h:160
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
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.
#define forall_expr(it, expr)
Definition: expr.h:31
std::string as_string() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool has_assertion() const
Does the goto program have an assertion?
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:122
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
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.
std::string as_string(const class namespacet &ns, const goto_programt::instructiont &i)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:459
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:207
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.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3364
subt & get_sub()
Definition: irep.h:317
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
unsigned target_number
A number to identify branch targets.
Definition: goto_program.h:376
std::list< exprt > expressions_read(const goto_programt::instructiont &instruction)
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...
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:335
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:680
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:271
argumentst & arguments()
Definition: std_code.h:1039
void compute_incoming_edges()
Compute for each instruction the set of instructions it is a successor of.
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
exprt & rhs()
Definition: std_code.h:276
void validate_full_code(const codet &code, const namespacet &ns, const validation_modet vm)
Check that the given code statement is well-formed (full check, including checks of all subexpression...
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
API to expression classes.
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_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:31
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3926
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1111
codet representation of a function call statement.
Definition: std_code.h:966
#define forall_operands(it, expr)
Definition: expr.h:20
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
void objects_read(const exprt &src, std::list< exprt > &dest)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
void compute_location_numbers()
Compute location numbers.
Definition: goto_program.h:606
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
std::list< exprt > expressions_written(const goto_programt::instructiont &instruction)
std::ostream & operator<<(std::ostream &out, goto_program_instruction_typet t)
Outputs a string representation of a goto_program_instruction_typet
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:1848
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
#define DATA_CHECK(condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs, expressions, instructions, etc.
Definition: validate.h:22
void parse_lhs_read(const exprt &src, std::list< exprt > &dest)
void compute_target_numbers()
Compute the target numbers.
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:467
void objects_written(const exprt &src, std::list< exprt > &dest)
validation_modet
Expression to hold a symbol (variable)
Definition: std_expr.h:143
const irep_idt & get_comment() const
#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
operandst & operands()
Definition: expr.h:78
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
bool is_target() const
Is this node a branch target?
Definition: goto_program.h:234
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1625
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
Concrete Goto Program.
A codet representing an assignment in the program.
Definition: std_code.h:258
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1058