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 <cassert>
15 
16 #include <util/arith_tools.h>
17 #include <util/cprover_prefix.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/symbol_table.h>
24 
25 #include <util/c_types.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 {
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  error() << "goto label `" << goto_label << "' not found" << eom;
123  throw 0;
124  }
125 
126  i.targets.push_back(l_it->second.first);
127  }
128  else if(i.code.get_statement()==ID_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  error() << "goto label `" << goto_label << "' not found" << eom;
138  throw 0;
139  }
140 
141  i.complete_goto(l_it->second.first);
142 
143  // If the goto recorded a destructor stack, execute as much as is
144  // appropriate for however many automatic variables leave scope.
145  // We don't currently handle variables *entering* scope, which is illegal
146  // for C++ non-pod types and impossible in Java in any case.
147  auto goto_stack=g_it.second;
148  const auto &label_stack=l_it->second.second;
149  bool stack_is_prefix = label_stack.size() <= goto_stack.size();
150  for(
151  std::size_t idx = 0, ilim = label_stack.size();
152  idx != ilim && stack_is_prefix; ++idx)
153  {
154  stack_is_prefix &= goto_stack[idx] == label_stack[idx];
155  }
156 
157  if(!stack_is_prefix)
158  {
160  debug() << "encountered goto `" << goto_label
161  << "' that enters one or more lexical blocks; "
162  << "omitting constructors and destructors" << eom;
163  }
164  else
165  {
166  auto unwind_to_size=label_stack.size();
167  if(unwind_to_size<goto_stack.size())
168  {
170  debug() << "adding goto-destructor code on jump to `"
171  << goto_label << "'" << eom;
172  goto_programt destructor_code;
175  unwind_to_size,
176  destructor_code,
177  goto_stack,
178  mode);
179  dest.destructive_insert(g_it.first, destructor_code);
180  // This should leave iterators intact, as long as
181  // goto_programt::instructionst is std::list.
182  }
183  }
184  }
185  else
186  {
188  error() << "finish_gotos: unexpected goto" << eom;
189  throw 0;
190  }
191  }
192 
193  targets.gotos.clear();
194 }
195 
197 {
198  for(auto &g_it : targets.computed_gotos)
199  {
201  exprt destination=i.code.op0();
202 
203  assert(destination.id()==ID_dereference);
204  assert(destination.operands().size()==1);
205 
206  exprt pointer=destination.op0();
207 
208  // remember the expression for later checks
209  i.type=OTHER;
210  i.code=code_expressiont(pointer);
211 
212  // insert huge case-split
213  for(const auto &label : targets.labels)
214  {
215  exprt label_expr(ID_label, empty_typet());
216  label_expr.set(ID_identifier, label.first);
217 
218  const equal_exprt guard(pointer, address_of_exprt(label_expr));
219 
222 
223  t->make_goto(label.second.first);
224  t->source_location=i.source_location;
225  t->guard=guard;
226  }
227  }
228 
229  targets.computed_gotos.clear();
230 }
231 
236 {
237  // We cannot use a set of targets, as target iterators
238  // cannot be compared at this stage.
239 
240  // collect targets: reset marking
241  for(auto &i : dest.instructions)
242  i.target_number = goto_programt::instructiont::nil_target;
243 
244  // mark the goto targets
245  unsigned cnt = 0;
246  for(const auto &i : dest.instructions)
247  if(i.is_goto())
248  i.get_target()->target_number = (++cnt);
249 
250  for(auto it = dest.instructions.begin(); it != dest.instructions.end(); it++)
251  {
252  if(!it->is_goto())
253  continue;
254 
255  auto it_goto_y = std::next(it);
256 
257  if(
258  it_goto_y == dest.instructions.end() || !it_goto_y->is_goto() ||
259  !it_goto_y->guard.is_true() || it_goto_y->is_target())
260  continue;
261 
262  auto it_z = std::next(it_goto_y);
263 
264  if(it_z == dest.instructions.end())
265  continue;
266 
267  // cannot compare iterators, so compare target number instead
268  if(it->get_target()->target_number == it_z->target_number)
269  {
270  it->set_target(it_goto_y->get_target());
271  it->guard = boolean_negate(it->guard);
272  it_goto_y->make_skip();
273  }
274  }
275 }
276 
278  const codet &code,
279  goto_programt &dest,
280  const irep_idt &mode)
281 {
282  goto_convert_rec(code, dest, mode);
283 }
284 
286  const codet &code,
287  goto_programt &dest,
288  const irep_idt &mode)
289 {
290  convert(code, dest, mode);
291 
292  finish_gotos(dest, mode);
293  finish_computed_gotos(dest);
296 }
297 
299  const codet &code,
301  goto_programt &dest)
302 {
304  t->code=code;
306 }
307 
309  const code_labelt &code,
310  goto_programt &dest,
311  const irep_idt &mode)
312 {
313  if(code.operands().size()!=1)
314  {
316  error() << "label statement expected to have one operand" << eom;
317  throw 0;
318  }
319 
320  // grab the label
321  const irep_idt &label=code.get_label();
322 
323  goto_programt tmp;
324 
325  // magic thread creation label.
326  // The "__CPROVER_ASYNC_" signals the start of a sequence of instructions
327  // that can be executed in parallel, i.e, a new thread.
328  if(has_prefix(id2string(label), "__CPROVER_ASYNC_"))
329  {
330  // the body of the thread is expected to be
331  // in the operand.
332  INVARIANT(code.op0().is_not_nil(),
333  "op0 in magic thread creation label is null");
334 
335  // replace the magic thread creation label with a
336  // thread block (START_THREAD...END_THREAD).
337  code_blockt thread_body;
338  thread_body.add(to_code(code.op0()));
339  thread_body.add_source_location()=code.source_location();
340  generate_thread_block(thread_body, dest, mode);
341  }
342  else
343  {
344  convert(to_code(code.op0()), tmp, mode);
345 
346  goto_programt::targett target=tmp.instructions.begin();
347  dest.destructive_append(tmp);
348 
349  targets.labels.insert({label, {target, targets.destructor_stack}});
350  target->labels.push_front(label);
351  }
352 }
353 
355  const codet &,
356  goto_programt &)
357 {
358  // ignore for now
359 }
360 
362  const code_switch_caset &code,
363  goto_programt &dest,
364  const irep_idt &mode)
365 {
366  goto_programt tmp;
367  convert(code.code(), tmp, mode);
368 
369  goto_programt::targett target=tmp.instructions.begin();
370  dest.destructive_append(tmp);
371 
372  // is a default target given?
373 
374  if(code.is_default())
375  targets.set_default(target);
376  else
377  {
378  // cases?
379 
380  cases_mapt::iterator cases_entry=targets.cases_map.find(target);
381  if(cases_entry==targets.cases_map.end())
382  {
383  targets.cases.push_back(std::make_pair(target, caset()));
384  cases_entry=targets.cases_map.insert(std::make_pair(
385  target, --targets.cases.end())).first;
386  }
387 
388  exprt::operandst &case_op_dest=cases_entry->second->second;
389  case_op_dest.push_back(code.case_op());
390  }
391 }
392 
394  const codet &code,
395  goto_programt &dest,
396  const irep_idt &mode)
397 {
398  if(code.operands().size()!=3)
399  {
401  error() << "GCC's switch-case-range statement expected to have "
402  << "three operands" << eom;
403  throw 0;
404  }
405 
406  const auto lb = numeric_cast<mp_integer>(code.op0());
407  const auto ub = numeric_cast<mp_integer>(code.op1());
408 
409  if(!lb.has_value() || !ub.has_value())
410  {
412  error() << "GCC's switch-case-range statement requires constant bounds"
413  << eom;
414  throw 0;
415  }
416  else if(*lb > *ub)
417  {
419  warning() << "GCC's switch-case-range statement with empty case range"
420  << eom;
421  }
422 
423  goto_programt tmp;
424  convert(to_code(code.op2()), tmp, mode);
425 
426  goto_programt::targett target = tmp.instructions.begin();
427  dest.destructive_append(tmp);
428 
429  cases_mapt::iterator cases_entry = targets.cases_map.find(target);
430  if(cases_entry == targets.cases_map.end())
431  {
432  targets.cases.push_back({target, caset()});
433  cases_entry =
434  targets.cases_map.insert({target, --targets.cases.end()}).first;
435  }
436 
437  exprt::operandst &case_op_dest = cases_entry->second->second;
438 
439  for(mp_integer i = *lb; i <= *ub; ++i)
440  case_op_dest.push_back(from_integer(i, code.op0().type()));
441 }
442 
445  const codet &code,
446  goto_programt &dest,
447  const irep_idt &mode)
448 {
449  const irep_idt &statement=code.get_statement();
450 
451  if(statement==ID_block)
452  convert_block(to_code_block(code), dest, mode);
453  else if(statement==ID_decl)
454  convert_decl(to_code_decl(code), dest, mode);
455  else if(statement==ID_decl_type)
456  convert_decl_type(code, dest);
457  else if(statement==ID_expression)
458  convert_expression(to_code_expression(code), dest, mode);
459  else if(statement==ID_assign)
460  convert_assign(to_code_assign(code), dest, mode);
461  else if(statement==ID_init)
462  convert_init(code, dest, mode);
463  else if(statement==ID_assert)
464  convert_assert(to_code_assert(code), dest, mode);
465  else if(statement==ID_assume)
466  convert_assume(to_code_assume(code), dest, mode);
467  else if(statement==ID_function_call)
468  convert_function_call(to_code_function_call(code), dest, mode);
469  else if(statement==ID_label)
470  convert_label(to_code_label(code), dest, mode);
471  else if(statement==ID_gcc_local_label)
472  convert_gcc_local_label(code, dest);
473  else if(statement==ID_switch_case)
474  convert_switch_case(to_code_switch_case(code), dest, mode);
475  else if(statement==ID_gcc_switch_case_range)
476  convert_gcc_switch_case_range(code, dest, mode);
477  else if(statement==ID_for)
478  convert_for(to_code_for(code), dest, mode);
479  else if(statement==ID_while)
480  convert_while(to_code_while(code), dest, mode);
481  else if(statement==ID_dowhile)
482  convert_dowhile(code, dest, mode);
483  else if(statement==ID_switch)
484  convert_switch(to_code_switch(code), dest, mode);
485  else if(statement==ID_break)
486  convert_break(to_code_break(code), dest, mode);
487  else if(statement==ID_return)
488  convert_return(to_code_return(code), dest, mode);
489  else if(statement==ID_continue)
490  convert_continue(to_code_continue(code), dest, mode);
491  else if(statement==ID_goto)
492  convert_goto(to_code_goto(code), dest);
493  else if(statement==ID_gcc_computed_goto)
494  convert_gcc_computed_goto(code, dest);
495  else if(statement==ID_skip)
496  convert_skip(code, dest);
497  else if(statement==ID_ifthenelse)
498  convert_ifthenelse(to_code_ifthenelse(code), dest, mode);
499  else if(statement==ID_start_thread)
500  convert_start_thread(code, dest);
501  else if(statement==ID_end_thread)
502  convert_end_thread(code, dest);
503  else if(statement==ID_atomic_begin)
504  convert_atomic_begin(code, dest);
505  else if(statement==ID_atomic_end)
506  convert_atomic_end(code, dest);
507  else if(statement==ID_cpp_delete ||
508  statement=="cpp_delete[]")
509  convert_cpp_delete(code, dest);
510  else if(statement==ID_msc_try_except)
511  convert_msc_try_except(code, dest, mode);
512  else if(statement==ID_msc_try_finally)
513  convert_msc_try_finally(code, dest, mode);
514  else if(statement==ID_msc_leave)
515  convert_msc_leave(code, dest, mode);
516  else if(statement==ID_try_catch) // C++ try/catch
517  convert_try_catch(code, dest, mode);
518  else if(statement==ID_CPROVER_try_catch) // CPROVER-homemade
519  convert_CPROVER_try_catch(code, dest, mode);
520  else if(statement==ID_CPROVER_throw) // CPROVER-homemade
521  convert_CPROVER_throw(code, dest, mode);
522  else if(statement==ID_CPROVER_try_finally)
523  convert_CPROVER_try_finally(code, dest, mode);
524  else if(statement==ID_asm)
525  convert_asm(to_code_asm(code), dest);
526  else if(statement==ID_static_assert)
527  {
528  assert(code.operands().size()==2);
529  exprt assertion=code.op0();
530  assertion.make_typecast(bool_typet());
531  simplify(assertion, ns);
532  if(assertion.is_false())
533  {
535  error() << "static assertion "
536  << get_string_constant(code.op1()) << eom;
537  throw 0;
538  }
539  else if(assertion.is_true())
540  {
541  }
542  else
543  {
544  // we may wish to complain
545  }
546  }
547  else if(statement==ID_dead)
548  copy(code, DEAD, dest);
549  else if(statement==ID_decl_block)
550  {
551  forall_operands(it, code)
552  convert(to_code(*it), dest, mode);
553  }
554  else if(statement==ID_push_catch ||
555  statement==ID_pop_catch ||
556  statement==ID_exception_landingpad)
557  copy(code, CATCH, dest);
558  else
559  copy(code, OTHER, dest);
560 
561  // make sure dest is never empty
562  if(dest.instructions.empty())
563  {
564  dest.add_instruction(SKIP);
565  dest.instructions.back().code.make_nil();
566  dest.instructions.back().source_location=code.source_location();
567  }
568 }
569 
571  const code_blockt &code,
572  goto_programt &dest,
573  const irep_idt &mode)
574 {
575  const source_locationt &end_location=code.end_location();
576 
577  // this saves the size of the destructor stack
578  std::size_t old_stack_size=targets.destructor_stack.size();
579 
580  // now convert block
581  forall_operands(it, code)
582  {
583  const codet &b_code=to_code(*it);
584  convert(b_code, dest, mode);
585  }
586 
587  // see if we need to do any destructors -- may have been processed
588  // in a prior break/continue/return already, don't create dead code
589  if(!dest.empty() &&
590  dest.instructions.back().is_goto() &&
591  dest.instructions.back().guard.is_true())
592  {
593  // don't do destructors when we are unreachable
594  }
595  else
596  unwind_destructor_stack(end_location, old_stack_size, dest, mode);
597 
598  // remove those destructors
599  targets.destructor_stack.resize(old_stack_size);
600 }
601 
603  const code_expressiont &code,
604  goto_programt &dest,
605  const irep_idt &mode)
606 {
607  if(code.operands().size()!=1)
608  {
610  error() << "expression statement takes one operand" << eom;
611  throw 0;
612  }
613 
614  exprt expr=code.op0();
615 
616  if(expr.id()==ID_if)
617  {
618  // We do a special treatment for c?t:f
619  // by compiling to if(c) t; else f;
620  const if_exprt &if_expr=to_if_expr(expr);
621  code_ifthenelset tmp_code;
622  tmp_code.add_source_location()=expr.source_location();
623  tmp_code.cond()=if_expr.cond();
624  tmp_code.then_case()=code_expressiont(if_expr.true_case());
625  tmp_code.then_case().add_source_location()=expr.source_location();
626  tmp_code.else_case()=code_expressiont(if_expr.false_case());
627  tmp_code.else_case().add_source_location()=expr.source_location();
628  convert_ifthenelse(tmp_code, dest, mode);
629  }
630  else
631  {
632  clean_expr(expr, dest, mode, false); // result _not_ used
633 
634  // Any residual expression?
635  // We keep it to add checks later.
636  if(expr.is_not_nil())
637  {
638  codet tmp=code;
639  tmp.op0()=expr;
641  copy(tmp, OTHER, dest);
642  }
643  }
644 }
645 
647  const code_declt &code,
648  goto_programt &dest,
649  const irep_idt &mode)
650 {
651  const exprt &op = code.symbol();
652 
653  if(op.id() != ID_symbol)
654  {
656  error() << "decl statement expects symbol as operand" << eom;
657  throw 0;
658  }
659 
660  const irep_idt &identifier = to_symbol_expr(op).get_identifier();
661 
662  const symbolt &symbol = ns.lookup(identifier);
663 
664  if(symbol.is_static_lifetime ||
665  symbol.type.id()==ID_code)
666  return; // this is a SKIP!
667 
668  if(code.operands().size()==1)
669  {
670  copy(code, DECL, dest);
671  }
672  else
673  {
674  // this is expected to go away
675  exprt initializer;
676 
677  codet tmp=code;
678  initializer=code.op1();
679  tmp.operands().resize(1);
680 
681  // Break up into decl and assignment.
682  // Decl must be visible before initializer.
683  copy(tmp, DECL, dest);
684 
685  code_assignt assign(code.op0(), initializer);
686  assign.add_source_location()=tmp.source_location();
687 
688  convert_assign(assign, dest, mode);
689  }
690 
691  // now create a 'dead' instruction -- will be added after the
692  // destructor created below as unwind_destructor_stack pops off the
693  // top of the destructor stack
694  const symbol_exprt symbol_expr(symbol.name, symbol.type);
695 
696  {
697  code_deadt code_dead(symbol_expr);
698  targets.destructor_stack.push_back(code_dead);
699  }
700 
701  // do destructor
702  code_function_callt destructor=get_destructor(ns, symbol.type);
703 
704  if(destructor.is_not_nil())
705  {
706  // add "this"
707  address_of_exprt this_expr(symbol_expr, pointer_type(symbol.type));
708  destructor.arguments().push_back(this_expr);
709 
710  targets.destructor_stack.push_back(destructor);
711  }
712 }
713 
715  const codet &,
716  goto_programt &)
717 {
718  // we remove these
719 }
720 
722  const code_assignt &code,
723  goto_programt &dest,
724  const irep_idt &mode)
725 {
726  exprt lhs=code.lhs(),
727  rhs=code.rhs();
728 
729  clean_expr(lhs, dest, mode);
730 
731  if(rhs.id()==ID_side_effect &&
732  rhs.get(ID_statement)==ID_function_call)
733  {
734  if(rhs.operands().size()!=2)
735  {
736  error().source_location=rhs.find_source_location();
737  error() << "function_call sideeffect takes two operands" << eom;
738  throw 0;
739  }
740 
741  Forall_operands(it, rhs)
742  clean_expr(*it, dest, mode);
743 
744  do_function_call(lhs, rhs.op0(), rhs.op1().operands(), dest, mode);
745  }
746  else if(rhs.id()==ID_side_effect &&
747  (rhs.get(ID_statement)==ID_cpp_new ||
748  rhs.get(ID_statement)==ID_cpp_new_array))
749  {
750  Forall_operands(it, rhs)
751  clean_expr(*it, dest, mode);
752 
753  // TODO: This should be done in a separate pass
754  do_cpp_new(lhs, to_side_effect_expr(rhs), dest);
755  }
756  else if(
757  rhs.id() == ID_side_effect &&
758  (rhs.get(ID_statement) == ID_assign ||
759  rhs.get(ID_statement) == ID_postincrement ||
760  rhs.get(ID_statement) == ID_preincrement ||
761  rhs.get(ID_statement) == ID_statement_expression ||
762  rhs.get(ID_statement) == ID_gcc_conditional_expression))
763  {
764  // handle above side effects
765  clean_expr(rhs, dest, mode);
766 
767  if(lhs.id() == ID_typecast)
768  {
770  lhs.operands().size() == 1, "Typecast must have one operand");
771 
772  // add a typecast to the rhs
773  exprt new_rhs = rhs;
774  rhs.make_typecast(lhs.op0().type());
775 
776  // remove typecast from lhs
777  exprt tmp = lhs.op0();
778  lhs.swap(tmp);
779  }
780 
781  code_assignt new_assign(code);
782  new_assign.lhs() = lhs;
783  new_assign.rhs() = rhs;
784 
785  copy(new_assign, ASSIGN, dest);
786  }
787  else if(rhs.id() == ID_side_effect)
788  {
789  // preserve side effects that will be handled at later stages,
790  // such as allocate, new operators of other languages, e.g. java, etc
791  Forall_operands(it, rhs)
792  clean_expr(*it, dest, mode);
793 
794  code_assignt new_assign(code);
795  new_assign.lhs()=lhs;
796  new_assign.rhs()=rhs;
797 
798  copy(new_assign, ASSIGN, dest);
799  }
800  else
801  {
802  // do everything else
803  clean_expr(rhs, dest, mode);
804 
805  if(lhs.id()==ID_typecast)
806  {
807  assert(lhs.operands().size()==1);
808 
809  // add a typecast to the rhs
810  exprt new_rhs=rhs;
811  rhs.make_typecast(lhs.op0().type());
812 
813  // remove typecast from lhs
814  exprt tmp=lhs.op0();
815  lhs.swap(tmp);
816  }
817 
818  code_assignt new_assign(code);
819  new_assign.lhs()=lhs;
820  new_assign.rhs()=rhs;
821 
822  copy(new_assign, ASSIGN, dest);
823  }
824 }
825 
827  const codet &code,
828  goto_programt &dest,
829  const irep_idt &mode)
830 {
831  if(code.operands().size()!=2)
832  {
834  error() <<"init statement takes two operands" << eom;
835  throw 0;
836  }
837 
838  // make it an assignment
839  codet assignment=code;
840  assignment.set_statement(ID_assign);
841 
842  convert(to_code_assign(assignment), dest, mode);
843 }
844 
846  const codet &code,
847  goto_programt &dest)
848 {
849  if(code.operands().size()!=1)
850  {
852  error() << "cpp_delete statement takes one operand" << eom;
853  throw 0;
854  }
855 
856  exprt tmp_op=code.op0();
857 
858  clean_expr(tmp_op, dest, ID_cpp);
859 
860  // we call the destructor, and then free
861  const exprt &destructor=
862  static_cast<const exprt &>(code.find(ID_destructor));
863 
864  irep_idt delete_identifier;
865 
866  if(code.get_statement()==ID_cpp_delete_array)
867  delete_identifier="__delete_array";
868  else if(code.get_statement()==ID_cpp_delete)
869  delete_identifier="__delete";
870  else
871  UNREACHABLE;
872 
873  if(destructor.is_not_nil())
874  {
875  if(code.get_statement()==ID_cpp_delete_array)
876  {
877  // build loop
878  }
879  else if(code.get_statement()==ID_cpp_delete)
880  {
881  // just one object
882  const dereference_exprt deref_op(tmp_op);
883 
884  codet tmp_code=to_code(destructor);
885  replace_new_object(deref_op, tmp_code);
886  convert(tmp_code, dest, ID_cpp);
887  }
888  else
889  UNREACHABLE;
890  }
891 
892  // now do "free"
893  exprt delete_symbol=ns.lookup(delete_identifier).symbol_expr();
894 
895  assert(to_code_type(delete_symbol.type()).parameters().size()==1);
896 
897  typet arg_type=
898  to_code_type(delete_symbol.type()).parameters().front().type();
899 
900  code_function_callt delete_call;
901  delete_call.function()=delete_symbol;
902  delete_call.arguments().push_back(typecast_exprt(tmp_op, arg_type));
903  delete_call.lhs().make_nil();
904  delete_call.add_source_location()=code.source_location();
905 
906  convert(delete_call, dest, ID_cpp);
907 }
908 
910  const code_assertt &code,
911  goto_programt &dest,
912  const irep_idt &mode)
913 {
914  exprt cond=code.assertion();
915 
916  clean_expr(cond, dest, mode);
917 
919  t->guard.swap(cond);
920  t->source_location=code.source_location();
921  t->source_location.set(ID_property, ID_assertion);
922  t->source_location.set("user-provided", true);
923 }
924 
926  const codet &code,
927  goto_programt &dest)
928 {
930  t->source_location=code.source_location();
931  t->code=code;
932 }
933 
935  const code_assumet &code,
936  goto_programt &dest,
937  const irep_idt &mode)
938 {
939  exprt op=code.assumption();
940 
941  clean_expr(op, dest, mode);
942 
944  t->guard.swap(op);
945  t->source_location=code.source_location();
946 }
947 
949  const codet &code,
951  const irep_idt &mode)
952 {
953  exprt invariant=
954  static_cast<const exprt&>(code.find(ID_C_spec_loop_invariant));
955 
956  if(invariant.is_nil())
957  return;
958 
959  goto_programt no_sideeffects;
960  clean_expr(invariant, no_sideeffects, mode);
961  if(!no_sideeffects.instructions.empty())
962  {
964  error() << "loop invariant is not side-effect free" << eom;
965  throw 0;
966  }
967 
968  assert(loop->is_goto());
969  loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);
970 }
971 
973  const code_fort &code,
974  goto_programt &dest,
975  const irep_idt &mode)
976 {
977  // turn for(A; c; B) { P } into
978  // A; while(c) { P; B; }
979  //-----------------------------
980  // A;
981  // u: sideeffects in c
982  // v: if(!c) goto z;
983  // w: P;
984  // x: B; <-- continue target
985  // y: goto u;
986  // z: ; <-- break target
987 
988  // A;
989  if(code.init().is_not_nil())
990  convert(to_code(code.init()), dest, mode);
991 
992  exprt cond=code.cond();
993 
994  goto_programt sideeffects;
995  clean_expr(cond, sideeffects, mode);
996 
997  // save break/continue targets
998  break_continue_targetst old_targets(targets);
999 
1000  // do the u label
1001  goto_programt::targett u=sideeffects.instructions.begin();
1002 
1003  // do the v label
1004  goto_programt tmp_v;
1006 
1007  // do the z label
1008  goto_programt tmp_z;
1010  z->source_location=code.source_location();
1011 
1012  // do the x label
1013  goto_programt tmp_x;
1014 
1015  if(code.op2().is_nil())
1016  {
1017  tmp_x.add_instruction(SKIP);
1018  tmp_x.instructions.back().source_location=code.source_location();
1019  }
1020  else
1021  {
1022  exprt tmp_B=code.iter();
1023 
1024  clean_expr(tmp_B, tmp_x, mode, false);
1025 
1026  if(tmp_x.instructions.empty())
1027  {
1028  tmp_x.add_instruction(SKIP);
1029  tmp_x.instructions.back().source_location=code.source_location();
1030  }
1031  }
1032 
1033  // optimize the v label
1034  if(sideeffects.instructions.empty())
1035  u=v;
1036 
1037  // set the targets
1038  targets.set_break(z);
1039  targets.set_continue(tmp_x.instructions.begin());
1040 
1041  // v: if(!c) goto z;
1042  v->make_goto(z);
1043  v->guard=cond;
1044  v->guard.make_not();
1045  v->source_location=cond.source_location();
1046 
1047  // do the w label
1048  goto_programt tmp_w;
1049  convert(code.body(), tmp_w, mode);
1050 
1051  // y: goto u;
1052  goto_programt tmp_y;
1054  y->make_goto(u);
1055  y->guard=true_exprt();
1056  y->source_location=code.source_location();
1057 
1058  // loop invariant
1059  convert_loop_invariant(code, y, mode);
1060 
1061  dest.destructive_append(sideeffects);
1062  dest.destructive_append(tmp_v);
1063  dest.destructive_append(tmp_w);
1064  dest.destructive_append(tmp_x);
1065  dest.destructive_append(tmp_y);
1066  dest.destructive_append(tmp_z);
1067 
1068  // restore break/continue
1069  old_targets.restore(targets);
1070 }
1071 
1073  const code_whilet &code,
1074  goto_programt &dest,
1075  const irep_idt &mode)
1076 {
1077  const exprt &cond=code.cond();
1078  const source_locationt &source_location=code.source_location();
1079 
1080  // while(c) P;
1081  //--------------------
1082  // v: sideeffects in c
1083  // if(!c) goto z;
1084  // x: P;
1085  // y: goto v; <-- continue target
1086  // z: ; <-- break target
1087 
1088  // save break/continue targets
1089  break_continue_targetst old_targets(targets);
1090 
1091  // do the z label
1092  goto_programt tmp_z;
1094  z->make_skip();
1095  z->source_location=source_location;
1096 
1097  goto_programt tmp_branch;
1099  boolean_negate(cond), z, source_location, tmp_branch, mode);
1100 
1101  // do the v label
1102  goto_programt::targett v=tmp_branch.instructions.begin();
1103 
1104  // do the y label
1105  goto_programt tmp_y;
1107 
1108  // set the targets
1109  targets.set_break(z);
1110  targets.set_continue(y);
1111 
1112  // do the x label
1113  goto_programt tmp_x;
1114  convert(code.body(), tmp_x, mode);
1115 
1116  // y: if(c) goto v;
1117  y->make_goto(v);
1118  y->guard=true_exprt();
1119  y->source_location=code.source_location();
1120 
1121  // loop invariant
1122  convert_loop_invariant(code, y, mode);
1123 
1124  dest.destructive_append(tmp_branch);
1125  dest.destructive_append(tmp_x);
1126  dest.destructive_append(tmp_y);
1127  dest.destructive_append(tmp_z);
1128 
1129  // restore break/continue
1130  old_targets.restore(targets);
1131 }
1132 
1134  const codet &code,
1135  goto_programt &dest,
1136  const irep_idt &mode)
1137 {
1138  if(code.operands().size()!=2)
1139  {
1141  error() << "dowhile takes two operands" << eom;
1142  throw 0;
1143  }
1144 
1145  // save source location
1146  source_locationt condition_location=code.op0().find_source_location();
1147 
1148  exprt cond=code.op0();
1149 
1150  goto_programt sideeffects;
1151  clean_expr(cond, sideeffects, mode);
1152 
1153  // do P while(c);
1154  //--------------------
1155  // w: P;
1156  // x: sideeffects in c <-- continue target
1157  // y: if(c) goto w;
1158  // z: ; <-- break target
1159 
1160  // save break/continue targets
1161  break_continue_targetst old_targets(targets);
1162 
1163  // do the y label
1164  goto_programt tmp_y;
1166 
1167  // do the z label
1168  goto_programt tmp_z;
1170  z->make_skip();
1171  z->source_location=code.source_location();
1172 
1173  // do the x label
1175  if(sideeffects.instructions.empty())
1176  x=y;
1177  else
1178  x=sideeffects.instructions.begin();
1179 
1180  // set the targets
1181  targets.set_break(z);
1182  targets.set_continue(x);
1183 
1184  // do the w label
1185  goto_programt tmp_w;
1186  convert(to_code(code.op1()), tmp_w, mode);
1187  goto_programt::targett w=tmp_w.instructions.begin();
1188 
1189  // y: if(c) goto w;
1190  y->make_goto(w);
1191  y->guard=cond;
1192  y->source_location=condition_location;
1193 
1194  // loop invariant
1195  convert_loop_invariant(code, y, mode);
1196 
1197  dest.destructive_append(tmp_w);
1198  dest.destructive_append(sideeffects);
1199  dest.destructive_append(tmp_y);
1200  dest.destructive_append(tmp_z);
1201 
1202  // restore break/continue targets
1203  old_targets.restore(targets);
1204 }
1205 
1207  const exprt &value,
1208  const exprt::operandst &case_op)
1209 {
1210  exprt dest=exprt(ID_or, bool_typet());
1211  dest.reserve_operands(case_op.size());
1212 
1213  forall_expr(it, case_op)
1214  {
1215  equal_exprt eq_expr;
1216  eq_expr.lhs()=value;
1217  eq_expr.rhs()=*it;
1218  dest.move_to_operands(eq_expr);
1219  }
1220 
1221  assert(!dest.operands().empty());
1222 
1223  if(dest.operands().size()==1)
1224  {
1225  exprt tmp;
1226  tmp.swap(dest.op0());
1227  dest.swap(tmp);
1228  }
1229 
1230  return dest;
1231 }
1232 
1234  const code_switcht &code,
1235  goto_programt &dest,
1236  const irep_idt &mode)
1237 {
1238  // switch(v) {
1239  // case x: Px;
1240  // case y: Py;
1241  // ...
1242  // default: Pd;
1243  // }
1244  // --------------------
1245  // location
1246  // x: if(v==x) goto X;
1247  // y: if(v==y) goto Y;
1248  // goto d;
1249  // X: Px;
1250  // Y: Py;
1251  // d: Pd;
1252  // z: ;
1253 
1254  // we first add a 'location' node for the switch statement,
1255  // which would otherwise not be recorded
1256  dest.add_instruction()->make_location(
1257  code.source_location());
1258 
1259  // get the location of the end of the body, but
1260  // default to location of switch, if none
1261  source_locationt body_end_location=
1262  code.body().get_statement()==ID_block?
1263  to_code_block(code.body()).end_location():
1264  code.source_location();
1265 
1266  // do the value we switch over
1267  exprt argument=code.value();
1268 
1269  goto_programt sideeffects;
1270  clean_expr(argument, sideeffects, mode);
1271 
1272  // save break/default/cases targets
1273  break_switch_targetst old_targets(targets);
1274 
1275  // do the z label
1276  goto_programt tmp_z;
1278  z->make_skip();
1279  z->source_location=body_end_location;
1280 
1281  // set the new targets -- continue stays as is
1282  targets.set_break(z);
1283  targets.set_default(z);
1284  targets.cases.clear();
1285  targets.cases_map.clear();
1286 
1287  goto_programt tmp;
1288  convert(code.body(), tmp, mode);
1289 
1290  goto_programt tmp_cases;
1291 
1292  // The case number represents which case this corresponds to in the sequence
1293  // of case statements.
1294  //
1295  // switch (x)
1296  // {
1297  // case 2: // case_number 1
1298  // ...;
1299  // case 3: // case_number 2
1300  // ...;
1301  // case 10: // case_number 3
1302  // ...;
1303  // }
1304  size_t case_number=1;
1305  for(auto &case_pair : targets.cases)
1306  {
1307  const caset &case_ops=case_pair.second;
1308 
1309  assert(!case_ops.empty());
1310 
1311  exprt guard_expr=case_guard(argument, case_ops);
1312 
1313  source_locationt source_location=case_ops.front().find_source_location();
1314  source_location.set_case_number(std::to_string(case_number));
1315  case_number++;
1316  guard_expr.add_source_location()=source_location;
1317 
1318  goto_programt::targett x=tmp_cases.add_instruction();
1319  x->make_goto(case_pair.first);
1320  x->guard.swap(guard_expr);
1321  x->source_location=source_location;
1322  }
1323 
1324  {
1325  goto_programt::targett d_jump=tmp_cases.add_instruction();
1326  d_jump->make_goto(targets.default_target);
1327  d_jump->source_location=targets.default_target->source_location;
1328  }
1329 
1330  dest.destructive_append(sideeffects);
1331  dest.destructive_append(tmp_cases);
1332  dest.destructive_append(tmp);
1333  dest.destructive_append(tmp_z);
1334 
1335  // restore old targets
1336  old_targets.restore(targets);
1337 }
1338 
1340  const code_breakt &code,
1341  goto_programt &dest,
1342  const irep_idt &mode)
1343 {
1344  if(!targets.break_set)
1345  {
1347  error() << "break without target" << eom;
1348  throw 0;
1349  }
1350 
1351  // need to process destructor stack
1353  code.source_location(), targets.break_stack_size, dest, mode);
1354 
1355  // add goto
1357  t->make_goto(targets.break_target);
1358  t->source_location=code.source_location();
1359 }
1360 
1362  const code_returnt &code,
1363  goto_programt &dest,
1364  const irep_idt &mode)
1365 {
1366  if(!targets.return_set)
1367  {
1369  error() << "return without target" << eom;
1370  throw 0;
1371  }
1372 
1373  if(!code.operands().empty() &&
1374  code.operands().size()!=1)
1375  {
1377  error() << "return takes none or one operand" << eom;
1378  throw 0;
1379  }
1380 
1381  code_returnt new_code(code);
1382 
1383  if(new_code.has_return_value())
1384  {
1385  bool result_is_used=
1386  new_code.return_value().type().id()!=ID_empty;
1387 
1388  goto_programt sideeffects;
1389  clean_expr(new_code.return_value(), sideeffects, mode, result_is_used);
1390  dest.destructive_append(sideeffects);
1391 
1392  // remove void-typed return value
1393  if(!result_is_used)
1394  new_code.return_value().make_nil();
1395  }
1396 
1398  {
1399  if(!new_code.has_return_value())
1400  {
1402  error() << "function must return value" << eom;
1403  throw 0;
1404  }
1405 
1406  // Now add a return node to set the return value.
1408  t->make_return();
1409  t->code=new_code;
1410  t->source_location=new_code.source_location();
1411  }
1412  else
1413  {
1414  if(new_code.has_return_value() &&
1415  new_code.return_value().type().id()!=ID_empty)
1416  {
1418  error() << "function must not return value" << eom;
1419  throw 0;
1420  }
1421  }
1422 
1423  // Need to process _entire_ destructor stack.
1424  unwind_destructor_stack(code.source_location(), 0, dest, mode);
1425 
1426  // add goto to end-of-function
1428  t->make_goto(targets.return_target, true_exprt());
1429  t->source_location=new_code.source_location();
1430 }
1431 
1433  const code_continuet &code,
1434  goto_programt &dest,
1435  const irep_idt &mode)
1436 {
1437  if(!targets.continue_set)
1438  {
1440  error() << "continue without target" << eom;
1441  throw 0;
1442  }
1443 
1444  // need to process destructor stack
1446  code.source_location(), targets.continue_stack_size, dest, mode);
1447 
1448  // add goto
1450  t->make_goto(targets.continue_target);
1451  t->source_location=code.source_location();
1452 }
1453 
1455 {
1456  // this instruction will be completed during post-processing
1458  t->make_incomplete_goto(code);
1459  t->source_location=code.source_location();
1460 
1461  // remember it to do the target later
1462  targets.gotos.push_back(std::make_pair(t, targets.destructor_stack));
1463 }
1464 
1466  const codet &code,
1467  goto_programt &dest)
1468 {
1469  // this instruction will turn into OTHER during post-processing
1471  t->source_location=code.source_location();
1472  t->code=code;
1473 
1474  // remember it to do this later
1475  targets.computed_gotos.push_back(t);
1476 }
1477 
1479  const codet &code,
1480  goto_programt &dest)
1481 {
1482  goto_programt::targett start_thread=
1484  start_thread->source_location=code.source_location();
1485  start_thread->code=code;
1486 
1487  // remember it to do target later
1488  targets.gotos.push_back(
1489  std::make_pair(start_thread, targets.destructor_stack));
1490 }
1491 
1493  const codet &code,
1494  goto_programt &dest)
1495 {
1496  if(!code.operands().empty())
1497  {
1499  error() << "end_thread expects no operands" << eom;
1500  throw 0;
1501  }
1502 
1503  copy(code, END_THREAD, dest);
1504 }
1505 
1507  const codet &code,
1508  goto_programt &dest)
1509 {
1510  if(!code.operands().empty())
1511  {
1513  error() << "atomic_begin expects no operands" << eom;
1514  throw 0;
1515  }
1516 
1517  copy(code, ATOMIC_BEGIN, dest);
1518 }
1519 
1521  const codet &code,
1522  goto_programt &dest)
1523 {
1524  if(!code.operands().empty())
1525  {
1527  error() << "atomic_end expects no operands" << eom;
1528  throw 0;
1529  }
1530 
1531  copy(code, ATOMIC_END, dest);
1532 }
1533 
1535  const code_ifthenelset &code,
1536  goto_programt &dest,
1537  const irep_idt &mode)
1538 {
1539  if(code.operands().size()!=3)
1540  {
1542  error() << "ifthenelse takes three operands" << eom;
1543  throw 0;
1544  }
1545 
1546  assert(code.then_case().is_not_nil());
1547 
1548  bool has_else=
1549  !code.else_case().is_nil();
1550 
1551  const source_locationt &source_location=code.source_location();
1552 
1553  // We do a bit of special treatment for && in the condition
1554  // in case cleaning would be needed otherwise.
1555  if(code.cond().id()==ID_and &&
1556  code.cond().operands().size()==2 &&
1557  (needs_cleaning(code.cond().op0()) || needs_cleaning(code.cond().op1())) &&
1558  !has_else)
1559  {
1560  // if(a && b) XX --> if(a) if(b) XX
1561  code_ifthenelset new_if0, new_if1;
1562  new_if0.cond()=code.cond().op0();
1563  new_if1.cond()=code.cond().op1();
1564  new_if0.add_source_location()=source_location;
1565  new_if1.add_source_location()=source_location;
1566  new_if1.then_case()=code.then_case();
1567  new_if0.then_case()=new_if1;
1568  return convert_ifthenelse(new_if0, dest, mode);
1569  }
1570 
1571  // convert 'then'-branch
1572  goto_programt tmp_then;
1573  convert(code.then_case(), tmp_then, mode);
1574 
1575  goto_programt tmp_else;
1576 
1577  if(has_else)
1578  convert(code.else_case(), tmp_else, mode);
1579 
1580  exprt tmp_guard=code.cond();
1581  clean_expr(tmp_guard, dest, mode);
1582 
1584  tmp_guard, tmp_then, tmp_else, source_location, dest, mode);
1585 }
1586 
1588  const exprt &expr,
1589  const irep_idt &id,
1590  std::list<exprt> &dest)
1591 {
1592  if(expr.id()!=id)
1593  {
1594  dest.push_back(expr);
1595  }
1596  else
1597  {
1598  // left-to-right is important
1599  forall_operands(it, expr)
1600  collect_operands(*it, id, dest);
1601  }
1602 }
1603 
1607 static inline bool is_size_one(const goto_programt &g)
1608 {
1609  return (!g.instructions.empty()) &&
1610  ++g.instructions.begin()==g.instructions.end();
1611 }
1612 
1615  const exprt &guard,
1616  goto_programt &true_case,
1617  goto_programt &false_case,
1618  const source_locationt &source_location,
1619  goto_programt &dest,
1620  const irep_idt &mode)
1621 {
1622  if(is_empty(true_case) &&
1623  is_empty(false_case))
1624  {
1625  // hmpf. Useless branch.
1626  goto_programt tmp_z;
1628  z->make_skip();
1630  v->make_goto(z, guard);
1631  v->source_location=source_location;
1632  dest.destructive_append(tmp_z);
1633  return;
1634  }
1635 
1636  // do guarded assertions directly
1637  if(is_size_one(true_case) &&
1638  true_case.instructions.back().is_assert() &&
1639  true_case.instructions.back().guard.is_false() &&
1640  true_case.instructions.back().labels.empty())
1641  {
1642  // The above conjunction deliberately excludes the instance
1643  // if(some) { label: assert(false); }
1644  true_case.instructions.back().guard=boolean_negate(guard);
1645  dest.destructive_append(true_case);
1646  true_case.instructions.clear();
1647  if(
1648  is_empty(false_case) ||
1649  (is_size_one(false_case) &&
1650  is_skip(false_case, false_case.instructions.begin())))
1651  return;
1652  }
1653 
1654  // similarly, do guarded assertions directly
1655  if(is_size_one(false_case) &&
1656  false_case.instructions.back().is_assert() &&
1657  false_case.instructions.back().guard.is_false() &&
1658  false_case.instructions.back().labels.empty())
1659  {
1660  // The above conjunction deliberately excludes the instance
1661  // if(some) ... else { label: assert(false); }
1662  false_case.instructions.back().guard=guard;
1663  dest.destructive_append(false_case);
1664  false_case.instructions.clear();
1665  if(
1666  is_empty(true_case) ||
1667  (is_size_one(true_case) &&
1668  is_skip(true_case, true_case.instructions.begin())))
1669  return;
1670  }
1671 
1672  // a special case for C libraries that use
1673  // (void)((cond) || (assert(0),0))
1674  if(
1675  is_empty(false_case) && true_case.instructions.size() == 2 &&
1676  true_case.instructions.front().is_assert() &&
1677  true_case.instructions.front().guard.is_false() &&
1678  true_case.instructions.front().labels.empty() &&
1679  true_case.instructions.back().labels.empty())
1680  {
1681  true_case.instructions.front().guard = boolean_negate(guard);
1682  true_case.instructions.erase(--true_case.instructions.end());
1683  dest.destructive_append(true_case);
1684  true_case.instructions.clear();
1685 
1686  return;
1687  }
1688 
1689  // Flip around if no 'true' case code.
1690  if(is_empty(true_case))
1691  return generate_ifthenelse(
1692  boolean_negate(guard),
1693  false_case,
1694  true_case,
1695  source_location,
1696  dest,
1697  mode);
1698 
1699  bool has_else=!is_empty(false_case);
1700 
1701  // if(c) P;
1702  //--------------------
1703  // v: if(!c) goto z;
1704  // w: P;
1705  // z: ;
1706 
1707  // if(c) P; else Q;
1708  //--------------------
1709  // v: if(!c) goto y;
1710  // w: P;
1711  // x: goto z;
1712  // y: Q;
1713  // z: ;
1714 
1715  // do the x label
1716  goto_programt tmp_x;
1718 
1719  // do the z label
1720  goto_programt tmp_z;
1722  z->make_skip();
1723  // We deliberately don't set a location for 'z', it's a dummy
1724  // target.
1725 
1726  // y: Q;
1727  goto_programt tmp_y;
1729  if(has_else)
1730  {
1731  tmp_y.swap(false_case);
1732  y=tmp_y.instructions.begin();
1733  }
1734 
1735  // v: if(!c) goto z/y;
1736  goto_programt tmp_v;
1738  boolean_negate(guard), has_else ? y : z, source_location, tmp_v, mode);
1739 
1740  // w: P;
1741  goto_programt tmp_w;
1742  tmp_w.swap(true_case);
1743 
1744  // x: goto z;
1745  x->make_goto(z);
1746  assert(!tmp_w.instructions.empty());
1747  x->source_location=tmp_w.instructions.back().source_location;
1748 
1749  dest.destructive_append(tmp_v);
1750  dest.destructive_append(tmp_w);
1751 
1752  if(has_else)
1753  {
1754  dest.destructive_append(tmp_x);
1755  dest.destructive_append(tmp_y);
1756  }
1757 
1758  dest.destructive_append(tmp_z);
1759 }
1760 
1762 static bool has_and_or(const exprt &expr)
1763 {
1764  forall_operands(it, expr)
1765  if(has_and_or(*it))
1766  return true;
1767 
1768  if(expr.id()==ID_and || expr.id()==ID_or)
1769  return true;
1770 
1771  return false;
1772 }
1773 
1775  const exprt &guard,
1776  goto_programt::targett target_true,
1777  const source_locationt &source_location,
1778  goto_programt &dest,
1779  const irep_idt &mode)
1780 {
1781  if(has_and_or(guard) && needs_cleaning(guard))
1782  {
1783  // if(guard) goto target;
1784  // becomes
1785  // if(guard) goto target; else goto next;
1786  // next: skip;
1787 
1788  goto_programt tmp;
1789  goto_programt::targett target_false=tmp.add_instruction();
1790  target_false->make_skip();
1791  target_false->source_location=source_location;
1792 
1794  guard, target_true, target_false, source_location, dest, mode);
1795 
1796  dest.destructive_append(tmp);
1797  }
1798  else
1799  {
1800  // simple branch
1801  exprt cond=guard;
1802  clean_expr(cond, dest, mode);
1803 
1804  goto_programt tmp;
1806  g->make_goto(target_true);
1807  g->guard=cond;
1808  g->source_location=source_location;
1809  dest.destructive_append(tmp);
1810  }
1811 }
1812 
1815  const exprt &guard,
1816  goto_programt::targett target_true,
1817  goto_programt::targett target_false,
1818  const source_locationt &source_location,
1819  goto_programt &dest,
1820  const irep_idt &mode)
1821 {
1822  if(guard.id()==ID_not)
1823  {
1824  assert(guard.operands().size()==1);
1825  // simply swap targets
1827  guard.op0(), target_false, target_true, source_location, dest, mode);
1828  return;
1829  }
1830 
1831  if(guard.id()==ID_and)
1832  {
1833  // turn
1834  // if(a && b) goto target_true; else goto target_false;
1835  // into
1836  // if(!a) goto target_false;
1837  // if(!b) goto target_false;
1838  // goto target_true;
1839 
1840  std::list<exprt> op;
1841  collect_operands(guard, guard.id(), op);
1842 
1843  for(const auto &expr : op)
1845  boolean_negate(expr), target_false, source_location, dest, mode);
1846 
1848  t_true->make_goto(target_true);
1849  t_true->guard=true_exprt();
1850  t_true->source_location=source_location;
1851 
1852  return;
1853  }
1854  else if(guard.id()==ID_or)
1855  {
1856  // turn
1857  // if(a || b) goto target_true; else goto target_false;
1858  // into
1859  // if(a) goto target_true;
1860  // if(b) goto target_true;
1861  // goto target_false;
1862 
1863  std::list<exprt> op;
1864  collect_operands(guard, guard.id(), op);
1865 
1866  for(const auto &expr : op)
1868  expr, target_true, source_location, dest, mode);
1869 
1870  goto_programt::targett t_false=dest.add_instruction();
1871  t_false->make_goto(target_false);
1872  t_false->guard=true_exprt();
1873  t_false->source_location=guard.source_location();
1874 
1875  return;
1876  }
1877 
1878  exprt cond=guard;
1879  clean_expr(cond, dest, mode);
1880 
1882  t_true->make_goto(target_true);
1883  t_true->guard=cond;
1884  t_true->source_location=source_location;
1885 
1886  goto_programt::targett t_false=dest.add_instruction();
1887  t_false->make_goto(target_false);
1888  t_false->guard=true_exprt();
1889  t_false->source_location=source_location;
1890 }
1891 
1893  const exprt &expr,
1894  irep_idt &value)
1895 {
1896  if(expr.id()==ID_typecast &&
1897  expr.operands().size()==1)
1898  return get_string_constant(expr.op0(), value);
1899 
1900  if(expr.id()==ID_address_of &&
1901  expr.operands().size()==1 &&
1902  expr.op0().id()==ID_index &&
1903  expr.op0().operands().size()==2)
1904  {
1905  exprt index_op=get_constant(expr.op0().op0());
1906  simplify(index_op, ns);
1907 
1908  if(index_op.id()==ID_string_constant)
1909  return value=index_op.get(ID_value), false;
1910  else if(index_op.id()==ID_array)
1911  {
1912  std::string result;
1913  forall_operands(it, index_op)
1914  if(it->is_constant())
1915  {
1916  unsigned long i=integer2ulong(
1918 
1919  if(i!=0) // to skip terminating 0
1920  result+=static_cast<char>(i);
1921  }
1922 
1923  return value=result, false;
1924  }
1925  }
1926 
1927  if(expr.id()==ID_string_constant)
1928  return value=expr.get(ID_value), false;
1929 
1930  return true;
1931 }
1932 
1934 {
1935  irep_idt result;
1936 
1937  if(get_string_constant(expr, result))
1938  {
1940  error() << "expected string constant, but got: "
1941  << expr.pretty() << eom;
1942 
1943  throw 0;
1944  }
1945 
1946  return result;
1947 }
1948 
1950 {
1951  if(expr.id()==ID_symbol)
1952  {
1953  const symbolt &symbol=
1954  ns.lookup(to_symbol_expr(expr));
1955 
1956  return symbol.value;
1957  }
1958  else if(expr.id()==ID_member)
1959  {
1960  exprt tmp=expr;
1961  tmp.op0()=get_constant(expr.op0());
1962  return tmp;
1963  }
1964  else if(expr.id()==ID_index)
1965  {
1966  exprt tmp=expr;
1967  tmp.op0()=get_constant(expr.op0());
1968  tmp.op1()=get_constant(expr.op1());
1969  return tmp;
1970  }
1971  else
1972  return expr;
1973 }
1974 
1976  const typet &type,
1977  const std::string &suffix,
1978  goto_programt &dest,
1979  const source_locationt &source_location,
1980  const irep_idt &mode)
1981 {
1982  PRECONDITION(!mode.empty());
1983  symbolt &new_symbol = get_fresh_aux_symbol(
1984  type,
1986  "tmp_" + suffix,
1987  source_location,
1988  mode,
1989  symbol_table);
1990 
1991  code_declt decl(new_symbol.symbol_expr());
1992  decl.add_source_location()=source_location;
1993  convert_decl(decl, dest, mode);
1994 
1995  return new_symbol;
1996 }
1997 
1999  exprt &expr,
2000  const std::string &suffix,
2001  goto_programt &dest,
2002  const irep_idt &mode)
2003 {
2004  const source_locationt source_location=expr.find_source_location();
2005 
2006  symbolt &new_symbol =
2007  new_tmp_symbol(expr.type(), suffix, dest, source_location, mode);
2008 
2009  code_assignt assignment;
2010  assignment.lhs()=new_symbol.symbol_expr();
2011  assignment.rhs()=expr;
2012  assignment.add_source_location()=source_location;
2013 
2014  convert(assignment, dest, mode);
2015 
2016  expr=new_symbol.symbol_expr();
2017 }
2018 
2020  const codet &code,
2021  symbol_table_baset &symbol_table,
2022  goto_programt &dest,
2024  const irep_idt &mode)
2025 {
2026  const std::size_t errors_before=
2027  message_handler.get_message_count(messaget::M_ERROR);
2028 
2030 
2031  try
2032  {
2033  goto_convert.goto_convert(code, dest, mode);
2034  }
2035 
2036  catch(int)
2037  {
2038  goto_convert.error();
2039  }
2040 
2041  catch(const char *e)
2042  {
2043  goto_convert.error() << e << messaget::eom;
2044  }
2045 
2046  catch(const std::string &e)
2047  {
2048  goto_convert.error() << e << messaget::eom;
2049  }
2050 
2051  if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
2052  throw 0;
2053 }
2054 
2056  symbol_table_baset &symbol_table,
2057  goto_programt &dest,
2059 {
2060  // find main symbol
2061  const symbol_tablet::symbolst::const_iterator s_it=
2062  symbol_table.symbols.find("main");
2063 
2064  if(s_it==symbol_table.symbols.end())
2065  throw "failed to find main symbol";
2066 
2067  const symbolt &symbol=s_it->second;
2068 
2070  to_code(symbol.value), symbol_table, dest, message_handler, symbol.mode);
2071 }
2072 
2087  const code_blockt &thread_body,
2088  goto_programt &dest,
2089  const irep_idt &mode)
2090 {
2091  goto_programt preamble, body, postamble;
2092 
2094  c->make_skip();
2095  convert(thread_body, body, mode);
2096 
2098  e->source_location=thread_body.source_location();
2100  z->make_skip();
2101 
2103  a->source_location=thread_body.source_location();
2104  a->targets.push_back(c);
2106  b->source_location=thread_body.source_location();
2107  b->make_goto(z);
2108 
2109  dest.destructive_append(preamble);
2110  dest.destructive_append(body);
2111  dest.destructive_append(postamble);
2112 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
void convert_atomic_begin(const codet &code, goto_programt &dest)
const irep_idt & get_statement() const
Definition: std_code.h:40
static bool is_empty(const goto_programt &goto_program)
The type of an expression.
Definition: type.h:22
irep_idt get_string_constant(const exprt &expr)
irep_idt name
The unique identifier.
Definition: symbol.h:43
void convert_skip(const codet &code, goto_programt &dest)
const codet & then_case() const
Definition: std_code.h:486
const exprt & return_value() const
Definition: std_code.h:937
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:291
exprt & true_case()
Definition: std_expr.h:3393
std::vector< exception_list_entryt > exception_listt
Definition: std_code.h:1589
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
exprt::operandst caset
A ‘switch’ instruction.
Definition: std_code.h:538
void set_case_number(const irep_idt &number)
void convert_gcc_switch_case_range(const codet &code, goto_programt &dest, const irep_idt &mode)
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
const exprt & init() const
Definition: std_code.h:736
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
goto_programt::targett return_target
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
const code_assumet & to_code_assume(const codet &code)
Definition: std_code.h:390
const exprt & cond() const
Definition: std_code.h:617
A continue for ‘for’ and ‘while’ loops.
Definition: std_code.h:1145
void convert_switch(const code_switcht &code, goto_programt &dest, const irep_idt &mode)
struct goto_convertt::targetst targets
static void finish_catch_push_targets(goto_programt &dest)
Populate the CATCH instructions with the targets corresponding to their associated labels...
irep_idt mode
Language mode.
Definition: symbol.h:52
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts &#39;code&#39; and appends the result to &#39;dest&#39;
const exprt & cond() const
Definition: std_code.h:476
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
exprt & symbol()
Definition: std_code.h:268
mp_integer::ullong_t integer2ulong(const mp_integer &n)
Definition: mp_arith.cpp:189
void finish_gotos(goto_programt &dest, const irep_idt &mode)
const codet & body() const
Definition: std_code.h:766
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Deprecated expression utility functions.
goto_programt::targett break_target
codet & code()
Definition: std_code.h:1080
void convert_assert(const code_assertt &code, goto_programt &dest, const irep_idt &mode)
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;
void convert_label(const code_labelt &code, goto_programt &dest, const irep_idt &mode)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:993
const irep_idt & get_identifier() const
Definition: std_expr.h:128
source_locationt end_location() const
Definition: std_code.h:126
#define forall_expr(it, expr)
Definition: expr.h:28
Destructor Calls.
void convert_gcc_computed_goto(const codet &code, goto_programt &dest)
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
Fresh auxiliary symbol creation.
void convert_atomic_end(const codet &code, goto_programt &dest)
const irep_idt & get_value() const
Definition: std_expr.h:4439
const code_breakt & to_code_break(const codet &code)
Definition: std_code.h:1131
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
Definition: goto_program.h:486
exprt value
Initial value of symbol.
Definition: symbol.h:37
void convert_assume(const code_assumet &code, goto_programt &dest, const irep_idt &mode)
The trinary if-then-else operator.
Definition: std_expr.h:3359
exprt & cond()
Definition: std_expr.h:3383
void convert_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
A ‘goto’ instruction.
Definition: std_code.h:803
typet & type()
Definition: expr.h:56
The proper Booleans.
Definition: std_types.h:34
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void convert_end_thread(const codet &code, goto_programt &dest)
static const unsigned nil_target
Uniquely identify an invalid target or location.
Definition: goto_program.h:357
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
void convert_dowhile(const codet &code, goto_programt &dest, const irep_idt &mode)
An expression statement.
Definition: std_code.h:1220
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1255
void set_default(goto_programt::targett _default_target)
bool is_static_lifetime
Definition: symbol.h:67
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
const exprt & case_op() const
Definition: std_code.h:1070
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1326
targetst targets
The list of successor instructions.
Definition: goto_program.h:198
mstreamt & warning() const
Definition: message.h:307
equality
Definition: std_expr.h:1354
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
void convert_return(const code_returnt &code, goto_programt &dest, const irep_idt &mode)
destructor_stackt destructor_stack
void convert_expression(const code_expressiont &code, goto_programt &dest, const irep_idt &mode)
void convert_ifthenelse(const code_ifthenelset &code, goto_programt &dest, const irep_idt &mode)
static void collect_operands(const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
void convert_block(const code_blockt &code, goto_programt &dest, const irep_idt &mode)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:240
void convert_loop_invariant(const codet &code, goto_programt::targett loop, const irep_idt &mode)
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:209
void convert_decl_type(const codet &code, goto_programt &dest)
void goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_switch_case(const code_switch_caset &code, goto_programt &dest, const irep_idt &mode)
void add(const codet &code)
Definition: std_code.h:112
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
The boolean constant true.
Definition: std_expr.h:4486
void convert_decl(const code_declt &code, goto_programt &dest, const irep_idt &mode)
argumentst & arguments()
Definition: std_code.h:890
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
std::string tmp_symbol_prefix
instructionst::iterator targett
Definition: goto_program.h:397
A declaration of a local variable.
Definition: std_code.h:254
static code_push_catcht & to_code_push_catch(codet &code)
Definition: std_code.h:1617
void complete_goto(targett _target)
Definition: goto_program.h:275
exprt & rhs()
Definition: std_code.h:214
const source_locationt & find_source_location() const
Definition: expr.cpp:246
const exprt & cond() const
Definition: std_code.h:746
source_locationt source_location
Definition: message.h:214
The empty type.
Definition: std_types.h:54
Operator to dereference a pointer.
Definition: std_expr.h:3282
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:648
Program Transformation.
void convert_init(const codet &code, goto_programt &dest, const irep_idt &mode)
void convert_function_call(const code_function_callt &code, goto_programt &dest, const irep_idt &mode)
goto_programt::targett default_target
exprt case_guard(const exprt &value, const caset &case_op)
const code_gotot & to_code_goto(const codet &code)
Definition: std_code.h:837
void goto_convert_rec(const codet &code, goto_programt &dest, const irep_idt &mode)
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:122
API to expression classes.
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
mstreamt & error() const
Definition: message.h:302
A label for branch targets.
Definition: std_code.h:977
void convert_assign(const code_assignt &code, goto_programt &dest, const irep_idt &mode)
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
goto_program_instruction_typet
The type of an instruction in a GOTO program.
Definition: goto_program.h:29
targett insert_after(const_targett target)
Insertion after the given target.
Definition: goto_program.h:480
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:963
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
Definition: goto_program.h:495
A function call.
Definition: std_code.h:858
#define forall_operands(it, expr)
Definition: expr.h:17
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
void convert_CPROVER_throw(const codet &code, goto_programt &dest, const irep_idt &mode)
A ‘while’ instruction.
Definition: std_code.h:601
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:1101
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
void convert_msc_leave(const codet &code, goto_programt &dest, const irep_idt &mode)
Author: Diffblue Ltd.
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
void convert_asm(const code_asmt &code, goto_programt &dest)
Definition: goto_asm.cpp:14
void finish_computed_gotos(goto_programt &dest)
Operator to return the address of an object.
Definition: std_expr.h:3168
void convert_cpp_delete(const codet &code, goto_programt &dest)
exprt & false_case()
Definition: std_expr.h:3403
const symbolst & symbols
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
const codet & body() const
Definition: std_code.h:564
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.
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:585
void convert_gcc_local_label(const codet &code, goto_programt &dest)
void convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode)
bool has_return_value() const
Definition: std_code.h:947
std::vector< exprt > operandst
Definition: expr.h:45
void swap(goto_programt &program)
Swap the goto program.
Definition: goto_program.h:605
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
static bool is_size_one(const goto_programt &g)
This is (believed to be) faster than using std::list.size.
A non-fatal assertion, which checks a condition then permits execution to continue.
Definition: std_code.h:404
An assumption, which must hold in subsequent code.
Definition: std_code.h:357
exprt get_constant(const exprt &expr)
void set_continue(goto_programt::targett _continue_target)
const exprt & value() const
Definition: std_code.h:554
typet type
Type of symbol.
Definition: symbol.h:34
void convert_while(const code_whilet &code, goto_programt &dest, const irep_idt &mode)
const code_continuet & to_code_continue(const codet &code)
Definition: std_code.h:1161
void make_not()
Definition: expr.cpp:91
static bool needs_cleaning(const exprt &expr)
goto_programt::targett continue_target
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...
mstreamt & result() const
Definition: message.h:312
void set_break(goto_programt::targett _break_target)
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, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
exprt & function()
Definition: std_code.h:878
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
void set_statement(const irep_idt &statement)
Definition: std_code.h:35
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
bool is_default() const
Definition: std_code.h:1060
Base class for all expressions.
Definition: expr.h:42
A break for ‘for’ and ‘while’ loops.
Definition: std_code.h:1115
The symbol table base class interface.
const exprt & assumption() const
Definition: std_code.h:371
computed_gotost computed_gotos
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const source_locationt & source_location() const
Definition: expr.h:125
bool empty() const
Is the program empty?
Definition: goto_program.h:590
const exprt & iter() const
Definition: std_code.h:756
void convert_msc_try_except(const codet &code, goto_programt &dest, const irep_idt &mode)
#define UNREACHABLE
Definition: invariant.h:271
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
void unwind_destructor_stack(const source_locationt &, std::size_t stack_size, goto_programt &dest, const irep_idt &mode)
Program Transformation.
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest, const irep_idt &mode)
symbol_table_baset & symbol_table
A removal of a local variable.
Definition: std_code.h:307
void make_nil()
Definition: irep.h:315
void swap(irept &irep)
Definition: irep.h:303
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
#define Forall_operands(it, expr)
Definition: expr.h:23
goto_programt & goto_program
Definition: cover.cpp:63
void convert_msc_try_finally(const codet &code, goto_programt &dest, const irep_idt &mode)
source_locationt & add_source_location()
Definition: expr.h:130
void convert_break(const code_breakt &code, goto_programt &dest, const irep_idt &mode)
Sequential composition.
Definition: std_code.h:89
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
const codet & to_code(const exprt &expr)
Definition: std_code.h:75
const irep_idt & get_label() const
Definition: std_code.h:1000
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:787
An if-then-else.
Definition: std_code.h:466
Expression to hold a symbol (variable)
Definition: std_expr.h:90
void convert_continue(const code_continuet &code, goto_programt &dest, const irep_idt &mode)
exprt & op2()
Definition: expr.h:78
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:165
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
A switch-case.
Definition: std_code.h:1045
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
mstreamt & debug() const
Definition: message.h:332
A statement in a programming language.
Definition: std_code.h:21
Return from a function.
Definition: std_code.h:923
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode)
code_function_callt get_destructor(const namespacet &ns, const typet &type)
Definition: destructor.cpp:18
A ‘for’ instruction.
Definition: std_code.h:727
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:1031
Program Transformation.
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:437
operandst & operands()
Definition: expr.h:66
void convert_start_thread(const codet &code, goto_programt &dest)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
const codet & else_case() const
Definition: std_code.h:496
exception_listt & exception_list()
Definition: std_code.h:1600
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:522
bool empty() const
Definition: dstring.h:73
void make_typecast(const typet &_type)
Definition: expr.cpp:84
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
Definition: expr_util.cpp:126
static void replace_new_object(const exprt &object, exprt &dest)
const codet & body() const
Definition: std_code.h:627
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
static bool has_and_or(const exprt &expr)
if(guard) goto target;
code_asmt & to_code_asm(codet &code)
Definition: std_code.h:1206
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
Assignment.
Definition: std_code.h:196
void convert_goto(const code_gotot &code, goto_programt &dest)
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
void reserve_operands(operandst::size_type n)
Definition: expr.h:96
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909
bool simplify(exprt &expr, const namespacet &ns)
const exprt & assertion() const
Definition: std_code.h:418
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;