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