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/expr_iterator.h>
18 #include <util/find_symbols.h>
19 #include <util/invariant.h>
20 #include <util/std_expr.h>
21 #include <util/validate.h>
22 
23 #include <langapi/language_util.h>
24 
39  const namespacet &ns,
40  const irep_idt &identifier,
41  std::ostream &out,
42  const instructiont &instruction) const
43 {
44  out << " // " << instruction.location_number << " ";
45 
46  if(!instruction.source_location.is_nil())
47  out << instruction.source_location.as_string();
48  else
49  out << "no location";
50 
51  out << "\n";
52 
53  if(!instruction.labels.empty())
54  {
55  out << " // Labels:";
56  for(const auto &label : instruction.labels)
57  out << " " << label;
58 
59  out << '\n';
60  }
61 
62  if(instruction.is_target())
63  out << std::setw(6) << instruction.target_number << ": ";
64  else
65  out << " ";
66 
67  switch(instruction.type)
68  {
70  out << "NO INSTRUCTION TYPE SET" << '\n';
71  break;
72 
73  case GOTO:
74  if(!instruction.guard.is_true())
75  {
76  out << "IF "
77  << from_expr(ns, identifier, instruction.guard)
78  << " THEN ";
79  }
80 
81  out << "GOTO ";
82 
83  for(instructiont::targetst::const_iterator
84  gt_it=instruction.targets.begin();
85  gt_it!=instruction.targets.end();
86  gt_it++)
87  {
88  if(gt_it!=instruction.targets.begin())
89  out << ", ";
90  out << (*gt_it)->target_number;
91  }
92 
93  out << '\n';
94  break;
95 
96  case RETURN:
97  case OTHER:
98  case DECL:
99  case DEAD:
100  case FUNCTION_CALL:
101  case ASSIGN:
102  out << from_expr(ns, identifier, instruction.code) << '\n';
103  break;
104 
105  case ASSUME:
106  case ASSERT:
107  if(instruction.is_assume())
108  out << "ASSUME ";
109  else
110  out << "ASSERT ";
111 
112  {
113  out << from_expr(ns, identifier, instruction.guard);
114 
115  const irep_idt &comment=instruction.source_location.get_comment();
116  if(comment!="")
117  out << " // " << comment;
118  }
119 
120  out << '\n';
121  break;
122 
123  case SKIP:
124  out << "SKIP" << '\n';
125  break;
126 
127  case END_FUNCTION:
128  out << "END_FUNCTION" << '\n';
129  break;
130 
131  case LOCATION:
132  out << "LOCATION" << '\n';
133  break;
134 
135  case THROW:
136  out << "THROW";
137 
138  {
139  const irept::subt &exception_list=
140  instruction.code.find(ID_exception_list).get_sub();
141 
142  for(const auto &ex : exception_list)
143  out << " " << ex.id();
144  }
145 
146  if(instruction.code.operands().size()==1)
147  out << ": " << from_expr(ns, identifier, instruction.code.op0());
148 
149  out << '\n';
150  break;
151 
152  case CATCH:
153  {
154  if(instruction.code.get_statement()==ID_exception_landingpad)
155  {
156  const auto &landingpad=to_code_landingpad(instruction.code);
157  out << "EXCEPTION LANDING PAD ("
158  << from_type(ns, identifier, landingpad.catch_expr().type())
159  << ' '
160  << from_expr(ns, identifier, landingpad.catch_expr())
161  << ")";
162  }
163  else if(instruction.code.get_statement()==ID_push_catch)
164  {
165  out << "CATCH-PUSH ";
166 
167  unsigned i=0;
168  const irept::subt &exception_list=
169  instruction.code.find(ID_exception_list).get_sub();
171  instruction.targets.size() == exception_list.size(),
172  "unexpected discrepancy between sizes of instruction"
173  "targets and exception list");
174  for(instructiont::targetst::const_iterator
175  gt_it=instruction.targets.begin();
176  gt_it!=instruction.targets.end();
177  gt_it++, i++)
178  {
179  if(gt_it!=instruction.targets.begin())
180  out << ", ";
181  out << exception_list[i].id() << "->"
182  << (*gt_it)->target_number;
183  }
184  }
185  else if(instruction.code.get_statement()==ID_pop_catch)
186  {
187  out << "CATCH-POP";
188  }
189  else
190  {
191  UNREACHABLE;
192  }
193 
194  out << '\n';
195  break;
196  }
197 
198  case ATOMIC_BEGIN:
199  out << "ATOMIC_BEGIN" << '\n';
200  break;
201 
202  case ATOMIC_END:
203  out << "ATOMIC_END" << '\n';
204  break;
205 
206  case START_THREAD:
207  out << "START THREAD "
208  << instruction.get_target()->target_number
209  << '\n';
210  break;
211 
212  case END_THREAD:
213  out << "END THREAD" << '\n';
214  break;
215 
216  default:
217  UNREACHABLE;
218  }
219 
220  return out;
221 }
222 
224  decl_identifierst &decl_identifiers) const
225 {
227  {
228  if(it->is_decl())
229  {
231  it->code.get_statement() == ID_decl,
232  "expected statement to be declaration statement");
234  it->code.operands().size() == 1,
235  "declaration statement expects one operand");
236  const symbol_exprt &symbol_expr=to_symbol_expr(it->code.op0());
237  decl_identifiers.insert(symbol_expr.get_identifier());
238  }
239  }
240 }
241 
242 void parse_lhs_read(const exprt &src, std::list<exprt> &dest)
243 {
244  if(src.id()==ID_dereference)
245  {
246  dest.push_back(to_dereference_expr(src).pointer());
247  }
248  else if(src.id()==ID_index)
249  {
250  auto &index_expr = to_index_expr(src);
251  dest.push_back(index_expr.index());
252  parse_lhs_read(index_expr.array(), dest);
253  }
254  else if(src.id()==ID_member)
255  {
256  parse_lhs_read(to_member_expr(src).compound(), dest);
257  }
258  else if(src.id()==ID_if)
259  {
260  auto &if_expr = to_if_expr(src);
261  dest.push_back(if_expr.cond());
262  parse_lhs_read(if_expr.true_case(), dest);
263  parse_lhs_read(if_expr.false_case(), dest);
264  }
265 }
266 
267 std::list<exprt> expressions_read(
268  const goto_programt::instructiont &instruction)
269 {
270  std::list<exprt> dest;
271 
272  switch(instruction.type)
273  {
274  case ASSUME:
275  case ASSERT:
276  case GOTO:
277  dest.push_back(instruction.guard);
278  break;
279 
280  case RETURN:
281  if(to_code_return(instruction.code).return_value().is_not_nil())
282  dest.push_back(to_code_return(instruction.code).return_value());
283  break;
284 
285  case FUNCTION_CALL:
286  {
287  const code_function_callt &function_call=
288  to_code_function_call(instruction.code);
289  forall_expr(it, function_call.arguments())
290  dest.push_back(*it);
291  if(function_call.lhs().is_not_nil())
292  parse_lhs_read(function_call.lhs(), dest);
293  }
294  break;
295 
296  case ASSIGN:
297  {
298  const code_assignt &assignment=to_code_assign(instruction.code);
299  dest.push_back(assignment.rhs());
300  parse_lhs_read(assignment.lhs(), dest);
301  }
302  break;
303 
304  default:
305  {
306  }
307  }
308 
309  return dest;
310 }
311 
312 std::list<exprt> expressions_written(
313  const goto_programt::instructiont &instruction)
314 {
315  std::list<exprt> dest;
316 
317  switch(instruction.type)
318  {
319  case FUNCTION_CALL:
320  {
321  const code_function_callt &function_call=
322  to_code_function_call(instruction.code);
323  if(function_call.lhs().is_not_nil())
324  dest.push_back(function_call.lhs());
325  }
326  break;
327 
328  case ASSIGN:
329  dest.push_back(to_code_assign(instruction.code).lhs());
330  break;
331 
332  default:
333  {
334  }
335  }
336 
337  return dest;
338 }
339 
341  const exprt &src,
342  std::list<exprt> &dest)
343 {
344  if(src.id()==ID_symbol)
345  dest.push_back(src);
346  else if(src.id()==ID_address_of)
347  {
348  // don't traverse!
349  }
350  else if(src.id()==ID_dereference)
351  {
352  // this reads what is pointed to plus the pointer
353  auto &deref = to_dereference_expr(src);
354  dest.push_back(deref);
355  objects_read(deref.pointer(), dest);
356  }
357  else
358  {
359  forall_operands(it, src)
360  objects_read(*it, dest);
361  }
362 }
363 
364 std::list<exprt> objects_read(
365  const goto_programt::instructiont &instruction)
366 {
367  std::list<exprt> expressions=expressions_read(instruction);
368 
369  std::list<exprt> dest;
370 
371  for(const auto &expr : expressions)
372  objects_read(expr, dest);
373 
374  return dest;
375 }
376 
378  const exprt &src,
379  std::list<exprt> &dest)
380 {
381  if(src.id()==ID_if)
382  {
383  auto &if_expr = to_if_expr(src);
384  objects_written(if_expr.true_case(), dest);
385  objects_written(if_expr.false_case(), dest);
386  }
387  else
388  dest.push_back(src);
389 }
390 
391 std::list<exprt> objects_written(
392  const goto_programt::instructiont &instruction)
393 {
394  std::list<exprt> expressions=expressions_written(instruction);
395 
396  std::list<exprt> dest;
397 
398  for(const auto &expr : expressions)
399  objects_written(expr, dest);
400 
401  return dest;
402 }
403 
404 std::string as_string(
405  const class namespacet &ns,
407 {
408  std::string result;
409 
410  switch(i.type)
411  {
412  case NO_INSTRUCTION_TYPE:
413  return "(NO INSTRUCTION TYPE)";
414 
415  case GOTO:
416  if(!i.guard.is_true())
417  {
418  result+="IF "
419  +from_expr(ns, i.function, i.guard)
420  +" THEN ";
421  }
422 
423  result+="GOTO ";
424 
425  for(goto_programt::instructiont::targetst::const_iterator
426  gt_it=i.targets.begin();
427  gt_it!=i.targets.end();
428  gt_it++)
429  {
430  if(gt_it!=i.targets.begin())
431  result+=", ";
432  result+=std::to_string((*gt_it)->target_number);
433  }
434  return result;
435 
436  case RETURN:
437  case OTHER:
438  case DECL:
439  case DEAD:
440  case FUNCTION_CALL:
441  case ASSIGN:
442  return from_expr(ns, i.function, i.code);
443 
444  case ASSUME:
445  case ASSERT:
446  if(i.is_assume())
447  result+="ASSUME ";
448  else
449  result+="ASSERT ";
450 
451  result+=from_expr(ns, i.function, i.guard);
452 
453  {
455  if(comment!="")
456  result+=" /* "+id2string(comment)+" */";
457  }
458  return result;
459 
460  case SKIP:
461  return "SKIP";
462 
463  case END_FUNCTION:
464  return "END_FUNCTION";
465 
466  case LOCATION:
467  return "LOCATION";
468 
469  case THROW:
470  return "THROW";
471 
472  case CATCH:
473  return "CATCH";
474 
475  case ATOMIC_BEGIN:
476  return "ATOMIC_BEGIN";
477 
478  case ATOMIC_END:
479  return "ATOMIC_END";
480 
481  case START_THREAD:
482  result+="START THREAD ";
483 
484  if(i.targets.size()==1)
485  result+=std::to_string(i.targets.front()->target_number);
486  return result;
487 
488  case END_THREAD:
489  return "END THREAD";
490 
491  default:
492  UNREACHABLE;
493  }
494 }
495 
500 {
501  unsigned nr=0;
502  for(auto &i : instructions)
503  if(i.is_backwards_goto())
504  i.loop_number=nr++;
505 }
506 
508 {
513 }
514 
515 std::ostream &goto_programt::output(
516  const namespacet &ns,
517  const irep_idt &identifier,
518  std::ostream &out) const
519 {
520  // output program
521 
522  for(const auto &instruction : instructions)
523  output_instruction(ns, identifier, out, instruction);
524 
525  return out;
526 }
527 
539 {
540  // reset marking
541 
542  for(auto &i : instructions)
543  i.target_number=instructiont::nil_target;
544 
545  // mark the goto targets
546 
547  for(const auto &i : instructions)
548  {
549  for(const auto &t : i.targets)
550  {
551  if(t!=instructions.end())
552  t->target_number=0;
553  }
554  }
555 
556  // number the targets properly
557  unsigned cnt=0;
558 
559  for(auto &i : instructions)
560  {
561  if(i.is_target())
562  {
563  i.target_number=++cnt;
565  i.target_number != 0, "GOTO instruction target cannot be zero");
566  }
567  }
568 
569  // check the targets!
570  // (this is a consistency check only)
571 
572  for(const auto &i : instructions)
573  {
574  for(const auto &t : i.targets)
575  {
576  if(t!=instructions.end())
577  {
579  t->target_number != 0, "instruction's number cannot be zero");
581  t->target_number != instructiont::nil_target,
582  "GOTO instruction target cannot be nil_target");
583  }
584  }
585  }
586 }
587 
593 {
594  // Definitions for mapping between the two programs
595  typedef std::map<const_targett, targett> targets_mappingt;
596  targets_mappingt targets_mapping;
597 
598  clear();
599 
600  // Loop over program - 1st time collects targets and copy
601 
602  for(instructionst::const_iterator
603  it=src.instructions.begin();
604  it!=src.instructions.end();
605  ++it)
606  {
607  auto new_instruction=add_instruction();
608  targets_mapping[it]=new_instruction;
609  *new_instruction=*it;
610  }
611 
612  // Loop over program - 2nd time updates targets
613 
614  for(auto &i : instructions)
615  {
616  for(auto &t : i.targets)
617  {
618  targets_mappingt::iterator
619  m_target_it=targets_mapping.find(t);
620 
621  CHECK_RETURN(m_target_it != targets_mapping.end());
622 
623  t=m_target_it->second;
624  }
625  }
626 
629 }
630 
634 {
635  for(const auto &i : instructions)
636  if(i.is_assert() && !i.guard.is_true())
637  return true;
638 
639  return false;
640 }
641 
644 {
645  for(auto &i : instructions)
646  {
647  i.incoming_edges.clear();
648  }
649 
650  for(instructionst::iterator
651  it=instructions.begin();
652  it!=instructions.end();
653  ++it)
654  {
655  for(const auto &s : get_successors(it))
656  {
657  if(s!=instructions.end())
658  s->incoming_edges.insert(it);
659  }
660  }
661 }
662 
664 {
665  // clang-format off
666  return
667  type == other.type &&
668  code == other.code &&
669  guard == other.guard &&
670  targets.size() == other.targets.size() &&
671  labels == other.labels;
672  // clang-format on
673 }
674 
676  const namespacet &ns,
677  const validation_modet vm) const
678 {
679  validate_full_code(code, ns, vm);
680  validate_full_expr(guard, ns, vm);
681 
682  const symbolt *table_symbol;
684  vm,
685  !ns.lookup(function, table_symbol),
686  id2string(function) + " not found",
687  source_location);
688 
689  auto expr_symbol_finder = [&](const exprt &e) {
690  find_symbols_sett typetags;
691  find_type_symbols(e.type(), typetags);
692  find_symbols(e, typetags);
693  const symbolt *symbol;
694  for(const auto &identifier : typetags)
695  {
697  vm,
698  !ns.lookup(identifier, symbol),
699  id2string(identifier) + " not found",
700  source_location);
701  }
702  };
703 
704  auto &current_source_location = source_location;
705  auto type_finder =
706  [&ns, vm, &table_symbol, &current_source_location](const exprt &e) {
707  if(e.id() == ID_symbol)
708  {
709  const auto &goto_symbol_expr = to_symbol_expr(e);
710  const auto &goto_id = goto_symbol_expr.get_identifier();
711 
712  if(!ns.lookup(goto_id, table_symbol))
714  vm,
715  base_type_eq(goto_symbol_expr.type(), table_symbol->type, ns),
716  id2string(goto_id) + " type inconsistency\n" +
717  "goto program type: " + goto_symbol_expr.type().id_string() +
718  "\n" + "symbol table type: " + table_symbol->type.id_string(),
719  current_source_location);
720  }
721  };
722 
723  switch(type)
724  {
725  case NO_INSTRUCTION_TYPE:
726  break;
727  case GOTO:
729  vm,
730  has_target(),
731  "goto instruction expects at least one target",
732  source_location);
733  // get_target checks that targets.size()==1
735  vm,
736  get_target()->is_target() && get_target()->target_number != 0,
737  "goto target has to be a target",
738  source_location);
739  break;
740  case ASSUME:
742  vm,
743  targets.empty(),
744  "assume instruction should not have a target",
745  source_location);
746  break;
747  case ASSERT:
749  vm,
750  targets.empty(),
751  "assert instruction should not have a target",
752  source_location);
753 
754  std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder);
755  std::for_each(guard.depth_begin(), guard.depth_end(), type_finder);
756  break;
757  case OTHER:
758  break;
759  case SKIP:
760  break;
761  case START_THREAD:
762  break;
763  case END_THREAD:
764  break;
765  case LOCATION:
766  break;
767  case END_FUNCTION:
768  break;
769  case ATOMIC_BEGIN:
770  break;
771  case ATOMIC_END:
772  break;
773  case RETURN:
775  vm,
776  code.get_statement() == ID_return,
777  "return instruction should contain a return statement",
778  source_location);
779  break;
780  case ASSIGN:
781  DATA_CHECK(
782  vm,
783  code.get_statement() == ID_assign,
784  "assign instruction should contain an assign statement");
785  DATA_CHECK(
786  vm, targets.empty(), "assign instruction should not have a target");
787  break;
788  case DECL:
790  vm,
791  code.get_statement() == ID_decl,
792  "declaration instructions should contain a declaration statement",
793  source_location);
795  vm,
796  !ns.lookup(to_code_decl(code).get_identifier(), table_symbol),
797  "declared symbols should be known",
798  id2string(to_code_decl(code).get_identifier()),
799  source_location);
800  break;
801  case DEAD:
803  vm,
804  code.get_statement() == ID_dead,
805  "dead instructions should contain a dead statement",
806  source_location);
808  vm,
809  !ns.lookup(to_code_dead(code).get_identifier(), table_symbol),
810  "removed symbols should be known",
811  id2string(to_code_dead(code).get_identifier()),
812  source_location);
813  break;
814  case FUNCTION_CALL:
816  vm,
817  code.get_statement() == ID_function_call,
818  "function call instruction should contain a call statement",
819  source_location);
820 
821  std::for_each(code.depth_begin(), code.depth_end(), expr_symbol_finder);
822  std::for_each(code.depth_begin(), code.depth_end(), type_finder);
823  break;
824  case THROW:
825  break;
826  case CATCH:
827  break;
828  case INCOMPLETE_GOTO:
829  break;
830  }
831 }
832 
833 bool goto_programt::equals(const goto_programt &other) const
834 {
835  if(instructions.size() != other.instructions.size())
836  return false;
837 
838  goto_programt::const_targett other_it = other.instructions.begin();
839  for(const auto &ins : instructions)
840  {
841  if(!ins.equals(*other_it))
842  return false;
843 
844  // the number of targets is the same as instructiont::equals returned "true"
845  auto other_target_it = other_it->targets.begin();
846  for(const auto t : ins.targets)
847  {
848  if(
849  t->location_number - ins.location_number !=
850  (*other_target_it)->location_number - other_it->location_number)
851  {
852  return false;
853  }
854 
855  ++other_target_it;
856  }
857 
858  ++other_it;
859  }
860 
861  return true;
862 }
863 
865 std::ostream &operator<<(std::ostream &out, goto_program_instruction_typet t)
866 {
867  switch(t)
868  {
869  case NO_INSTRUCTION_TYPE:
870  out << "NO_INSTRUCTION_TYPE";
871  break;
872  case GOTO:
873  out << "GOTO";
874  break;
875  case ASSUME:
876  out << "ASSUME";
877  break;
878  case ASSERT:
879  out << "ASSERT";
880  break;
881  case OTHER:
882  out << "OTHER";
883  break;
884  case DECL:
885  out << "DECL";
886  break;
887  case DEAD:
888  out << "DEAD";
889  break;
890  case SKIP:
891  out << "SKIP";
892  break;
893  case START_THREAD:
894  out << "START_THREAD";
895  break;
896  case END_THREAD:
897  out << "END_THREAD";
898  break;
899  case LOCATION:
900  out << "LOCATION";
901  break;
902  case END_FUNCTION:
903  out << "END_FUNCTION";
904  break;
905  case ATOMIC_BEGIN:
906  out << "ATOMIC_BEGIN";
907  break;
908  case ATOMIC_END:
909  out << "ATOMIC_END";
910  break;
911  case RETURN:
912  out << "RETURN";
913  break;
914  case ASSIGN:
915  out << "ASSIGN";
916  break;
917  case FUNCTION_CALL:
918  out << "FUNCTION_CALL";
919  break;
920  default:
921  out << "?";
922  }
923 
924  return out;
925 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3538
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:1205
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:399
bool is_nil() const
Definition: irep.h:169
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:170
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.
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:473
unsigned location_number
A globally unique number to identify a program location.
Definition: goto_program.h:369
std::vector< irept > subt
Definition: irep.h:157
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
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:318
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:90
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Symbol table entry.
Definition: symbol.h:27
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:470
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Definition: goto_program.h:207
Forward depth-first search iterators These iterators&#39; copy operations are expensive, so use auto&, and avoid std::next(), std::prev() and post-increment iterator.
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:3453
subt & get_sub()
Definition: irep.h:314
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:334
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:680
const irep_idt & id() const
Definition: irep.h:256
exprt & lhs()
Definition: std_code.h:269
argumentst & arguments()
Definition: std_code.h:1109
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:274
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:93
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:4014
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1238
codet representation of a function call statement.
Definition: std_code.h:1036
#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:262
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:1994
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
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:478
void objects_written(const exprt &src, std::list< exprt > &dest)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs, expressions, instructions, etc.
Definition: validate.h:22
validation_modet
Expression to hold a symbol (variable)
Definition: std_expr.h:154
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
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:485
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
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:1664
const irept & find(const irep_namet &name) const
Definition: irep.cpp:277
void find_symbols(const exprt &src, find_symbols_sett &dest)
Concrete Goto Program.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:165
A codet representing an assignment in the program.
Definition: std_code.h:256
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)
Definition: validate.h:37