cprover
builtin_functions.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_class.h"
13 
14 #include <cassert>
15 
16 #include <util/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/cprover_prefix.h>
19 #include <util/expr_initializer.h>
20 #include <util/expr_util.h>
21 #include <util/mathematical_expr.h>
23 #include <util/prefix.h>
24 #include <util/rational.h>
25 #include <util/rational_tools.h>
26 
27 #include <langapi/language_util.h>
28 
29 #include "format_strings.h"
30 #include "class_identifier.h"
31 
33  const exprt &lhs,
34  const symbol_exprt &function,
35  const exprt::operandst &arguments,
36  goto_programt &dest)
37 {
38  const irep_idt &identifier = function.get_identifier();
39 
40  // make it a side effect if there is an LHS
41  if(arguments.size()!=2)
42  {
43  error().source_location=function.find_source_location();
44  error() << "'" << identifier << "' expected to have two arguments" << eom;
45  throw 0;
46  }
47 
48  if(lhs.is_nil())
49  {
50  error().source_location=function.find_source_location();
51  error() << "'" << identifier << "' expected to have LHS" << eom;
52  throw 0;
53  }
54 
55  auto rhs =
56  side_effect_exprt("prob_uniform", lhs.type(), function.source_location());
57 
58  if(lhs.type().id()!=ID_unsignedbv &&
59  lhs.type().id()!=ID_signedbv)
60  {
61  error().source_location=function.find_source_location();
62  error() << "'" << identifier << "' expected other type" << eom;
63  throw 0;
64  }
65 
66  if(arguments[0].type().id()!=lhs.type().id() ||
67  arguments[1].type().id()!=lhs.type().id())
68  {
69  error().source_location=function.find_source_location();
70  error() << "'" << identifier
71  << "' expected operands to be of same type as LHS" << eom;
72  throw 0;
73  }
74 
75  if(!arguments[0].is_constant() ||
76  !arguments[1].is_constant())
77  {
78  error().source_location=function.find_source_location();
79  error() << "'" << identifier
80  << "' expected operands to be constant literals" << eom;
81  throw 0;
82  }
83 
84  mp_integer lb, ub;
85 
86  if(
87  to_integer(to_constant_expr(arguments[0]), lb) ||
88  to_integer(to_constant_expr(arguments[1]), ub))
89  {
90  error().source_location=function.find_source_location();
91  error() << "error converting operands" << eom;
92  throw 0;
93  }
94 
95  if(lb > ub)
96  {
97  error().source_location=function.find_source_location();
98  error() << "expected lower bound to be smaller or equal to the "
99  << "upper bound" << eom;
100  throw 0;
101  }
102 
103  rhs.copy_to_operands(arguments[0], arguments[1]);
104 
105  code_assignt assignment(lhs, rhs);
106  assignment.add_source_location()=function.source_location();
107  copy(assignment, ASSIGN, dest);
108 }
109 
111  const exprt &lhs,
112  const symbol_exprt &function,
113  const exprt::operandst &arguments,
114  goto_programt &dest)
115 {
116  const irep_idt &identifier = function.get_identifier();
117 
118  // make it a side effect if there is an LHS
119  if(arguments.size()!=2)
120  {
121  error().source_location=function.find_source_location();
122  error() << "'" << identifier << "' expected to have two arguments" << eom;
123  throw 0;
124  }
125 
126  if(lhs.is_nil())
127  {
128  error().source_location=function.find_source_location();
129  error() << "'" << identifier << "' expected to have LHS" << eom;
130  throw 0;
131  }
132 
133  side_effect_exprt rhs("prob_coin", lhs.type(), function.source_location());
134 
135  if(lhs.type()!=bool_typet())
136  {
137  error().source_location=function.find_source_location();
138  error() << "'" << identifier << "' expected bool" << eom;
139  throw 0;
140  }
141 
142  if(arguments[0].type().id()!=ID_unsignedbv ||
143  arguments[0].id()!=ID_constant)
144  {
145  error().source_location=function.find_source_location();
146  error() << "'" << identifier << "' expected first operand to be "
147  << "a constant literal of type unsigned long" << eom;
148  throw 0;
149  }
150 
151  if(
152  arguments[1].type().id() != ID_unsignedbv ||
153  arguments[1].id() != ID_constant)
154  {
155  error().source_location = function.find_source_location();
156  error() << "'" << identifier << "' expected second operand to be "
157  << "a constant literal of type unsigned long" << eom;
158  throw 0;
159  }
160 
161  mp_integer num, den;
162 
163  if(
164  to_integer(to_constant_expr(arguments[0]), num) ||
165  to_integer(to_constant_expr(arguments[1]), den))
166  {
167  error().source_location=function.find_source_location();
168  error() << "error converting operands" << eom;
169  throw 0;
170  }
171 
172  if(num-den > mp_integer(0))
173  {
174  error().source_location=function.find_source_location();
175  error() << "probability has to be smaller than 1" << eom;
176  throw 0;
177  }
178 
179  if(den == mp_integer(0))
180  {
181  error().source_location=function.find_source_location();
182  error() << "denominator may not be zero" << eom;
183  throw 0;
184  }
185 
186  rationalt numerator(num), denominator(den);
187  rationalt prob = numerator / denominator;
188 
189  rhs.copy_to_operands(from_rational(prob));
190 
191  code_assignt assignment(lhs, rhs);
192  assignment.add_source_location()=function.source_location();
193  copy(assignment, ASSIGN, dest);
194 }
195 
197  const exprt &lhs,
198  const symbol_exprt &function,
199  const exprt::operandst &arguments,
200  goto_programt &dest)
201 {
202  const irep_idt &f_id = function.get_identifier();
203 
204  PRECONDITION(f_id == CPROVER_PREFIX "printf");
205 
206  codet printf_code(ID_printf, arguments, function.source_location());
207  copy(printf_code, OTHER, dest);
208 }
209 
211  const exprt &lhs,
212  const symbol_exprt &function,
213  const exprt::operandst &arguments,
214  goto_programt &dest)
215 {
216  const irep_idt &f_id = function.get_identifier();
217 
218  if(f_id==CPROVER_PREFIX "scanf")
219  {
220  if(arguments.empty())
221  {
222  error().source_location=function.find_source_location();
223  error() << "scanf takes at least one argument" << eom;
224  throw 0;
225  }
226 
227  irep_idt format_string;
228 
229  if(!get_string_constant(arguments[0], format_string))
230  {
231  // use our model
232  format_token_listt token_list=
233  parse_format_string(id2string(format_string));
234 
235  std::size_t argument_number=1;
236 
237  for(const auto &t : token_list)
238  {
239  const auto type = get_type(t);
240 
241  if(type.has_value())
242  {
243  if(argument_number<arguments.size())
244  {
245  const typecast_exprt ptr(
246  arguments[argument_number], pointer_type(*type));
247  argument_number++;
248 
249  if(type->id() == ID_array)
250  {
251  #if 0
252  // A string. We first need a nondeterministic size.
254  to_array_type(*type).size()=size;
255 
256  const symbolt &tmp_symbol=
258  *type, "scanf_string", dest, function.source_location());
259 
260  const address_of_exprt rhs(
261  index_exprt(
262  tmp_symbol.symbol_expr(),
263  from_integer(0, index_type())));
264 
265  // now use array copy
266  codet array_copy_statement;
267  array_copy_statement.set_statement(ID_array_copy);
268  array_copy_statement.operands().resize(2);
269  array_copy_statement.op0()=ptr;
270 \ array_copy_statement.op1()=rhs;
271  array_copy_statement.add_source_location()=
272  function.source_location();
273 
274  copy(array_copy_statement, OTHER, dest);
275  #else
276  const index_exprt new_lhs(
278  const side_effect_expr_nondett rhs(
279  type->subtype(), function.source_location());
280  code_assignt assign(new_lhs, rhs);
281  assign.add_source_location()=function.source_location();
282  copy(assign, ASSIGN, dest);
283  #endif
284  }
285  else
286  {
287  // make it nondet for now
288  const dereference_exprt new_lhs{ptr};
289  const side_effect_expr_nondett rhs(
290  *type, function.source_location());
291  code_assignt assign(new_lhs, rhs);
292  assign.add_source_location()=function.source_location();
293  copy(assign, ASSIGN, dest);
294  }
295  }
296  }
297  }
298  }
299  else
300  {
301  // we'll just do nothing
302  code_function_callt function_call(lhs, function, arguments);
303  function_call.add_source_location()=function.source_location();
304 
305  copy(function_call, FUNCTION_CALL, dest);
306  }
307  }
308  else
309  UNREACHABLE;
310 }
311 
313  const exprt &function,
314  const exprt::operandst &arguments,
315  goto_programt &dest)
316 {
317  if(arguments.size()<2)
318  {
319  error().source_location=function.find_source_location();
320  error() << "input takes at least two arguments" << eom;
321  throw 0;
322  }
323 
324  copy(code_inputt{arguments, function.source_location()}, OTHER, dest);
325 }
326 
328  const exprt &function,
329  const exprt::operandst &arguments,
330  goto_programt &dest)
331 {
332  if(arguments.size()<2)
333  {
334  error().source_location=function.find_source_location();
335  error() << "output takes at least two arguments" << eom;
336  throw 0;
337  }
338 
339  copy(code_outputt{arguments, function.source_location()}, OTHER, dest);
340 }
341 
343  const exprt &lhs,
344  const symbol_exprt &function,
345  const exprt::operandst &arguments,
346  goto_programt &dest)
347 {
348  if(lhs.is_not_nil())
349  {
351  error() << "atomic_begin does not expect an LHS" << eom;
352  throw 0;
353  }
354 
355  if(!arguments.empty())
356  {
357  error().source_location=function.find_source_location();
358  error() << "atomic_begin takes no arguments" << eom;
359  throw 0;
360  }
361 
362  dest.add(goto_programt::make_atomic_begin(function.source_location()));
363 }
364 
366  const exprt &lhs,
367  const symbol_exprt &function,
368  const exprt::operandst &arguments,
369  goto_programt &dest)
370 {
371  if(lhs.is_not_nil())
372  {
374  error() << "atomic_end does not expect an LHS" << eom;
375  throw 0;
376  }
377 
378  if(!arguments.empty())
379  {
380  error().source_location=function.find_source_location();
381  error() << "atomic_end takes no arguments" << eom;
382  throw 0;
383  }
384 
385  dest.add(goto_programt::make_atomic_end(function.source_location()));
386 }
387 
389  const exprt &lhs,
390  const side_effect_exprt &rhs,
391  goto_programt &dest)
392 {
393  if(lhs.is_nil())
394  {
396  error() << "do_cpp_new without lhs is yet to be implemented" << eom;
397  throw 0;
398  }
399 
400  // build size expression
402  static_cast<const exprt &>(rhs.find(ID_sizeof));
403 
404  bool new_array=rhs.get(ID_statement)==ID_cpp_new_array;
405 
406  exprt count;
407 
408  if(new_array)
409  {
411  static_cast<const exprt &>(rhs.find(ID_size)), object_size.type());
412 
413  // might have side-effect
414  clean_expr(count, dest, ID_cpp);
415  }
416 
417  exprt tmp_symbol_expr;
418 
419  // is this a placement new?
420  if(rhs.operands().empty()) // no, "regular" one
421  {
422  // call __new or __new_array
423  exprt new_symbol=
424  ns.lookup(new_array?"__new_array":"__new").symbol_expr();
425 
426  const code_typet &code_type=
427  to_code_type(new_symbol.type());
428 
429  const typet &return_type=
430  code_type.return_type();
431 
432  assert(code_type.parameters().size()==1 ||
433  code_type.parameters().size()==2);
434 
435  const symbolt &tmp_symbol =
436  new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
437 
438  tmp_symbol_expr=tmp_symbol.symbol_expr();
439 
440  code_function_callt new_call(new_symbol);
441  if(new_array)
442  new_call.arguments().push_back(count);
443  new_call.arguments().push_back(object_size);
444  new_call.set(ID_C_cxx_alloc_type, lhs.type().subtype());
445  new_call.lhs()=tmp_symbol_expr;
446  new_call.add_source_location()=rhs.source_location();
447 
448  convert(new_call, dest, ID_cpp);
449  }
450  else if(rhs.operands().size()==1)
451  {
452  // call __placement_new
453  exprt new_symbol=
454  ns.lookup(
455  new_array?"__placement_new_array":"__placement_new").symbol_expr();
456 
457  const code_typet &code_type=
458  to_code_type(new_symbol.type());
459 
460  const typet &return_type=code_type.return_type();
461 
462  assert(code_type.parameters().size()==2 ||
463  code_type.parameters().size()==3);
464 
465  const symbolt &tmp_symbol =
466  new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
467 
468  tmp_symbol_expr=tmp_symbol.symbol_expr();
469 
470  code_function_callt new_call(new_symbol);
471  if(new_array)
472  new_call.arguments().push_back(count);
473  new_call.arguments().push_back(object_size);
474  new_call.arguments().push_back(to_unary_expr(rhs).op()); // memory location
475  new_call.set(ID_C_cxx_alloc_type, lhs.type().subtype());
476  new_call.lhs()=tmp_symbol_expr;
477  new_call.add_source_location()=rhs.source_location();
478 
479  for(std::size_t i=0; i<code_type.parameters().size(); i++)
480  {
482  new_call.arguments()[i], code_type.parameters()[i].type());
483  }
484 
485  convert(new_call, dest, ID_cpp);
486  }
487  else
488  {
490  error() << "cpp_new expected to have 0 or 1 operands" << eom;
491  throw 0;
492  }
493 
495  lhs,
496  typecast_exprt(tmp_symbol_expr, lhs.type()),
497  rhs.find_source_location()));
498 
499  // grab initializer
500  goto_programt tmp_initializer;
501  cpp_new_initializer(lhs, rhs, tmp_initializer);
502 
503  dest.destructive_append(tmp_initializer);
504 }
505 
508  const exprt &lhs,
509  const side_effect_exprt &rhs,
510  goto_programt &dest)
511 {
512  exprt initializer=
513  static_cast<const exprt &>(rhs.find(ID_initializer));
514 
515  if(initializer.is_not_nil())
516  {
517  if(rhs.get_statement()=="cpp_new[]")
518  {
519  // build loop
520  }
521  else if(rhs.get_statement()==ID_cpp_new)
522  {
523  // just one object
524  const dereference_exprt deref_lhs(lhs, rhs.type().subtype());
525 
526  replace_new_object(deref_lhs, initializer);
527  convert(to_code(initializer), dest, ID_cpp);
528  }
529  else
530  UNREACHABLE;
531  }
532 }
533 
535 {
536  if(src.id()==ID_typecast)
537  return get_array_argument(to_typecast_expr(src).op());
538 
539  if(src.id()!=ID_address_of)
540  {
542  error() << "expected array-pointer as argument" << eom;
543  throw 0;
544  }
545 
546  const auto &address_of_expr = to_address_of_expr(src);
547 
548  if(address_of_expr.object().id() != ID_index)
549  {
551  error() << "expected array-element as argument" << eom;
552  throw 0;
553  }
554 
555  const auto &index_expr = to_index_expr(address_of_expr.object());
556 
557  if(index_expr.array().type().id() != ID_array)
558  {
560  error() << "expected array as argument" << eom;
561  throw 0;
562  }
563 
564  return index_expr.array();
565 }
566 
568  const irep_idt &id,
569  const exprt &lhs,
570  const symbol_exprt &function,
571  const exprt::operandst &arguments,
572  goto_programt &dest)
573 {
574  if(arguments.size()!=2)
575  {
576  error().source_location=function.find_source_location();
577  error() << id << " expects two arguments" << eom;
578  throw 0;
579  }
580 
581  codet array_op_statement(id);
582  array_op_statement.operands()=arguments;
583  array_op_statement.add_source_location()=function.source_location();
584 
585  // lhs is only used with array_equal, in all other cases it should be nil (as
586  // they are of type void)
587  if(id == ID_array_equal)
588  array_op_statement.copy_to_operands(lhs);
589 
590  copy(array_op_statement, OTHER, dest);
591 }
592 
594 {
595  exprt result = skip_typecast(expr);
596 
597  // if it's an address of an lvalue, we take that
598  if(result.id() == ID_address_of)
599  {
600  const auto &address_of_expr = to_address_of_expr(result);
601  if(is_lvalue(address_of_expr.object()))
602  result = address_of_expr.object();
603  }
604 
605  while(result.type().id() == ID_array &&
606  to_array_type(result.type()).size().is_one())
607  {
608  result = index_exprt{result, from_integer(0, index_type())};
609  }
610 
611  return result;
612 }
613 
616  const exprt &lhs,
617  const symbol_exprt &function,
618  const exprt::operandst &arguments,
619  goto_programt &dest)
620 {
621  if(function.get_bool(ID_C_invalid_object))
622  return; // ignore
623 
624  // lookup symbol
625  const irep_idt &identifier=function.get_identifier();
626 
627  const symbolt *symbol;
628  if(ns.lookup(identifier, symbol))
629  {
630  error().source_location=function.find_source_location();
631  error() << "error: function '" << identifier << "' not found" << eom;
632  throw 0;
633  }
634 
635  if(symbol->type.id()!=ID_code)
636  {
637  error().source_location=function.find_source_location();
638  error() << "error: function '" << identifier
639  << "' type mismatch: expected code" << eom;
640  throw 0;
641  }
642 
643  // User-provided function definitions always take precedence over built-ins.
644  // Front-ends do not (yet) consistently set ID_C_incomplete, thus also test
645  // whether the symbol actually has some non-nil value (which might be
646  // "compiled").
647  if(!symbol->type.get_bool(ID_C_incomplete) && symbol->value.is_not_nil())
648  {
649  do_function_call_symbol(*symbol);
650 
651  code_function_callt function_call(lhs, function, arguments);
652  function_call.add_source_location() = function.source_location();
653 
654  copy(function_call, FUNCTION_CALL, dest);
655 
656  return;
657  }
658 
659  if(identifier==CPROVER_PREFIX "assume" ||
660  identifier=="__VERIFIER_assume")
661  {
662  if(arguments.size()!=1)
663  {
664  error().source_location=function.find_source_location();
665  error() << "'" << identifier << "' expected to have one argument" << eom;
666  throw 0;
667  }
668 
669  // let's double-check the type of the argument
671  typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
672  function.source_location()));
673 
674  t->source_location.set("user-provided", true);
675 
676  if(lhs.is_not_nil())
677  {
678  error().source_location=function.find_source_location();
679  error() << identifier << " expected not to have LHS" << eom;
680  throw 0;
681  }
682  }
683  else if(identifier=="__VERIFIER_error")
684  {
685  if(!arguments.empty())
686  {
687  error().source_location=function.find_source_location();
688  error() << "'" << identifier << "' expected to have no arguments" << eom;
689  throw 0;
690  }
691 
692  goto_programt::targett t = dest.add(
693  goto_programt::make_assertion(false_exprt(), function.source_location()));
694 
695  t->source_location.set("user-provided", true);
696  t->source_location.set_property_class(ID_assertion);
697 
698  if(lhs.is_not_nil())
699  {
700  error().source_location=function.find_source_location();
701  error() << identifier << " expected not to have LHS" << eom;
702  throw 0;
703  }
704 
705  // __VERIFIER_error has abort() semantics, even if no assertions
706  // are being checked
708  false_exprt(), function.source_location()));
709  a->source_location.set("user-provided", true);
710  }
711  else if(
712  identifier == "assert" &&
714  {
715  if(arguments.size()!=1)
716  {
717  error().source_location=function.find_source_location();
718  error() << "'" << identifier << "' expected to have one argument" << eom;
719  throw 0;
720  }
721 
722  // let's double-check the type of the argument
724  typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
725  function.source_location()));
726  t->source_location.set("user-provided", true);
727  t->source_location.set_property_class(ID_assertion);
728  t->source_location.set_comment(
729  "assertion " + from_expr(ns, identifier, arguments.front()));
730 
731  if(lhs.is_not_nil())
732  {
733  error().source_location=function.find_source_location();
734  error() << identifier << " expected not to have LHS" << eom;
735  throw 0;
736  }
737  }
738  else if(
739  identifier == CPROVER_PREFIX "assert" ||
740  identifier == CPROVER_PREFIX "precondition" ||
741  identifier == CPROVER_PREFIX "postcondition")
742  {
743  if(arguments.size()!=2)
744  {
745  error().source_location=function.find_source_location();
746  error() << "'" << identifier << "' expected to have two arguments" << eom;
747  throw 0;
748  }
749 
750  bool is_precondition=
751  identifier==CPROVER_PREFIX "precondition";
752  bool is_postcondition = identifier == CPROVER_PREFIX "postcondition";
753 
754  const irep_idt description=
755  get_string_constant(arguments[1]);
756 
757  // let's double-check the type of the argument
760  function.source_location()));
761 
762  if(is_precondition)
763  {
764  t->source_location.set_property_class(ID_precondition);
765  }
766  else if(is_postcondition)
767  {
768  t->source_location.set_property_class(ID_postcondition);
769  }
770  else
771  {
772  t->source_location.set(
773  "user-provided",
774  !function.source_location().is_built_in());
775  t->source_location.set_property_class(ID_assertion);
776  }
777 
778  t->source_location.set_comment(description);
779 
780  if(lhs.is_not_nil())
781  {
782  error().source_location=function.find_source_location();
783  error() << identifier << " expected not to have LHS" << eom;
784  throw 0;
785  }
786  }
787  else if(identifier==CPROVER_PREFIX "havoc_object")
788  {
789  if(arguments.size()!=1)
790  {
791  error().source_location=function.find_source_location();
792  error() << "'" << identifier << "' expected to have one argument" << eom;
793  throw 0;
794  }
795 
796  if(lhs.is_not_nil())
797  {
798  error().source_location=function.find_source_location();
799  error() << identifier << " expected not to have LHS" << eom;
800  throw 0;
801  }
802 
803  codet havoc(ID_havoc_object);
804  havoc.add_source_location() = function.source_location();
805  havoc.copy_to_operands(arguments[0]);
806 
807  dest.add(goto_programt::make_other(havoc, function.source_location()));
808  }
809  else if(identifier==CPROVER_PREFIX "printf")
810  {
811  do_printf(lhs, function, arguments, dest);
812  }
813  else if(identifier==CPROVER_PREFIX "scanf")
814  {
815  do_scanf(lhs, function, arguments, dest);
816  }
817  else if(identifier==CPROVER_PREFIX "input" ||
818  identifier=="__CPROVER::input")
819  {
820  if(lhs.is_not_nil())
821  {
822  error().source_location=function.find_source_location();
823  error() << identifier << " expected not to have LHS" << eom;
824  throw 0;
825  }
826 
827  do_input(function, arguments, dest);
828  }
829  else if(identifier==CPROVER_PREFIX "output" ||
830  identifier=="__CPROVER::output")
831  {
832  if(lhs.is_not_nil())
833  {
834  error().source_location=function.find_source_location();
835  error() << identifier << " expected not to have LHS" << eom;
836  throw 0;
837  }
838 
839  do_output(function, arguments, dest);
840  }
841  else if(identifier==CPROVER_PREFIX "atomic_begin" ||
842  identifier=="__CPROVER::atomic_begin" ||
843  identifier=="java::org.cprover.CProver.atomicBegin:()V" ||
844  identifier=="__VERIFIER_atomic_begin")
845  {
846  do_atomic_begin(lhs, function, arguments, dest);
847  }
848  else if(identifier==CPROVER_PREFIX "atomic_end" ||
849  identifier=="__CPROVER::atomic_end" ||
850  identifier=="java::org.cprover.CProver.atomicEnd:()V" ||
851  identifier=="__VERIFIER_atomic_end")
852  {
853  do_atomic_end(lhs, function, arguments, dest);
854  }
855  else if(identifier==CPROVER_PREFIX "prob_biased_coin")
856  {
857  do_prob_coin(lhs, function, arguments, dest);
858  }
859  else if(has_prefix(id2string(identifier), CPROVER_PREFIX "prob_uniform_"))
860  {
861  do_prob_uniform(lhs, function, arguments, dest);
862  }
863  else if(has_prefix(id2string(identifier), "nondet_") ||
864  has_prefix(id2string(identifier), "__VERIFIER_nondet_"))
865  {
866  // make it a side effect if there is an LHS
867  if(lhs.is_nil())
868  return;
869 
870  exprt rhs;
871 
872  // We need to special-case for _Bool, which
873  // can only be 0 or 1.
874  if(lhs.type().id()==ID_c_bool)
875  {
876  rhs = side_effect_expr_nondett(bool_typet(), function.source_location());
877  rhs.set(ID_C_identifier, identifier);
878  rhs=typecast_exprt(rhs, lhs.type());
879  }
880  else
881  {
882  rhs = side_effect_expr_nondett(lhs.type(), function.source_location());
883  rhs.set(ID_C_identifier, identifier);
884  }
885 
886  code_assignt assignment(lhs, rhs);
887  assignment.add_source_location()=function.source_location();
888  copy(assignment, ASSIGN, dest);
889  }
890  else if(has_prefix(id2string(identifier), CPROVER_PREFIX "uninterpreted_"))
891  {
892  // make it a side effect if there is an LHS
893  if(lhs.is_nil())
894  return;
895 
896  const function_application_exprt rhs(function, arguments, lhs.type());
897 
898  code_assignt assignment(lhs, rhs);
899  assignment.add_source_location()=function.source_location();
900  copy(assignment, ASSIGN, dest);
901  }
902  else if(identifier==CPROVER_PREFIX "array_equal")
903  {
904  do_array_op(ID_array_equal, lhs, function, arguments, dest);
905  }
906  else if(identifier==CPROVER_PREFIX "array_set")
907  {
908  do_array_op(ID_array_set, lhs, function, arguments, dest);
909  }
910  else if(identifier==CPROVER_PREFIX "array_copy")
911  {
912  do_array_op(ID_array_copy, lhs, function, arguments, dest);
913  }
914  else if(identifier==CPROVER_PREFIX "array_replace")
915  {
916  do_array_op(ID_array_replace, lhs, function, arguments, dest);
917  }
918  else if(identifier=="__assert_fail" ||
919  identifier=="_assert" ||
920  identifier=="__assert_c99" ||
921  identifier=="_wassert")
922  {
923  // __assert_fail is Linux
924  // These take four arguments:
925  // "expression", "file.c", line, __func__
926  // klibc has __assert_fail with 3 arguments
927  // "expression", "file.c", line
928 
929  // MingW has
930  // void _assert (const char*, const char*, int);
931  // with three arguments:
932  // "expression", "file.c", line
933 
934  // This has been seen in Solaris 11.
935  // Signature:
936  // void __assert_c99(
937  // const char *desc, const char *file, int line, const char *func);
938 
939  // _wassert is Windows. The arguments are
940  // L"expression", L"file.c", line
941 
942  if(arguments.size()!=4 &&
943  arguments.size()!=3)
944  {
945  error().source_location=function.find_source_location();
946  error() << "'" << identifier << "' expected to have four arguments"
947  << eom;
948  throw 0;
949  }
950 
951  const irep_idt description=
952  "assertion "+id2string(get_string_constant(arguments[0]));
953 
954  goto_programt::targett t = dest.add(
955  goto_programt::make_assertion(false_exprt(), function.source_location()));
956 
957  t->source_location.set("user-provided", true);
958  t->source_location.set_property_class(ID_assertion);
959  t->source_location.set_comment(description);
960  // we ignore any LHS
961  }
962  else if(identifier=="__assert_rtn" ||
963  identifier=="__assert")
964  {
965  // __assert_rtn has been seen on MacOS;
966  // __assert is FreeBSD and Solaris 11.
967  // These take four arguments:
968  // __func__, "file.c", line, "expression"
969  // On Solaris 11, it's three arguments:
970  // "expression", "file", line
971 
972  irep_idt description;
973 
974  if(arguments.size()==4)
975  {
976  description=
977  "assertion "+id2string(get_string_constant(arguments[3]));
978  }
979  else if(arguments.size()==3)
980  {
981  description=
982  "assertion "+id2string(get_string_constant(arguments[1]));
983  }
984  else
985  {
986  error().source_location=function.find_source_location();
987  error() << "'" << identifier << "' expected to have four arguments"
988  << eom;
989  throw 0;
990  }
991 
992  goto_programt::targett t = dest.add(
993  goto_programt::make_assertion(false_exprt(), function.source_location()));
994 
995  t->source_location.set("user-provided", true);
996  t->source_location.set_property_class(ID_assertion);
997  t->source_location.set_comment(description);
998  // we ignore any LHS
999  }
1000  else if(identifier=="__assert_func")
1001  {
1002  // __assert_func is newlib (used by, e.g., cygwin)
1003  // These take four arguments:
1004  // "file.c", line, __func__, "expression"
1005  if(arguments.size()!=4)
1006  {
1007  error().source_location=function.find_source_location();
1008  error() << "'" << identifier << "' expected to have four arguments"
1009  << eom;
1010  throw 0;
1011  }
1012 
1013  irep_idt description;
1014  try
1015  {
1016  description="assertion "+id2string(get_string_constant(arguments[3]));
1017  }
1018  catch(int)
1019  {
1020  // we might be building newlib, where __assert_func is passed
1021  // a pointer-typed symbol; the warning will still have been
1022  // printed
1023  description="assertion";
1024  }
1025 
1026  goto_programt::targett t = dest.add(
1027  goto_programt::make_assertion(false_exprt(), function.source_location()));
1028 
1029  t->source_location.set("user-provided", true);
1030  t->source_location.set_property_class(ID_assertion);
1031  t->source_location.set_comment(description);
1032  // we ignore any LHS
1033  }
1034  else if(identifier==CPROVER_PREFIX "fence")
1035  {
1036  if(arguments.empty())
1037  {
1038  error().source_location=function.find_source_location();
1039  error() << "'" << identifier << "' expected to have at least one argument"
1040  << eom;
1041  throw 0;
1042  }
1043 
1044  codet fence(ID_fence);
1045 
1046  forall_expr(it, arguments)
1047  fence.set(get_string_constant(*it), true);
1048 
1049  dest.add(goto_programt::make_other(fence, function.source_location()));
1050  }
1051  else if(identifier=="__builtin_prefetch")
1052  {
1053  // does nothing
1054  }
1055  else if(identifier=="__builtin_unreachable")
1056  {
1057  // says something like UNREACHABLE;
1058  }
1059  else if(identifier==ID_gcc_builtin_va_arg)
1060  {
1061  // This does two things.
1062  // 1) Return value of argument.
1063  // This is just dereferencing.
1064  // 2) Move list pointer to next argument.
1065  // This is just an increment.
1066 
1067  if(arguments.size()!=1)
1068  {
1069  error().source_location=function.find_source_location();
1070  error() << "'" << identifier << "' expected to have one argument" << eom;
1071  throw 0;
1072  }
1073 
1074  exprt list_arg=make_va_list(arguments[0]);
1075 
1076  if(lhs.is_not_nil())
1077  {
1078  exprt list_arg_cast = list_arg;
1079  if(
1080  list_arg.type().id() == ID_pointer &&
1081  to_pointer_type(list_arg.type()).subtype().id() == ID_empty)
1082  {
1083  list_arg_cast =
1085  }
1086 
1087  typet t=pointer_type(lhs.type());
1088  dereference_exprt rhs{
1089  typecast_exprt{dereference_exprt{std::move(list_arg_cast)}, t}};
1090  rhs.add_source_location()=function.source_location();
1091  dest.add(
1092  goto_programt::make_assignment(lhs, rhs, function.source_location()));
1093  }
1094 
1095  code_assignt assign{
1096  list_arg, plus_exprt{list_arg, from_integer(1, pointer_diff_type())}};
1097  assign.rhs().set(
1098  ID_C_va_arg_type, to_code_type(function.type()).return_type());
1100  std::move(assign), function.source_location()));
1101  }
1102  else if(identifier=="__builtin_va_copy")
1103  {
1104  if(arguments.size()!=2)
1105  {
1106  error().source_location=function.find_source_location();
1107  error() << "'" << identifier << "' expected to have two arguments" << eom;
1108  throw 0;
1109  }
1110 
1111  exprt dest_expr=make_va_list(arguments[0]);
1112  const typecast_exprt src_expr(arguments[1], dest_expr.type());
1113 
1114  if(!is_lvalue(dest_expr))
1115  {
1117  error() << "va_copy argument expected to be lvalue" << eom;
1118  throw 0;
1119  }
1120 
1122  dest_expr, src_expr, function.source_location()));
1123  }
1124  else if(identifier == "__builtin_va_start" || identifier == "__va_start")
1125  {
1126  // Set the list argument to be the address of the
1127  // parameter argument.
1128  if(arguments.size()!=2)
1129  {
1130  error().source_location=function.find_source_location();
1131  error() << "'" << identifier << "' expected to have two arguments" << eom;
1132  throw 0;
1133  }
1134 
1135  exprt dest_expr=make_va_list(arguments[0]);
1136 
1137  if(!is_lvalue(dest_expr))
1138  {
1140  error() << "va_start argument expected to be lvalue" << eom;
1141  throw 0;
1142  }
1143 
1144  if(
1145  dest_expr.type().id() == ID_pointer &&
1146  to_pointer_type(dest_expr.type()).subtype().id() == ID_empty)
1147  {
1148  dest_expr =
1150  }
1151 
1152  side_effect_exprt rhs{
1153  ID_va_start, dest_expr.type(), function.source_location()};
1154  rhs.add_to_operands(
1155  typecast_exprt{address_of_exprt{arguments[1]}, dest_expr.type()});
1156 
1158  std::move(dest_expr), std::move(rhs), function.source_location()));
1159  }
1160  else if(identifier=="__builtin_va_end")
1161  {
1162  // Invalidates the argument. We do so by setting it to NULL.
1163  if(arguments.size()!=1)
1164  {
1165  error().source_location=function.find_source_location();
1166  error() << "'" << identifier << "' expected to have one argument" << eom;
1167  throw 0;
1168  }
1169 
1170  exprt dest_expr=make_va_list(arguments[0]);
1171 
1172  if(!is_lvalue(dest_expr))
1173  {
1175  error() << "va_end argument expected to be lvalue" << eom;
1176  throw 0;
1177  }
1178 
1179  // our __builtin_va_list is a pointer
1180  if(dest_expr.type().id() == ID_pointer)
1181  {
1182  const auto zero =
1183  zero_initializer(dest_expr.type(), function.source_location(), ns);
1184  CHECK_RETURN(zero.has_value());
1186  dest_expr, *zero, function.source_location()));
1187  }
1188  }
1189  else if(
1190  identifier == "__builtin_isgreater" ||
1191  identifier == "__builtin_isgreaterequal" ||
1192  identifier == "__builtin_isless" || identifier == "__builtin_islessequal" ||
1193  identifier == "__builtin_islessgreater" ||
1194  identifier == "__builtin_isunordered")
1195  {
1196  // these support two double or two float arguments; we call the
1197  // appropriate internal version
1198  if(arguments.size()!=2 ||
1199  (arguments[0].type()!=double_type() &&
1200  arguments[0].type()!=float_type()) ||
1201  (arguments[1].type()!=double_type() &&
1202  arguments[1].type()!=float_type()))
1203  {
1204  error().source_location=function.find_source_location();
1205  error() << "'" << identifier
1206  << "' expected to have two float/double arguments" << eom;
1207  throw 0;
1208  }
1209 
1210  exprt::operandst new_arguments=arguments;
1211 
1212  bool use_double=arguments[0].type()==double_type();
1213  if(arguments[0].type()!=arguments[1].type())
1214  {
1215  if(use_double)
1216  {
1217  new_arguments[1] =
1218  typecast_exprt(new_arguments[1], arguments[0].type());
1219  }
1220  else
1221  {
1222  new_arguments[0] =
1223  typecast_exprt(new_arguments[0], arguments[1].type());
1224  use_double=true;
1225  }
1226  }
1227 
1228  code_typet f_type=to_code_type(function.type());
1229  f_type.remove_ellipsis();
1230  const typet &a_t=new_arguments[0].type();
1231  f_type.parameters()=
1233 
1234  // replace __builtin_ by CPROVER_PREFIX
1235  std::string name=CPROVER_PREFIX+id2string(identifier).substr(10);
1236  // append d or f for double/float
1237  name+=use_double?'d':'f';
1238 
1239  symbol_exprt new_function=function;
1240  new_function.set_identifier(name);
1241  new_function.type()=f_type;
1242 
1243  code_function_callt function_call(lhs, new_function, new_arguments);
1244  function_call.add_source_location()=function.source_location();
1245 
1246  if(!symbol_table.has_symbol(name))
1247  {
1248  symbolt new_symbol;
1249  new_symbol.base_name=name;
1250  new_symbol.name=name;
1251  new_symbol.type=f_type;
1252  new_symbol.location=function.source_location();
1253  symbol_table.add(new_symbol);
1254  }
1255 
1256  copy(function_call, FUNCTION_CALL, dest);
1257  }
1258  else
1259  {
1260  do_function_call_symbol(*symbol);
1261 
1262  // insert function call
1263  code_function_callt function_call(lhs, function, arguments);
1264  function_call.add_source_location()=function.source_location();
1265 
1266  copy(function_call, FUNCTION_CALL, dest);
1267  }
1268 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:150
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
goto_convertt::do_cpp_new
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
Definition: builtin_functions.cpp:388
typet::subtype
const typet & subtype() const
Definition: type.h:47
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:217
goto_convertt::do_output
void do_output(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:327
parse_format_string
format_token_listt parse_format_string(const std::string &arg_string)
Definition: format_strings.cpp:187
goto_convertt::ns
namespacet ns
Definition: goto_convert_class.h:50
arith_tools.h
codet::op0
exprt & op0()
Definition: expr.h:102
rational.h
rational_tools.h
goto_convertt::replace_new_object
static void replace_new_object(const exprt &object, exprt &dest)
Definition: goto_convert_side_effect.cpp:347
goto_convertt::convert
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
Definition: goto_convert.cpp:426
goto_convertt::copy
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
Definition: goto_convert.cpp:296
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
goto_convertt::clean_expr
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
Definition: goto_clean_expr.cpp:161
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
goto_convertt::get_array_argument
exprt get_array_argument(const exprt &src)
Definition: builtin_functions.cpp:534
goto_convertt::cpp_new_initializer
void cpp_new_initializer(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
builds a goto program for object initialization after new
Definition: builtin_functions.cpp:507
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
goto_convertt::do_atomic_end
void do_atomic_end(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:365
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
prefix.h
goto_convert_class.h
Program Transformation.
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
format_strings.h
Format String Parser.
exprt
Base class for all expressions.
Definition: expr.h:53
unary_exprt::op1
const exprt & op1() const =delete
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
bool_typet
The Boolean type.
Definition: std_types.h:37
messaget::eom
static eomt eom
Definition: message.h:297
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
code_typet::remove_ellipsis
void remove_ellipsis()
Definition: std_types.h:842
from_rational
constant_exprt from_rational(const rationalt &a)
Definition: rational_tools.cpp:81
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1024
zero_initializer
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Definition: expr_initializer.cpp:318
goto_convertt::new_tmp_symbol
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
Definition: goto_convert.cpp:1802
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
array_typet::size
const exprt & size() const
Definition: std_types.h:973
code_outputt
A codet representing the declaration that an output of a particular description has a value which cor...
Definition: std_code.h:692
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
format_token_listt
std::list< format_tokent > format_token_listt
Definition: format_strings.h:87
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
expr_initializer.h
Expression Initialization.
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
messaget::error
mstreamt & error() const
Definition: message.h:399
empty_typet
The empty type.
Definition: std_types.h:46
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
goto_convertt::do_scanf
void do_scanf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:210
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
goto_convertt::get_string_constant
irep_idt get_string_constant(const exprt &expr)
Definition: goto_convert.cpp:1762
language_util.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:231
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
float_type
floatbv_typet float_type()
Definition: c_types.cpp:185
goto_convertt::do_function_call_symbol
virtual void do_function_call_symbol(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
add function calls to function queue for later processing
Definition: builtin_functions.cpp:615
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
goto_programt::make_atomic_begin
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:935
code_typet
Base type of functions.
Definition: std_types.h:736
OTHER
@ OTHER
Definition: goto_program.h:37
object_size
exprt object_size(const exprt &pointer)
Definition: pointer_predicates.cpp:32
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
cprover_prefix.h
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:76
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
double_type
floatbv_typet double_type()
Definition: c_types.cpp:193
side_effect_exprt::get_statement
const irep_idt & get_statement() const
Definition: std_code.h:1897
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:669
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
expr_util.h
Deprecated expression utility functions.
ASSIGN
@ ASSIGN
Definition: goto_program.h:46
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
goto_convertt::do_input
void do_input(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:312
goto_convertt::do_printf
void do_printf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:196
goto_convertt::do_atomic_begin
void do_atomic_begin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:342
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
code_inputt
A codet representing the declaration that an input of a particular description has a value which corr...
Definition: std_code.h:645
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
goto_programt::make_other
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:913
get_type
optionalt< typet > get_type(const format_tokent &token)
Definition: format_strings.cpp:229
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
code_typet::parametert
Definition: std_types.h:753
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:49
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_convertt::do_array_op
void do_array_op(const irep_idt &id, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:567
class_identifier.h
Extract class identifier.
goto_convertt::symbol_table
symbol_table_baset & symbol_table
Definition: goto_convert_class.h:49
exprt::is_one
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:182
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
codet::set_statement
void set_statement(const irep_idt &statement)
Definition: std_code.h:66
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
exprt::operands
operandst & operands()
Definition: expr.h:95
forall_expr
#define forall_expr(it, expr)
Definition: expr.h:29
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
pointer_diff_type
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:228
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
is_constant
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:30
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
make_va_list
exprt make_va_list(const exprt &expr)
Definition: builtin_functions.cpp:593
c_types.h
rationalt
Definition: rational.h:18
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:106
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
goto_convertt::do_prob_uniform
void do_prob_uniform(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:32
goto_convertt::do_prob_coin
void do_prob_coin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Definition: builtin_functions.cpp:110
goto_programt::make_atomic_end
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:946
is_lvalue
bool is_lvalue(const exprt &expr)
Returns true iff the argument is (syntactically) an lvalue.
Definition: expr_util.cpp:23
mathematical_expr.h
API to expression classes for 'mathematical' expressions.
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939