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 <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/cprover_prefix.h>
17 #include <util/expr_initializer.h>
18 #include <util/expr_util.h>
19 #include <util/mathematical_expr.h>
21 #include <util/pointer_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 
615  const exprt &lhs,
616  const symbol_exprt &function,
617  const exprt::operandst &arguments,
618  goto_programt &dest)
619 {
620  PRECONDITION(arguments.size() == 1);
621  const auto enum_expr = arguments.front();
622  const auto enum_type =
623  type_try_dynamic_cast<c_enum_tag_typet>(enum_expr.type());
624  PRECONDITION(enum_type);
625  const c_enum_typet &c_enum_type = ns.follow_tag(*enum_type);
626  const c_enum_typet::memberst enum_values = c_enum_type.members();
627 
628  exprt::operandst disjuncts;
629  for(const auto &enum_value : enum_values)
630  {
631  constant_exprt val{enum_value.get_value(), *enum_type};
632  disjuncts.push_back(equal_exprt(enum_expr, std::move(val)));
633  }
634 
635  code_assignt assignment(lhs, disjunction(disjuncts));
636  assignment.add_source_location() = function.source_location();
637  copy(assignment, ASSIGN, dest);
638 }
639 
642  const exprt &lhs,
643  const symbol_exprt &function,
644  const exprt::operandst &arguments,
645  goto_programt &dest)
646 {
647  if(function.get_bool(ID_C_invalid_object))
648  return; // ignore
649 
650  // lookup symbol
651  const irep_idt &identifier=function.get_identifier();
652 
653  const symbolt *symbol;
654  if(ns.lookup(identifier, symbol))
655  {
656  error().source_location=function.find_source_location();
657  error() << "error: function '" << identifier << "' not found" << eom;
658  throw 0;
659  }
660 
661  if(symbol->type.id()!=ID_code)
662  {
663  error().source_location=function.find_source_location();
664  error() << "error: function '" << identifier
665  << "' type mismatch: expected code" << eom;
666  throw 0;
667  }
668 
669  // User-provided function definitions always take precedence over built-ins.
670  // Front-ends do not (yet) consistently set ID_C_incomplete, thus also test
671  // whether the symbol actually has some non-nil value (which might be
672  // "compiled").
673  if(!symbol->type.get_bool(ID_C_incomplete) && symbol->value.is_not_nil())
674  {
675  do_function_call_symbol(*symbol);
676 
677  code_function_callt function_call(lhs, function, arguments);
678  function_call.add_source_location() = function.source_location();
679 
680  copy(function_call, FUNCTION_CALL, dest);
681 
682  return;
683  }
684 
685  if(identifier==CPROVER_PREFIX "assume" ||
686  identifier=="__VERIFIER_assume")
687  {
688  if(arguments.size()!=1)
689  {
690  error().source_location=function.find_source_location();
691  error() << "'" << identifier << "' expected to have one argument" << eom;
692  throw 0;
693  }
694 
695  // let's double-check the type of the argument
697  typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
698  function.source_location()));
699 
700  t->source_location.set("user-provided", true);
701 
702  if(lhs.is_not_nil())
703  {
704  error().source_location=function.find_source_location();
705  error() << identifier << " expected not to have LHS" << eom;
706  throw 0;
707  }
708  }
709  else if(identifier=="__VERIFIER_error")
710  {
711  if(!arguments.empty())
712  {
713  error().source_location=function.find_source_location();
714  error() << "'" << identifier << "' expected to have no arguments" << eom;
715  throw 0;
716  }
717 
718  goto_programt::targett t = dest.add(
719  goto_programt::make_assertion(false_exprt(), function.source_location()));
720 
721  t->source_location.set("user-provided", true);
722  t->source_location.set_property_class(ID_assertion);
723 
724  if(lhs.is_not_nil())
725  {
726  error().source_location=function.find_source_location();
727  error() << identifier << " expected not to have LHS" << eom;
728  throw 0;
729  }
730 
731  // __VERIFIER_error has abort() semantics, even if no assertions
732  // are being checked
734  false_exprt(), function.source_location()));
735  a->source_location.set("user-provided", true);
736  }
737  else if(
738  identifier == "assert" &&
740  {
741  if(arguments.size()!=1)
742  {
743  error().source_location=function.find_source_location();
744  error() << "'" << identifier << "' expected to have one argument" << eom;
745  throw 0;
746  }
747 
748  // let's double-check the type of the argument
750  typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
751  function.source_location()));
752  t->source_location.set("user-provided", true);
753  t->source_location.set_property_class(ID_assertion);
754  t->source_location.set_comment(
755  "assertion " + from_expr(ns, identifier, arguments.front()));
756 
757  if(lhs.is_not_nil())
758  {
759  error().source_location=function.find_source_location();
760  error() << identifier << " expected not to have LHS" << eom;
761  throw 0;
762  }
763  }
764  else if(identifier == CPROVER_PREFIX "enum_is_in_range")
765  {
766  do_enum_is_in_range(lhs, function, arguments, dest);
767  }
768  else if(
769  identifier == CPROVER_PREFIX "assert" ||
770  identifier == CPROVER_PREFIX "precondition" ||
771  identifier == CPROVER_PREFIX "postcondition")
772  {
773  if(arguments.size()!=2)
774  {
775  error().source_location=function.find_source_location();
776  error() << "'" << identifier << "' expected to have two arguments" << eom;
777  throw 0;
778  }
779 
780  bool is_precondition=
781  identifier==CPROVER_PREFIX "precondition";
782  bool is_postcondition = identifier == CPROVER_PREFIX "postcondition";
783 
784  const irep_idt description=
785  get_string_constant(arguments[1]);
786 
787  // let's double-check the type of the argument
790  function.source_location()));
791 
792  if(is_precondition)
793  {
794  t->source_location.set_property_class(ID_precondition);
795  }
796  else if(is_postcondition)
797  {
798  t->source_location.set_property_class(ID_postcondition);
799  }
800  else
801  {
802  t->source_location.set(
803  "user-provided",
804  !function.source_location().is_built_in());
805  t->source_location.set_property_class(ID_assertion);
806  }
807 
808  t->source_location.set_comment(description);
809 
810  if(lhs.is_not_nil())
811  {
812  error().source_location=function.find_source_location();
813  error() << identifier << " expected not to have LHS" << eom;
814  throw 0;
815  }
816  }
817  else if(identifier==CPROVER_PREFIX "havoc_object")
818  {
819  if(arguments.size()!=1)
820  {
821  error().source_location=function.find_source_location();
822  error() << "'" << identifier << "' expected to have one argument" << eom;
823  throw 0;
824  }
825 
826  if(lhs.is_not_nil())
827  {
828  error().source_location=function.find_source_location();
829  error() << identifier << " expected not to have LHS" << eom;
830  throw 0;
831  }
832 
833  codet havoc(ID_havoc_object);
834  havoc.add_source_location() = function.source_location();
835  havoc.copy_to_operands(arguments[0]);
836 
837  dest.add(goto_programt::make_other(havoc, function.source_location()));
838  }
839  else if(identifier==CPROVER_PREFIX "printf")
840  {
841  do_printf(lhs, function, arguments, dest);
842  }
843  else if(identifier==CPROVER_PREFIX "scanf")
844  {
845  do_scanf(lhs, function, arguments, dest);
846  }
847  else if(identifier==CPROVER_PREFIX "input" ||
848  identifier=="__CPROVER::input")
849  {
850  if(lhs.is_not_nil())
851  {
852  error().source_location=function.find_source_location();
853  error() << identifier << " expected not to have LHS" << eom;
854  throw 0;
855  }
856 
857  do_input(function, arguments, dest);
858  }
859  else if(identifier==CPROVER_PREFIX "output" ||
860  identifier=="__CPROVER::output")
861  {
862  if(lhs.is_not_nil())
863  {
864  error().source_location=function.find_source_location();
865  error() << identifier << " expected not to have LHS" << eom;
866  throw 0;
867  }
868 
869  do_output(function, arguments, dest);
870  }
871  else if(identifier==CPROVER_PREFIX "atomic_begin" ||
872  identifier=="__CPROVER::atomic_begin" ||
873  identifier=="java::org.cprover.CProver.atomicBegin:()V" ||
874  identifier=="__VERIFIER_atomic_begin")
875  {
876  do_atomic_begin(lhs, function, arguments, dest);
877  }
878  else if(identifier==CPROVER_PREFIX "atomic_end" ||
879  identifier=="__CPROVER::atomic_end" ||
880  identifier=="java::org.cprover.CProver.atomicEnd:()V" ||
881  identifier=="__VERIFIER_atomic_end")
882  {
883  do_atomic_end(lhs, function, arguments, dest);
884  }
885  else if(identifier==CPROVER_PREFIX "prob_biased_coin")
886  {
887  do_prob_coin(lhs, function, arguments, dest);
888  }
889  else if(has_prefix(id2string(identifier), CPROVER_PREFIX "prob_uniform_"))
890  {
891  do_prob_uniform(lhs, function, arguments, dest);
892  }
893  else if(has_prefix(id2string(identifier), "nondet_") ||
894  has_prefix(id2string(identifier), "__VERIFIER_nondet_"))
895  {
896  // make it a side effect if there is an LHS
897  if(lhs.is_nil())
898  return;
899 
900  exprt rhs;
901 
902  // We need to special-case for _Bool, which
903  // can only be 0 or 1.
904  if(lhs.type().id()==ID_c_bool)
905  {
906  rhs = side_effect_expr_nondett(bool_typet(), function.source_location());
907  rhs.set(ID_C_identifier, identifier);
908  rhs=typecast_exprt(rhs, lhs.type());
909  }
910  else
911  {
912  rhs = side_effect_expr_nondett(lhs.type(), function.source_location());
913  rhs.set(ID_C_identifier, identifier);
914  }
915 
916  code_assignt assignment(lhs, rhs);
917  assignment.add_source_location()=function.source_location();
918  copy(assignment, ASSIGN, dest);
919  }
920  else if(has_prefix(id2string(identifier), CPROVER_PREFIX "uninterpreted_"))
921  {
922  // make it a side effect if there is an LHS
923  if(lhs.is_nil())
924  return;
925 
926  if(function.type().get_bool(ID_C_incomplete))
927  {
928  error().source_location = function.find_source_location();
929  error() << "'" << identifier << "' is not declared, "
930  << "missing type information required to construct call to "
931  << "uninterpreted function" << eom;
932  throw 0;
933  }
934 
935  const code_typet &function_call_type = to_code_type(function.type());
937  for(const auto &parameter : function_call_type.parameters())
938  domain.push_back(parameter.type());
939  mathematical_function_typet function_type{domain,
940  function_call_type.return_type()};
941  const function_application_exprt rhs(
942  symbol_exprt{function.get_identifier(), function_type}, arguments);
943 
944  code_assignt assignment(lhs, rhs);
945  assignment.add_source_location()=function.source_location();
946  copy(assignment, ASSIGN, dest);
947  }
948  else if(identifier==CPROVER_PREFIX "array_equal")
949  {
950  do_array_op(ID_array_equal, lhs, function, arguments, dest);
951  }
952  else if(identifier==CPROVER_PREFIX "array_set")
953  {
954  do_array_op(ID_array_set, lhs, function, arguments, dest);
955  }
956  else if(identifier==CPROVER_PREFIX "array_copy")
957  {
958  do_array_op(ID_array_copy, lhs, function, arguments, dest);
959  }
960  else if(identifier==CPROVER_PREFIX "array_replace")
961  {
962  do_array_op(ID_array_replace, lhs, function, arguments, dest);
963  }
964  else if(identifier=="__assert_fail" ||
965  identifier=="_assert" ||
966  identifier=="__assert_c99" ||
967  identifier=="_wassert")
968  {
969  // __assert_fail is Linux
970  // These take four arguments:
971  // "expression", "file.c", line, __func__
972  // klibc has __assert_fail with 3 arguments
973  // "expression", "file.c", line
974 
975  // MingW has
976  // void _assert (const char*, const char*, int);
977  // with three arguments:
978  // "expression", "file.c", line
979 
980  // This has been seen in Solaris 11.
981  // Signature:
982  // void __assert_c99(
983  // const char *desc, const char *file, int line, const char *func);
984 
985  // _wassert is Windows. The arguments are
986  // L"expression", L"file.c", line
987 
988  if(arguments.size()!=4 &&
989  arguments.size()!=3)
990  {
991  error().source_location=function.find_source_location();
992  error() << "'" << identifier << "' expected to have four arguments"
993  << eom;
994  throw 0;
995  }
996 
997  const irep_idt description=
998  "assertion "+id2string(get_string_constant(arguments[0]));
999 
1000  goto_programt::targett t = dest.add(
1001  goto_programt::make_assertion(false_exprt(), function.source_location()));
1002 
1003  t->source_location.set("user-provided", true);
1004  t->source_location.set_property_class(ID_assertion);
1005  t->source_location.set_comment(description);
1006  // we ignore any LHS
1007  }
1008  else if(identifier=="__assert_rtn" ||
1009  identifier=="__assert")
1010  {
1011  // __assert_rtn has been seen on MacOS;
1012  // __assert is FreeBSD and Solaris 11.
1013  // These take four arguments:
1014  // __func__, "file.c", line, "expression"
1015  // On Solaris 11, it's three arguments:
1016  // "expression", "file", line
1017 
1018  irep_idt description;
1019 
1020  if(arguments.size()==4)
1021  {
1022  description=
1023  "assertion "+id2string(get_string_constant(arguments[3]));
1024  }
1025  else if(arguments.size()==3)
1026  {
1027  description=
1028  "assertion "+id2string(get_string_constant(arguments[1]));
1029  }
1030  else
1031  {
1032  error().source_location=function.find_source_location();
1033  error() << "'" << identifier << "' expected to have four arguments"
1034  << eom;
1035  throw 0;
1036  }
1037 
1038  goto_programt::targett t = dest.add(
1039  goto_programt::make_assertion(false_exprt(), function.source_location()));
1040 
1041  t->source_location.set("user-provided", true);
1042  t->source_location.set_property_class(ID_assertion);
1043  t->source_location.set_comment(description);
1044  // we ignore any LHS
1045  }
1046  else if(identifier=="__assert_func")
1047  {
1048  // __assert_func is newlib (used by, e.g., cygwin)
1049  // These take four arguments:
1050  // "file.c", line, __func__, "expression"
1051  if(arguments.size()!=4)
1052  {
1053  error().source_location=function.find_source_location();
1054  error() << "'" << identifier << "' expected to have four arguments"
1055  << eom;
1056  throw 0;
1057  }
1058 
1059  irep_idt description;
1060  try
1061  {
1062  description="assertion "+id2string(get_string_constant(arguments[3]));
1063  }
1064  catch(int)
1065  {
1066  // we might be building newlib, where __assert_func is passed
1067  // a pointer-typed symbol; the warning will still have been
1068  // printed
1069  description="assertion";
1070  }
1071 
1072  goto_programt::targett t = dest.add(
1073  goto_programt::make_assertion(false_exprt(), function.source_location()));
1074 
1075  t->source_location.set("user-provided", true);
1076  t->source_location.set_property_class(ID_assertion);
1077  t->source_location.set_comment(description);
1078  // we ignore any LHS
1079  }
1080  else if(identifier==CPROVER_PREFIX "fence")
1081  {
1082  if(arguments.empty())
1083  {
1084  error().source_location=function.find_source_location();
1085  error() << "'" << identifier << "' expected to have at least one argument"
1086  << eom;
1087  throw 0;
1088  }
1089 
1090  codet fence(ID_fence);
1091 
1092  for(const auto &argument : arguments)
1093  fence.set(get_string_constant(argument), true);
1094 
1095  dest.add(goto_programt::make_other(fence, function.source_location()));
1096  }
1097  else if(identifier=="__builtin_prefetch")
1098  {
1099  // does nothing
1100  }
1101  else if(identifier=="__builtin_unreachable")
1102  {
1103  // says something like UNREACHABLE;
1104  }
1105  else if(identifier==ID_gcc_builtin_va_arg)
1106  {
1107  // This does two things.
1108  // 1) Return value of argument.
1109  // This is just dereferencing.
1110  // 2) Move list pointer to next argument.
1111  // This is just an increment.
1112 
1113  if(arguments.size()!=1)
1114  {
1115  error().source_location=function.find_source_location();
1116  error() << "'" << identifier << "' expected to have one argument" << eom;
1117  throw 0;
1118  }
1119 
1120  exprt list_arg=make_va_list(arguments[0]);
1121 
1122  if(lhs.is_not_nil())
1123  {
1124  exprt list_arg_cast = list_arg;
1125  if(
1126  list_arg.type().id() == ID_pointer &&
1127  to_pointer_type(list_arg.type()).subtype().id() == ID_empty)
1128  {
1129  list_arg_cast =
1131  }
1132 
1133  typet t=pointer_type(lhs.type());
1134  dereference_exprt rhs{
1135  typecast_exprt{dereference_exprt{std::move(list_arg_cast)}, t}};
1136  rhs.add_source_location()=function.source_location();
1137  dest.add(
1138  goto_programt::make_assignment(lhs, rhs, function.source_location()));
1139  }
1140 
1141  code_assignt assign{
1142  list_arg, plus_exprt{list_arg, from_integer(1, pointer_diff_type())}};
1143  assign.rhs().set(
1144  ID_C_va_arg_type, to_code_type(function.type()).return_type());
1146  std::move(assign), function.source_location()));
1147  }
1148  else if(identifier=="__builtin_va_copy")
1149  {
1150  if(arguments.size()!=2)
1151  {
1152  error().source_location=function.find_source_location();
1153  error() << "'" << identifier << "' expected to have two arguments" << eom;
1154  throw 0;
1155  }
1156 
1157  exprt dest_expr=make_va_list(arguments[0]);
1158  const typecast_exprt src_expr(arguments[1], dest_expr.type());
1159 
1160  if(!is_lvalue(dest_expr))
1161  {
1163  error() << "va_copy argument expected to be lvalue" << eom;
1164  throw 0;
1165  }
1166 
1168  dest_expr, src_expr, function.source_location()));
1169  }
1170  else if(identifier == "__builtin_va_start" || identifier == "__va_start")
1171  {
1172  // Set the list argument to be the address of the
1173  // parameter argument.
1174  if(arguments.size()!=2)
1175  {
1176  error().source_location=function.find_source_location();
1177  error() << "'" << identifier << "' expected to have two arguments" << eom;
1178  throw 0;
1179  }
1180 
1181  exprt dest_expr=make_va_list(arguments[0]);
1182 
1183  if(!is_lvalue(dest_expr))
1184  {
1186  error() << "va_start argument expected to be lvalue" << eom;
1187  throw 0;
1188  }
1189 
1190  if(
1191  dest_expr.type().id() == ID_pointer &&
1192  to_pointer_type(dest_expr.type()).subtype().id() == ID_empty)
1193  {
1194  dest_expr =
1196  }
1197 
1198  side_effect_exprt rhs{
1199  ID_va_start, dest_expr.type(), function.source_location()};
1200  rhs.add_to_operands(
1201  typecast_exprt{address_of_exprt{arguments[1]}, dest_expr.type()});
1202 
1204  std::move(dest_expr), std::move(rhs), function.source_location()));
1205  }
1206  else if(identifier=="__builtin_va_end")
1207  {
1208  // Invalidates the argument. We do so by setting it to NULL.
1209  if(arguments.size()!=1)
1210  {
1211  error().source_location=function.find_source_location();
1212  error() << "'" << identifier << "' expected to have one argument" << eom;
1213  throw 0;
1214  }
1215 
1216  exprt dest_expr=make_va_list(arguments[0]);
1217 
1218  if(!is_lvalue(dest_expr))
1219  {
1221  error() << "va_end argument expected to be lvalue" << eom;
1222  throw 0;
1223  }
1224 
1225  // our __builtin_va_list is a pointer
1226  if(dest_expr.type().id() == ID_pointer)
1227  {
1228  const auto zero =
1229  zero_initializer(dest_expr.type(), function.source_location(), ns);
1230  CHECK_RETURN(zero.has_value());
1232  dest_expr, *zero, function.source_location()));
1233  }
1234  }
1235  else if(
1236  identifier == "__builtin_isgreater" ||
1237  identifier == "__builtin_isgreaterequal" ||
1238  identifier == "__builtin_isless" || identifier == "__builtin_islessequal" ||
1239  identifier == "__builtin_islessgreater" ||
1240  identifier == "__builtin_isunordered")
1241  {
1242  // these support two double or two float arguments; we call the
1243  // appropriate internal version
1244  if(arguments.size()!=2 ||
1245  (arguments[0].type()!=double_type() &&
1246  arguments[0].type()!=float_type()) ||
1247  (arguments[1].type()!=double_type() &&
1248  arguments[1].type()!=float_type()))
1249  {
1250  error().source_location=function.find_source_location();
1251  error() << "'" << identifier
1252  << "' expected to have two float/double arguments" << eom;
1253  throw 0;
1254  }
1255 
1256  exprt::operandst new_arguments=arguments;
1257 
1258  bool use_double=arguments[0].type()==double_type();
1259  if(arguments[0].type()!=arguments[1].type())
1260  {
1261  if(use_double)
1262  {
1263  new_arguments[1] =
1264  typecast_exprt(new_arguments[1], arguments[0].type());
1265  }
1266  else
1267  {
1268  new_arguments[0] =
1269  typecast_exprt(new_arguments[0], arguments[1].type());
1270  use_double=true;
1271  }
1272  }
1273 
1274  code_typet f_type=to_code_type(function.type());
1275  f_type.remove_ellipsis();
1276  const typet &a_t=new_arguments[0].type();
1277  f_type.parameters()=
1279 
1280  // replace __builtin_ by CPROVER_PREFIX
1281  std::string name=CPROVER_PREFIX+id2string(identifier).substr(10);
1282  // append d or f for double/float
1283  name+=use_double?'d':'f';
1284 
1285  symbol_exprt new_function=function;
1286  new_function.set_identifier(name);
1287  new_function.type()=f_type;
1288 
1289  code_function_callt function_call(lhs, new_function, new_arguments);
1290  function_call.add_source_location()=function.source_location();
1291 
1292  if(!symbol_table.has_symbol(name))
1293  {
1294  symbolt new_symbol;
1295  new_symbol.base_name=name;
1296  new_symbol.name=name;
1297  new_symbol.type=f_type;
1298  new_symbol.location=function.source_location();
1299  symbol_table.add(new_symbol);
1300  }
1301 
1302  copy(function_call, FUNCTION_CALL, dest);
1303  }
1304  else
1305  {
1306  do_function_call_symbol(*symbol);
1307 
1308  // insert function call
1309  code_function_callt function_call(lhs, function, arguments);
1310  function_call.add_source_location()=function.source_location();
1311 
1312  copy(function_call, FUNCTION_CALL, dest);
1313  }
1314 }
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:137
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:1788
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
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
c_enum_typet
The type of C enums.
Definition: c_types.h:204
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:219
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:52
arith_tools.h
codet::op0
exprt & op0()
Definition: expr.h:103
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:401
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:429
goto_convertt::copy
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
Definition: goto_convert.cpp:299
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:535
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:162
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1296
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: pointer_expr.h:386
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
c_enum_typet::memberst
std::vector< c_enum_membert > memberst
Definition: c_types.h:240
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:112
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:670
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
format_strings.h
Format String Parser.
exprt
Base class for all expressions.
Definition: expr.h:54
unary_exprt::op1
const exprt & op1() const =delete
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:66
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:20
bool_typet
The Boolean type.
Definition: std_types.h:36
messaget::eom
static eomt eom
Definition: message.h:297
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1139
code_typet::remove_ellipsis
void remove_ellipsis()
Definition: std_types.h:634
from_rational
constant_exprt from_rational(const rationalt &a)
Definition: rational_tools.cpp:81
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1240
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:1008
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:1819
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
mathematical_types.h
Mathematical types.
array_typet::size
const exprt & size() const
Definition: std_types.h:765
code_outputt
A codet representing the declaration that an output of a particular description has a value which cor...
Definition: std_code.h:724
goto_convertt::do_enum_is_in_range
void do_enum_is_in_range(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Converts calls to the built in enum_is_in_range function to a test that the given enum value is in th...
Definition: builtin_functions.cpp:614
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:141
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
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:391
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:738
disjunction
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:29
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:877
messaget::error
mstreamt & error() const
Definition: message.h:399
empty_typet
The empty type.
Definition: std_types.h:45
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
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
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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:1779
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:192
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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
pointer_expr.h
API to expression classes for Pointers.
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:641
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:194
mathematical_function_typet::domaint
std::vector< typet > domaint
Definition: mathematical_types.h:63
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
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:919
code_typet
Base type of functions.
Definition: std_types.h:533
OTHER
@ OTHER
Definition: goto_program.h:38
object_size
exprt object_size(const exprt &pointer)
Definition: pointer_predicates.cpp:33
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:649
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:1260
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:1920
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:653
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
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:47
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:677
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1814
goto_programt::make_other
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:897
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:807
code_typet::parametert
Definition: std_types.h:550
FUNCTION_CALL
@ FUNCTION_CALL
Definition: goto_program.h:50
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
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:51
exprt::is_one
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:141
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:639
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:889
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:367
exprt::operands
operandst & operands()
Definition: expr.h:96
index_exprt
Array index operator.
Definition: std_expr.h:1242
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:243
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
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
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
is_constant
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2675
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
make_va_list
exprt make_va_list(const exprt &expr)
Definition: builtin_functions.cpp:593
mathematical_function_typet
A type for mathematical functions (do not confuse with functions/methods in code)
Definition: mathematical_types.h:59
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:104
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:563
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1898
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
c_enum_typet::members
const memberst & members() const
Definition: c_types.h:242
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:930
is_lvalue
bool is_lvalue(const exprt &expr)
Returns true iff the argument is (syntactically) an lvalue.
Definition: expr_util.cpp:25
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:2700