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/cprover_prefix.h>
17 #include <util/expr_util.h>
18 #include <util/fresh_symbol.h>
19 #include <util/prefix.h>
20 #include <util/std_expr.h>
21 #include <util/symbol_table.h>
22 #include <util/simplify_expr.h>
23 #include <util/rename.h>
24 
25 #include <util/c_types.h>
26 
27 #include "goto_convert_class.h"
28 #include "destructor.h"
29 
30 static bool is_empty(const goto_programt &goto_program)
31 {
32  forall_goto_program_instructions(it, goto_program)
33  if(!it->is_skip() ||
34  !it->labels.empty() ||
35  !it->code.is_nil())
36  return false;
37 
38  return true;
39 }
40 
44 {
45  std::map<irep_idt, goto_programt::targett> label_targets;
46 
47  // in the first pass collect the labels and the corresponding targets
49  {
50  if(!it->labels.empty())
51  {
52  for(auto label : it->labels)
53  // record the label and the corresponding target
54  label_targets.insert(std::make_pair(label, it));
55  }
56  }
57 
58  // in the second pass set the targets
60  {
61  if(it->is_catch())
62  {
63  bool handler_added=true;
64  irept exceptions=it->code.find(ID_exception_list);
65 
66  if(exceptions.is_nil() &&
67  it->code.has_operands())
68  exceptions=it->code.op0().find(ID_exception_list);
69 
70  const irept::subt &exception_list=exceptions.get_sub();
71 
72  if(!exception_list.empty())
73  {
74  // in this case we have a CATCH_PUSH
75  irept handlers=it->code.find(ID_label);
76  if(handlers.is_nil() &&
77  it->code.has_operands())
78  handlers=it->code.op0().find(ID_label);
79  const irept::subt &handler_list=handlers.get_sub();
80 
81  // some handlers may not have been converted (if there was no
82  // exception to be caught); in such a situation we abort
83  for(const auto &handler : handler_list)
84  {
85  if(label_targets.find(handler.id())==label_targets.end())
86  {
87  handler_added=false;
88  break;
89  }
90  }
91 
92  if(!handler_added)
93  continue;
94 
95  for(const auto &handler : handler_list)
96  {
97  std::map<irep_idt,
98  goto_programt::targett>::const_iterator handler_it=
99  label_targets.find(handler.id());
100  assert(handler_it!=label_targets.end());
101  // set the target
102  it->targets.push_back(handler_it->second);
103  }
104  }
105  }
106  }
107 }
108 
109 /******************************************************************* \
110 
111 Function: goto_convertt::finish_gotos
112 
113  Inputs:
114 
115  Outputs:
116 
117  Purpose:
118 
119 \*******************************************************************/
120 
122 {
123  for(const auto &g_it : targets.gotos)
124  {
125  goto_programt::instructiont &i=*(g_it.first);
126 
127  if(i.code.get_statement()=="non-deterministic-goto")
128  {
129  const irept &destinations=i.code.find("destinations");
130 
131  i.make_goto();
132 
133  forall_irep(it, destinations.get_sub())
134  {
135  labelst::const_iterator l_it=
136  targets.labels.find(it->id_string());
137 
138  if(l_it==targets.labels.end())
139  {
140  error().source_location=i.code.find_source_location();
141  error() << "goto label `" << it->id() << "' not found" << eom;
142  throw 0;
143  }
144 
145  i.targets.push_back(l_it->second.first);
146  }
147  }
148  else if(i.is_start_thread())
149  {
150  const irep_idt &goto_label=i.code.get(ID_destination);
151 
152  labelst::const_iterator l_it=
153  targets.labels.find(goto_label);
154 
155  if(l_it==targets.labels.end())
156  {
157  error().source_location=i.code.find_source_location();
158  error() << "goto label `" << goto_label << "' not found" << eom;
159  throw 0;
160  }
161 
162  i.targets.push_back(l_it->second.first);
163  }
164  else if(i.code.get_statement()==ID_goto)
165  {
166  const irep_idt &goto_label=i.code.get(ID_destination);
167 
168  labelst::const_iterator l_it=targets.labels.find(goto_label);
169 
170  if(l_it==targets.labels.end())
171  {
172  error().source_location=i.code.find_source_location();
173  error() << "goto label `" << goto_label << "' not found" << eom;
174  throw 0;
175  }
176 
177  i.targets.clear();
178  i.targets.push_back(l_it->second.first);
179 
180  // If the goto recorded a destructor stack, execute as much as is
181  // appropriate for however many automatic variables leave scope.
182  // We don't currently handle variables *entering* scope, which is illegal
183  // for C++ non-pod types and impossible in Java in any case.
184  auto goto_stack=g_it.second;
185  const auto &label_stack=l_it->second.second;
186  bool stack_is_prefix=true;
187  if(label_stack.size()>goto_stack.size())
188  stack_is_prefix=false;
189  for(unsigned i=0, ilim=label_stack.size();
190  i!=ilim && stack_is_prefix;
191  ++i)
192  {
193  if(goto_stack[i]!=label_stack[i])
194  stack_is_prefix=false;
195  }
196 
197  if(!stack_is_prefix)
198  {
199  debug().source_location=i.code.find_source_location();
200  debug() << "encountered goto `" << goto_label
201  << "' that enters one or more lexical blocks; "
202  << "omitting constructors and destructors" << eom;
203  }
204  else
205  {
206  auto unwind_to_size=label_stack.size();
207  if(unwind_to_size<goto_stack.size())
208  {
209  debug().source_location=i.code.find_source_location();
210  debug() << "adding goto-destructor code on jump to `"
211  << goto_label << "'" << eom;
212  goto_programt destructor_code;
214  i.code.add_source_location(),
215  unwind_to_size,
216  destructor_code,
217  goto_stack);
218  dest.destructive_insert(g_it.first, destructor_code);
219  // This should leave iterators intact, as long as
220  // goto_programt::instructionst is std::list.
221  }
222  }
223  }
224  else
225  {
226  error().source_location=i.code.find_source_location();
227  error() << "finish_gotos: unexpected goto" << eom;
228  throw 0;
229  }
230  }
231 
232  targets.gotos.clear();
233 }
234 
236 {
237  for(auto &g_it : targets.computed_gotos)
238  {
239  goto_programt::instructiont &i=*g_it;
240  exprt destination=i.code.op0();
241 
242  assert(destination.id()==ID_dereference);
243  assert(destination.operands().size()==1);
244 
245  exprt pointer=destination.op0();
246 
247  // remember the expression for later checks
248  i.type=OTHER;
249  i.code=code_expressiont(pointer);
250 
251  // insert huge case-split
252  for(const auto &label : targets.labels)
253  {
254  exprt label_expr(ID_label, empty_typet());
255  label_expr.set(ID_identifier, label.first);
256 
257  equal_exprt guard;
258 
259  guard.lhs()=pointer;
260  guard.rhs()=address_of_exprt(label_expr);
261 
263  goto_program.insert_after(g_it);
264 
265  t->make_goto(label.second.first);
266  t->source_location=i.source_location;
267  t->guard=guard;
268  }
269  }
270 
271  targets.computed_gotos.clear();
272 }
273 
278 {
279  for(auto &gg : guarded_gotos)
280  {
281  // Check if any destructor code has been inserted:
282  bool destructor_present=false;
283  for(auto it=gg.ifiter;
284  it!=gg.gotoiter && !destructor_present;
285  ++it)
286  {
287  if(!(it->is_goto() || it->is_skip()))
288  destructor_present=true;
289  }
290 
291  // If so, can't simplify.
292  if(destructor_present)
293  continue;
294 
295  // Simplify: remove whatever code was generated for the condition
296  // and attach the original guard to the goto instruction.
297  gg.gotoiter->guard=gg.guard;
298  // goto_programt doesn't provide an erase operation,
299  // perhaps for a good reason, so let's be cautious and just
300  // flatten the unneeded instructions into skips.
301  for(auto it=gg.ifiter, itend=gg.gotoiter; it!=itend; ++it)
302  it->make_skip();
303  }
304 }
305 
307 {
308  goto_convert_rec(code, dest);
309 }
310 
312  const codet &code,
313  goto_programt &dest)
314 {
315  convert(code, dest);
316 
317  finish_gotos(dest);
318  finish_computed_gotos(dest);
319  finish_guarded_gotos(dest);
321 }
322 
324  const codet &code,
326  goto_programt &dest)
327 {
329  t->code=code;
331 }
332 
334  const code_labelt &code,
335  goto_programt &dest)
336 {
337  if(code.operands().size()!=1)
338  {
340  error() << "label statement expected to have one operand" << eom;
341  throw 0;
342  }
343 
344  // grab the label
345  const irep_idt &label=code.get_label();
346 
347  goto_programt tmp;
348 
349  // magic thread creation label?
350  if(has_prefix(id2string(label), "__CPROVER_ASYNC_"))
351  {
352  // this is like a START_THREAD
353  codet tmp_code(ID_start_thread);
354  tmp_code.copy_to_operands(code.op0());
355  tmp_code.add_source_location()=code.source_location();
356  convert(tmp_code, tmp);
357  }
358  else
359  convert(to_code(code.op0()), tmp);
360 
361  goto_programt::targett target=tmp.instructions.begin();
362  dest.destructive_append(tmp);
363 
364  targets.labels.insert({label, {target, targets.destructor_stack}});
365  target->labels.push_front(label);
366 }
367 
369  const codet &code,
370  goto_programt &dest)
371 {
372  // ignore for now
373 }
374 
376  const code_switch_caset &code,
377  goto_programt &dest)
378 {
379  if(code.operands().size()!=2)
380  {
382  error() << "switch-case statement expected to have two operands"
383  << eom;
384  throw 0;
385  }
386 
387  goto_programt tmp;
388  convert(code.code(), tmp);
389 
390  goto_programt::targett target=tmp.instructions.begin();
391  dest.destructive_append(tmp);
392 
393  // default?
394 
395  if(code.is_default())
396  targets.set_default(target);
397  else
398  {
399  // cases?
400 
401  cases_mapt::iterator cases_entry=targets.cases_map.find(target);
402  if(cases_entry==targets.cases_map.end())
403  {
404  targets.cases.push_back(std::make_pair(target, caset()));
405  cases_entry=targets.cases_map.insert(std::make_pair(
406  target, --targets.cases.end())).first;
407  }
408 
409  exprt::operandst &case_op_dest=cases_entry->second->second;
410  case_op_dest.push_back(code.case_op());
411  }
412 }
413 
415  const codet &code,
416  goto_programt &dest)
417 {
418  if(code.operands().size()!=3)
419  {
421  error() << "GCC's switch-case-range statement expected to have "
422  << "three operands" << eom;
423  throw 0;
424  }
425 
426  goto_programt tmp;
427  convert(to_code(code.op2()), tmp);
428 
429  // goto_programt::targett target=tmp.instructions.begin();
430  dest.destructive_append(tmp);
431 
432  #if 0
433  cases_mapt::iterator cases_entry=targets.cases_map.find(target);
434  if(cases_entry==targets.cases_map.end())
435  {
436  targets.cases.push_back(std::make_pair(target, caset()));
437  cases_entry=targets.cases_map.insert(std::make_pair(
438  target, --targets.cases.end())).first;
439  }
440 
441  // TODO
442  exprt::operandst &case_op_dest=cases_entry->second->second;
443  case_op_dest.push_back(code.case_op());
444  #endif
445 }
446 
449  const codet &code,
450  goto_programt &dest)
451 {
452  const irep_idt &statement=code.get_statement();
453 
454  if(statement==ID_block)
455  convert_block(to_code_block(code), dest);
456  else if(statement==ID_decl)
457  convert_decl(to_code_decl(code), dest);
458  else if(statement==ID_decl_type)
459  convert_decl_type(code, dest);
460  else if(statement==ID_expression)
462  else if(statement==ID_assign)
463  convert_assign(to_code_assign(code), dest);
464  else if(statement==ID_init)
465  convert_init(code, dest);
466  else if(statement==ID_assert)
467  convert_assert(to_code_assert(code), dest);
468  else if(statement==ID_assume)
469  convert_assume(to_code_assume(code), dest);
470  else if(statement==ID_function_call)
472  else if(statement==ID_label)
473  convert_label(to_code_label(code), dest);
474  else if(statement==ID_gcc_local_label)
475  convert_gcc_local_label(code, dest);
476  else if(statement==ID_switch_case)
478  else if(statement==ID_gcc_switch_case_range)
479  convert_gcc_switch_case_range(code, dest);
480  else if(statement==ID_for)
481  convert_for(to_code_for(code), dest);
482  else if(statement==ID_while)
483  convert_while(to_code_while(code), dest);
484  else if(statement==ID_dowhile)
485  convert_dowhile(code, dest);
486  else if(statement==ID_switch)
487  convert_switch(to_code_switch(code), dest);
488  else if(statement==ID_break)
489  convert_break(to_code_break(code), dest);
490  else if(statement==ID_return)
491  convert_return(to_code_return(code), dest);
492  else if(statement==ID_continue)
493  convert_continue(to_code_continue(code), dest);
494  else if(statement==ID_goto)
495  convert_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=="non-deterministic-goto")
501  convert_non_deterministic_goto(code, dest);
502  else if(statement==ID_ifthenelse)
504  else if(statement==ID_specc_notify)
505  convert_specc_notify(code, dest);
506  else if(statement==ID_specc_wait)
507  convert_specc_wait(code, dest);
508  else if(statement==ID_specc_par)
509  convert_specc_par(code, dest);
510  else if(statement==ID_start_thread)
511  convert_start_thread(code, dest);
512  else if(statement==ID_end_thread)
513  convert_end_thread(code, dest);
514  else if(statement==ID_atomic_begin)
515  convert_atomic_begin(code, dest);
516  else if(statement==ID_atomic_end)
517  convert_atomic_end(code, dest);
518  else if(statement==ID_bp_enforce)
519  convert_bp_enforce(code, dest);
520  else if(statement==ID_bp_abortif)
521  convert_bp_abortif(code, dest);
522  else if(statement==ID_cpp_delete ||
523  statement=="cpp_delete[]")
524  convert_cpp_delete(code, dest);
525  else if(statement==ID_msc_try_except)
526  convert_msc_try_except(code, dest);
527  else if(statement==ID_msc_try_finally)
528  convert_msc_try_finally(code, dest);
529  else if(statement==ID_msc_leave)
530  convert_msc_leave(code, dest);
531  else if(statement==ID_try_catch) // C++ try/catch
532  convert_try_catch(code, dest);
533  else if(statement==ID_CPROVER_try_catch) // CPROVER-homemade
534  convert_CPROVER_try_catch(code, dest);
535  else if(statement==ID_CPROVER_throw) // CPROVER-homemade
536  convert_CPROVER_throw(code, dest);
537  else if(statement==ID_CPROVER_try_finally)
538  convert_CPROVER_try_finally(code, dest);
539  else if(statement==ID_asm)
540  convert_asm(to_code_asm(code), dest);
541  else if(statement==ID_static_assert)
542  {
543  assert(code.operands().size()==2);
544  exprt assertion=code.op0();
545  assertion.make_typecast(bool_typet());
546  simplify(assertion, ns);
547  if(assertion.is_false())
548  {
550  error() << "static assertion "
551  << get_string_constant(code.op1()) << eom;
552  throw 0;
553  }
554  else if(assertion.is_true())
555  {
556  }
557  else
558  {
559  // we may wish to complain
560  }
561  }
562  else if(statement==ID_dead)
563  copy(code, DEAD, dest);
564  else if(statement==ID_decl_block)
565  {
566  forall_operands(it, code)
567  convert(to_code(*it), dest);
568  }
569  else
570  copy(code, OTHER, dest);
571 
572  // make sure dest is never empty
573  if(dest.instructions.empty())
574  {
575  dest.add_instruction(SKIP);
576  dest.instructions.back().code.make_nil();
577  dest.instructions.back().source_location=code.source_location();
578  }
579 }
580 
582  const code_blockt &code,
583  goto_programt &dest)
584 {
585  const source_locationt &end_location=code.end_location();
586 
587  // this saves the size of the destructor stack
588  std::size_t old_stack_size=targets.destructor_stack.size();
589 
590  // now convert block
591  forall_operands(it, code)
592  {
593  const codet &b_code=to_code(*it);
594  convert(b_code, dest);
595  }
596 
597  // see if we need to do any destructors -- may have been processed
598  // in a prior break/continue/return already, don't create dead code
599  if(!dest.empty() &&
600  dest.instructions.back().is_goto() &&
601  dest.instructions.back().guard.is_true())
602  {
603  // don't do destructors when we are unreachable
604  }
605  else
606  unwind_destructor_stack(end_location, old_stack_size, dest);
607 
608  // remove those destructors
609  targets.destructor_stack.resize(old_stack_size);
610 }
611 
613  const code_expressiont &code,
614  goto_programt &dest)
615 {
616  if(code.operands().size()!=1)
617  {
619  error() << "expression statement takes one operand" << eom;
620  throw 0;
621  }
622 
623  exprt expr=code.op0();
624 
625  if(expr.id()==ID_if)
626  {
627  // We do a special treatment for c?t:f
628  // by compiling to if(c) t; else f;
629  const if_exprt &if_expr=to_if_expr(expr);
630  code_ifthenelset tmp_code;
631  tmp_code.add_source_location()=expr.source_location();
632  tmp_code.cond()=if_expr.cond();
633  tmp_code.then_case()=code_expressiont(if_expr.true_case());
634  tmp_code.then_case().add_source_location()=expr.source_location();
635  tmp_code.else_case()=code_expressiont(if_expr.false_case());
636  tmp_code.else_case().add_source_location()=expr.source_location();
637  convert_ifthenelse(tmp_code, dest);
638  }
639  else
640  {
641  clean_expr(expr, dest, false); // result _not_ used
642 
643  // Any residual expression?
644  // We keep it to add checks later.
645  if(expr.is_not_nil())
646  {
647  codet tmp=code;
648  tmp.op0()=expr;
650  copy(tmp, OTHER, dest);
651  }
652  }
653 }
654 
656  const code_declt &code,
657  goto_programt &dest)
658 {
659  const exprt &op0=code.op0();
660 
661  if(op0.id()!=ID_symbol)
662  {
664  error() << "decl statement expects symbol as first operand" << eom;
665  throw 0;
666  }
667 
668  const irep_idt &identifier=op0.get(ID_identifier);
669 
670  const symbolt &symbol=lookup(identifier);
671 
672  if(symbol.is_static_lifetime ||
673  symbol.type.id()==ID_code)
674  return; // this is a SKIP!
675 
676  if(code.operands().size()==1)
677  {
678  copy(code, DECL, dest);
679  }
680  else
681  {
682  // this is expected to go away
683  exprt initializer;
684 
685  codet tmp=code;
686  initializer=code.op1();
687  tmp.operands().resize(1);
688 
689  // Break up into decl and assignment.
690  // Decl must be visible before initializer.
691  copy(tmp, DECL, dest);
692 
693  code_assignt assign(code.op0(), initializer);
694  assign.add_source_location()=tmp.source_location();
695 
696  convert_assign(assign, dest);
697  }
698 
699  // now create a 'dead' instruction -- will be added after the
700  // destructor created below as unwind_destructor_stack pops off the
701  // top of the destructor stack
702  const symbol_exprt symbol_expr(symbol.name, symbol.type);
703 
704  {
705  code_deadt code_dead(symbol_expr);
706  targets.destructor_stack.push_back(code_dead);
707  }
708 
709  // do destructor
710  code_function_callt destructor=get_destructor(ns, symbol.type);
711 
712  if(destructor.is_not_nil())
713  {
714  // add "this"
715  address_of_exprt this_expr(symbol_expr, pointer_type(symbol.type));
716  destructor.arguments().push_back(this_expr);
717 
718  targets.destructor_stack.push_back(destructor);
719  }
720 }
721 
723  const codet &code,
724  goto_programt &dest)
725 {
726  // we remove these
727 }
728 
730  const code_assignt &code,
731  goto_programt &dest)
732 {
733  exprt lhs=code.lhs(),
734  rhs=code.rhs();
735 
736  clean_expr(lhs, dest);
737 
738  if(rhs.id()==ID_side_effect &&
739  rhs.get(ID_statement)==ID_function_call)
740  {
741  if(rhs.operands().size()!=2)
742  {
743  error().source_location=rhs.find_source_location();
744  error() << "function_call sideeffect takes two operands" << eom;
745  throw 0;
746  }
747 
748  Forall_operands(it, rhs)
749  clean_expr(*it, dest);
750 
751  do_function_call(lhs, rhs.op0(), rhs.op1().operands(), dest);
752  }
753  else if(rhs.id()==ID_side_effect &&
754  (rhs.get(ID_statement)==ID_cpp_new ||
755  rhs.get(ID_statement)==ID_cpp_new_array))
756  {
757  Forall_operands(it, rhs)
758  clean_expr(*it, dest);
759 
760  do_cpp_new(lhs, to_side_effect_expr(rhs), dest);
761  }
762  else if(rhs.id()==ID_side_effect &&
763  rhs.get(ID_statement)==ID_java_new)
764  {
765  Forall_operands(it, rhs)
766  clean_expr(*it, dest);
767 
768  do_java_new(lhs, to_side_effect_expr(rhs), dest);
769  }
770  else if(rhs.id()==ID_side_effect &&
771  rhs.get(ID_statement)==ID_java_new_array)
772  {
773  Forall_operands(it, rhs)
774  clean_expr(*it, dest);
775 
776  do_java_new_array(lhs, to_side_effect_expr(rhs), dest);
777  }
778  else if(rhs.id()==ID_side_effect &&
779  rhs.get(ID_statement)==ID_malloc)
780  {
781  // just preserve
782  Forall_operands(it, rhs)
783  clean_expr(*it, dest);
784 
785  code_assignt new_assign(code);
786  new_assign.lhs()=lhs;
787  new_assign.rhs()=rhs;
788 
789  copy(new_assign, ASSIGN, dest);
790  }
791  else
792  {
793  clean_expr(rhs, dest);
794 
795  if(lhs.id()==ID_typecast)
796  {
797  assert(lhs.operands().size()==1);
798 
799  // add a typecast to the rhs
800  exprt new_rhs=rhs;
801  rhs.make_typecast(lhs.op0().type());
802 
803  // remove typecast from lhs
804  exprt tmp=lhs.op0();
805  lhs.swap(tmp);
806  }
807 
808  code_assignt new_assign(code);
809  new_assign.lhs()=lhs;
810  new_assign.rhs()=rhs;
811 
812  copy(new_assign, ASSIGN, dest);
813  }
814 }
815 
817  const codet &code,
818  goto_programt &dest)
819 {
820  if(code.operands().size()!=2)
821  {
823  error() <<"init statement takes two operands" << eom;
824  throw 0;
825  }
826 
827  // make it an assignment
828  codet assignment=code;
829  assignment.set_statement(ID_assign);
830 
831  convert(to_code_assign(assignment), dest);
832 }
833 
835  const codet &code,
836  goto_programt &dest)
837 {
838  if(code.operands().size()!=1)
839  {
841  error() << "cpp_delete statement takes one operand" << eom;
842  throw 0;
843  }
844 
845  exprt tmp_op=code.op0();
846 
847  clean_expr(tmp_op, dest);
848 
849  // we call the destructor, and then free
850  const exprt &destructor=
851  static_cast<const exprt &>(code.find(ID_destructor));
852 
853  irep_idt delete_identifier;
854 
855  if(code.get_statement()==ID_cpp_delete_array)
856  delete_identifier="__delete_array";
857  else if(code.get_statement()==ID_cpp_delete)
858  delete_identifier="__delete";
859  else
860  assert(false);
861 
862  if(destructor.is_not_nil())
863  {
864  if(code.get_statement()==ID_cpp_delete_array)
865  {
866  // build loop
867  }
868  else if(code.get_statement()==ID_cpp_delete)
869  {
870  // just one object
871  exprt deref_op(ID_dereference, tmp_op.type().subtype());
872  deref_op.copy_to_operands(tmp_op);
873 
874  codet tmp_code=to_code(destructor);
875  replace_new_object(deref_op, tmp_code);
876  convert(tmp_code, dest);
877  }
878  else
879  assert(false);
880  }
881 
882  // now do "free"
883  exprt delete_symbol=ns.lookup(delete_identifier).symbol_expr();
884 
885  assert(to_code_type(delete_symbol.type()).parameters().size()==1);
886 
887  typet arg_type=
888  to_code_type(delete_symbol.type()).parameters().front().type();
889 
890  code_function_callt delete_call;
891  delete_call.function()=delete_symbol;
892  delete_call.arguments().push_back(typecast_exprt(tmp_op, arg_type));
893  delete_call.lhs().make_nil();
894  delete_call.add_source_location()=code.source_location();
895 
896  convert(delete_call, dest);
897 }
898 
900  const code_assertt &code,
901  goto_programt &dest)
902 {
903  exprt cond=code.assertion();
904 
905  clean_expr(cond, dest);
906 
908  t->guard.swap(cond);
909  t->source_location=code.source_location();
910  t->source_location.set(ID_property, ID_assertion);
911  t->source_location.set("user-provided", true);
912 }
913 
915  const codet &code,
916  goto_programt &dest)
917 {
919  t->source_location=code.source_location();
920  t->code=code;
921 }
922 
924  const code_assumet &code,
925  goto_programt &dest)
926 {
927  exprt op=code.assumption();
928 
929  clean_expr(op, dest);
930 
932  t->guard.swap(op);
933  t->source_location=code.source_location();
934 }
935 
937  const codet &code,
939 {
940  exprt invariant=
941  static_cast<const exprt&>(code.find(ID_C_spec_loop_invariant));
942 
943  if(invariant.is_nil())
944  return;
945 
946  goto_programt no_sideeffects;
947  clean_expr(invariant, no_sideeffects);
948  if(!no_sideeffects.instructions.empty())
949  {
951  error() << "loop invariant is not side-effect free" << eom;
952  throw 0;
953  }
954 
955  assert(loop->is_goto());
956  loop->guard.add(ID_C_spec_loop_invariant).swap(invariant);
957 }
958 
960  const code_fort &code,
961  goto_programt &dest)
962 {
963  // turn for(A; c; B) { P } into
964  // A; while(c) { P; B; }
965  //-----------------------------
966  // A;
967  // u: sideeffects in c
968  // v: if(!c) goto z;
969  // w: P;
970  // x: B; <-- continue target
971  // y: goto u;
972  // z: ; <-- break target
973 
974  // A;
975  if(code.init().is_not_nil())
976  convert(to_code(code.init()), dest);
977 
978  exprt cond=code.cond();
979 
980  goto_programt sideeffects;
981  clean_expr(cond, sideeffects);
982 
983  // save break/continue targets
984  break_continue_targetst old_targets(targets);
985 
986  // do the u label
987  goto_programt::targett u=sideeffects.instructions.begin();
988 
989  // do the v label
990  goto_programt tmp_v;
992 
993  // do the z label
994  goto_programt tmp_z;
996  z->source_location=code.source_location();
997 
998  // do the x label
999  goto_programt tmp_x;
1000 
1001  if(code.op2().is_nil())
1002  {
1003  tmp_x.add_instruction(SKIP);
1004  tmp_x.instructions.back().source_location=code.source_location();
1005  }
1006  else
1007  {
1008  exprt tmp_B=code.iter();
1009 
1010  clean_expr(tmp_B, tmp_x, false);
1011 
1012  if(tmp_x.instructions.empty())
1013  {
1014  tmp_x.add_instruction(SKIP);
1015  tmp_x.instructions.back().source_location=code.source_location();
1016  }
1017  }
1018 
1019  // optimize the v label
1020  if(sideeffects.instructions.empty())
1021  u=v;
1022 
1023  // set the targets
1024  targets.set_break(z);
1025  targets.set_continue(tmp_x.instructions.begin());
1026 
1027  // v: if(!c) goto z;
1028  v->make_goto(z);
1029  v->guard=cond;
1030  v->guard.make_not();
1031  v->source_location=cond.source_location();
1032 
1033  // do the w label
1034  goto_programt tmp_w;
1035  convert(code.body(), tmp_w);
1036 
1037  // y: goto u;
1038  goto_programt tmp_y;
1039  goto_programt::targett y=tmp_y.add_instruction();
1040  y->make_goto(u);
1041  y->guard=true_exprt();
1042  y->source_location=code.source_location();
1043 
1044  // loop invariant
1045  convert_loop_invariant(code, y);
1046 
1047  dest.destructive_append(sideeffects);
1048  dest.destructive_append(tmp_v);
1049  dest.destructive_append(tmp_w);
1050  dest.destructive_append(tmp_x);
1051  dest.destructive_append(tmp_y);
1052  dest.destructive_append(tmp_z);
1053 
1054  // restore break/continue
1055  old_targets.restore(targets);
1056 }
1057 
1059  const code_whilet &code,
1060  goto_programt &dest)
1061 {
1062  const exprt &cond=code.cond();
1063  const source_locationt &source_location=code.source_location();
1064 
1065  // while(c) P;
1066  //--------------------
1067  // v: sideeffects in c
1068  // if(!c) goto z;
1069  // x: P;
1070  // y: goto v; <-- continue target
1071  // z: ; <-- break target
1072 
1073  // save break/continue targets
1074  break_continue_targetst old_targets(targets);
1075 
1076  // do the z label
1077  goto_programt tmp_z;
1079  z->make_skip();
1080  z->source_location=source_location;
1081 
1082  goto_programt tmp_branch;
1084  boolean_negate(cond), z, source_location, tmp_branch);
1085 
1086  // do the v label
1087  goto_programt::targett v=tmp_branch.instructions.begin();
1088 
1089  // do the y label
1090  goto_programt tmp_y;
1092 
1093  // set the targets
1094  targets.set_break(z);
1095  targets.set_continue(y);
1096 
1097  // do the x label
1098  goto_programt tmp_x;
1099  convert(code.body(), tmp_x);
1100 
1101  // y: if(c) goto v;
1102  y->make_goto(v);
1103  y->guard=true_exprt();
1104  y->source_location=code.source_location();
1105 
1106  // loop invariant
1107  convert_loop_invariant(code, y);
1108 
1109  dest.destructive_append(tmp_branch);
1110  dest.destructive_append(tmp_x);
1111  dest.destructive_append(tmp_y);
1112  dest.destructive_append(tmp_z);
1113 
1114  // restore break/continue
1115  old_targets.restore(targets);
1116 }
1117 
1119  const codet &code,
1120  goto_programt &dest)
1121 {
1122  if(code.operands().size()!=2)
1123  {
1125  error() << "dowhile takes two operands" << eom;
1126  throw 0;
1127  }
1128 
1129  // save source location
1130  source_locationt condition_location=code.op0().find_source_location();
1131 
1132  exprt cond=code.op0();
1133 
1134  goto_programt sideeffects;
1135  clean_expr(cond, sideeffects);
1136 
1137  // do P while(c);
1138  //--------------------
1139  // w: P;
1140  // x: sideeffects in c <-- continue target
1141  // y: if(c) goto w;
1142  // z: ; <-- break target
1143 
1144  // save break/continue targets
1145  break_continue_targetst old_targets(targets);
1146 
1147  // do the y label
1148  goto_programt tmp_y;
1150 
1151  // do the z label
1152  goto_programt tmp_z;
1154  z->make_skip();
1155  z->source_location=code.source_location();
1156 
1157  // do the x label
1159  if(sideeffects.instructions.empty())
1160  x=y;
1161  else
1162  x=sideeffects.instructions.begin();
1163 
1164  // set the targets
1165  targets.set_break(z);
1166  targets.set_continue(x);
1167 
1168  // do the w label
1169  goto_programt tmp_w;
1170  convert(to_code(code.op1()), tmp_w);
1171  goto_programt::targett w=tmp_w.instructions.begin();
1172 
1173  // y: if(c) goto w;
1174  y->make_goto(w);
1175  y->guard=cond;
1176  y->source_location=condition_location;
1177 
1178  // loop invariant
1179  convert_loop_invariant(code, y);
1180 
1181  dest.destructive_append(tmp_w);
1182  dest.destructive_append(sideeffects);
1183  dest.destructive_append(tmp_y);
1184  dest.destructive_append(tmp_z);
1185 
1186  // restore break/continue targets
1187  old_targets.restore(targets);
1188 }
1189 
1191  const exprt &value,
1192  const exprt::operandst &case_op)
1193 {
1194  exprt dest=exprt(ID_or, bool_typet());
1195  dest.reserve_operands(case_op.size());
1196 
1197  forall_expr(it, case_op)
1198  {
1199  equal_exprt eq_expr;
1200  eq_expr.lhs()=value;
1201  eq_expr.rhs()=*it;
1202  dest.move_to_operands(eq_expr);
1203  }
1204 
1205  assert(!dest.operands().empty());
1206 
1207  if(dest.operands().size()==1)
1208  {
1209  exprt tmp;
1210  tmp.swap(dest.op0());
1211  dest.swap(tmp);
1212  }
1213 
1214  return dest;
1215 }
1216 
1218  const code_switcht &code,
1219  goto_programt &dest)
1220 {
1221  // switch(v) {
1222  // case x: Px;
1223  // case y: Py;
1224  // ...
1225  // default: Pd;
1226  // }
1227  // --------------------
1228  // x: if(v==x) goto X;
1229  // y: if(v==y) goto Y;
1230  // goto d;
1231  // X: Px;
1232  // Y: Py;
1233  // d: Pd;
1234  // z: ;
1235 
1236  if(code.operands().size()<2)
1237  {
1239  error() << "switch takes at least two operands" << eom;
1240  throw 0;
1241  }
1242 
1243  exprt argument=code.value();
1244 
1245  goto_programt sideeffects;
1246  clean_expr(argument, sideeffects);
1247 
1248  // save break/default/cases targets
1249  break_switch_targetst old_targets(targets);
1250 
1251  // do the z label
1252  goto_programt tmp_z;
1254  z->make_skip();
1255  z->source_location=code.source_location();
1256 
1257  // set the new targets -- continue stays as is
1258  targets.set_break(z);
1259  targets.set_default(z);
1260  targets.cases.clear();
1261  targets.cases_map.clear();
1262 
1263  goto_programt tmp;
1264 
1265  forall_operands(it, code)
1266  if(it!=code.operands().begin())
1267  convert(to_code(*it), tmp);
1268 
1269  goto_programt tmp_cases;
1270 
1271  for(auto &case_pair : targets.cases)
1272  {
1273  const caset &case_ops=case_pair.second;
1274 
1275  assert(!case_ops.empty());
1276 
1277  exprt guard_expr=case_guard(argument, case_ops);
1278 
1280  x->make_goto(case_pair.first);
1281  x->guard.swap(guard_expr);
1282  x->source_location=case_ops.front().find_source_location();
1283  }
1284 
1285  {
1286  goto_programt::targett d_jump=tmp_cases.add_instruction();
1287  d_jump->make_goto(targets.default_target);
1288  d_jump->source_location=targets.default_target->source_location;
1289  }
1290 
1291  dest.destructive_append(sideeffects);
1292  dest.destructive_append(tmp_cases);
1293  dest.destructive_append(tmp);
1294  dest.destructive_append(tmp_z);
1295 
1296  // restore old targets
1297  old_targets.restore(targets);
1298 }
1299 
1301  const code_breakt &code,
1302  goto_programt &dest)
1303 {
1304  if(!targets.break_set)
1305  {
1307  error() << "break without target" << eom;
1308  throw 0;
1309  }
1310 
1311  // need to process destructor stack
1313  code.source_location(), targets.break_stack_size, dest);
1314 
1315  // add goto
1317  t->make_goto(targets.break_target);
1318  t->source_location=code.source_location();
1319 }
1320 
1322  const code_returnt &code,
1323  goto_programt &dest)
1324 {
1325  if(!targets.return_set)
1326  {
1328  error() << "return without target" << eom;
1329  throw 0;
1330  }
1331 
1332  if(!code.operands().empty() &&
1333  code.operands().size()!=1)
1334  {
1336  error() << "return takes none or one operand" << eom;
1337  throw 0;
1338  }
1339 
1340  code_returnt new_code(code);
1341 
1342  if(new_code.has_return_value())
1343  {
1344  bool result_is_used=
1345  new_code.return_value().type().id()!=ID_empty;
1346 
1347  goto_programt sideeffects;
1348  clean_expr(new_code.return_value(), sideeffects, result_is_used);
1349  dest.destructive_append(sideeffects);
1350 
1351  // remove void-typed return value
1352  if(!result_is_used)
1353  new_code.return_value().make_nil();
1354  }
1355 
1357  {
1358  if(!new_code.has_return_value())
1359  {
1361  error() << "function must return value" << eom;
1362  throw 0;
1363  }
1364 
1365  // Now add a return node to set the return value.
1367  t->make_return();
1368  t->code=new_code;
1369  t->source_location=new_code.source_location();
1370  }
1371  else
1372  {
1373  if(new_code.has_return_value() &&
1374  new_code.return_value().type().id()!=ID_empty)
1375  {
1377  error() << "function must not return value" << eom;
1378  throw 0;
1379  }
1380  }
1381 
1382  // Need to process _entire_ destructor stack.
1383  unwind_destructor_stack(code.source_location(), 0, dest);
1384 
1385  // add goto to end-of-function
1387  t->make_goto(targets.return_target, true_exprt());
1388  t->source_location=new_code.source_location();
1389 }
1390 
1392  const code_continuet &code,
1393  goto_programt &dest)
1394 {
1395  if(!targets.continue_set)
1396  {
1398  error() << "continue without target" << eom;
1399  throw 0;
1400  }
1401 
1402  // need to process destructor stack
1405 
1406  // add goto
1408  t->make_goto(targets.continue_target);
1409  t->source_location=code.source_location();
1410 }
1411 
1413  const codet &code,
1414  goto_programt &dest)
1415 {
1417  t->make_goto();
1418  t->source_location=code.source_location();
1419  t->code=code;
1420 
1421  // remember it to do target later
1422  targets.gotos.push_back(std::make_pair(t, targets.destructor_stack));
1423 }
1424 
1426  const codet &code,
1427  goto_programt &dest)
1428 {
1430  t->make_skip();
1431  t->source_location=code.source_location();
1432  t->code=code;
1433 
1434  // remember it to do this later
1435  targets.computed_gotos.push_back(t);
1436 }
1437 
1439  const codet &code,
1440  goto_programt &dest)
1441 {
1442  convert_goto(code, dest);
1443 }
1444 
1446  const codet &code,
1447  goto_programt &dest)
1448 {
1449  #if 0
1451 
1452  forall_operands(it, code)
1453  convert_specc_event(*it, t->events);
1454 
1455  t->code.swap(code);
1456  t->source_location=code.source_location();
1457  #endif
1458 
1459  copy(code, OTHER, dest);
1460 }
1461 
1463  const exprt &op,
1464  std::set<irep_idt> &events)
1465 {
1466  if(op.id()==ID_or || op.id()==ID_and)
1467  {
1468  forall_operands(it, op)
1469  convert_specc_event(*it, events);
1470  }
1471  else if(op.id()==ID_specc_event)
1472  {
1473  irep_idt event=op.get(ID_identifier);
1474 
1475  if(has_prefix(id2string(event), "specc::"))
1476  event=std::string(id2string(event), 7, std::string::npos);
1477 
1478  events.insert(event);
1479  }
1480  else
1481  {
1483  error() << "convert_convert_event got " << op.id() << eom;
1484  throw 0;
1485  }
1486 }
1487 
1489  const codet &code,
1490  goto_programt &dest)
1491 {
1492  #if 0
1494 
1495  if(code.operands().size()!=1)
1496  {
1498  error() << "specc_wait expects one operand" << eom;
1499  throw 0;
1500  }
1501 
1502  const exprt &op=code.op0();
1503 
1504  if(op.id()=="or")
1505  t->or_semantics=true;
1506 
1507  convert_specc_event(op, t->events);
1508 
1509  t->code.swap(code);
1510  t->source_location=code.source_location();
1511  #endif
1512 
1513  copy(code, OTHER, dest);
1514 }
1515 
1517  const codet &code,
1518  goto_programt &dest)
1519 {
1520  copy(code, OTHER, dest);
1521 }
1522 
1524  const codet &code,
1525  goto_programt &dest)
1526 {
1527  if(code.operands().size()!=1)
1528  {
1530  error() << "start_thread expects one operand" << eom;
1531  throw 0;
1532  }
1533 
1534  goto_programt::targett start_thread=
1536 
1537  start_thread->source_location=code.source_location();
1538 
1539  {
1540  // start_thread label;
1541  // goto tmp;
1542  // label: op0-code
1543  // end_thread
1544  // tmp: skip
1545 
1546  goto_programt::targett goto_instruction=dest.add_instruction(GOTO);
1547  goto_instruction->guard=true_exprt();
1548  goto_instruction->source_location=code.source_location();
1549 
1550  goto_programt tmp;
1551  convert(to_code(code.op0()), tmp);
1553  end_thread->source_location=code.source_location();
1554 
1555  start_thread->targets.push_back(tmp.instructions.begin());
1556  dest.destructive_append(tmp);
1557  goto_instruction->targets.push_back(dest.add_instruction(SKIP));
1558  dest.instructions.back().source_location=code.source_location();
1559  }
1560 }
1561 
1563  const codet &code,
1564  goto_programt &dest)
1565 {
1566  if(!code.operands().empty())
1567  {
1569  error() << "end_thread expects no operands" << eom;
1570  throw 0;
1571  }
1572 
1573  copy(code, END_THREAD, dest);
1574 }
1575 
1577  const codet &code,
1578  goto_programt &dest)
1579 {
1580  if(!code.operands().empty())
1581  {
1583  error() << "atomic_begin expects no operands" << eom;
1584  throw 0;
1585  }
1586 
1587  copy(code, ATOMIC_BEGIN, dest);
1588 }
1589 
1591  const codet &code,
1592  goto_programt &dest)
1593 {
1594  if(!code.operands().empty())
1595  {
1597  error() << "atomic_end expects no operands" << eom;
1598  throw 0;
1599  }
1600 
1601  copy(code, ATOMIC_END, dest);
1602 }
1603 
1605  const codet &code,
1606  goto_programt &dest)
1607 {
1608  if(code.operands().size()!=2)
1609  {
1611  error() << "bp_enfroce expects two arguments" << eom;
1612  throw 0;
1613  }
1614 
1615  // do an assume
1616  exprt op=code.op0();
1617 
1618  clean_expr(op, dest);
1619 
1621  t->guard=op;
1622  t->source_location=code.source_location();
1623 
1624  // change the assignments
1625 
1626  goto_programt tmp;
1627  convert(to_code(code.op1()), tmp);
1628 
1629  if(!op.is_true())
1630  {
1631  exprt constraint(op);
1632  make_next_state(constraint);
1633 
1635  {
1636  if(it->is_assign())
1637  {
1638  assert(it->code.get(ID_statement)==ID_assign);
1639 
1640  // add constrain
1641  codet constrain(ID_bp_constrain);
1642  constrain.reserve_operands(2);
1643  constrain.move_to_operands(it->code);
1644  constrain.copy_to_operands(constraint);
1645  it->code.swap(constrain);
1646 
1647  it->type=OTHER;
1648  }
1649  else if(it->is_other() &&
1650  it->code.get(ID_statement)==ID_bp_constrain)
1651  {
1652  // add to constraint
1653  assert(it->code.operands().size()==2);
1654  it->code.op1()=
1655  and_exprt(it->code.op1(), constraint);
1656  }
1657  }
1658  }
1659 
1660  dest.destructive_append(tmp);
1661 }
1662 
1664  const codet &code,
1665  goto_programt &dest)
1666 {
1667  if(code.operands().size()!=1)
1668  {
1670  error() << "bp_abortif expects one argument" << eom;
1671  throw 0;
1672  }
1673 
1674  // do an assert
1675  exprt op=code.op0();
1676 
1677  clean_expr(op, dest);
1678 
1679  op.make_not();
1680 
1682  t->guard.swap(op);
1683  t->source_location=code.source_location();
1684 }
1685 
1687  const code_ifthenelset &code,
1688  goto_programt &dest)
1689 {
1690  if(code.operands().size()!=3)
1691  {
1693  error() << "ifthenelse takes three operands" << eom;
1694  throw 0;
1695  }
1696 
1697  assert(code.then_case().is_not_nil());
1698 
1699  bool has_else=
1700  !code.else_case().is_nil();
1701 
1702  const source_locationt &source_location=code.source_location();
1703 
1704  // We do a bit of special treatment for && in the condition
1705  // in case cleaning would be needed otherwise.
1706  if(code.cond().id()==ID_and &&
1707  code.cond().operands().size()==2 &&
1708  (needs_cleaning(code.cond().op0()) || needs_cleaning(code.cond().op1())) &&
1709  !has_else)
1710  {
1711  // if(a && b) XX --> if(a) if(b) XX
1712  code_ifthenelset new_if0, new_if1;
1713  new_if0.cond()=code.cond().op0();
1714  new_if1.cond()=code.cond().op1();
1715  new_if0.add_source_location()=source_location;
1716  new_if1.add_source_location()=source_location;
1717  new_if1.then_case()=code.then_case();
1718  new_if0.then_case()=new_if1;
1719  return convert_ifthenelse(new_if0, dest);
1720  }
1721 
1722  // convert 'then'-branch
1723  goto_programt tmp_then;
1724  convert(to_code(code.then_case()), tmp_then);
1725 
1726  goto_programt tmp_else;
1727 
1728  if(has_else)
1729  convert(to_code(code.else_case()), tmp_else);
1730 
1731  exprt tmp_guard=code.cond();
1732  clean_expr(tmp_guard, dest);
1733 
1734  generate_ifthenelse(tmp_guard, tmp_then, tmp_else, source_location, dest);
1735 }
1736 
1738  const exprt &expr,
1739  const irep_idt &id,
1740  std::list<exprt> &dest)
1741 {
1742  if(expr.id()!=id)
1743  {
1744  dest.push_back(expr);
1745  }
1746  else
1747  {
1748  // left-to-right is important
1749  forall_operands(it, expr)
1750  collect_operands(*it, id, dest);
1751  }
1752 }
1753 
1757 static inline bool is_size_one(const goto_programt &g)
1758 {
1759  return (!g.instructions.empty()) &&
1760  ++g.instructions.begin()==g.instructions.end();
1761 }
1762 
1765  const exprt &guard,
1766  goto_programt &true_case,
1767  goto_programt &false_case,
1768  const source_locationt &source_location,
1769  goto_programt &dest)
1770 {
1771  if(is_empty(true_case) &&
1772  is_empty(false_case))
1773  {
1774  // hmpf. Useless branch.
1775  goto_programt tmp_z;
1777  z->make_skip();
1779  v->make_goto(z, guard);
1780  v->source_location=source_location;
1781  dest.destructive_append(tmp_z);
1782  return;
1783  }
1784 
1785  bool is_guarded_goto=false;
1786 
1787  // do guarded gotos directly
1788  if(is_empty(false_case) &&
1789  is_size_one(true_case) &&
1790  true_case.instructions.back().is_goto() &&
1791  true_case.instructions.back().guard.is_true() &&
1792  true_case.instructions.back().labels.empty())
1793  {
1794  // The above conjunction deliberately excludes the instance
1795  // if(some) { label: goto somewhere; }
1796  // Don't perform the transformation here, as code might get inserted into
1797  // the true case to perform destructors.
1798  // This will be attempted in finish_guarded_gotos.
1799  is_guarded_goto=true;
1800  }
1801 
1802  // similarly, do guarded assertions directly
1803  if(is_size_one(true_case) &&
1804  true_case.instructions.back().is_assert() &&
1805  true_case.instructions.back().guard.is_false() &&
1806  true_case.instructions.back().labels.empty())
1807  {
1808  // The above conjunction deliberately excludes the instance
1809  // if(some) { label: assert(0); }
1810  true_case.instructions.back().guard=boolean_negate(guard);
1811  dest.destructive_append(true_case);
1812  true_case.instructions.clear();
1813  }
1814 
1815  // similarly, do guarded assertions directly
1816  if(is_size_one(false_case) &&
1817  false_case.instructions.back().is_assert() &&
1818  false_case.instructions.back().guard.is_false() &&
1819  false_case.instructions.back().labels.empty())
1820  {
1821  // The above conjunction deliberately excludes the instance
1822  // if(some) ... else { label: assert(0); }
1823  false_case.instructions.back().guard=guard;
1824  dest.destructive_append(false_case);
1825  false_case.instructions.clear();
1826  }
1827 
1828  // Flip around if no 'true' case code.
1829  if(is_empty(true_case))
1830  return generate_ifthenelse(
1831  boolean_negate(guard), false_case, true_case, source_location, dest);
1832 
1833  bool has_else=!is_empty(false_case);
1834 
1835  // if(c) P;
1836  //--------------------
1837  // v: if(!c) goto z;
1838  // w: P;
1839  // z: ;
1840 
1841  // if(c) P; else Q;
1842  //--------------------
1843  // v: if(!c) goto y;
1844  // w: P;
1845  // x: goto z;
1846  // y: Q;
1847  // z: ;
1848 
1849  // do the x label
1850  goto_programt tmp_x;
1852 
1853  // do the z label
1854  goto_programt tmp_z;
1856  z->make_skip();
1857  // We deliberately don't set a location for 'z', it's a dummy
1858  // target.
1859 
1860  // y: Q;
1861  goto_programt tmp_y;
1863  if(has_else)
1864  {
1865  tmp_y.swap(false_case);
1866  y=tmp_y.instructions.begin();
1867  }
1868 
1869  // v: if(!c) goto z/y;
1870  goto_programt tmp_v;
1872  boolean_negate(guard), has_else?y:z, source_location, tmp_v);
1873 
1874  // w: P;
1875  goto_programt tmp_w;
1876  tmp_w.swap(true_case);
1877 
1878  // x: goto z;
1879  x->make_goto(z);
1880  assert(!tmp_w.instructions.empty());
1881  x->source_location=tmp_w.instructions.back().source_location;
1882 
1883  // See if we can simplify this guarded goto later.
1884  // Note this depends on the fact that `instructions` is a std::list
1885  // and so goto-program-destructive-append preserves iterator validity.
1886  if(is_guarded_goto)
1887  guarded_gotos.push_back({ // NOLINT(whitespace/braces)
1888  tmp_v.instructions.begin(),
1889  tmp_w.instructions.begin(),
1890  guard});
1891 
1892  dest.destructive_append(tmp_v);
1893  dest.destructive_append(tmp_w);
1894 
1895  if(has_else)
1896  {
1897  dest.destructive_append(tmp_x);
1898  dest.destructive_append(tmp_y);
1899  }
1900 
1901  dest.destructive_append(tmp_z);
1902 }
1903 
1905 static bool has_and_or(const exprt &expr)
1906 {
1907  forall_operands(it, expr)
1908  if(has_and_or(*it))
1909  return true;
1910 
1911  if(expr.id()==ID_and || expr.id()==ID_or)
1912  return true;
1913 
1914  return false;
1915 }
1916 
1918  const exprt &guard,
1919  goto_programt::targett target_true,
1920  const source_locationt &source_location,
1921  goto_programt &dest)
1922 {
1923  if(has_and_or(guard) && needs_cleaning(guard))
1924  {
1925  // if(guard) goto target;
1926  // becomes
1927  // if(guard) goto target; else goto next;
1928  // next: skip;
1929 
1930  goto_programt tmp;
1931  goto_programt::targett target_false=tmp.add_instruction();
1932  target_false->make_skip();
1933  target_false->source_location=source_location;
1934 
1936  guard, target_true, target_false, source_location, dest);
1937 
1938  dest.destructive_append(tmp);
1939  }
1940  else
1941  {
1942  // simple branch
1943  exprt cond=guard;
1944  clean_expr(cond, dest);
1945 
1946  goto_programt tmp;
1948  g->make_goto(target_true);
1949  g->guard=cond;
1950  g->source_location=source_location;
1951  dest.destructive_append(tmp);
1952  }
1953 }
1954 
1957  const exprt &guard,
1958  goto_programt::targett target_true,
1959  goto_programt::targett target_false,
1960  const source_locationt &source_location,
1961  goto_programt &dest)
1962 {
1963  if(guard.id()==ID_not)
1964  {
1965  assert(guard.operands().size()==1);
1966  // simply swap targets
1968  guard.op0(), target_false, target_true, source_location, dest);
1969  return;
1970  }
1971 
1972  if(guard.id()==ID_and)
1973  {
1974  // turn
1975  // if(a && b) goto target_true; else goto target_false;
1976  // into
1977  // if(!a) goto target_false;
1978  // if(!b) goto target_false;
1979  // goto target_true;
1980 
1981  std::list<exprt> op;
1982  collect_operands(guard, guard.id(), op);
1983 
1984  forall_expr_list(it, op)
1986  boolean_negate(*it), target_false, source_location, dest);
1987 
1989  t_true->make_goto(target_true);
1990  t_true->guard=true_exprt();
1991  t_true->source_location=source_location;
1992 
1993  return;
1994  }
1995  else if(guard.id()==ID_or)
1996  {
1997  // turn
1998  // if(a || b) goto target_true; else goto target_false;
1999  // into
2000  // if(a) goto target_true;
2001  // if(b) goto target_true;
2002  // goto target_false;
2003 
2004  std::list<exprt> op;
2005  collect_operands(guard, guard.id(), op);
2006 
2007  forall_expr_list(it, op)
2009  *it, target_true, source_location, dest);
2010 
2011  goto_programt::targett t_false=dest.add_instruction();
2012  t_false->make_goto(target_false);
2013  t_false->guard=true_exprt();
2014  t_false->source_location=guard.source_location();
2015 
2016  return;
2017  }
2018 
2019  exprt cond=guard;
2020  clean_expr(cond, dest);
2021 
2023  t_true->make_goto(target_true);
2024  t_true->guard=cond;
2025  t_true->source_location=source_location;
2026 
2027  goto_programt::targett t_false=dest.add_instruction();
2028  t_false->make_goto(target_false);
2029  t_false->guard=true_exprt();
2030  t_false->source_location=source_location;
2031 }
2032 
2034  const exprt &expr,
2035  irep_idt &value)
2036 {
2037  if(expr.id()==ID_typecast &&
2038  expr.operands().size()==1)
2039  return get_string_constant(expr.op0(), value);
2040 
2041  if(expr.id()==ID_address_of &&
2042  expr.operands().size()==1 &&
2043  expr.op0().id()==ID_index &&
2044  expr.op0().operands().size()==2)
2045  {
2046  exprt index_op=get_constant(expr.op0().op0());
2047  simplify(index_op, ns);
2048 
2049  if(index_op.id()==ID_string_constant)
2050  return value=index_op.get(ID_value), false;
2051  else if(index_op.id()==ID_array)
2052  {
2053  std::string result;
2054  forall_operands(it, index_op)
2055  if(it->is_constant())
2056  {
2057  unsigned long i=integer2ulong(
2059 
2060  if(i!=0) // to skip terminating 0
2061  result+=static_cast<char>(i);
2062  }
2063 
2064  return value=result, false;
2065  }
2066  }
2067 
2068  if(expr.id()==ID_string_constant)
2069  return value=expr.get(ID_value), false;
2070 
2071  return true;
2072 }
2073 
2075 {
2076  irep_idt result;
2077 
2078  if(get_string_constant(expr, result))
2079  {
2081  error() << "expected string constant, but got: "
2082  << expr.pretty() << eom;
2083 
2084  throw 0;
2085  }
2086 
2087  return result;
2088 }
2089 
2091 {
2092  if(expr.id()==ID_symbol)
2093  {
2094  const symbolt &symbol=
2095  ns.lookup(to_symbol_expr(expr));
2096 
2097  return symbol.value;
2098  }
2099  else if(expr.id()==ID_member)
2100  {
2101  exprt tmp=expr;
2102  tmp.op0()=get_constant(expr.op0());
2103  return tmp;
2104  }
2105  else if(expr.id()==ID_index)
2106  {
2107  exprt tmp=expr;
2108  tmp.op0()=get_constant(expr.op0());
2109  tmp.op1()=get_constant(expr.op1());
2110  return tmp;
2111  }
2112  else
2113  return expr;
2114 }
2115 
2117  const typet &type,
2118  const std::string &suffix,
2119  goto_programt &dest,
2120  const source_locationt &source_location)
2121 {
2122  symbolt &new_symbol=
2124  type,
2126  "tmp_"+suffix,
2127  source_location,
2128  irep_idt(),
2129  symbol_table);
2130 
2131  code_declt decl;
2132  decl.symbol()=new_symbol.symbol_expr();
2133  decl.add_source_location()=source_location;
2134  convert_decl(decl, dest);
2135 
2136  return new_symbol;
2137 }
2138 
2140  exprt &expr,
2141  const std::string &suffix,
2142  goto_programt &dest)
2143 {
2144  const source_locationt source_location=expr.find_source_location();
2145 
2146  symbolt &new_symbol=
2147  new_tmp_symbol(expr.type(), suffix, dest, source_location);
2148 
2149  code_assignt assignment;
2150  assignment.lhs()=new_symbol.symbol_expr();
2151  assignment.rhs()=expr;
2152  assignment.add_source_location()=source_location;
2153 
2154  convert(assignment, dest);
2155 
2156  expr=new_symbol.symbol_expr();
2157 }
2158 
2160 {
2161  // rename it
2162  get_new_name(symbol, ns);
2163 
2164  // store in symbol_table
2165  symbol_table.add(symbol);
2166 }
2167 
2168 const symbolt &goto_convertt::lookup(const irep_idt &identifier)
2169 {
2170  const symbolt *symbol;
2171  if(ns.lookup(identifier, symbol))
2172  {
2173  error() << "failed to find symbol " << identifier << eom;
2174  throw 0;
2175  }
2176  return *symbol;
2177 }
2178 
2180  const codet &code,
2182  goto_programt &dest,
2184 {
2185  const unsigned errors_before=
2186  message_handler.get_message_count(messaget::M_ERROR);
2187 
2188  goto_convertt goto_convert(symbol_table, message_handler);
2189 
2190  try
2191  {
2192  goto_convert.goto_convert(code, dest);
2193  }
2194 
2195  catch(int)
2196  {
2197  goto_convert.error();
2198  }
2199 
2200  catch(const char *e)
2201  {
2202  goto_convert.error() << e << messaget::eom;
2203  }
2204 
2205  catch(const std::string &e)
2206  {
2207  goto_convert.error() << e << messaget::eom;
2208  }
2209 
2210  if(message_handler.get_message_count(messaget::M_ERROR)!=errors_before)
2211  throw 0;
2212 }
2213 
2216  goto_programt &dest,
2218 {
2219  // find main symbol
2220  const symbol_tablet::symbolst::const_iterator s_it=
2221  symbol_table.symbols.find("main");
2222 
2223  if(s_it==symbol_table.symbols.end())
2224  throw "failed to find main symbol";
2225 
2226  const symbolt &symbol=s_it->second;
2227 
2228  ::goto_convert(to_code(symbol.value), symbol_table, dest, message_handler);
2229 }
void convert_atomic_begin(const codet &code, goto_programt &dest)
const irep_idt & get_statement() const
Definition: std_code.h:37
void convert_specc_event(const exprt &op, std::set< irep_idt > &events)
static bool is_empty(const goto_programt &goto_program)
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
void convert_skip(const codet &code, goto_programt &dest)
const codet & then_case() const
Definition: std_code.h:370
mstreamt & result()
Definition: message.h:233
void convert_gcc_switch_case_range(const codet &code, goto_programt &dest)
const exprt & return_value() const
Definition: std_code.h:728
goto_program_instruction_typet
The type of an instruction in a GOTO program.
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:218
exprt & true_case()
Definition: std_expr.h:2805
semantic type conversion
Definition: std_expr.h:1725
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
exprt::operandst caset
targett add_instruction()
Adds an instruction at the end.
A `switch&#39; instruction.
Definition: std_code.h:412
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
void convert(const codet &code, goto_programt &dest)
converts &#39;code&#39; and appends the result to &#39;dest&#39;
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
const exprt & init() const
Definition: std_code.h:556
symbol_tablet & symbol_table
goto_programt::targett return_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_tablet &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
exprt & op0()
Definition: expr.h:84
void unwind_destructor_stack(const source_locationt &, std::size_t stack_size, goto_programt &dest)
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:298
const exprt & cond() const
Definition: std_code.h:465
A continue for `for&#39; and `while&#39; loops.
Definition: std_code.h:898
void convert_ifthenelse(const code_ifthenelset &code, goto_programt &dest)
virtual void do_function_call(const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest)
std::vector< irept > subt
Definition: irep.h:91
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...
const exprt & cond() const
Definition: std_code.h:360
exprt & symbol()
Definition: std_code.h:205
mp_integer::ullong_t integer2ulong(const mp_integer &n)
Definition: mp_arith.cpp:189
guarded_gotost guarded_gotos
const codet & body() const
Definition: std_code.h:586
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
goto_programt::targett break_target
codet & code()
Definition: std_code.h:851
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
source_locationt end_location() const
Definition: std_code.h:89
#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:28
Fresh auxiliary symbol creation.
void convert_atomic_end(const codet &code, goto_programt &dest)
const irep_idt & get_value() const
Definition: std_expr.h:3702
const code_breakt & to_code_break(const codet &code)
Definition: std_code.h:884
void convert_assign(const code_assignt &code, goto_programt &dest)
void convert_dowhile(const codet &code, goto_programt &dest)
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
exprt value
Initial value of symbol.
Definition: symbol.h:40
void convert_init(const codet &code, goto_programt &dest)
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
bool is_true() const
Definition: expr.cpp:133
bool empty() const
Is the program empty?
void convert_goto(const codet &code, goto_programt &dest)
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void convert_end_thread(const codet &code, goto_programt &dest)
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
An expression statement.
Definition: std_code.h:957
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:981
void set_default(goto_programt::targett _default_target)
bool is_static_lifetime
Definition: symbol.h:70
const exprt & case_op() const
Definition: std_code.h:841
subt & get_sub()
Definition: irep.h:245
void convert_specc_wait(const codet &code, goto_programt &dest)
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1023
equality
Definition: std_expr.h:1082
destructor_stackt destructor_stack
static void collect_operands(const exprt &expr, const irep_idt &id, std::list< exprt > &dest)
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
void goto_convert(const codet &code, goto_programt &dest)
const irep_idt & id() const
Definition: irep.h:189
void convert_switch(const code_switcht &code, goto_programt &dest)
exprt & lhs()
Definition: std_code.h:157
void convert_decl_type(const codet &code, goto_programt &dest)
void do_java_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
The boolean constant true.
Definition: std_expr.h:3742
irep_idt get_string_constant(const exprt &expr)
argumentst & arguments()
Definition: std_code.h:689
symbolst symbols
Definition: symbol_table.h:57
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void make_next_state(exprt &expr)
Definition: expr_util.cpp:20
void convert_bp_abortif(const codet &code, goto_programt &dest)
void convert_for(const code_fort &code, goto_programt &dest)
std::string tmp_symbol_prefix
void convert_msc_try_finally(const codet &code, goto_programt &dest)
A declaration of a local variable.
Definition: std_code.h:192
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
exprt & rhs()
Definition: std_code.h:162
void convert_label(const code_labelt &code, goto_programt &dest)
const source_locationt & find_source_location() const
Definition: expr.cpp:466
const exprt & cond() const
Definition: std_code.h:566
source_locationt source_location
Definition: message.h:175
The empty type.
Definition: std_types.h:53
const code_whilet & to_code_while(const codet &code)
Definition: std_code.h:486
Program Transformation.
goto_programt::targett default_target
exprt case_guard(const exprt &value, const caset &case_op)
boolean AND
Definition: std_expr.h:1852
API to expression classes.
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:52
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
void convert_specc_notify(const codet &code, goto_programt &dest)
void convert_continue(const code_continuet &code, goto_programt &dest)
void convert_while(const code_whilet &code, goto_programt &dest)
void convert_CPROVER_try_finally(const codet &code, goto_programt &dest)
A label for branch targets.
Definition: std_code.h:760
const code_returnt & to_code_return(const codet &code)
Definition: std_code.h:746
Base class for tree-like data structures with sharing.
Definition: irep.h:87
A function call.
Definition: std_code.h:657
#define forall_operands(it, expr)
Definition: expr.h:17
void convert_msc_leave(const codet &code, goto_programt &dest)
A `while&#39; instruction.
Definition: std_code.h:457
const code_switch_caset & to_code_switch_case(const codet &code)
Definition: std_code.h:862
targett insert_after(const_targett target)
Insertion after the given target.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table.
void convert_asm(const code_asmt &code, goto_programt &dest)
Definition: goto_asm.cpp:14
void do_java_new_array(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void convert_specc_par(const codet &code, goto_programt &dest)
void finish_computed_gotos(goto_programt &dest)
Operator to return the address of an object.
Definition: std_expr.h:2593
void convert_return(const code_returnt &code, goto_programt &dest)
void convert_cpp_delete(const codet &code, goto_programt &dest)
void clean_expr(exprt &expr, goto_programt &dest, bool result_is_used=true)
#define forall_expr_list(it, expr)
Definition: expr.h:36
exprt & false_case()
Definition: std_expr.h:2815
void goto_convert_rec(const codet &code, goto_programt &dest)
const code_switcht & to_code_switch(const codet &code)
Definition: std_code.h:441
void convert_gcc_local_label(const codet &code, goto_programt &dest)
bool has_return_value() const
Definition: std_code.h:738
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
void convert_function_call(const code_function_callt &code, goto_programt &dest)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
static bool is_size_one(const goto_programt &g)
This is (believed to be) faster than using std::list.size.
void convert_assert(const code_assertt &code, goto_programt &dest)
An assertion.
Definition: std_code.h:312
void convert_CPROVER_try_catch(const codet &code, goto_programt &dest)
An assumption.
Definition: std_code.h:274
exprt get_constant(const exprt &expr)
void set_continue(goto_programt::targett _continue_target)
const exprt & value() const
Definition: std_code.h:420
typet type
Type of symbol.
Definition: symbol.h:37
const code_continuet & to_code_continue(const codet &code)
Definition: std_code.h:906
mstreamt & debug()
Definition: message.h:253
void make_not()
Definition: expr.cpp:100
static bool needs_cleaning(const exprt &expr)
goto_programt::targett continue_target
void convert_decl(const code_declt &code, goto_programt &dest)
void new_name(symbolt &symbol)
void convert_try_catch(const codet &code, goto_programt &dest)
void finish_guarded_gotos(goto_programt &dest)
For each if(x) goto z; goto y; z: emitted, see if any destructor statements were inserted between got...
void generate_conditional_branch(const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const source_locationt &, goto_programt &dest)
if(guard) goto target_true; else goto target_false;
void set_break(goto_programt::targett _break_target)
exprt & function()
Definition: std_code.h:677
void set_statement(const irep_idt &statement)
Definition: std_code.h:32
bool is_default() const
Definition: std_code.h:831
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &)
Base class for all expressions.
Definition: expr.h:46
const symbolt & lookup(const irep_idt &identifier)
A break for `for&#39; and `while&#39; loops.
Definition: std_code.h:876
void finish_gotos(goto_programt &dest)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
void convert_break(const code_breakt &code, goto_programt &dest)
void convert_loop_invariant(const codet &code, goto_programt::targett loop)
void convert_switch_case(const code_switch_caset &code, goto_programt &dest)
const exprt & assumption() const
Definition: std_code.h:287
computed_gotost computed_gotos
const source_locationt & source_location() const
Definition: expr.h:142
const exprt & iter() const
Definition: std_code.h:576
void make_temp_symbol(exprt &expr, const std::string &suffix, goto_programt &)
Program Transformation.
void convert_assume(const code_assumet &code, goto_programt &dest)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void convert_block(const code_blockt &code, goto_programt &dest)
A removal of a local variable.
Definition: std_code.h:234
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
Sequential composition.
Definition: std_code.h:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
const irep_idt & get_label() const
Definition: std_code.h:782
void destructive_insert(const_targett target, goto_program_templatet< codeT, guardT > &p)
Inserts the given program at the given location.
const code_fort & to_code_for(const codet &code)
Definition: std_code.h:597
An if-then-else.
Definition: std_code.h:350
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt & op2()
Definition: expr.h:90
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:120
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
A switch-case.
Definition: std_code.h:817
dstringt irep_idt
Definition: irep.h:32
A statement in a programming language.
Definition: std_code.h:19
void convert_msc_try_except(const codet &code, goto_programt &dest)
Return from a function.
Definition: std_code.h:714
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
code_function_callt get_destructor(const namespacet &ns, const typet &type)
Definition: destructor.cpp:17
A `for&#39; instruction.
Definition: std_code.h:547
const code_labelt & to_code_label(const codet &code)
Definition: std_code.h:803
void convert_bp_enforce(const codet &code, goto_programt &dest)
const typet & subtype() const
Definition: type.h:31
const code_assertt & to_code_assert(const codet &code)
Definition: std_code.h:336
void convert_expression(const code_expressiont &code, goto_programt &dest)
operandst & operands()
Definition: expr.h:70
void convert_start_thread(const codet &code, goto_programt &dest)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
const codet & else_case() const
Definition: std_code.h:380
void get_new_name(symbolt &symbol, const namespacet &ns)
automated variable renaming
Definition: rename.cpp:20
message_handlert * message_handler
Definition: message.h:259
const code_ifthenelset & to_code_ifthenelse(const codet &code)
Definition: std_code.h:396
void make_typecast(const typet &_type)
Definition: expr.cpp:90
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
Definition: expr_util.cpp:120
static void replace_new_object(const exprt &object, exprt &dest)
const codet & body() const
Definition: std_code.h:475
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:943
Assignment.
Definition: std_code.h:144
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
void swap(goto_program_templatet< codeT, guardT > &program)
Swap the goto program.
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700
void convert_CPROVER_throw(const codet &code, goto_programt &dest)
bool simplify(exprt &expr, const namespacet &ns)
const exprt & assertion() const
Definition: std_code.h:325
void generate_ifthenelse(const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest)
if(guard) true_case; else false_case;
void convert_non_deterministic_goto(const codet &code, goto_programt &dest)
#define forall_irep(it, irep)
Definition: irep.h:62
unsigned get_message_count(unsigned level) const
Definition: message.h:47