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