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