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