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