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 
868  if(invariant.is_nil())
869  return;
870 
871  goto_programt no_sideeffects;
872  clean_expr(invariant, no_sideeffects, mode);
873 
875  no_sideeffects.instructions.empty(),
876  "loop invariant is not side-effect free",
877  code.find_source_location());
878 
879  PRECONDITION(loop->is_goto());
880  loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);
881 }
882 
884  const code_fort &code,
885  goto_programt &dest,
886  const irep_idt &mode)
887 {
888  // turn for(A; c; B) { P } into
889  // A; while(c) { P; B; }
890  //-----------------------------
891  // A;
892  // u: sideeffects in c
893  // v: if(!c) goto z;
894  // w: P;
895  // x: B; <-- continue target
896  // y: goto u;
897  // z: ; <-- break target
898 
899  // A;
900  if(code.init().is_not_nil())
901  convert(to_code(code.init()), dest, mode);
902 
903  exprt cond=code.cond();
904 
905  goto_programt sideeffects;
906  clean_expr(cond, sideeffects, mode);
907 
908  // save break/continue targets
909  break_continue_targetst old_targets(targets);
910 
911  // do the u label
912  goto_programt::targett u=sideeffects.instructions.begin();
913 
914  // do the v label
915  goto_programt tmp_v;
917 
918  // do the z label
919  goto_programt tmp_z;
922 
923  // do the x label
924  goto_programt tmp_x;
925 
926  if(code.iter().is_nil())
927  {
929  }
930  else
931  {
932  exprt tmp_B=code.iter();
933 
934  clean_expr(tmp_B, tmp_x, mode, false);
935 
936  if(tmp_x.instructions.empty())
938  }
939 
940  // optimize the v label
941  if(sideeffects.instructions.empty())
942  u=v;
943 
944  // set the targets
945  targets.set_break(z);
946  targets.set_continue(tmp_x.instructions.begin());
947 
948  // v: if(!c) goto z;
949  *v =
951 
952  // do the w label
953  goto_programt tmp_w;
954  convert(code.body(), tmp_w, mode);
955 
956  // y: goto u;
957  goto_programt tmp_y;
958  goto_programt::targett y = tmp_y.add(
960 
961  // loop invariant
962  convert_loop_invariant(code, y, mode);
963 
964  dest.destructive_append(sideeffects);
965  dest.destructive_append(tmp_v);
966  dest.destructive_append(tmp_w);
967  dest.destructive_append(tmp_x);
968  dest.destructive_append(tmp_y);
969  dest.destructive_append(tmp_z);
970 
971  // restore break/continue
972  old_targets.restore(targets);
973 }
974 
976  const code_whilet &code,
977  goto_programt &dest,
978  const irep_idt &mode)
979 {
980  const exprt &cond=code.cond();
981  const source_locationt &source_location=code.source_location();
982 
983  // while(c) P;
984  //--------------------
985  // v: sideeffects in c
986  // if(!c) goto z;
987  // x: P;
988  // y: goto v; <-- continue target
989  // z: ; <-- break target
990 
991  // save break/continue targets
992  break_continue_targetst old_targets(targets);
993 
994  // do the z label
995  goto_programt tmp_z;
997  tmp_z.add(goto_programt::make_skip(source_location));
998 
999  goto_programt tmp_branch;
1001  boolean_negate(cond), z, source_location, tmp_branch, mode);
1002 
1003  // do the v label
1004  goto_programt::targett v=tmp_branch.instructions.begin();
1005 
1006  // y: goto v;
1007  goto_programt tmp_y;
1008  goto_programt::targett y = tmp_y.add(
1010 
1011  // set the targets
1012  targets.set_break(z);
1013  targets.set_continue(y);
1014 
1015  // do the x label
1016  goto_programt tmp_x;
1017  convert(code.body(), tmp_x, mode);
1018 
1019  // loop invariant
1020  convert_loop_invariant(code, y, mode);
1021 
1022  dest.destructive_append(tmp_branch);
1023  dest.destructive_append(tmp_x);
1024  dest.destructive_append(tmp_y);
1025  dest.destructive_append(tmp_z);
1026 
1027  // restore break/continue
1028  old_targets.restore(targets);
1029 }
1030 
1032  const code_dowhilet &code,
1033  goto_programt &dest,
1034  const irep_idt &mode)
1035 {
1037  code.operands().size() == 2,
1038  "dowhile takes two operands",
1039  code.find_source_location());
1040 
1041  // save source location
1042  source_locationt condition_location=code.cond().find_source_location();
1043 
1044  exprt cond=code.cond();
1045 
1046  goto_programt sideeffects;
1047  clean_expr(cond, sideeffects, mode);
1048 
1049  // do P while(c);
1050  //--------------------
1051  // w: P;
1052  // x: sideeffects in c <-- continue target
1053  // y: if(c) goto w;
1054  // z: ; <-- break target
1055 
1056  // save break/continue targets
1057  break_continue_targetst old_targets(targets);
1058 
1059  // do the y label
1060  goto_programt tmp_y;
1062  tmp_y.add(goto_programt::make_incomplete_goto(cond, condition_location));
1063 
1064  // do the z label
1065  goto_programt tmp_z;
1068 
1069  // do the x label
1071  if(sideeffects.instructions.empty())
1072  x=y;
1073  else
1074  x=sideeffects.instructions.begin();
1075 
1076  // set the targets
1077  targets.set_break(z);
1078  targets.set_continue(x);
1079 
1080  // do the w label
1081  goto_programt tmp_w;
1082  convert(code.body(), tmp_w, mode);
1083  goto_programt::targett w=tmp_w.instructions.begin();
1084 
1085  // y: if(c) goto w;
1086  y->complete_goto(w);
1087 
1088  // loop invariant
1089  convert_loop_invariant(code, y, mode);
1090 
1091  dest.destructive_append(tmp_w);
1092  dest.destructive_append(sideeffects);
1093  dest.destructive_append(tmp_y);
1094  dest.destructive_append(tmp_z);
1095 
1096  // restore break/continue targets
1097  old_targets.restore(targets);
1098 }
1099 
1101  const exprt &value,
1102  const exprt::operandst &case_op)
1103 {
1104  PRECONDITION(!case_op.empty());
1105 
1106  exprt::operandst disjuncts;
1107  disjuncts.reserve(case_op.size());
1108 
1109  for(const auto &op : case_op)
1110  {
1111  // could be a skeleton generated by convert_gcc_switch_case_range
1112  if(op.id() == ID_and)
1113  {
1114  const binary_exprt &and_expr = to_binary_expr(op);
1115  PRECONDITION(to_binary_expr(and_expr.op0()).op1().is_nil());
1116  PRECONDITION(to_binary_expr(and_expr.op1()).op0().is_nil());
1117  binary_exprt skeleton = and_expr;
1118  to_binary_expr(skeleton.op0()).op1() = value;
1119  to_binary_expr(skeleton.op1()).op0() = value;
1120  disjuncts.push_back(skeleton);
1121  }
1122  else
1123  disjuncts.push_back(equal_exprt(value, op));
1124  }
1125 
1126  return disjunction(disjuncts);
1127 }
1128 
1130  const code_switcht &code,
1131  goto_programt &dest,
1132  const irep_idt &mode)
1133 {
1134  // switch(v) {
1135  // case x: Px;
1136  // case y: Py;
1137  // ...
1138  // default: Pd;
1139  // }
1140  // --------------------
1141  // location
1142  // x: if(v==x) goto X;
1143  // y: if(v==y) goto Y;
1144  // goto d;
1145  // X: Px;
1146  // Y: Py;
1147  // d: Pd;
1148  // z: ;
1149 
1150  // we first add a 'location' node for the switch statement,
1151  // which would otherwise not be recorded
1153 
1154  // get the location of the end of the body, but
1155  // default to location of switch, if none
1156  source_locationt body_end_location=
1157  code.body().get_statement()==ID_block?
1158  to_code_block(code.body()).end_location():
1159  code.source_location();
1160 
1161  // do the value we switch over
1162  exprt argument=code.value();
1163 
1164  goto_programt sideeffects;
1165  clean_expr(argument, sideeffects, mode);
1166 
1167  // save break/default/cases targets
1168  break_switch_targetst old_targets(targets);
1169 
1170  // do the z label
1171  goto_programt tmp_z;
1173  tmp_z.add(goto_programt::make_skip(body_end_location));
1174 
1175  // set the new targets -- continue stays as is
1176  targets.set_break(z);
1177  targets.set_default(z);
1178  targets.cases.clear();
1179  targets.cases_map.clear();
1180 
1181  goto_programt tmp;
1182  convert(code.body(), tmp, mode);
1183 
1184  goto_programt tmp_cases;
1185 
1186  // The case number represents which case this corresponds to in the sequence
1187  // of case statements.
1188  //
1189  // switch (x)
1190  // {
1191  // case 2: // case_number 1
1192  // ...;
1193  // case 3: // case_number 2
1194  // ...;
1195  // case 10: // case_number 3
1196  // ...;
1197  // }
1198  size_t case_number=1;
1199  for(auto &case_pair : targets.cases)
1200  {
1201  const caset &case_ops=case_pair.second;
1202 
1203  if (case_ops.empty())
1204  continue;
1205 
1206  exprt guard_expr=case_guard(argument, case_ops);
1207 
1208  source_locationt source_location=case_ops.front().find_source_location();
1209  source_location.set_case_number(std::to_string(case_number));
1210  case_number++;
1211  guard_expr.add_source_location()=source_location;
1212 
1213  tmp_cases.add(goto_programt::make_goto(
1214  case_pair.first, std::move(guard_expr), source_location));
1215  }
1216 
1217  tmp_cases.add(goto_programt::make_goto(
1218  targets.default_target, targets.default_target->source_location));
1219 
1220  dest.destructive_append(sideeffects);
1221  dest.destructive_append(tmp_cases);
1222  dest.destructive_append(tmp);
1223  dest.destructive_append(tmp_z);
1224 
1225  // restore old targets
1226  old_targets.restore(targets);
1227 }
1228 
1230  const code_breakt &code,
1231  goto_programt &dest,
1232  const irep_idt &mode)
1233 {
1235  targets.break_set, "break without target", code.find_source_location());
1236 
1237  // need to process destructor stack
1239  code.source_location(), dest, mode, targets.break_stack_node);
1240 
1241  // add goto
1242  dest.add(
1244 }
1245 
1247  const code_returnt &code,
1248  goto_programt &dest,
1249  const irep_idt &mode)
1250 {
1251  if(!targets.return_set)
1252  {
1254  "return without target", code.find_source_location());
1255  }
1256 
1258  code.operands().empty() || code.operands().size() == 1,
1259  "return takes none or one operand",
1260  code.find_source_location());
1261 
1262  code_returnt new_code(code);
1263 
1264  if(new_code.has_return_value())
1265  {
1266  bool result_is_used=
1267  new_code.return_value().type().id()!=ID_empty;
1268 
1269  goto_programt sideeffects;
1270  clean_expr(new_code.return_value(), sideeffects, mode, result_is_used);
1271  dest.destructive_append(sideeffects);
1272 
1273  // remove void-typed return value
1274  if(!result_is_used)
1275  new_code.return_value().make_nil();
1276  }
1277 
1279  {
1281  new_code.has_return_value(),
1282  "function must return value",
1283  new_code.find_source_location());
1284 
1285  // Now add a return node to set the return value.
1286  dest.add(goto_programt::make_return(new_code, new_code.source_location()));
1287  }
1288  else
1289  {
1291  !new_code.has_return_value() ||
1292  new_code.return_value().type().id() == ID_empty,
1293  "function must not return value",
1294  code.find_source_location());
1295  }
1296 
1297  // Need to process _entire_ destructor stack.
1298  unwind_destructor_stack(code.source_location(), dest, mode);
1299 
1300  // add goto to end-of-function
1302  targets.return_target, new_code.source_location()));
1303 }
1304 
1306  const code_continuet &code,
1307  goto_programt &dest,
1308  const irep_idt &mode)
1309 {
1312  "continue without target",
1313  code.find_source_location());
1314 
1315  // need to process destructor stack
1317  code.source_location(), dest, mode, targets.continue_stack_node);
1318 
1319  // add goto
1320  dest.add(
1322 }
1323 
1325 {
1326  // this instruction will be completed during post-processing
1329 
1330  // remember it to do the target later
1332 }
1333 
1335  const codet &code,
1336  goto_programt &dest)
1337 {
1338  // this instruction will turn into OTHER during post-processing
1340  code, code.source_location(), NO_INSTRUCTION_TYPE, nil_exprt(), {}));
1341 
1342  // remember it to do this later
1343  targets.computed_gotos.push_back(t);
1344 }
1345 
1347  const codet &code,
1348  goto_programt &dest)
1349 {
1351  code, code.source_location(), START_THREAD, nil_exprt(), {}));
1352 
1353  // remember it to do target later
1354  targets.gotos.emplace_back(
1355  start_thread, targets.destructor_stack.get_current_node());
1356 }
1357 
1359  const codet &code,
1360  goto_programt &dest)
1361 {
1363  code.operands().empty(),
1364  "end_thread expects no operands",
1365  code.find_source_location());
1366 
1367  copy(code, END_THREAD, dest);
1368 }
1369 
1371  const codet &code,
1372  goto_programt &dest)
1373 {
1375  code.operands().empty(),
1376  "atomic_begin expects no operands",
1377  code.find_source_location());
1378 
1379  copy(code, ATOMIC_BEGIN, dest);
1380 }
1381 
1383  const codet &code,
1384  goto_programt &dest)
1385 {
1387  code.operands().empty(),
1388  ": atomic_end expects no operands",
1389  code.find_source_location());
1390 
1391  copy(code, ATOMIC_END, dest);
1392 }
1393 
1395  const code_ifthenelset &code,
1396  goto_programt &dest,
1397  const irep_idt &mode)
1398 {
1399  DATA_INVARIANT(code.then_case().is_not_nil(), "cannot accept an empty body");
1400 
1401  bool has_else=
1402  !code.else_case().is_nil();
1403 
1404  const source_locationt &source_location=code.source_location();
1405 
1406  // We do a bit of special treatment for && in the condition
1407  // in case cleaning would be needed otherwise.
1408  if(
1409  code.cond().id() == ID_and && code.cond().operands().size() == 2 &&
1410  (needs_cleaning(to_binary_expr(code.cond()).op0()) ||
1411  needs_cleaning(to_binary_expr(code.cond()).op1())) &&
1412  !has_else)
1413  {
1414  // if(a && b) XX --> if(a) if(b) XX
1415  code_ifthenelset new_if1(
1416  to_binary_expr(code.cond()).op1(), code.then_case());
1417  new_if1.add_source_location() = source_location;
1418  code_ifthenelset new_if0(
1419  to_binary_expr(code.cond()).op0(), std::move(new_if1));
1420  new_if0.add_source_location() = source_location;
1421  return convert_ifthenelse(new_if0, dest, mode);
1422  }
1423 
1424  // convert 'then'-branch
1425  goto_programt tmp_then;
1426  convert(code.then_case(), tmp_then, mode);
1427 
1428  goto_programt tmp_else;
1429 
1430  if(has_else)
1431  convert(code.else_case(), tmp_else, mode);
1432 
1433  exprt tmp_guard=code.cond();
1434  clean_expr(tmp_guard, dest, mode);
1435 
1437  tmp_guard, tmp_then, tmp_else, source_location, dest, mode);
1438 }
1439 
1441  const exprt &expr,
1442  const irep_idt &id,
1443  std::list<exprt> &dest)
1444 {
1445  if(expr.id()!=id)
1446  {
1447  dest.push_back(expr);
1448  }
1449  else
1450  {
1451  // left-to-right is important
1452  forall_operands(it, expr)
1453  collect_operands(*it, id, dest);
1454  }
1455 }
1456 
1460 static inline bool is_size_one(const goto_programt &g)
1461 {
1462  return (!g.instructions.empty()) &&
1463  ++g.instructions.begin()==g.instructions.end();
1464 }
1465 
1468  const exprt &guard,
1469  goto_programt &true_case,
1470  goto_programt &false_case,
1471  const source_locationt &source_location,
1472  goto_programt &dest,
1473  const irep_idt &mode)
1474 {
1475  if(is_empty(true_case) &&
1476  is_empty(false_case))
1477  {
1478  // hmpf. Useless branch.
1479  goto_programt tmp_z;
1481  dest.add(goto_programt::make_goto(z, guard, source_location));
1482  dest.destructive_append(tmp_z);
1483  return;
1484  }
1485 
1486  // do guarded assertions directly
1487  if(
1488  is_size_one(true_case) && true_case.instructions.back().is_assert() &&
1489  true_case.instructions.back().get_condition().is_false() &&
1490  true_case.instructions.back().labels.empty())
1491  {
1492  // The above conjunction deliberately excludes the instance
1493  // if(some) { label: assert(false); }
1494  true_case.instructions.back().set_condition(boolean_negate(guard));
1495  dest.destructive_append(true_case);
1496  true_case.instructions.clear();
1497  if(
1498  is_empty(false_case) ||
1499  (is_size_one(false_case) &&
1500  is_skip(false_case, false_case.instructions.begin())))
1501  return;
1502  }
1503 
1504  // similarly, do guarded assertions directly
1505  if(
1506  is_size_one(false_case) && false_case.instructions.back().is_assert() &&
1507  false_case.instructions.back().get_condition().is_false() &&
1508  false_case.instructions.back().labels.empty())
1509  {
1510  // The above conjunction deliberately excludes the instance
1511  // if(some) ... else { label: assert(false); }
1512  false_case.instructions.back().set_condition(guard);
1513  dest.destructive_append(false_case);
1514  false_case.instructions.clear();
1515  if(
1516  is_empty(true_case) ||
1517  (is_size_one(true_case) &&
1518  is_skip(true_case, true_case.instructions.begin())))
1519  return;
1520  }
1521 
1522  // a special case for C libraries that use
1523  // (void)((cond) || (assert(0),0))
1524  if(
1525  is_empty(false_case) && true_case.instructions.size() == 2 &&
1526  true_case.instructions.front().is_assert() &&
1527  true_case.instructions.front().get_condition().is_false() &&
1528  true_case.instructions.front().labels.empty() &&
1529  true_case.instructions.back().labels.empty())
1530  {
1531  true_case.instructions.front().set_condition(boolean_negate(guard));
1532  true_case.instructions.erase(--true_case.instructions.end());
1533  dest.destructive_append(true_case);
1534  true_case.instructions.clear();
1535 
1536  return;
1537  }
1538 
1539  // Flip around if no 'true' case code.
1540  if(is_empty(true_case))
1541  return generate_ifthenelse(
1542  boolean_negate(guard),
1543  false_case,
1544  true_case,
1545  source_location,
1546  dest,
1547  mode);
1548 
1549  bool has_else=!is_empty(false_case);
1550 
1551  // if(c) P;
1552  //--------------------
1553  // v: if(!c) goto z;
1554  // w: P;
1555  // z: ;
1556 
1557  // if(c) P; else Q;
1558  //--------------------
1559  // v: if(!c) goto y;
1560  // w: P;
1561  // x: goto z;
1562  // y: Q;
1563  // z: ;
1564 
1565  // do the x label
1566  goto_programt tmp_x;
1569 
1570  // do the z label
1571  goto_programt tmp_z;
1573  // We deliberately don't set a location for 'z', it's a dummy
1574  // target.
1575 
1576  // y: Q;
1577  goto_programt tmp_y;
1579  if(has_else)
1580  {
1581  tmp_y.swap(false_case);
1582  y=tmp_y.instructions.begin();
1583  }
1584 
1585  // v: if(!c) goto z/y;
1586  goto_programt tmp_v;
1588  boolean_negate(guard), has_else ? y : z, source_location, tmp_v, mode);
1589 
1590  // w: P;
1591  goto_programt tmp_w;
1592  tmp_w.swap(true_case);
1593 
1594  // x: goto z;
1595  CHECK_RETURN(!tmp_w.instructions.empty());
1596  x->complete_goto(z);
1597  x->source_location = tmp_w.instructions.back().source_location;
1598 
1599  dest.destructive_append(tmp_v);
1600  dest.destructive_append(tmp_w);
1601 
1602  if(has_else)
1603  {
1604  dest.destructive_append(tmp_x);
1605  dest.destructive_append(tmp_y);
1606  }
1607 
1608  dest.destructive_append(tmp_z);
1609 }
1610 
1612 static bool has_and_or(const exprt &expr)
1613 {
1614  forall_operands(it, expr)
1615  if(has_and_or(*it))
1616  return true;
1617 
1618  if(expr.id()==ID_and || expr.id()==ID_or)
1619  return true;
1620 
1621  return false;
1622 }
1623 
1625  const exprt &guard,
1626  goto_programt::targett target_true,
1627  const source_locationt &source_location,
1628  goto_programt &dest,
1629  const irep_idt &mode)
1630 {
1631  if(has_and_or(guard) && needs_cleaning(guard))
1632  {
1633  // if(guard) goto target;
1634  // becomes
1635  // if(guard) goto target; else goto next;
1636  // next: skip;
1637 
1638  goto_programt tmp;
1639  goto_programt::targett target_false =
1640  tmp.add(goto_programt::make_skip(source_location));
1641 
1643  guard, target_true, target_false, source_location, dest, mode);
1644 
1645  dest.destructive_append(tmp);
1646  }
1647  else
1648  {
1649  // simple branch
1650  exprt cond=guard;
1651  clean_expr(cond, dest, mode);
1652 
1653  dest.add(goto_programt::make_goto(target_true, cond, source_location));
1654  }
1655 }
1656 
1659  const exprt &guard,
1660  goto_programt::targett target_true,
1661  goto_programt::targett target_false,
1662  const source_locationt &source_location,
1663  goto_programt &dest,
1664  const irep_idt &mode)
1665 {
1666  if(guard.id()==ID_not)
1667  {
1668  // simply swap targets
1670  to_not_expr(guard).op(),
1671  target_false,
1672  target_true,
1673  source_location,
1674  dest,
1675  mode);
1676  return;
1677  }
1678 
1679  if(guard.id()==ID_and)
1680  {
1681  // turn
1682  // if(a && b) goto target_true; else goto target_false;
1683  // into
1684  // if(!a) goto target_false;
1685  // if(!b) goto target_false;
1686  // goto target_true;
1687 
1688  std::list<exprt> op;
1689  collect_operands(guard, guard.id(), op);
1690 
1691  for(const auto &expr : op)
1693  boolean_negate(expr), target_false, source_location, dest, mode);
1694 
1695  dest.add(goto_programt::make_goto(target_true, source_location));
1696 
1697  return;
1698  }
1699  else if(guard.id()==ID_or)
1700  {
1701  // turn
1702  // if(a || b) goto target_true; else goto target_false;
1703  // into
1704  // if(a) goto target_true;
1705  // if(b) goto target_true;
1706  // goto target_false;
1707 
1708  std::list<exprt> op;
1709  collect_operands(guard, guard.id(), op);
1710 
1711  // true branch(es)
1712  for(const auto &expr : op)
1714  expr, target_true, source_location, dest, mode);
1715 
1716  // false branch
1717  dest.add(goto_programt::make_goto(target_false, guard.source_location()));
1718 
1719  return;
1720  }
1721 
1722  exprt cond=guard;
1723  clean_expr(cond, dest, mode);
1724 
1725  // true branch
1726  dest.add(goto_programt::make_goto(target_true, cond, source_location));
1727 
1728  // false branch
1729  dest.add(goto_programt::make_goto(target_false, source_location));
1730 }
1731 
1733  const exprt &expr,
1734  irep_idt &value)
1735 {
1736  if(expr.id() == ID_typecast)
1737  return get_string_constant(to_typecast_expr(expr).op(), value);
1738 
1739  if(
1740  expr.id() == ID_address_of &&
1741  to_address_of_expr(expr).object().id() == ID_index)
1742  {
1743  exprt index_op =
1744  get_constant(to_index_expr(to_address_of_expr(expr).object()).array());
1745  simplify(index_op, ns);
1746 
1747  if(index_op.id()==ID_string_constant)
1748  {
1749  value = to_string_constant(index_op).get_value();
1750  return false;
1751  }
1752  else if(index_op.id()==ID_array)
1753  {
1754  std::string result;
1755  forall_operands(it, index_op)
1756  if(it->is_constant())
1757  {
1758  const auto i = numeric_cast<std::size_t>(*it);
1759  if(!i.has_value())
1760  return true;
1761 
1762  if(i.value() != 0) // to skip terminating 0
1763  result += static_cast<char>(i.value());
1764  }
1765 
1766  return value=result, false;
1767  }
1768  }
1769 
1770  if(expr.id()==ID_string_constant)
1771  {
1772  value = to_string_constant(expr).get_value();
1773  return false;
1774  }
1775 
1776  return true;
1777 }
1778 
1780 {
1781  irep_idt result;
1782 
1783  const bool res = get_string_constant(expr, result);
1785  !res,
1786  "expected string constant",
1787  expr.find_source_location(),
1788  expr.pretty());
1789 
1790  return result;
1791 }
1792 
1794 {
1795  if(expr.id()==ID_symbol)
1796  {
1797  const symbolt &symbol=
1798  ns.lookup(to_symbol_expr(expr));
1799 
1800  return symbol.value;
1801  }
1802  else if(expr.id()==ID_member)
1803  {
1804  auto tmp = to_member_expr(expr);
1805  tmp.compound() = get_constant(tmp.compound());
1806  return std::move(tmp);
1807  }
1808  else if(expr.id()==ID_index)
1809  {
1810  auto tmp = to_index_expr(expr);
1811  tmp.op0() = get_constant(tmp.op0());
1812  tmp.op1() = get_constant(tmp.op1());
1813  return std::move(tmp);
1814  }
1815  else
1816  return expr;
1817 }
1818 
1820  const typet &type,
1821  const std::string &suffix,
1822  goto_programt &dest,
1823  const source_locationt &source_location,
1824  const irep_idt &mode)
1825 {
1826  PRECONDITION(!mode.empty());
1827  symbolt &new_symbol = get_fresh_aux_symbol(
1828  type,
1830  "tmp_" + suffix,
1831  source_location,
1832  mode,
1833  symbol_table);
1834 
1835  code_declt decl(new_symbol.symbol_expr());
1836  decl.add_source_location()=source_location;
1837  convert_decl(decl, dest, mode);
1838 
1839  return new_symbol;
1840 }
1841 
1843  exprt &expr,
1844  const std::string &suffix,
1845  goto_programt &dest,
1846  const irep_idt &mode)
1847 {
1848  const source_locationt source_location=expr.find_source_location();
1849 
1850  symbolt &new_symbol =
1851  new_tmp_symbol(expr.type(), suffix, dest, source_location, mode);
1852 
1853  code_assignt assignment;
1854  assignment.lhs()=new_symbol.symbol_expr();
1855  assignment.rhs()=expr;
1856  assignment.add_source_location()=source_location;
1857 
1858  convert(assignment, dest, mode);
1859 
1860  expr=new_symbol.symbol_expr();
1861 }
1862 
1864  const codet &code,
1865  symbol_table_baset &symbol_table,
1866  goto_programt &dest,
1867  message_handlert &message_handler,
1868  const irep_idt &mode)
1869 {
1870  symbol_table_buildert symbol_table_builder =
1871  symbol_table_buildert::wrap(symbol_table);
1872  goto_convertt goto_convert(symbol_table_builder, message_handler);
1873  goto_convert.goto_convert(code, dest, mode);
1874 }
1875 
1877  symbol_table_baset &symbol_table,
1878  goto_programt &dest,
1879  message_handlert &message_handler)
1880 {
1881  // find main symbol
1882  const symbol_tablet::symbolst::const_iterator s_it=
1883  symbol_table.symbols.find("main");
1884 
1886  s_it != symbol_table.symbols.end(), "failed to find main symbol");
1887 
1888  const symbolt &symbol=s_it->second;
1889 
1891  to_code(symbol.value), symbol_table, dest, message_handler, symbol.mode);
1892 }
1893 
1909  const code_blockt &thread_body,
1910  goto_programt &dest,
1911  const irep_idt &mode)
1912 {
1913  goto_programt preamble, body, postamble;
1914 
1916  convert(thread_body, body, mode);
1917 
1919  static_cast<const codet &>(get_nil_irep()),
1920  thread_body.source_location(),
1921  END_THREAD,
1922  nil_exprt(),
1923  {}));
1924  e->source_location=thread_body.source_location();
1926 
1928  static_cast<const codet &>(get_nil_irep()),
1929  thread_body.source_location(),
1930  START_THREAD,
1931  nil_exprt(),
1932  {c}));
1933  preamble.add(goto_programt::make_goto(z, thread_body.source_location()));
1934 
1935  dest.destructive_append(preamble);
1936  dest.destructive_append(body);
1937  dest.destructive_append(postamble);
1938 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1185
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:1488
goto_convertt::convert_dowhile
void convert_dowhile(const code_dowhilet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1031
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:1788
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:1876
goto_programt::instructiont::source_location
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:347
code_switch_caset
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1471
goto_convertt::targetst::set_break
void set_break(goto_programt::targett _break_target)
Definition: goto_convert_class.h:408
goto_convertt::needs_cleaning
static bool needs_cleaning(const exprt &expr)
Definition: goto_clean_expr.cpp:66
to_side_effect_expr_function_call
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2187
goto_programt::instructiont::complete_goto
void complete_goto(targett _target)
Definition: goto_program.h:434
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:1658
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
goto_convertt::ns
namespacet ns
Definition: goto_convert_class.h:52
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:1077
arith_tools.h
code_whilet
codet representing a while statement.
Definition: std_code.h:928
codet::op0
exprt & op0()
Definition: expr.h:103
to_code_decl
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:482
goto_convertt::replace_new_object
static void replace_new_object(const exprt &object, exprt &dest)
Definition: goto_convert_side_effect.cpp:401
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:429
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:442
code_fort
codet representation of a for statement.
Definition: std_code.h:1052
goto_convertt::copy
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
Definition: goto_convert.cpp:299
irept::make_nil
void make_nil()
Definition: irep.h:465
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
code_ifthenelset::then_case
const codet & then_case() const
Definition: std_code.h:806
fresh_symbol.h
Fresh auxiliary symbol creation.
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:501
code_gcc_switch_case_ranget::upper
const exprt & upper() const
upper bound of range
Definition: std_code.h:1567
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:162
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2151
to_code_break
const code_breakt & to_code_break(const codet &code)
Definition: std_code.h:1651
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:286
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:386
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
goto_convertt::convert_skip
void convert_skip(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:840
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:350
goto_convertt::convert_assert
void convert_assert(const code_assertt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:825
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:43
has_and_or
static bool has_and_or(const exprt &expr)
if(guard) goto target;
Definition: goto_convert.cpp:1612
goto_convertt::tmp_symbol_prefix
std::string tmp_symbol_prefix
Definition: goto_convert_class.h:53
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:109
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:112
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:619
goto_convert_class.h
Program Transformation.
and_exprt
Boolean AND.
Definition: std_expr.h:1834
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:573
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:670
goto_convertt::convert_ifthenelse
void convert_ifthenelse(const code_ifthenelset &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1394
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:1467
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:848
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:746
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:54
goto_convertt::convert_block
void convert_block(const code_blockt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:542
goto_convertt::targetst::cases_map
cases_mapt cases_map
Definition: goto_convert_class.h:385
code_fort::iter
const exprt & iter() const
Definition: std_code.h:1087
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:550
code_continuet
codet representation of a continue statement (within a for or while loop).
Definition: std_code.h:1666
to_code_while
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:972
bool_typet
The Boolean type.
Definition: std_types.h:36
code_gcc_switch_case_ranget
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1545
code_ifthenelset::cond
const exprt & cond() const
Definition: std_code.h:796
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:384
messaget::eom
static eomt eom
Definition: message.h:297
goto_programt::instructiont::is_incomplete_goto
bool is_incomplete_goto() const
Definition: goto_program.h:460
to_side_effect_expr
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1954
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:80
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:1908
code_declt::get_identifier
const irep_idt & get_identifier() const
Definition: std_code.h:418
equal_exprt
Equality.
Definition: std_expr.h:1139
to_code_for
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:1141
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:356
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:778
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2123
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:1819
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:982
goto_convertt::goto_convert
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:278
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:69
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:1555
goto_programt::instructiont::get_code
const codet & get_code() const
Get the code represented by this instruction.
Definition: goto_program.h:187
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:627
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:1863
to_code_switch_case
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1525
goto_convertt::targetst::has_return_value
bool has_return_value
Definition: goto_convert_class.h:376
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:178
goto_convertt::targetst::labels
labelst labels
Definition: goto_convert_class.h:379
goto_convertt::convert_break
void convert_break(const code_breakt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1229
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
to_code_assume
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:600
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:141
to_code_assert
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:652
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
goto_convertt::targetst::gotos
gotost gotos
Definition: goto_convert_class.h:380
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:738
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:625
code_dowhilet
codet representation of a do while statement.
Definition: std_code.h:990
goto_convertt::break_switch_targetst::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:489
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:572
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:877
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:1067
empty_typet
The empty type.
Definition: std_types.h:45
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
code_switch_caset::is_default
bool is_default() const
Definition: std_code.h:1478
goto_convertt::convert_continue
void convert_continue(const code_continuet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1305
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:661
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:1630
goto_convertt
Definition: goto_convert_class.h:31
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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:1579
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:1779
goto_convertt::targetst::break_stack_node
node_indext break_stack_node
Definition: goto_convert_class.h:390
to_code_goto
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:1193
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:835
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1159
goto_convertt::targetst::break_target
goto_programt::targett break_target
Definition: goto_convert_class.h:387
to_code_ifthenelse
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:848
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1407
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:192
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:234
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
nil_exprt
The NIL expression.
Definition: std_expr.h:2734
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:399
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:129
code_assumet
An assumption, which must hold in subsequent code.
Definition: std_code.h:567
to_code_label
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1452
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
pointer_expr.h
API to expression classes for Pointers.
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:2552
to_code_dowhile
const code_dowhilet & to_code_dowhile(const codet &code)
Definition: std_code.h:1034
goto_convertt::convert_goto
void convert_goto(const code_gotot &code, goto_programt &dest)
Definition: goto_convert.cpp:1324
code_push_catcht::exception_list
exception_listt & exception_list()
Definition: std_code.h:2308
NO_INSTRUCTION_TYPE
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:34
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:376
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
OTHER
@ OTHER
Definition: goto_program.h:38
code_whilet::cond
const exprt & cond() const
Definition: std_code.h:935
code_whilet::body
const codet & body() const
Definition: std_code.h:945
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
goto_convertt::targetst::continue_set
bool continue_set
Definition: goto_convert_class.h:376
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:1460
goto_convertt::break_continue_targetst::restore
void restore(targetst &targets)
Definition: goto_convert_class.h:461
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1326
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
dstringt::empty
bool empty() const
Definition: dstring.h:88
goto_convertt::targetst::break_set
bool break_set
Definition: goto_convert_class.h:376
to_code_return
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:1391
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:883
goto_convertt::caset
exprt::operandst caset
Definition: goto_convert_class.h:370
goto_convertt::get_constant
exprt get_constant(const exprt &expr)
Definition: goto_convert.cpp:1793
SKIP
@ SKIP
Definition: goto_program.h:39
code_deadt
A codet representing the removal of a local variable going out of scope.
Definition: std_code.h:499
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:649
goto_convertt::convert_decl
void convert_decl(const code_declt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:609
cprover_prefix.h
is_empty
static bool is_empty(const goto_programt &goto_program)
Definition: goto_convert.cpp:32
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
goto_convertt::convert_while
void convert_while(const code_whilet &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:975
goto_convertt::convert_assign
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:680
destructor.h
Destructor Calls.
goto_convertt::targetst::default_target
goto_programt::targett default_target
Definition: goto_convert_class.h:388
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:653
goto_convertt::collect_operands
static void collect_operands(const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
Definition: goto_convert.cpp:1440
goto_program_instruction_typet
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:33
goto_programt::make_return
static instructiont make_return(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:822
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:1609
code_labelt::get_label
const irep_idt & get_label() const
Definition: std_code.h:1415
to_code_asm
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1730
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:569
expr_util.h
Deprecated expression utility functions.
ASSIGN
@ ASSIGN
Definition: goto_program.h:47
code_switcht::value
const exprt & value() const
Definition: std_code.h:873
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:1362
goto_convertt::finish_computed_gotos
void finish_computed_gotos(goto_programt &dest)
Definition: goto_convert.cpp:202
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:52
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1342
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2113
DECL
@ DECL
Definition: goto_program.h:48
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:382
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2066
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:1100
goto_convertt::convert_gcc_local_label
void convert_gcc_local_label(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:349
goto_convertt::convert_return
void convert_return(const code_returnt &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1246
code_push_catcht::exception_listt
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:2297
code_switcht
codet representing a switch statement.
Definition: std_code.h:866
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:1346
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
goto_convertt::targetst::cases
casest cases
Definition: goto_convert_class.h:384
code_dowhilet::body
const codet & body() const
Definition: std_code.h:1007
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:1814
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:860
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2103
code_fort::body
const codet & body() const
Definition: std_code.h:1097
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
code_ifthenelset::else_case
const codet & else_case() const
Definition: std_code.h:816
to_code_switch
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:910
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:40
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:415
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
code_switch_caset::code
codet & code()
Definition: std_code.h:1498
code_dowhilet::cond
const exprt & cond() const
Definition: std_code.h:997
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:639
goto_convertt::symbol_table
symbol_table_baset & symbol_table
Definition: goto_convert_class.h:51
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:2611
ATOMIC_END
@ ATOMIC_END
Definition: goto_program.h:45
goto_convertt::convert_cpp_delete
void convert_cpp_delete(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:763
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
code_expressiont::expression
const exprt & expression() const
Definition: std_code.h:1849
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:889
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:367
DEAD
@ DEAD
Definition: goto_program.h:49
exprt::operands
operandst & operands()
Definition: expr.h:96
messaget::debug
mstreamt & debug() const
Definition: message.h:429
codet::op1
exprt & op1()
Definition: expr.h:106
goto_convertt::convert_atomic_end
void convert_atomic_end(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1382
goto_convertt::targetst::continue_target
goto_programt::targett continue_target
Definition: goto_convert_class.h:387
ATOMIC_BEGIN
@ ATOMIC_BEGIN
Definition: goto_program.h:44
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:243
goto_convertt::break_switch_targetst
Definition: goto_convert_class.h:475
symbol_table.h
Author: Diffblue Ltd.
code_switcht::body
const codet & body() const
Definition: std_code.h:883
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
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:1352
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:308
goto_programt::instructiont::is_start_thread
bool is_start_thread() const
Definition: goto_program.h:457
true_exprt
The Boolean constant true.
Definition: std_expr.h:2716
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:388
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:106
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
goto_convertt::break_continue_targetst
Definition: goto_convert_class.h:450
goto_convertt::targetst::set_default
void set_default(goto_programt::targett _default_target)
Definition: goto_convert_class.h:422
goto_convertt::targetst::continue_stack_node
node_indext continue_stack_node
Definition: goto_convert_class.h:390
goto_programt::instructiont::code_nonconst
codet & code_nonconst()
Set the code represented by this instruction.
Definition: goto_program.h:193
c_types.h
goto_programt::instructiont::nil_target
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:505
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:845
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:1687
string_constantt::get_value
const irep_idt & get_value() const
Definition: string_constant.h:22
END_THREAD
@ END_THREAD
Definition: goto_program.h:41
goto_programt::swap
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:761
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1180
goto_convertt::convert_atomic_begin
void convert_atomic_begin(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1370
goto_convertt::convert_decl_type
void convert_decl_type(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:673
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:951
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
goto_convertt::targetst::computed_gotos
computed_gotost computed_gotos
Definition: goto_convert_class.h:381
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1842
goto_convertt::convert_switch
void convert_switch(const code_switcht &code, goto_programt &dest, const irep_idt &mode)
Definition: goto_convert.cpp:1129
to_code_push_catch
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:2331
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:387
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:1842
goto_convertt::convert_end_thread
void convert_end_thread(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1358
goto_convertt::convert_gcc_computed_goto
void convert_gcc_computed_goto(const codet &code, goto_programt &dest)
Definition: goto_convert.cpp:1334