cprover
goto_convert.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_convert.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/cprover_prefix.h>
17 #include <util/exception_utils.h>
18 #include <util/expr_util.h>
19 #include <util/fresh_symbol.h>
20 #include <util/pointer_expr.h>
21 #include <util/prefix.h>
22 #include <util/simplify_expr.h>
23 #include <util/std_expr.h>
24 #include <util/string_constant.h>
25 #include <util/symbol_table.h>
27 
28 #include "goto_convert_class.h"
29 #include "destructor.h"
30 #include "remove_skip.h"
31 
32 static bool is_empty(const goto_programt &goto_program)
33 {
34  forall_goto_program_instructions(it, goto_program)
35  if(!is_skip(goto_program, it))
36  return false;
37 
38  return true;
39 }
40 
44 {
45  std::map<irep_idt, goto_programt::targett> label_targets;
46 
47  // in the first pass collect the labels and the corresponding targets
49  {
50  if(!it->labels.empty())
51  {
52  for(auto label : it->labels)
53  // record the label and the corresponding target
54  label_targets.insert(std::make_pair(label, it));
55  }
56  }
57 
58  // in the second pass set the targets
59  for(auto &instruction : dest.instructions)
60  {
61  if(
62  instruction.is_catch() &&
63  instruction.get_code().get_statement() == ID_push_catch)
64  {
65  // Populate `targets` with a GOTO instruction target per
66  // exception handler if it isn't already populated.
67  // (Java handlers, for example, need this finish step; C++
68  // handlers will already be populated by now)
69 
70  if(instruction.targets.empty())
71  {
72  bool handler_added=true;
73  const code_push_catcht::exception_listt &handler_list =
74  to_code_push_catch(instruction.get_code()).exception_list();
75 
76  for(const auto &handler : handler_list)
77  {
78  // some handlers may not have been converted (if there was no
79  // exception to be caught); in such a situation we abort
80  if(label_targets.find(handler.get_label())==label_targets.end())
81  {
82  handler_added=false;
83  break;
84  }
85  }
86 
87  if(!handler_added)
88  continue;
89 
90  for(const auto &handler : handler_list)
91  instruction.targets.push_back(label_targets.at(handler.get_label()));
92  }
93  }
94  }
95 }
96 
97 /******************************************************************* \
98 
99 Function: goto_convertt::finish_gotos
100 
101  Inputs:
102 
103  Outputs:
104 
105  Purpose:
106 
107 \*******************************************************************/
108 
110 {
111  for(const auto &g_it : targets.gotos)
112  {
113  goto_programt::instructiont &i=*(g_it.first);
114 
115  if(i.is_start_thread())
116  {
117  const irep_idt &goto_label = i.get_code().get(ID_destination);
118 
119  labelst::const_iterator l_it=
120  targets.labels.find(goto_label);
121 
122  if(l_it == targets.labels.end())
123  {
125  "goto label \'" + id2string(goto_label) + "\' not found",
127  }
128 
129  i.targets.push_back(l_it->second.first);
130  }
131  else if(i.is_incomplete_goto())
132  {
133  const irep_idt &goto_label = i.get_code().get(ID_destination);
134 
135  labelst::const_iterator l_it=targets.labels.find(goto_label);
136 
137  if(l_it == targets.labels.end())
138  {
140  "goto label \'" + id2string(goto_label) + "\' not found",
142  }
143 
144  i.complete_goto(l_it->second.first);
145 
146  node_indext label_target = l_it->second.second;
147  node_indext goto_target = g_it.second;
148 
149  // Compare the currently-live variables on the path of the GOTO and label.
150  // We want to work out what variables should die during the jump.
151  ancestry_resultt intersection_result =
153  goto_target, label_target);
154 
155  bool not_prefix =
156  intersection_result.right_depth_below_common_ancestor != 0;
157 
158  // If our goto had no variables of note, just skip
159  if(goto_target != 0)
160  {
161  // If the goto recorded a destructor stack, execute as much as is
162  // appropriate for however many automatic variables leave scope.
163  // We don't currently handle variables *entering* scope, which
164  // is illegal for C++ non-pod types and impossible in Java in any case.
165  if(not_prefix)
166  {
168  debug() << "encountered goto '" << goto_label
169  << "' that enters one or more lexical blocks; "
170  << "omitting constructors and destructors" << eom;
171  }
172  else
173  {
175  debug() << "adding goto-destructor code on jump to '" << goto_label
176  << "'" << eom;
177 
178  node_indext end_destruct = intersection_result.common_ancestor;
179  goto_programt destructor_code;
181  i.source_location,
182  destructor_code,
183  mode,
184  end_destruct,
185  goto_target);
186  dest.destructive_insert(g_it.first, destructor_code);
187 
188  // This should leave iterators intact, as long as
189  // goto_programt::instructionst is std::list.
190  }
191  }
192  }
193  else
194  {
195  UNREACHABLE;
196  }
197  }
198 
199  targets.gotos.clear();
200 }
201 
203 {
204  for(auto &g_it : targets.computed_gotos)
205  {
207  dereference_exprt destination = to_dereference_expr(i.get_code().op0());
208  const exprt pointer = destination.pointer();
209 
210  // remember the expression for later checks
211  i.type=OTHER;
212  i.code_nonconst() = code_expressiont(pointer);
213 
214  // insert huge case-split
215  for(const auto &label : targets.labels)
216  {
217  exprt label_expr(ID_label, empty_typet());
218  label_expr.set(ID_identifier, label.first);
219 
220  const equal_exprt guard(pointer, address_of_exprt(label_expr));
221 
222  goto_program.insert_after(
223  g_it,
224  goto_programt::make_goto(label.second.first, guard, i.source_location));
225  }
226  }
227 
228  targets.computed_gotos.clear();
229 }
230 
235 {
236  // We cannot use a set of targets, as target iterators
237  // cannot be compared at this stage.
238 
239  // collect targets: reset marking
240  for(auto &i : dest.instructions)
241  i.target_number = goto_programt::instructiont::nil_target;
242 
243  // mark the goto targets
244  unsigned cnt = 0;
245  for(const auto &i : dest.instructions)
246  if(i.is_goto())
247  i.get_target()->target_number = (++cnt);
248 
249  for(auto it = dest.instructions.begin(); it != dest.instructions.end(); it++)
250  {
251  if(!it->is_goto())
252  continue;
253 
254  auto it_goto_y = std::next(it);
255 
256  if(
257  it_goto_y == dest.instructions.end() || !it_goto_y->is_goto() ||
258  !it_goto_y->get_condition().is_true() || it_goto_y->is_target())
259  {
260  continue;
261  }
262 
263  auto it_z = std::next(it_goto_y);
264 
265  if(it_z == dest.instructions.end())
266  continue;
267 
268  // cannot compare iterators, so compare target number instead
269  if(it->get_target()->target_number == it_z->target_number)
270  {
271  it->set_target(it_goto_y->get_target());
272  it->set_condition(boolean_negate(it->get_condition()));
273  it_goto_y->turn_into_skip();
274  }
275  }
276 }
277 
279  const codet &code,
280  goto_programt &dest,
281  const irep_idt &mode)
282 {
283  goto_convert_rec(code, dest, mode);
284 }
285 
287  const codet &code,
288  goto_programt &dest,
289  const irep_idt &mode)
290 {
291  convert(code, dest, mode);
292 
293  finish_gotos(dest, mode);
294  finish_computed_gotos(dest);
297 }
298 
300  const codet &code,
302  goto_programt &dest)
303 {
305  code, code.source_location(), type, nil_exprt(), {}));
306 }
307 
309  const code_labelt &code,
310  goto_programt &dest,
311  const irep_idt &mode)
312 {
313  // grab the label
314  const irep_idt &label=code.get_label();
315 
316  goto_programt tmp;
317 
318  // magic thread creation label.
319  // The "__CPROVER_ASYNC_" signals the start of a sequence of instructions
320  // that can be executed in parallel, i.e, a new thread.
321  if(has_prefix(id2string(label), CPROVER_PREFIX "ASYNC_"))
322  {
323  // the body of the thread is expected to be
324  // in the operand.
326  to_code_label(code).code().is_not_nil(),
327  "code() in magic thread creation label is null");
328 
329  // replace the magic thread creation label with a
330  // thread block (START_THREAD...END_THREAD).
331  code_blockt thread_body;
332  thread_body.add(to_code_label(code).code());
333  thread_body.add_source_location()=code.source_location();
334  generate_thread_block(thread_body, dest, mode);
335  }
336  else
337  {
338  convert(to_code_label(code).code(), tmp, mode);
339 
340  goto_programt::targett target=tmp.instructions.begin();
341  dest.destructive_append(tmp);
342 
343  targets.labels.insert(
344  {label, {target, targets.destructor_stack.get_current_node()}});
345  target->labels.push_front(label);
346  }
347 }
348 
350  const codet &,
351  goto_programt &)
352 {
353  // ignore for now
354 }
355 
357  const code_switch_caset &code,
358  goto_programt &dest,
359  const irep_idt &mode)
360 {
361  goto_programt tmp;
362  convert(code.code(), tmp, mode);
363 
364  goto_programt::targett target=tmp.instructions.begin();
365  dest.destructive_append(tmp);
366 
367  // is a default target given?
368 
369  if(code.is_default())
370  targets.set_default(target);
371  else
372  {
373  // cases?
374 
375  cases_mapt::iterator cases_entry=targets.cases_map.find(target);
376  if(cases_entry==targets.cases_map.end())
377  {
378  targets.cases.push_back(std::make_pair(target, caset()));
379  cases_entry=targets.cases_map.insert(std::make_pair(
380  target, --targets.cases.end())).first;
381  }
382 
383  exprt::operandst &case_op_dest=cases_entry->second->second;
384  case_op_dest.push_back(code.case_op());
385  }
386 }
387 
389  const code_gcc_switch_case_ranget &code,
390  goto_programt &dest,
391  const irep_idt &mode)
392 {
393  const auto lb = numeric_cast<mp_integer>(code.lower());
394  const auto ub = numeric_cast<mp_integer>(code.upper());
395 
397  lb.has_value() && ub.has_value(),
398  "GCC's switch-case-range statement requires constant bounds",
399  code.find_source_location());
400 
401  if(*lb > *ub)
402  {
404  warning() << "GCC's switch-case-range statement with empty case range"
405  << eom;
406  }
407 
408  goto_programt tmp;
409  convert(code.code(), tmp, mode);
410 
411  goto_programt::targett target = tmp.instructions.begin();
412  dest.destructive_append(tmp);
413 
414  cases_mapt::iterator cases_entry = targets.cases_map.find(target);
415  if(cases_entry == targets.cases_map.end())
416  {
417  targets.cases.push_back({target, caset()});
418  cases_entry =
419  targets.cases_map.insert({target, --targets.cases.end()}).first;
420  }
421 
422  // create a skeleton for case_guard
423  cases_entry->second->second.push_back(
425  binary_relation_exprt{nil_exprt{}, ID_le, code.upper()}});
426 }
427 
430  const codet &code,
431  goto_programt &dest,
432  const irep_idt &mode)
433 {
434  const irep_idt &statement=code.get_statement();
435 
436  if(statement==ID_block)
437  convert_block(to_code_block(code), dest, mode);
438  else if(statement==ID_decl)
439  convert_decl(to_code_decl(code), dest, mode);
440  else if(statement==ID_decl_type)
441  convert_decl_type(code, dest);
442  else if(statement==ID_expression)
443  convert_expression(to_code_expression(code), dest, mode);
444  else if(statement==ID_assign)
445  convert_assign(to_code_assign(code), dest, mode);
446  else if(statement==ID_assert)
447  convert_assert(to_code_assert(code), dest, mode);
448  else if(statement==ID_assume)
449  convert_assume(to_code_assume(code), dest, mode);
450  else if(statement==ID_function_call)
451  convert_function_call(to_code_function_call(code), dest, mode);
452  else if(statement==ID_label)
453  convert_label(to_code_label(code), dest, mode);
454  else if(statement==ID_gcc_local_label)
455  convert_gcc_local_label(code, dest);
456  else if(statement==ID_switch_case)
457  convert_switch_case(to_code_switch_case(code), dest, mode);
458  else if(statement==ID_gcc_switch_case_range)
460  to_code_gcc_switch_case_range(code), dest, mode);
461  else if(statement==ID_for)
462  convert_for(to_code_for(code), dest, mode);
463  else if(statement==ID_while)
464  convert_while(to_code_while(code), dest, mode);
465  else if(statement==ID_dowhile)
466  convert_dowhile(to_code_dowhile(code), dest, mode);
467  else if(statement==ID_switch)
468  convert_switch(to_code_switch(code), dest, mode);
469  else if(statement==ID_break)
470  convert_break(to_code_break(code), dest, mode);
471  else if(statement==ID_return)
472  convert_return(to_code_return(code), dest, mode);
473  else if(statement==ID_continue)
474  convert_continue(to_code_continue(code), dest, mode);
475  else if(statement==ID_goto)
476  convert_goto(to_code_goto(code), dest);
477  else if(statement==ID_gcc_computed_goto)
478  convert_gcc_computed_goto(code, dest);
479  else if(statement==ID_skip)
480  convert_skip(code, dest);
481  else if(statement==ID_ifthenelse)
482  convert_ifthenelse(to_code_ifthenelse(code), dest, mode);
483  else if(statement==ID_start_thread)
484  convert_start_thread(code, dest);
485  else if(statement==ID_end_thread)
486  convert_end_thread(code, dest);
487  else if(statement==ID_atomic_begin)
488  convert_atomic_begin(code, dest);
489  else if(statement==ID_atomic_end)
490  convert_atomic_end(code, dest);
491  else if(statement==ID_cpp_delete ||
492  statement=="cpp_delete[]")
493  convert_cpp_delete(code, dest);
494  else if(statement==ID_msc_try_except)
495  convert_msc_try_except(code, dest, mode);
496  else if(statement==ID_msc_try_finally)
497  convert_msc_try_finally(code, dest, mode);
498  else if(statement==ID_msc_leave)
499  convert_msc_leave(code, dest, mode);
500  else if(statement==ID_try_catch) // C++ try/catch
501  convert_try_catch(code, dest, mode);
502  else if(statement==ID_CPROVER_try_catch) // CPROVER-homemade
503  convert_CPROVER_try_catch(code, dest, mode);
504  else if(statement==ID_CPROVER_throw) // CPROVER-homemade
505  convert_CPROVER_throw(code, dest, mode);
506  else if(statement==ID_CPROVER_try_finally)
507  convert_CPROVER_try_finally(code, dest, mode);
508  else if(statement==ID_asm)
509  convert_asm(to_code_asm(code), dest);
510  else if(statement==ID_static_assert)
511  {
512  PRECONDITION(code.operands().size() == 2);
513  exprt assertion =
515  simplify(assertion, ns);
517  !assertion.is_false(),
518  "static assertion " + id2string(get_string_constant(code.op1())),
519  code.op0().find_source_location());
520  }
521  else if(statement==ID_dead)
522  copy(code, DEAD, dest);
523  else if(statement==ID_decl_block)
524  {
525  forall_operands(it, code)
526  convert(to_code(*it), dest, mode);
527  }
528  else if(statement==ID_push_catch ||
529  statement==ID_pop_catch ||
530  statement==ID_exception_landingpad)
531  copy(code, CATCH, dest);
532  else
533  copy(code, OTHER, dest);
534 
535  // make sure dest is never empty
536  if(dest.instructions.empty())
537  {
539  }
540 }
541 
543  const code_blockt &code,
544  goto_programt &dest,
545  const irep_idt &mode)
546 {
547  const source_locationt &end_location=code.end_location();
548 
549  // this saves the index of the destructor stack
550  node_indext old_stack_top =
552 
553  // now convert block
554  for(const auto &b_code : code.statements())
555  convert(b_code, dest, mode);
556 
557  // see if we need to do any destructors -- may have been processed
558  // in a prior break/continue/return already, don't create dead code
559  if(
560  !dest.empty() && dest.instructions.back().is_goto() &&
561  dest.instructions.back().get_condition().is_true())
562  {
563  // don't do destructors when we are unreachable
564  }
565  else
566  unwind_destructor_stack(end_location, dest, mode, old_stack_top);
567 
568  // Set the current node of our destructor stack back to before the block.
570 }
571 
573  const code_expressiont &code,
574  goto_programt &dest,
575  const irep_idt &mode)
576 {
577  exprt expr = code.expression();
578 
579  if(expr.id()==ID_if)
580  {
581  // We do a special treatment for c?t:f
582  // by compiling to if(c) t; else f;
583  const if_exprt &if_expr=to_if_expr(expr);
584  code_ifthenelset tmp_code(
585  if_expr.cond(),
586  code_expressiont(if_expr.true_case()),
587  code_expressiont(if_expr.false_case()));
588  tmp_code.add_source_location()=expr.source_location();
589  tmp_code.then_case().add_source_location()=expr.source_location();
590  tmp_code.else_case().add_source_location()=expr.source_location();
591  convert_ifthenelse(tmp_code, dest, mode);
592  }
593  else
594  {
595  clean_expr(expr, dest, mode, false); // result _not_ used
596 
597  // Any residual expression?
598  // We keep it to add checks later.
599  if(expr.is_not_nil())
600  {
601  codet tmp=code;
602  tmp.op0()=expr;
604  copy(tmp, OTHER, dest);
605  }
606  }
607 }
608 
610  const code_declt &code,
611  goto_programt &dest,
612  const irep_idt &mode)
613 {
614  const irep_idt &identifier = code.get_identifier();
615 
616  const symbolt &symbol = ns.lookup(identifier);
617 
618  if(symbol.is_static_lifetime ||
619  symbol.type.id()==ID_code)
620  return; // this is a SKIP!
621 
622  if(code.operands().size()==1)
623  {
624  copy(code, DECL, dest);
625  }
626  else
627  {
628  // this is expected to go away
629  exprt initializer;
630 
631  codet tmp=code;
632  initializer=code.op1();
633  tmp.operands().resize(1);
634 
635  // Break up into decl and assignment.
636  // Decl must be visible before initializer.
637  copy(tmp, DECL, dest);
638 
639  clean_expr(initializer, dest, mode);
640 
641  if(initializer.is_not_nil())
642  {
643  code_assignt assign(code.op0(), initializer);
644  assign.add_source_location() = tmp.source_location();
645 
646  convert_assign(assign, dest, mode);
647  }
648  }
649 
650  // now create a 'dead' instruction -- will be added after the
651  // destructor created below as unwind_destructor_stack pops off the
652  // top of the destructor stack
653  const symbol_exprt symbol_expr(symbol.name, symbol.type);
654 
655  {
656  code_deadt code_dead(symbol_expr);
657  targets.destructor_stack.add(code_dead);
658  }
659 
660  // do destructor
661  code_function_callt destructor=get_destructor(ns, symbol.type);
662 
663  if(destructor.is_not_nil())
664  {
665  // add "this"
666  address_of_exprt this_expr(symbol_expr, pointer_type(symbol.type));
667  destructor.arguments().push_back(this_expr);
668 
669  targets.destructor_stack.add(destructor);
670  }
671 }
672 
674  const codet &,
675  goto_programt &)
676 {
677  // we remove these
678 }
679 
681  const code_assignt &code,
682  goto_programt &dest,
683  const irep_idt &mode)
684 {
685  exprt lhs=code.lhs(),
686  rhs=code.rhs();
687 
688  clean_expr(lhs, dest, mode);
689 
690  if(rhs.id()==ID_side_effect &&
691  rhs.get(ID_statement)==ID_function_call)
692  {
693  const auto &rhs_function_call = to_side_effect_expr_function_call(rhs);
694 
696  rhs.operands().size() == 2,
697  "function_call sideeffect takes two operands",
698  rhs.find_source_location());
699 
700  Forall_operands(it, rhs)
701  clean_expr(*it, dest, mode);
702 
704  lhs,
705  rhs_function_call.function(),
706  rhs_function_call.arguments(),
707  dest,
708  mode);
709  }
710  else if(rhs.id()==ID_side_effect &&
711  (rhs.get(ID_statement)==ID_cpp_new ||
712  rhs.get(ID_statement)==ID_cpp_new_array))
713  {
714  Forall_operands(it, rhs)
715  clean_expr(*it, dest, mode);
716 
717  // TODO: This should be done in a separate pass
718  do_cpp_new(lhs, to_side_effect_expr(rhs), dest);
719  }
720  else if(
721  rhs.id() == ID_side_effect &&
722  (rhs.get(ID_statement) == ID_assign ||
723  rhs.get(ID_statement) == ID_postincrement ||
724  rhs.get(ID_statement) == ID_preincrement ||
725  rhs.get(ID_statement) == ID_statement_expression ||
726  rhs.get(ID_statement) == ID_gcc_conditional_expression))
727  {
728  // handle above side effects
729  clean_expr(rhs, dest, mode);
730 
731  code_assignt new_assign(code);
732  new_assign.lhs() = lhs;
733  new_assign.rhs() = rhs;
734 
735  copy(new_assign, ASSIGN, dest);
736  }
737  else if(rhs.id() == ID_side_effect)
738  {
739  // preserve side effects that will be handled at later stages,
740  // such as allocate, new operators of other languages, e.g. java, etc
741  Forall_operands(it, rhs)
742  clean_expr(*it, dest, mode);
743 
744  code_assignt new_assign(code);
745  new_assign.lhs()=lhs;
746  new_assign.rhs()=rhs;
747 
748  copy(new_assign, ASSIGN, dest);
749  }
750  else
751  {
752  // do everything else
753  clean_expr(rhs, dest, mode);
754 
755  code_assignt new_assign(code);
756  new_assign.lhs()=lhs;
757  new_assign.rhs()=rhs;
758 
759  copy(new_assign, ASSIGN, dest);
760  }
761 }
762 
764  const codet &code,
765  goto_programt &dest)
766 {
768  code.operands().size() == 1,
769  "cpp_delete statement takes one operand",
770  code.find_source_location());
771 
772  exprt tmp_op=code.op0();
773 
774  clean_expr(tmp_op, dest, ID_cpp);
775 
776  // we call the destructor, and then free
777  const exprt &destructor=
778  static_cast<const exprt &>(code.find(ID_destructor));
779 
780  irep_idt delete_identifier;
781 
782  if(code.get_statement()==ID_cpp_delete_array)
783  delete_identifier="__delete_array";
784  else if(code.get_statement()==ID_cpp_delete)
785  delete_identifier="__delete";
786  else
787  UNREACHABLE;
788 
789  if(destructor.is_not_nil())
790  {
791  if(code.get_statement()==ID_cpp_delete_array)
792  {
793  // build loop
794  }
795  else if(code.get_statement()==ID_cpp_delete)
796  {
797  // just one object
798  const dereference_exprt deref_op(tmp_op);
799 
800  codet tmp_code=to_code(destructor);
801  replace_new_object(deref_op, tmp_code);
802  convert(tmp_code, dest, ID_cpp);
803  }
804  else
805  UNREACHABLE;
806  }
807 
808  // now do "free"
809  exprt delete_symbol=ns.lookup(delete_identifier).symbol_expr();
810 
812  to_code_type(delete_symbol.type()).parameters().size() == 1,
813  "delete statement takes 1 parameter");
814 
815  typet arg_type=
816  to_code_type(delete_symbol.type()).parameters().front().type();
817 
818  code_function_callt delete_call(
819  delete_symbol, {typecast_exprt(tmp_op, arg_type)});
820  delete_call.add_source_location()=code.source_location();
821 
822  convert(delete_call, dest, ID_cpp);
823 }
824 
826  const code_assertt &code,
827  goto_programt &dest,
828  const irep_idt &mode)
829 {
830  exprt cond=code.assertion();
831 
832  clean_expr(cond, dest, mode);
833 
836  t->source_location.set(ID_property, ID_assertion);
837  t->source_location.set("user-provided", true);
838 }
839 
841  const codet &code,
842  goto_programt &dest)
843 {
845  code, code.source_location(), SKIP, nil_exprt(), {}));
846 }
847 
849  const code_assumet &code,
850  goto_programt &dest,
851  const irep_idt &mode)
852 {
853  exprt op=code.assumption();
854 
855  clean_expr(op, dest, mode);
856 
858 }
859 
861  const codet &code,
863  const irep_idt &mode)
864 {
865  exprt invariant =
866  static_cast<const exprt &>(code.find(ID_C_spec_loop_invariant));
867  exprt decreases_clause =
868  static_cast<const exprt &>(code.find(ID_C_spec_decreases));
869 
870  if(!invariant.is_nil())
871  {
872  if(has_subexpr(invariant, ID_side_effect))
873  {
875  "Loop invariant is not side-effect free.", code.find_source_location());
876  }
877 
878  PRECONDITION(loop->is_goto());
879  loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);
880  }
881 
882  if(!decreases_clause.is_nil())
883  {
884  if(has_subexpr(decreases_clause, ID_side_effect))
885  {
887  "Decreases clause is not side-effect free.",
888  code.find_source_location());
889  }
890 
891  PRECONDITION(loop->is_goto());
892  loop->guard.add(ID_C_spec_decreases).swap(decreases_clause);
893  }
894 }
895 
897  const code_fort &code,
898  goto_programt &dest,
899  const irep_idt &mode)
900 {
901  // turn for(A; c; B) { P } into
902  // A; while(c) { P; B; }
903  //-----------------------------
904  // A;
905  // u: sideeffects in c
906  // v: if(!c) goto z;
907  // w: P;
908  // x: B; <-- continue target
909  // y: goto u;
910  // z: ; <-- break target
911 
912  // A;
913  if(code.init().is_not_nil())
914  convert(to_code(code.init()), dest, mode);
915 
916  exprt cond=code.cond();
917 
918  goto_programt sideeffects;
919  clean_expr(cond, sideeffects, mode);
920 
921  // save break/continue targets
922  break_continue_targetst old_targets(targets);
923 
924  // do the u label
925  goto_programt::targett u=sideeffects.instructions.begin();
926 
927  // do the v label
928  goto_programt tmp_v;
930 
931  // do the z label
932  goto_programt tmp_z;
935 
936  // do the x label
937  goto_programt tmp_x;
938 
939  if(code.iter().is_nil())
940  {
942  }
943  else
944  {
945  exprt tmp_B=code.iter();
946 
947  clean_expr(tmp_B, tmp_x, mode, false);
948 
949  if(tmp_x.instructions.empty())
951  }
952 
953  // optimize the v label
954  if(sideeffects.instructions.empty())
955  u=v;
956 
957  // set the targets
958  targets.set_break(z);
959  targets.set_continue(tmp_x.instructions.begin());
960 
961  // v: if(!c) goto z;
962  *v =
964 
965  // do the w label
966  goto_programt tmp_w;
967  convert(code.body(), tmp_w, mode);
968 
969  // y: goto u;
970  goto_programt tmp_y;
971  goto_programt::targett y = tmp_y.add(
973 
974  // loop invariant and decreases clause
975  convert_loop_contracts(code, y, mode);
976 
977  dest.destructive_append(sideeffects);
978  dest.destructive_append(tmp_v);
979  dest.destructive_append(tmp_w);
980  dest.destructive_append(tmp_x);
981  dest.destructive_append(tmp_y);
982  dest.destructive_append(tmp_z);
983 
984  // restore break/continue
985  old_targets.restore(targets);
986 }
987 
989  const code_whilet &code,
990  goto_programt &dest,
991  const irep_idt &mode)
992 {
993  const exprt &cond=code.cond();
994  const source_locationt &source_location=code.source_location();
995 
996  // while(c) P;
997  //--------------------
998  // v: sideeffects in c
999  // if(!c) goto z;
1000  // x: P;
1001  // y: goto v; <-- continue target
1002  // z: ; <-- break target
1003 
1004  // save break/continue targets
1005  break_continue_targetst old_targets(targets);
1006 
1007  // do the z label
1008  goto_programt tmp_z;
1010  tmp_z.add(goto_programt::make_skip(source_location));
1011 
1012  goto_programt tmp_branch;
1014  boolean_negate(cond), z, source_location, tmp_branch, mode);
1015 
1016  // do the v label
1017  goto_programt::targett v=tmp_branch.instructions.begin();
1018 
1019  // y: goto v;
1020  goto_programt tmp_y;
1021  goto_programt::targett y = tmp_y.add(
1023 
1024  // set the targets
1025  targets.set_break(z);
1026  targets.set_continue(y);
1027 
1028  // do the x label
1029  goto_programt tmp_x;
1030  convert(code.body(), tmp_x, mode);
1031 
1032  // loop invariant and decreases clause
1033  convert_loop_contracts(code, y, mode);
1034 
1035  dest.destructive_append(tmp_branch);
1036  dest.destructive_append(tmp_x);
1037  dest.destructive_append(tmp_y);
1038  dest.destructive_append(tmp_z);
1039 
1040  // restore break/continue
1041  old_targets.restore(targets);
1042 }
1043 
1045  const code_dowhilet &code,
1046  goto_programt &dest,
1047  const irep_idt &mode)
1048 {
1050  code.operands().size() == 2,
1051  "dowhile takes two operands",
1052  code.find_source_location());
1053 
1054  // save source location
1055  source_locationt condition_location=code.cond().find_source_location();
1056 
1057  exprt cond=code.cond();
1058 
1059  goto_programt sideeffects;
1060  clean_expr(cond, sideeffects, mode);
1061 
1062  // do P while(c);
1063  //--------------------
1064  // w: P;
1065  // x: sideeffects in c <-- continue target
1066  // y: if(c) goto w;
1067  // z: ; <-- break target
1068 
1069  // save break/continue targets
1070  break_continue_targetst old_targets(targets);
1071 
1072  // do the y label
1073  goto_programt tmp_y;
1075  tmp_y.add(goto_programt::make_incomplete_goto(cond, condition_location));
1076 
1077  // do the z label
1078  goto_programt tmp_z;
1081 
1082  // do the x label
1084  if(sideeffects.instructions.empty())
1085  x=y;
1086  else
1087  x=sideeffects.instructions.begin();
1088 
1089  // set the targets
1090  targets.set_break(z);
1091  targets.set_continue(x);
1092 
1093  // do the w label
1094  goto_programt tmp_w;
1095  convert(code.body(), tmp_w, mode);
1096  goto_programt::targett w=tmp_w.instructions.begin();
1097 
1098  // y: if(c) goto w;
1099  y->complete_goto(w);
1100 
1101  // loop invariant and decreases clause
1102  convert_loop_contracts(code, y, mode);
1103 
1104  dest.destructive_append(tmp_w);
1105  dest.destructive_append(sideeffects);
1106  dest.destructive_append(tmp_y);
1107  dest.destructive_append(tmp_z);
1108 
1109  // restore break/continue targets
1110  old_targets.restore(targets);
1111 }
1112 
1114  const exprt &value,
1115  const exprt::operandst &case_op)
1116 {
1117  PRECONDITION(!case_op.empty());
1118 
1119  exprt::operandst disjuncts;
1120  disjuncts.reserve(case_op.size());
1121 
1122  for(const auto &op : case_op)
1123  {
1124  // could be a skeleton generated by convert_gcc_switch_case_range
1125  if(op.id() == ID_and)
1126  {
1127  const binary_exprt &and_expr = to_binary_expr(op);
1128  PRECONDITION(to_binary_expr(and_expr.op0()).op1().is_nil());
1129  PRECONDITION(to_binary_expr(and_expr.op1()).op0().is_nil());
1130  binary_exprt skeleton = and_expr;
1131  to_binary_expr(skeleton.op0()).op1() = value;
1132  to_binary_expr(skeleton.op1()).op0() = value;
1133  disjuncts.push_back(skeleton);
1134  }
1135  else
1136  disjuncts.push_back(equal_exprt(value, op));
1137  }
1138 
1139  return disjunction(disjuncts);
1140 }
1141 
1143  const code_switcht &code,
1144  goto_programt &dest,
1145  const irep_idt &mode)
1146 {
1147  // switch(v) {
1148  // case x: Px;
1149  // case y: Py;
1150  // ...
1151  // default: Pd;
1152  // }
1153  // --------------------
1154  // location
1155  // x: if(v==x) goto X;
1156  // y: if(v==y) goto Y;
1157  // goto d;
1158  // X: Px;
1159  // Y: Py;
1160  // d: Pd;
1161  // z: ;
1162 
1163  // we first add a 'location' node for the switch statement,
1164  // which would otherwise not be recorded
1166 
1167  // get the location of the end of the body, but
1168  // default to location of switch, if none
1169  source_locationt body_end_location=
1170  code.body().get_statement()==ID_block?
1171  to_code_block(code.body()).end_location():
1172  code.source_location();
1173 
1174  // do the value we switch over
1175  exprt argument=code.value();
1176 
1177  goto_programt sideeffects;
1178  clean_expr(argument, sideeffects, mode);
1179 
1180  // save break/default/cases targets
1181  break_switch_targetst old_targets(targets);
1182 
1183  // do the z label
1184  goto_programt tmp_z;
1186  tmp_z.add(goto_programt::make_skip(body_end_location));
1187 
1188  // set the new targets -- continue stays as is
1189  targets.set_break(z);
1190  targets.set_default(z);
1191  targets.cases.clear();
1192  targets.cases_map.clear();
1193 
1194  goto_programt tmp;
1195  convert(code.body(), tmp, mode);
1196 
1197  goto_programt tmp_cases;
1198 
1199  // The case number represents which case this corresponds to in the sequence
1200  // of case statements.
1201  //
1202  // switch (x)
1203  // {
1204  // case 2: // case_number 1
1205  // ...;
1206  // case 3: // case_number 2
1207  // ...;
1208  // case 10: // case_number 3
1209  // ...;
1210  // }
1211  size_t case_number=1;
1212  for(auto &case_pair : targets.cases)
1213  {
1214  const caset &case_ops=case_pair.second;
1215 
1216  if (case_ops.empty())
1217  continue;
1218 
1219  exprt guard_expr=case_guard(argument, case_ops);
1220 
1221  source_locationt source_location=case_ops.front().find_source_location();
1222  source_location.set_case_number(std::to_string(case_number));
1223  case_number++;
1224  guard_expr.add_source_location()=source_location;
1225 
1226  tmp_cases.add(goto_programt::make_goto(
1227  case_pair.first, std::move(guard_expr), source_location));
1228  }
1229 
1230  tmp_cases.add(goto_programt::make_goto(
1231  targets.default_target, targets.default_target->source_location));
1232 
1233  dest.destructive_append(sideeffects);
1234  dest.destructive_append(tmp_cases);
1235  dest.destructive_append(tmp);
1236  dest.destructive_append(tmp_z);
1237 
1238  // restore old targets
1239  old_targets.restore(targets);
1240 }
1241 
1243  const code_breakt &code,
1244  goto_programt &dest,
1245  const irep_idt &mode)
1246 {
1248  targets.break_set, "break without target", code.find_source_location());
1249 
1250  // need to process destructor stack
1252  code.source_location(), dest, mode, targets.break_stack_node);
1253 
1254  // add goto
1255  dest.add(
1257 }
1258 
1260  const code_returnt &code,
1261  goto_programt &dest,
1262  const irep_idt &mode)
1263 {
1264  if(!targets.return_set)
1265  {
1267  "return without target", code.find_source_location());
1268  }
1269 
1271  code.operands().empty() || code.operands().size() == 1,
1272  "return takes none or one operand",
1273  code.find_source_location());
1274 
1275  code_returnt new_code(code);
1276 
1277  if(new_code.has_return_value())
1278  {
1279  bool result_is_used=
1280  new_code.return_value().type().id()!=ID_empty;
1281 
1282  goto_programt sideeffects;
1283  clean_expr(new_code.return_value(), sideeffects, mode, result_is_used);
1284  dest.destructive_append(sideeffects);
1285 
1286  // remove void-typed return value
1287  if(!result_is_used)
1288  new_code.return_value().make_nil();
1289  }
1290 
1292  {
1294  new_code.has_return_value(),
1295  "function must return value",
1296  new_code.find_source_location());
1297 
1298  // Now add a return node to set the return value.
1299  dest.add(goto_programt::make_return(new_code, new_code.source_location()));
1300  }
1301  else
1302  {
1304  !new_code.has_return_value() ||
1305  new_code.return_value().type().id() == ID_empty,
1306  "function must not return value",
1307  code.find_source_location());
1308  }
1309 
1310  // Need to process _entire_ destructor stack.
1311  unwind_destructor_stack(code.source_location(), dest, mode);
1312 
1313  // add goto to end-of-function
1315  targets.return_target, new_code.source_location()));
1316 }
1317 
1319  const code_continuet &code,
1320  goto_programt &dest,
1321  const irep_idt &mode)
1322 {
1325  "continue without target",
1326  code.find_source_location());
1327 
1328  // need to process destructor stack
1330  code.source_location(), dest, mode, targets.continue_stack_node);
1331 
1332  // add goto
1333  dest.add(
1335 }
1336 
1338 {
1339  // this instruction will be completed during post-processing
1342 
1343  // remember it to do the target later
1345 }
1346 
1348  const codet &code,
1349  goto_programt &dest)
1350 {
1351  // this instruction will turn into OTHER during post-processing
1353  code, code.source_location(), NO_INSTRUCTION_TYPE, nil_exprt(), {}));
1354 
1355  // remember it to do this later
1356  targets.computed_gotos.push_back(t);
1357 }
1358 
1360  const codet &code,
1361  goto_programt &dest)
1362 {
1364  code, code.source_location(), START_THREAD, nil_exprt(), {}));
1365 
1366  // remember it to do target later
1367  targets.gotos.emplace_back(
1368  start_thread, targets.destructor_stack.get_current_node());
1369 }
1370 
1372  const codet &code,
1373  goto_programt &dest)
1374 {
1376  code.operands().empty(),
1377  "end_thread expects no operands",
1378  code.find_source_location());
1379 
1380  copy(code, END_THREAD, dest);
1381 }
1382 
1384  const codet &code,
1385  goto_programt &dest)
1386 {
1388  code.operands().empty(),
1389  "atomic_begin expects no operands",
1390  code.find_source_location());
1391 
1392  copy(code, ATOMIC_BEGIN, dest);
1393 }
1394 
1396  const codet &code,
1397  goto_programt &dest)
1398 {
1400  code.operands().empty(),
1401  ": atomic_end expects no operands",
1402  code.find_source_location());
1403 
1404  copy(code, ATOMIC_END, dest);
1405 }
1406 
1408  const code_ifthenelset &code,
1409  goto_programt &dest,
1410  const irep_idt &mode)
1411 {
1412  DATA_INVARIANT(code.then_case().is_not_nil(), "cannot accept an empty body");
1413 
1414  bool has_else=
1415  !code.else_case().is_nil();
1416 
1417  const source_locationt &source_location=code.source_location();
1418 
1419  // We do a bit of special treatment for && in the condition
1420  // in case cleaning would be needed otherwise.
1421  if(
1422  code.cond().id() == ID_and && code.cond().operands().size() == 2 &&
1423  (needs_cleaning(to_binary_expr(code.cond()).op0()) ||
1424  needs_cleaning(to_binary_expr(code.cond()).op1())) &&
1425  !has_else)
1426  {
1427  // if(a && b) XX --> if(a) if(b) XX
1428  code_ifthenelset new_if1(
1429  to_binary_expr(code.cond()).op1(), code.then_case());
1430  new_if1.add_source_location() = source_location;
1431  code_ifthenelset new_if0(
1432  to_binary_expr(code.cond()).op0(), std::move(new_if1));
1433  new_if0.add_source_location() = source_location;
1434  return convert_ifthenelse(new_if0, dest, mode);
1435  }
1436 
1437  // convert 'then'-branch
1438  goto_programt tmp_then;
1439  convert(code.then_case(), tmp_then, mode);
1440 
1441  goto_programt tmp_else;
1442 
1443  if(has_else)
1444  convert(code.else_case(), tmp_else, mode);
1445 
1446  exprt tmp_guard=code.cond();
1447  clean_expr(tmp_guard, dest, mode);
1448 
1450  tmp_guard, tmp_then, tmp_else, source_location, dest, mode);
1451 }
1452 
1454  const exprt &expr,
1455  const irep_idt &id,
1456  std::list<exprt> &dest)
1457 {
1458  if(expr.id()!=id)
1459  {
1460  dest.push_back(expr);
1461  }
1462  else
1463  {
1464  // left-to-right is important
1465  forall_operands(it, expr)
1466  collect_operands(*it, id, dest);
1467  }
1468 }
1469 
1473 static inline bool is_size_one(const goto_programt &g)
1474 {
1475  return (!g.instructions.empty()) &&
1476  ++g.instructions.begin()==g.instructions.end();
1477 }
1478 
1481  const exprt &guard,
1482  goto_programt &true_case,
1483  goto_programt &false_case,
1484  const source_locationt &source_location,
1485  goto_programt &dest,
1486  const irep_idt &mode)
1487 {
1488  if(is_empty(true_case) &&
1489  is_empty(false_case))
1490  {
1491  // hmpf. Useless branch.
1492  goto_programt tmp_z;
1494  dest.add(goto_programt::make_goto(z, guard, source_location));
1495  dest.destructive_append(tmp_z);
1496  return;
1497  }
1498 
1499  // do guarded assertions directly
1500  if(
1501  is_size_one(true_case) && true_case.instructions.back().is_assert() &&
1502  true_case.instructions.back().get_condition().is_false() &&
1503  true_case.instructions.back().labels.empty())
1504  {
1505  // The above conjunction deliberately excludes the instance
1506  // if(some) { label: assert(false); }
1507  true_case.instructions.back().set_condition(boolean_negate(guard));
1508  dest.destructive_append(true_case);
1509  true_case.instructions.clear();
1510  if(
1511  is_empty(false_case) ||
1512  (is_size_one(false_case) &&
1513  is_skip(false_case, false_case.instructions.begin())))
1514  return;
1515  }
1516 
1517  // similarly, do guarded assertions directly
1518  if(
1519  is_size_one(false_case) && false_case.instructions.back().is_assert() &&
1520  false_case.instructions.back().get_condition().is_false() &&
1521  false_case.instructions.back().labels.empty())
1522  {
1523  // The above conjunction deliberately excludes the instance
1524  // if(some) ... else { label: assert(false); }
1525  false_case.instructions.back().set_condition(guard);
1526  dest.destructive_append(false_case);
1527  false_case.instructions.clear();
1528  if(
1529  is_empty(true_case) ||
1530  (is_size_one(true_case) &&
1531  is_skip(true_case, true_case.instructions.begin())))
1532  return;
1533  }
1534 
1535  // a special case for C libraries that use
1536  // (void)((cond) || (assert(0),0))
1537  if(
1538  is_empty(false_case) && true_case.instructions.size() == 2 &&
1539  true_case.instructions.front().is_assert() &&
1540  true_case.instructions.front().get_condition().is_false() &&
1541  true_case.instructions.front().labels.empty() &&
1542  true_case.instructions.back().labels.empty())
1543  {
1544  true_case.instructions.front().set_condition(boolean_negate(guard));
1545  true_case.instructions.erase(--true_case.instructions.end());
1546  dest.destructive_append(true_case);
1547  true_case.instructions.clear();
1548 
1549  return;
1550  }
1551 
1552  // Flip around if no 'true' case code.
1553  if(is_empty(true_case))
1554  return generate_ifthenelse(
1555  boolean_negate(guard),
1556  false_case,
1557  true_case,
1558  source_location,
1559  dest,
1560  mode);
1561 
1562  bool has_else=!is_empty(false_case);
1563 
1564  // if(c) P;
1565  //--------------------
1566  // v: if(!c) goto z;
1567  // w: P;
1568  // z: ;
1569 
1570  // if(c) P; else Q;
1571  //--------------------
1572  // v: if(!c) goto y;
1573  // w: P;
1574  // x: goto z;
1575  // y: Q;
1576  // z: ;
1577 
1578  // do the x label
1579  goto_programt tmp_x;
1582 
1583  // do the z label
1584  goto_programt tmp_z;
1586  // We deliberately don't set a location for 'z', it's a dummy
1587  // target.
1588 
1589  // y: Q;
1590  goto_programt tmp_y;
1592  if(has_else)
1593  {
1594  tmp_y.swap(false_case);
1595  y=tmp_y.instructions.begin();
1596  }
1597 
1598  // v: if(!c) goto z/y;
1599  goto_programt tmp_v;
1601  boolean_negate(guard), has_else ? y : z, source_location, tmp_v, mode);
1602 
1603  // w: P;
1604  goto_programt tmp_w;
1605  tmp_w.swap(true_case);
1606 
1607  // x: goto z;
1608  CHECK_RETURN(!tmp_w.instructions.empty());
1609  x->complete_goto(z);
1610  x->source_location = tmp_w.instructions.back().source_location;
1611 
1612  dest.destructive_append(tmp_v);
1613  dest.destructive_append(tmp_w);
1614 
1615  if(has_else)
1616  {
1617  dest.destructive_append(tmp_x);
1618  dest.destructive_append(tmp_y);
1619  }
1620 
1621  dest.destructive_append(tmp_z);
1622 }
1623 
1625 static bool has_and_or(const exprt &expr)
1626 {
1627  forall_operands(it, expr)
1628  if(has_and_or(*it))
1629  return true;
1630 
1631  if(expr.id()==ID_and || expr.id()==ID_or)
1632  return true;
1633 
1634  return false;
1635 }
1636 
1638  const exprt &guard,
1639  goto_programt::targett target_true,
1640  const source_locationt &source_location,
1641  goto_programt &dest,
1642  const irep_idt &mode)
1643 {
1644  if(has_and_or(guard) && needs_cleaning(guard))
1645  {
1646  // if(guard) goto target;
1647  // becomes
1648  // if(guard) goto target; else goto next;
1649  // next: skip;
1650 
1651  goto_programt tmp;
1652  goto_programt::targett target_false =
1653  tmp.add(goto_programt::make_skip(source_location));
1654 
1656  guard, target_true, target_false, source_location, dest, mode);
1657 
1658  dest.destructive_append(tmp);
1659  }
1660  else
1661  {
1662  // simple branch
1663  exprt cond=guard;
1664  clean_expr(cond, dest, mode);
1665 
1666  dest.add(goto_programt::make_goto(target_true, cond, source_location));
1667  }
1668 }
1669 
1672  const exprt &guard,
1673  goto_programt::targett target_true,
1674  goto_programt::targett target_false,
1675  const source_locationt &source_location,
1676  goto_programt &dest,
1677  const irep_idt &mode)
1678 {
1679  if(guard.id()==ID_not)
1680  {
1681  // simply swap targets
1683  to_not_expr(guard).op(),
1684  target_false,
1685  target_true,
1686  source_location,
1687  dest,
1688  mode);
1689  return;
1690  }
1691 
1692  if(guard.id()==ID_and)
1693  {
1694  // turn
1695  // if(a && b) goto target_true; else goto target_false;
1696  // into
1697  // if(!a) goto target_false;
1698  // if(!b) goto target_false;
1699  // goto target_true;
1700 
1701  std::list<exprt> op;
1702  collect_operands(guard, guard.id(), op);
1703 
1704  for(const auto &expr : op)
1706  boolean_negate(expr), target_false, source_location, dest, mode);
1707 
1708  dest.add(goto_programt::make_goto(target_true, source_location));
1709 
1710  return;
1711  }
1712  else if(guard.id()==ID_or)
1713  {
1714  // turn
1715  // if(a || b) goto target_true; else goto target_false;
1716  // into
1717  // if(a) goto target_true;
1718  // if(b) goto target_true;
1719  // goto target_false;
1720 
1721  std::list<exprt> op;
1722  collect_operands(guard, guard.id(), op);
1723 
1724  // true branch(es)
1725  for(const auto &expr : op)
1727  expr, target_true, source_location, dest, mode);
1728 
1729  // false branch
1730  dest.add(goto_programt::make_goto(target_false, guard.source_location()));
1731 
1732  return;
1733  }
1734 
1735  exprt cond=guard;
1736  clean_expr(cond, dest, mode);
1737 
1738  // true branch
1739  dest.add(goto_programt::make_goto(target_true, cond, source_location));
1740 
1741  // false branch
1742  dest.add(goto_programt::make_goto(target_false, source_location));
1743 }
1744 
1746  const exprt &expr,
1747  irep_idt &value)
1748 {
1749  if(expr.id() == ID_typecast)
1750  return get_string_constant(to_typecast_expr(expr).op(), value);
1751 
1752  if(
1753  expr.id() == ID_address_of &&
1754  to_address_of_expr(expr).object().id() == ID_index)
1755  {
1756  exprt index_op =
1757  get_constant(to_index_expr(to_address_of_expr(expr).object()).array());
1758  simplify(index_op, ns);
1759 
1760  if(index_op.id()==ID_string_constant)
1761  {
1762  value = to_string_constant(index_op).get_value();
1763  return false;
1764  }
1765  else if(index_op.id()==ID_array)
1766  {
1767  std::string result;
1768  forall_operands(it, index_op)
1769  if(it->is_constant())
1770  {
1771  const auto i = numeric_cast<std::size_t>(*it);
1772  if(!i.has_value())
1773  return true;
1774 
1775  if(i.value() != 0) // to skip terminating 0
1776  result += static_cast<char>(i.value());
1777  }
1778 
1779  return value=result, false;
1780  }
1781  }
1782 
1783  if(expr.id()==ID_string_constant)
1784  {
1785  value = to_string_constant(expr).get_value();
1786  return false;
1787  }
1788 
1789  return true;
1790 }
1791 
1793 {
1794  irep_idt result;
1795 
1796  const bool res = get_string_constant(expr, result);
1798  !res,
1799  "expected string constant",
1800  expr.find_source_location(),
1801  expr.pretty());
1802 
1803  return result;
1804 }
1805 
1807 {
1808  if(expr.id()==ID_symbol)
1809  {
1810  const symbolt &symbol=
1811  ns.lookup(to_symbol_expr(expr));
1812 
1813  return symbol.value;
1814  }
1815  else if(expr.id()==ID_member)
1816  {
1817  auto tmp = to_member_expr(expr);
1818  tmp.compound() = get_constant(tmp.compound());
1819  return std::move(tmp);
1820  }
1821  else if(expr.id()==ID_index)
1822  {
1823  auto tmp = to_index_expr(expr);
1824  tmp.op0() = get_constant(tmp.op0());
1825  tmp.op1() = get_constant(tmp.op1());
1826  return std::move(tmp);
1827  }
1828  else
1829  return expr;
1830 }
1831 
1833  const typet &type,
1834  const std::string &suffix,
1835  goto_programt &dest,
1836  const source_locationt &source_location,
1837  const irep_idt &mode)
1838 {
1839  PRECONDITION(!mode.empty());
1840  symbolt &new_symbol = get_fresh_aux_symbol(
1841  type,
1843  "tmp_" + suffix,
1844  source_location,
1845  mode,
1846  symbol_table);
1847 
1848  code_declt decl(new_symbol.symbol_expr());
1849  decl.add_source_location()=source_location;
1850  convert_decl(decl, dest, mode);
1851 
1852  return new_symbol;
1853 }
1854 
1856  exprt &expr,
1857  const std::string &suffix,
1858  goto_programt &dest,
1859  const irep_idt &mode)
1860 {
1861  const source_locationt source_location=expr.find_source_location();
1862 
1863  symbolt &new_symbol =
1864  new_tmp_symbol(expr.type(), suffix, dest, source_location, mode);
1865 
1866  code_assignt assignment;
1867  assignment.lhs()=new_symbol.symbol_expr();
1868  assignment.rhs()=expr;
1869  assignment.add_source_location()=source_location;
1870 
1871  convert(assignment, dest, mode);
1872 
1873  expr=new_symbol.symbol_expr();
1874 }
1875 
1877  const codet &code,
1878  symbol_table_baset &symbol_table,
1879  goto_programt &dest,
1880  message_handlert &message_handler,
1881  const irep_idt &mode)
1882 {
1883  symbol_table_buildert symbol_table_builder =
1884  symbol_table_buildert::wrap(symbol_table);
1885  goto_convertt goto_convert(symbol_table_builder, message_handler);
1886  goto_convert.goto_convert(code, dest, mode);
1887 }
1888 
1890  symbol_table_baset &symbol_table,
1891  goto_programt &dest,
1892  message_handlert &message_handler)
1893 {
1894  // find main symbol
1895  const symbol_tablet::symbolst::const_iterator s_it=
1896  symbol_table.symbols.find("main");
1897 
1899  s_it != symbol_table.symbols.end(), "failed to find main symbol");
1900 
1901  const symbolt &symbol=s_it->second;
1902 
1904  to_code(symbol.value), symbol_table, dest, message_handler, symbol.mode);
1905 }
1906 
1922  const code_blockt &thread_body,
1923  goto_programt &dest,
1924  const irep_idt &mode)
1925 {
1926  goto_programt preamble, body, postamble;
1927 
1929  convert(thread_body, body, mode);
1930 
1932  static_cast<const codet &>(get_nil_irep()),
1933  thread_body.source_location(),
1934  END_THREAD,
1935  nil_exprt(),
1936  {}));
1937  e->source_location=thread_body.source_location();
1939 
1941  static_cast<const codet &>(get_nil_irep()),
1942  thread_body.source_location(),
1943  START_THREAD,
1944  nil_exprt(),
1945  {c}));
1946  preamble.add(goto_programt::make_goto(z, thread_body.source_location()));
1947 
1948  dest.destructive_append(preamble);
1949  dest.destructive_append(body);
1950  dest.destructive_append(postamble);
1951 }
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
Operator to return the address of an object.
Definition: pointer_expr.h:341
Result of an attempt to find ancestor information about two nodes.
std::size_t right_depth_below_common_ancestor
node_indext common_ancestor
Boolean AND.
Definition: std_expr.h:1920
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
The Boolean type.
Definition: std_types.h:36
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:617
const exprt & assertion() const
Definition: std_code.h:623
A codet representing an assignment in the program.
Definition: std_code.h:293
exprt & rhs()
Definition: std_code.h:315
exprt & lhs()
Definition: std_code.h:310
An assumption, which must hold in subsequent code.
Definition: std_code.h:565
const exprt & assumption() const
Definition: std_code.h:571
A codet representing sequential composition of program statements.
Definition: std_code.h:168
source_locationt end_location() const
Definition: std_code.h:225
void add(const codet &code)
Definition: std_code.h:206
code_operandst & statements()
Definition: std_code.h:176
codet representation of a break statement (within a for or while loop).
Definition: std_code.h:1628
codet representation of a continue statement (within a for or while loop).
Definition: std_code.h:1664
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:497
A codet representing the declaration of a local variable.
Definition: std_code.h:400
const irep_idt & get_identifier() const
Definition: std_code.h:416
codet representation of a do while statement.
Definition: std_code.h:988
const exprt & cond() const
Definition: std_code.h:995
const codet & body() const
Definition: std_code.h:1005
codet representation of an expression statement.
Definition: std_code.h:1840
const exprt & expression() const
Definition: std_code.h:1847
codet representation of a for statement.
Definition: std_code.h:1050
const exprt & init() const
Definition: std_code.h:1065
const exprt & iter() const
Definition: std_code.h:1085
const exprt & cond() const
Definition: std_code.h:1075
const codet & body() const
Definition: std_code.h:1095
codet representation of a function call statement.
Definition: std_code.h:1213
argumentst & arguments()
Definition: std_code.h:1258
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1543
codet & code()
the statement to be executed when the case applies
Definition: std_code.h:1577
const exprt & lower() const
lower bound of range
Definition: std_code.h:1553
const exprt & upper() const
upper bound of range
Definition: std_code.h:1565
codet representation of a goto statement.
Definition: std_code.h:1157
codet representation of an if-then-else statement.
Definition: std_code.h:776
const codet & then_case() const
Definition: std_code.h:804
const exprt & cond() const
Definition: std_code.h:794
const codet & else_case() const
Definition: std_code.h:814
codet representation of a label for branch targets.
Definition: std_code.h:1405
const irep_idt & get_label() const
Definition: std_code.h:1413
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:2295
exception_listt & exception_list()
Definition: std_code.h:2306
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
const exprt & return_value() const
Definition: std_code.h:1350
bool has_return_value() const
Definition: std_code.h:1360
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1469
codet & code()
Definition: std_code.h:1496
const exprt & case_op() const
Definition: std_code.h:1486
bool is_default() const
Definition: std_code.h:1476
codet representing a switch statement.
Definition: std_code.h:864
const exprt & value() const
Definition: std_code.h:871
const codet & body() const
Definition: std_code.h:881
const parameterst & parameters() const
Definition: std_types.h:655
codet representing a while statement.
Definition: std_code.h:926
const exprt & cond() const
Definition: std_code.h:933
const codet & body() const
Definition: std_code.h:943
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code.h:69
Operator to dereference a pointer.
Definition: pointer_expr.h:628
void set_current_node(optionalt< node_indext > val)
Sets the current node.
void add(const codet &destructor)
Adds a destructor to the current stack, attaching itself to the current node.
const ancestry_resultt get_nearest_common_ancestor_info(node_indext left_index, node_indext right_index)
Finds the nearest common ancestor of two nodes and then returns it.
node_indext get_current_node() const
Gets the node that the next addition will be added to as a child.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
The empty type.
Definition: std_types.h:51
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
std::vector< exprt > operandst
Definition: expr.h:56
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
void convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode)
void convert_assume(const code_assumet &code, goto_programt &dest, const irep_idt &mode)
void convert_return(const code_returnt &code, goto_programt &dest, const irep_idt &mode)
symbol_table_baset & symbol_table
void convert_expression(const code_expressiont &code, goto_programt &dest, const irep_idt &mode)
void convert_while(const code_whilet &code, goto_programt &dest, const irep_idt &mode)
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
void convert_gcc_computed_goto(const codet &code, goto_programt &dest)
void goto_convert_rec(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_CPROVER_throw(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_decl(const code_declt &code, goto_programt &dest, const irep_idt &mode)
void optimize_guarded_gotos(goto_programt &dest)
Rewrite "if(x) goto z; goto y; z:" into "if(!x) goto y;" This only works if the "goto y" is not a bra...
void convert_atomic_begin(const codet &code, goto_programt &dest)
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_msc_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_gcc_switch_case_range(const code_gcc_switch_case_ranget &, goto_programt &dest, const irep_idt &mode)
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
irep_idt get_string_constant(const exprt &expr)
void convert_label(const code_labelt &code, goto_programt &dest, const irep_idt &mode)
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
exprt get_constant(const exprt &expr)
void convert_start_thread(const codet &code, goto_programt &dest)
void finish_gotos(goto_programt &dest, const irep_idt &mode)
void generate_conditional_branch(const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) goto target_true; else goto target_false;
void convert_ifthenelse(const code_ifthenelset &code, goto_programt &dest, const irep_idt &mode)
void convert_atomic_end(const codet &code, goto_programt &dest)
std::string tmp_symbol_prefix
void convert_gcc_local_label(const codet &code, goto_programt &dest)
struct goto_convertt::targetst targets
void convert_break(const code_breakt &code, goto_programt &dest, const irep_idt &mode)
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
void convert_goto(const code_gotot &code, goto_programt &dest)
exprt case_guard(const exprt &value, const caset &case_op)
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_cpp_delete(const codet &code, goto_programt &dest)
void convert_switch(const code_switcht &code, goto_programt &dest, const irep_idt &mode)
static void collect_operands(const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
void convert_decl_type(const codet &code, goto_programt &dest)
void convert_dowhile(const code_dowhilet &code, goto_programt &dest, const irep_idt &mode)
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
void convert_loop_contracts(const codet &code, goto_programt::targett loop, const irep_idt &mode)
void convert_skip(const codet &code, goto_programt &dest)
void convert_asm(const code_asmt &code, goto_programt &dest)
Definition: goto_asm.cpp:14
void convert_switch_case(const code_switch_caset &code, goto_programt &dest, const irep_idt &mode)
void unwind_destructor_stack(const source_locationt &source_location, goto_programt &dest, const irep_idt &mode, optionalt< node_indext > destructor_start_point={}, optionalt< node_indext > destructor_end_point={})
Unwinds the destructor stack and creates destructors for each node between destructor_start_point and...
void convert_msc_try_except(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_continue(const code_continuet &code, goto_programt &dest, const irep_idt &mode)
void convert_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_assert(const code_assertt &code, goto_programt &dest, const irep_idt &mode)
static bool needs_cleaning(const exprt &expr)
void finish_computed_gotos(goto_programt &dest)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
exprt::operandst caset
void generate_ifthenelse(const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode)
if(guard) true_case; else false_case;
static void replace_new_object(const exprt &object, exprt &dest)
void convert_msc_leave(const codet &code, goto_programt &dest, const irep_idt &mode)
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void convert_block(const code_blockt &code, goto_programt &dest, const irep_idt &mode)
void generate_thread_block(const code_blockt &thread_body, goto_programt &dest, const irep_idt &mode)
Generates the necessary goto-instructions to represent a thread-block.
void convert_end_thread(const codet &code, goto_programt &dest)
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
void complete_goto(targett _target)
Definition: goto_program.h:518
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:431
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:434
targetst targets
The list of successor instructions.
Definition: goto_program.h:468
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:185
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:588
codet & code_nonconst()
Set the code represented by this instruction.
Definition: goto_program.h:191
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:963
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:744
instructionst::iterator targett
Definition: goto_program.h:646
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:736
static instructiont make_return(code_returnt c, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:901
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:909
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:722
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:841
static instructiont make_location(const source_locationt &l)
Definition: goto_program.h:919
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:753
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
bool empty() const
Is the program empty?
Definition: goto_program.h:826
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:951
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
The trinary if-then-else operator.
Definition: std_expr.h:2172
exprt & true_case()
Definition: std_expr.h:2199
exprt & false_case()
Definition: std_expr.h:2209
exprt & cond()
Definition: std_expr.h:2189
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void make_nil()
Definition: irep.h:465
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
bool is_nil() const
Definition: irep.h:387
source_locationt source_location
Definition: message.h:247
mstreamt & warning() const
Definition: message.h:404
mstreamt & result() const
Definition: message.h:409
mstreamt & debug() const
Definition: message.h:429
static eomt eom
Definition: message.h:297
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2820
void set_case_number(const irep_idt &number)
const irep_idt & get_value() const
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Author: Diffblue Ltd.
static symbol_table_buildert wrap(symbol_table_baset &base_symbol_table)
Symbol table entry.
Definition: symbol.h:28
bool is_static_lifetime
Definition: symbol.h:65
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
The Boolean constant true.
Definition: std_expr.h:2802
Semantic type conversion.
Definition: std_expr.h:1866
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
The type of an expression, extends irept.
Definition: type.h:28
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
code_function_callt get_destructor(const namespacet &ns, const typet &type)
Definition: destructor.cpp:17
Destructor Calls.
std::size_t node_indext
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:137
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:125
Deprecated expression utility functions.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
static bool has_and_or(const exprt &expr)
if(guard) goto target;
static bool is_size_one(const goto_programt &g)
This is (believed to be) faster than using std::list.size.
static void finish_catch_push_targets(goto_programt &dest)
Populate the CATCH instructions with the targets corresponding to their associated labels.
static bool is_empty(const goto_programt &goto_program)
Program Transformation.
Program Transformation.
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:30
@ ATOMIC_END
Definition: goto_program.h:42
@ DEAD
Definition: goto_program.h:46
@ ASSIGN
Definition: goto_program.h:44
@ ATOMIC_BEGIN
Definition: goto_program.h:41
@ CATCH
Definition: goto_program.h:49
@ END_THREAD
Definition: goto_program.h:38
@ SKIP
Definition: goto_program.h:36
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:31
@ START_THREAD
Definition: goto_program.h:37
@ DECL
Definition: goto_program.h:45
@ OTHER
Definition: goto_program.h:35
const irept & get_nil_irep()
Definition: irep.cpp:20
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
bool is_skip(const goto_programt &body, goto_programt::const_targett it, bool ignore_labels)
Determine whether the instruction is semantically equivalent to a skip (no-op).
Definition: remove_skip.cpp:25
Program Transformation.
bool simplify(exprt &expr, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
Definition: invariant.h:437
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:846
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1389
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:1191
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:970
const code_continuet & to_code_continue(const codet &code)
Definition: std_code.h:1685
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1952
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:598
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1523
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1450
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2185
const codet & to_code(const exprt &expr)
Definition: std_code.h:153
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:1032
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:908
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:480
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1874
const code_breakt & to_code_break(const codet &code)
Definition: std_code.h:1649
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:2329
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:254
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:650
const code_gcc_switch_case_ranget & to_code_gcc_switch_case_range(const codet &code)
Definition: std_code.h:1607
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:1139
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1324
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1728
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:381
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:22
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2152
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
computed_gotost computed_gotos
goto_programt::targett continue_target
void set_break(goto_programt::targett _break_target)
destructor_treet destructor_stack
goto_programt::targett default_target
goto_programt::targett return_target
void set_default(goto_programt::targett _default_target)
void set_continue(goto_programt::targett _continue_target)
goto_programt::targett break_target
Author: Diffblue Ltd.