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/simplify_expr.h>
26 #include <util/symbol_table.h>
27 
28 #include <langapi/language_util.h>
29 
30 #include "format_strings.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, c_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  to_array_type(*type).element_type(),
280  function.source_location());
281  code_assignt assign(new_lhs, rhs);
282  assign.add_source_location()=function.source_location();
283  copy(assign, ASSIGN, dest);
284  #endif
285  }
286  else
287  {
288  // make it nondet for now
289  const dereference_exprt new_lhs{ptr};
290  const side_effect_expr_nondett rhs(
291  *type, function.source_location());
292  code_assignt assign(new_lhs, rhs);
293  assign.add_source_location()=function.source_location();
294  copy(assign, ASSIGN, dest);
295  }
296  }
297  }
298  }
299  }
300  else
301  {
302  // we'll just do nothing
303  code_function_callt function_call(lhs, function, arguments);
304  function_call.add_source_location()=function.source_location();
305 
306  copy(function_call, FUNCTION_CALL, dest);
307  }
308  }
309  else
310  UNREACHABLE;
311 }
312 
314  const exprt &function,
315  const exprt::operandst &arguments,
316  goto_programt &dest)
317 {
318  if(arguments.size()<2)
319  {
320  error().source_location=function.find_source_location();
321  error() << "input takes at least two arguments" << eom;
322  throw 0;
323  }
324 
325  copy(code_inputt{arguments, function.source_location()}, OTHER, dest);
326 }
327 
329  const exprt &function,
330  const exprt::operandst &arguments,
331  goto_programt &dest)
332 {
333  if(arguments.size()<2)
334  {
335  error().source_location=function.find_source_location();
336  error() << "output takes at least two arguments" << eom;
337  throw 0;
338  }
339 
340  copy(code_outputt{arguments, function.source_location()}, OTHER, dest);
341 }
342 
344  const exprt &lhs,
345  const symbol_exprt &function,
346  const exprt::operandst &arguments,
347  goto_programt &dest)
348 {
349  if(lhs.is_not_nil())
350  {
352  error() << "atomic_begin does not expect an LHS" << eom;
353  throw 0;
354  }
355 
356  if(!arguments.empty())
357  {
358  error().source_location=function.find_source_location();
359  error() << "atomic_begin takes no arguments" << eom;
360  throw 0;
361  }
362 
363  dest.add(goto_programt::make_atomic_begin(function.source_location()));
364 }
365 
367  const exprt &lhs,
368  const symbol_exprt &function,
369  const exprt::operandst &arguments,
370  goto_programt &dest)
371 {
372  if(lhs.is_not_nil())
373  {
375  error() << "atomic_end does not expect an LHS" << eom;
376  throw 0;
377  }
378 
379  if(!arguments.empty())
380  {
381  error().source_location=function.find_source_location();
382  error() << "atomic_end takes no arguments" << eom;
383  throw 0;
384  }
385 
386  dest.add(goto_programt::make_atomic_end(function.source_location()));
387 }
388 
390  const exprt &lhs,
391  const side_effect_exprt &rhs,
392  goto_programt &dest)
393 {
394  if(lhs.is_nil())
395  {
397  error() << "do_cpp_new without lhs is yet to be implemented" << eom;
398  throw 0;
399  }
400 
401  // build size expression
403  static_cast<const exprt &>(rhs.find(ID_sizeof));
404 
405  bool new_array=rhs.get(ID_statement)==ID_cpp_new_array;
406 
407  exprt count;
408 
409  if(new_array)
410  {
412  static_cast<const exprt &>(rhs.find(ID_size)), object_size.type());
413 
414  // might have side-effect
415  clean_expr(count, dest, ID_cpp);
416  }
417 
418  exprt tmp_symbol_expr;
419 
420  // is this a placement new?
421  if(rhs.operands().empty()) // no, "regular" one
422  {
423  // call __new or __new_array
424  exprt new_symbol=
425  ns.lookup(new_array?"__new_array":"__new").symbol_expr();
426 
427  const code_typet &code_type=
428  to_code_type(new_symbol.type());
429 
430  const typet &return_type=
431  code_type.return_type();
432 
433  assert(code_type.parameters().size()==1 ||
434  code_type.parameters().size()==2);
435 
436  const symbolt &tmp_symbol =
437  new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
438 
439  tmp_symbol_expr=tmp_symbol.symbol_expr();
440 
441  code_function_callt new_call(new_symbol);
442  if(new_array)
443  new_call.arguments().push_back(count);
444  new_call.arguments().push_back(object_size);
445  new_call.set(
446  ID_C_cxx_alloc_type, to_type_with_subtype(lhs.type()).subtype());
447  new_call.lhs()=tmp_symbol_expr;
448  new_call.add_source_location()=rhs.source_location();
449 
450  convert(new_call, dest, ID_cpp);
451  }
452  else if(rhs.operands().size()==1)
453  {
454  // call __placement_new
455  exprt new_symbol=
456  ns.lookup(
457  new_array?"__placement_new_array":"__placement_new").symbol_expr();
458 
459  const code_typet &code_type=
460  to_code_type(new_symbol.type());
461 
462  const typet &return_type=code_type.return_type();
463 
464  assert(code_type.parameters().size()==2 ||
465  code_type.parameters().size()==3);
466 
467  const symbolt &tmp_symbol =
468  new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
469 
470  tmp_symbol_expr=tmp_symbol.symbol_expr();
471 
472  code_function_callt new_call(new_symbol);
473  if(new_array)
474  new_call.arguments().push_back(count);
475  new_call.arguments().push_back(object_size);
476  new_call.arguments().push_back(to_unary_expr(rhs).op()); // memory location
477  new_call.set(
478  ID_C_cxx_alloc_type, to_type_with_subtype(lhs.type()).subtype());
479  new_call.lhs()=tmp_symbol_expr;
480  new_call.add_source_location()=rhs.source_location();
481 
482  for(std::size_t i=0; i<code_type.parameters().size(); i++)
483  {
485  new_call.arguments()[i], code_type.parameters()[i].type());
486  }
487 
488  convert(new_call, dest, ID_cpp);
489  }
490  else
491  {
493  error() << "cpp_new expected to have 0 or 1 operands" << eom;
494  throw 0;
495  }
496 
498  lhs,
499  typecast_exprt(tmp_symbol_expr, lhs.type()),
500  rhs.find_source_location()));
501 
502  // grab initializer
503  goto_programt tmp_initializer;
504  cpp_new_initializer(lhs, rhs, tmp_initializer);
505 
506  dest.destructive_append(tmp_initializer);
507 }
508 
511  const exprt &lhs,
512  const side_effect_exprt &rhs,
513  goto_programt &dest)
514 {
515  exprt initializer=
516  static_cast<const exprt &>(rhs.find(ID_initializer));
517 
518  if(initializer.is_not_nil())
519  {
520  if(rhs.get_statement()=="cpp_new[]")
521  {
522  // build loop
523  }
524  else if(rhs.get_statement()==ID_cpp_new)
525  {
526  // just one object
527  const dereference_exprt deref_lhs(
528  lhs, to_pointer_type(rhs.type()).base_type());
529 
530  replace_new_object(deref_lhs, initializer);
531  convert(to_code(initializer), dest, ID_cpp);
532  }
533  else
534  UNREACHABLE;
535  }
536 }
537 
539 {
540  if(src.id()==ID_typecast)
541  return get_array_argument(to_typecast_expr(src).op());
542 
543  if(src.id()!=ID_address_of)
544  {
546  error() << "expected array-pointer as argument" << eom;
547  throw 0;
548  }
549 
550  const auto &address_of_expr = to_address_of_expr(src);
551 
552  if(address_of_expr.object().id() != ID_index)
553  {
555  error() << "expected array-element as argument" << eom;
556  throw 0;
557  }
558 
559  const auto &index_expr = to_index_expr(address_of_expr.object());
560 
561  if(index_expr.array().type().id() != ID_array)
562  {
564  error() << "expected array as argument" << eom;
565  throw 0;
566  }
567 
568  return index_expr.array();
569 }
570 
572  const irep_idt &id,
573  const exprt &lhs,
574  const symbol_exprt &function,
575  const exprt::operandst &arguments,
576  goto_programt &dest)
577 {
578  if(arguments.size()!=2)
579  {
580  error().source_location=function.find_source_location();
581  error() << id << " expects two arguments" << eom;
582  throw 0;
583  }
584 
585  codet array_op_statement(id);
586  array_op_statement.operands()=arguments;
587  array_op_statement.add_source_location()=function.source_location();
588 
589  // lhs is only used with array_equal, in all other cases it should be nil (as
590  // they are of type void)
591  if(id == ID_array_equal)
592  array_op_statement.copy_to_operands(lhs);
593 
594  copy(array_op_statement, OTHER, dest);
595 }
596 
598 {
599  exprt result = skip_typecast(expr);
600 
601  // if it's an address of an lvalue, we take that
602  if(result.id() == ID_address_of)
603  {
604  const auto &address_of_expr = to_address_of_expr(result);
605  if(is_assignable(address_of_expr.object()))
606  result = address_of_expr.object();
607  }
608 
609  while(result.type().id() == ID_array &&
610  to_array_type(result.type()).size().is_one())
611  {
612  result = index_exprt{result, from_integer(0, c_index_type())};
613  }
614 
615  return result;
616 }
617 
619  const exprt &lhs,
620  const symbol_exprt &function,
621  const exprt::operandst &arguments,
622  goto_programt &dest)
623 {
624  PRECONDITION(arguments.size() == 1);
625  const auto enum_expr = arguments.front();
626  const auto enum_type =
627  type_try_dynamic_cast<c_enum_tag_typet>(enum_expr.type());
628  PRECONDITION(enum_type);
629  const c_enum_typet &c_enum_type = ns.follow_tag(*enum_type);
630  const c_enum_typet::memberst enum_values = c_enum_type.members();
631 
632  exprt::operandst disjuncts;
633  for(const auto &enum_value : enum_values)
634  {
635  constant_exprt val{enum_value.get_value(), *enum_type};
636  disjuncts.push_back(equal_exprt(enum_expr, std::move(val)));
637  }
638 
639  code_assignt assignment(lhs, disjunction(disjuncts));
640  assignment.add_source_location() = function.source_location();
641  copy(assignment, ASSIGN, dest);
642 }
643 
645  const exprt &lhs,
646  const symbol_exprt &function,
647  const exprt::operandst &arguments,
648  goto_programt &dest,
649  const irep_idt &mode)
650 {
651  irep_idt identifier = CPROVER_PREFIX "havoc_slice";
652 
653  // We disable checks on the generated instructions
654  // because we add our own rw_ok assertion that takes size into account
655  auto source_location = function.find_source_location();
656  source_location.add_pragma("disable:pointer-check");
657  source_location.add_pragma("disable:pointer-overflow-check");
658  source_location.add_pragma("disable:pointer-primitive-check");
659 
660  // check # arguments
661  if(arguments.size() != 2)
662  {
663  error().source_location = source_location;
664  error() << "'" << identifier << "' expected to have two arguments" << eom;
665  throw 0;
666  }
667 
668  // check argument types
669  if(arguments[0].type().id() != ID_pointer)
670  {
671  error().source_location = source_location;
672  error() << "'" << identifier
673  << "' first argument expected to have `void *` type" << eom;
674  throw 0;
675  }
676 
677  if(arguments[1].type().id() != ID_unsignedbv)
678  {
679  error().source_location = source_location;
680  error() << "'" << identifier
681  << "' second argument expected to have `size_t` type" << eom;
682  throw 0;
683  }
684 
685  // check nil lhs
686  if(lhs.is_not_nil())
687  {
688  error().source_location = source_location;
689  error() << "'" << identifier << "' not expected to have a LHS" << eom;
690  throw 0;
691  }
692 
693  // insert instructions
694  // assert(rw_ok(argument[0], argument[1]));
695  // char nondet_contents[argument[1]];
696  // __CPROVER_array_replace(p, nondet_contents);
697 
698  r_or_w_ok_exprt ok_expr(ID_w_ok, arguments[0], arguments[1]);
699  ok_expr.add_source_location() = source_location;
701  dest.add(goto_programt::make_assertion(ok_expr, source_location));
702  t->source_location_nonconst().set("user-provided", false);
703  t->source_location_nonconst().set_property_class(ID_assertion);
704  t->source_location_nonconst().set_comment(
705  "assertion havoc_slice " + from_expr(ns, identifier, ok_expr));
706 
707  const array_typet array_type(char_type(), simplify_expr(arguments[1], ns));
708 
709  const symbolt &nondet_contents =
710  new_tmp_symbol(array_type, "nondet_contents", dest, source_location, mode);
711  const exprt &nondet_contents_expr = address_of_exprt{index_exprt{
712  nondet_contents.symbol_expr(), from_integer(0, c_index_type())}};
713 
714  const exprt &arg0 =
717  nondet_contents_expr, pointer_type(empty_typet{}));
718 
719  codet array_replace(ID_array_replace, {arg0, arg1}, source_location);
720  dest.add(goto_programt::make_other(array_replace, source_location));
721 }
722 
725  const exprt &lhs,
726  const symbol_exprt &function,
727  const exprt::operandst &arguments,
728  goto_programt &dest,
729  const irep_idt &mode)
730 {
731  if(function.get_bool(ID_C_invalid_object))
732  return; // ignore
733 
734  // lookup symbol
735  const irep_idt &identifier=function.get_identifier();
736 
737  const symbolt *symbol;
738  if(ns.lookup(identifier, symbol))
739  {
740  error().source_location=function.find_source_location();
741  error() << "error: function '" << identifier << "' not found" << eom;
742  throw 0;
743  }
744 
745  if(symbol->type.id()!=ID_code)
746  {
747  error().source_location=function.find_source_location();
748  error() << "error: function '" << identifier
749  << "' type mismatch: expected code" << eom;
750  throw 0;
751  }
752 
753  // User-provided function definitions always take precedence over built-ins.
754  // Front-ends do not (yet) consistently set ID_C_incomplete, thus also test
755  // whether the symbol actually has some non-nil value (which might be
756  // "compiled").
757  if(!symbol->type.get_bool(ID_C_incomplete) && symbol->value.is_not_nil())
758  {
759  do_function_call_symbol(*symbol);
760 
761  code_function_callt function_call(lhs, function, arguments);
762  function_call.add_source_location() = function.source_location();
763 
764  copy(function_call, FUNCTION_CALL, dest);
765 
766  return;
767  }
768 
769  if(identifier == CPROVER_PREFIX "havoc_slice")
770  {
771  do_havoc_slice(lhs, function, arguments, dest, mode);
772  }
773  else if(
774  identifier == CPROVER_PREFIX "assume" || identifier == "__VERIFIER_assume")
775  {
776  if(arguments.size()!=1)
777  {
778  error().source_location=function.find_source_location();
779  error() << "'" << identifier << "' expected to have one argument" << eom;
780  throw 0;
781  }
782 
783  // let's double-check the type of the argument
785  typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
786  function.source_location()));
787 
788  t->source_location_nonconst().set("user-provided", true);
789 
790  if(lhs.is_not_nil())
791  {
792  error().source_location=function.find_source_location();
793  error() << identifier << " expected not to have LHS" << eom;
794  throw 0;
795  }
796  }
797  else if(identifier=="__VERIFIER_error")
798  {
799  if(!arguments.empty())
800  {
801  error().source_location=function.find_source_location();
802  error() << "'" << identifier << "' expected to have no arguments" << eom;
803  throw 0;
804  }
805 
806  goto_programt::targett t = dest.add(
807  goto_programt::make_assertion(false_exprt(), function.source_location()));
808 
809  t->source_location_nonconst().set("user-provided", true);
810  t->source_location_nonconst().set_property_class(ID_assertion);
811 
812  if(lhs.is_not_nil())
813  {
814  error().source_location=function.find_source_location();
815  error() << identifier << " expected not to have LHS" << eom;
816  throw 0;
817  }
818 
819  // __VERIFIER_error has abort() semantics, even if no assertions
820  // are being checked
822  false_exprt(), function.source_location()));
823  a->source_location_nonconst().set("user-provided", true);
824  }
825  else if(
826  identifier == "assert" &&
828  {
829  if(arguments.size()!=1)
830  {
831  error().source_location=function.find_source_location();
832  error() << "'" << identifier << "' expected to have one argument" << eom;
833  throw 0;
834  }
835 
836  // let's double-check the type of the argument
838  typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
839  function.source_location()));
840  t->source_location_nonconst().set("user-provided", true);
841  t->source_location_nonconst().set_property_class(ID_assertion);
842  t->source_location_nonconst().set_comment(
843  "assertion " + from_expr(ns, identifier, arguments.front()));
844 
845  if(lhs.is_not_nil())
846  {
847  error().source_location=function.find_source_location();
848  error() << identifier << " expected not to have LHS" << eom;
849  throw 0;
850  }
851  }
852  else if(identifier == CPROVER_PREFIX "enum_is_in_range")
853  {
854  do_enum_is_in_range(lhs, function, arguments, dest);
855  }
856  else if(
857  identifier == CPROVER_PREFIX "assert" ||
858  identifier == CPROVER_PREFIX "precondition" ||
859  identifier == CPROVER_PREFIX "postcondition")
860  {
861  if(arguments.size()!=2)
862  {
863  error().source_location=function.find_source_location();
864  error() << "'" << identifier << "' expected to have two arguments" << eom;
865  throw 0;
866  }
867 
868  bool is_precondition=
869  identifier==CPROVER_PREFIX "precondition";
870  bool is_postcondition = identifier == CPROVER_PREFIX "postcondition";
871 
872  const irep_idt description=
873  get_string_constant(arguments[1]);
874 
875  // let's double-check the type of the argument
878  function.source_location()));
879 
880  if(is_precondition)
881  {
882  t->source_location_nonconst().set_property_class(ID_precondition);
883  }
884  else if(is_postcondition)
885  {
886  t->source_location_nonconst().set_property_class(ID_postcondition);
887  }
888  else
889  {
890  t->source_location_nonconst().set(
891  "user-provided", !function.source_location().is_built_in());
892  t->source_location_nonconst().set_property_class(ID_assertion);
893  }
894 
895  t->source_location_nonconst().set_comment(description);
896 
897  if(lhs.is_not_nil())
898  {
899  error().source_location=function.find_source_location();
900  error() << identifier << " expected not to have LHS" << eom;
901  throw 0;
902  }
903  }
904  else if(identifier==CPROVER_PREFIX "havoc_object")
905  {
906  if(arguments.size()!=1)
907  {
908  error().source_location=function.find_source_location();
909  error() << "'" << identifier << "' expected to have one argument" << eom;
910  throw 0;
911  }
912 
913  if(lhs.is_not_nil())
914  {
915  error().source_location=function.find_source_location();
916  error() << identifier << " expected not to have LHS" << eom;
917  throw 0;
918  }
919 
920  codet havoc(ID_havoc_object);
921  havoc.add_source_location() = function.source_location();
922  havoc.copy_to_operands(arguments[0]);
923 
924  dest.add(goto_programt::make_other(havoc, function.source_location()));
925  }
926  else if(identifier==CPROVER_PREFIX "printf")
927  {
928  do_printf(lhs, function, arguments, dest);
929  }
930  else if(identifier==CPROVER_PREFIX "scanf")
931  {
932  do_scanf(lhs, function, arguments, dest);
933  }
934  else if(identifier==CPROVER_PREFIX "input" ||
935  identifier=="__CPROVER::input")
936  {
937  if(lhs.is_not_nil())
938  {
939  error().source_location=function.find_source_location();
940  error() << identifier << " expected not to have LHS" << eom;
941  throw 0;
942  }
943 
944  do_input(function, arguments, dest);
945  }
946  else if(identifier==CPROVER_PREFIX "output" ||
947  identifier=="__CPROVER::output")
948  {
949  if(lhs.is_not_nil())
950  {
951  error().source_location=function.find_source_location();
952  error() << identifier << " expected not to have LHS" << eom;
953  throw 0;
954  }
955 
956  do_output(function, arguments, dest);
957  }
958  else if(identifier==CPROVER_PREFIX "atomic_begin" ||
959  identifier=="__CPROVER::atomic_begin" ||
960  identifier=="java::org.cprover.CProver.atomicBegin:()V" ||
961  identifier=="__VERIFIER_atomic_begin")
962  {
963  do_atomic_begin(lhs, function, arguments, dest);
964  }
965  else if(identifier==CPROVER_PREFIX "atomic_end" ||
966  identifier=="__CPROVER::atomic_end" ||
967  identifier=="java::org.cprover.CProver.atomicEnd:()V" ||
968  identifier=="__VERIFIER_atomic_end")
969  {
970  do_atomic_end(lhs, function, arguments, dest);
971  }
972  else if(identifier==CPROVER_PREFIX "prob_biased_coin")
973  {
974  do_prob_coin(lhs, function, arguments, dest);
975  }
976  else if(has_prefix(id2string(identifier), CPROVER_PREFIX "prob_uniform_"))
977  {
978  do_prob_uniform(lhs, function, arguments, dest);
979  }
980  else if(has_prefix(id2string(identifier), "nondet_") ||
981  has_prefix(id2string(identifier), "__VERIFIER_nondet_"))
982  {
983  // make it a side effect if there is an LHS
984  if(lhs.is_nil())
985  return;
986 
987  exprt rhs;
988 
989  // We need to special-case for _Bool, which
990  // can only be 0 or 1.
991  if(lhs.type().id()==ID_c_bool)
992  {
993  rhs = side_effect_expr_nondett(bool_typet(), function.source_location());
994  rhs.set(ID_C_identifier, identifier);
995  rhs=typecast_exprt(rhs, lhs.type());
996  }
997  else
998  {
999  rhs = side_effect_expr_nondett(lhs.type(), function.source_location());
1000  rhs.set(ID_C_identifier, identifier);
1001  }
1002 
1003  code_assignt assignment(lhs, rhs);
1004  assignment.add_source_location()=function.source_location();
1005  copy(assignment, ASSIGN, dest);
1006  }
1007  else if(has_prefix(id2string(identifier), CPROVER_PREFIX "uninterpreted_"))
1008  {
1009  // make it a side effect if there is an LHS
1010  if(lhs.is_nil())
1011  return;
1012 
1013  if(function.type().get_bool(ID_C_incomplete))
1014  {
1015  error().source_location = function.find_source_location();
1016  error() << "'" << identifier << "' is not declared, "
1017  << "missing type information required to construct call to "
1018  << "uninterpreted function" << eom;
1019  throw 0;
1020  }
1021 
1022  const code_typet &function_call_type = to_code_type(function.type());
1024  for(const auto &parameter : function_call_type.parameters())
1025  domain.push_back(parameter.type());
1026  mathematical_function_typet function_type{domain,
1027  function_call_type.return_type()};
1028  const function_application_exprt rhs(
1029  symbol_exprt{function.get_identifier(), function_type}, arguments);
1030 
1031  code_assignt assignment(lhs, rhs);
1032  assignment.add_source_location()=function.source_location();
1033  copy(assignment, ASSIGN, dest);
1034  }
1035  else if(identifier==CPROVER_PREFIX "array_equal")
1036  {
1037  do_array_op(ID_array_equal, lhs, function, arguments, dest);
1038  }
1039  else if(identifier==CPROVER_PREFIX "array_set")
1040  {
1041  do_array_op(ID_array_set, lhs, function, arguments, dest);
1042  }
1043  else if(identifier==CPROVER_PREFIX "array_copy")
1044  {
1045  do_array_op(ID_array_copy, lhs, function, arguments, dest);
1046  }
1047  else if(identifier==CPROVER_PREFIX "array_replace")
1048  {
1049  do_array_op(ID_array_replace, lhs, function, arguments, dest);
1050  }
1051  else if(identifier=="__assert_fail" ||
1052  identifier=="_assert" ||
1053  identifier=="__assert_c99" ||
1054  identifier=="_wassert")
1055  {
1056  // __assert_fail is Linux
1057  // These take four arguments:
1058  // "expression", "file.c", line, __func__
1059  // klibc has __assert_fail with 3 arguments
1060  // "expression", "file.c", line
1061 
1062  // MingW has
1063  // void _assert (const char*, const char*, int);
1064  // with three arguments:
1065  // "expression", "file.c", line
1066 
1067  // This has been seen in Solaris 11.
1068  // Signature:
1069  // void __assert_c99(
1070  // const char *desc, const char *file, int line, const char *func);
1071 
1072  // _wassert is Windows. The arguments are
1073  // L"expression", L"file.c", line
1074 
1075  if(arguments.size()!=4 &&
1076  arguments.size()!=3)
1077  {
1078  error().source_location=function.find_source_location();
1079  error() << "'" << identifier << "' expected to have four arguments"
1080  << eom;
1081  throw 0;
1082  }
1083 
1084  const irep_idt description=
1085  "assertion "+id2string(get_string_constant(arguments[0]));
1086 
1087  goto_programt::targett t = dest.add(
1088  goto_programt::make_assertion(false_exprt(), function.source_location()));
1089 
1090  t->source_location_nonconst().set("user-provided", true);
1091  t->source_location_nonconst().set_property_class(ID_assertion);
1092  t->source_location_nonconst().set_comment(description);
1093  // we ignore any LHS
1094  }
1095  else if(identifier=="__assert_rtn" ||
1096  identifier=="__assert")
1097  {
1098  // __assert_rtn has been seen on MacOS;
1099  // __assert is FreeBSD and Solaris 11.
1100  // These take four arguments:
1101  // __func__, "file.c", line, "expression"
1102  // On Solaris 11, it's three arguments:
1103  // "expression", "file", line
1104 
1105  irep_idt description;
1106 
1107  if(arguments.size()==4)
1108  {
1109  description=
1110  "assertion "+id2string(get_string_constant(arguments[3]));
1111  }
1112  else if(arguments.size()==3)
1113  {
1114  description=
1115  "assertion "+id2string(get_string_constant(arguments[1]));
1116  }
1117  else
1118  {
1119  error().source_location=function.find_source_location();
1120  error() << "'" << identifier << "' expected to have four arguments"
1121  << eom;
1122  throw 0;
1123  }
1124 
1125  goto_programt::targett t = dest.add(
1126  goto_programt::make_assertion(false_exprt(), function.source_location()));
1127 
1128  t->source_location_nonconst().set("user-provided", true);
1129  t->source_location_nonconst().set_property_class(ID_assertion);
1130  t->source_location_nonconst().set_comment(description);
1131  // we ignore any LHS
1132  }
1133  else if(identifier=="__assert_func")
1134  {
1135  // __assert_func is newlib (used by, e.g., cygwin)
1136  // These take four arguments:
1137  // "file.c", line, __func__, "expression"
1138  if(arguments.size()!=4)
1139  {
1140  error().source_location=function.find_source_location();
1141  error() << "'" << identifier << "' expected to have four arguments"
1142  << eom;
1143  throw 0;
1144  }
1145 
1146  irep_idt description;
1147  try
1148  {
1149  description="assertion "+id2string(get_string_constant(arguments[3]));
1150  }
1151  catch(int)
1152  {
1153  // we might be building newlib, where __assert_func is passed
1154  // a pointer-typed symbol; the warning will still have been
1155  // printed
1156  description="assertion";
1157  }
1158 
1159  goto_programt::targett t = dest.add(
1160  goto_programt::make_assertion(false_exprt(), function.source_location()));
1161 
1162  t->source_location_nonconst().set("user-provided", true);
1163  t->source_location_nonconst().set_property_class(ID_assertion);
1164  t->source_location_nonconst().set_comment(description);
1165  // we ignore any LHS
1166  }
1167  else if(identifier==CPROVER_PREFIX "fence")
1168  {
1169  if(arguments.empty())
1170  {
1171  error().source_location=function.find_source_location();
1172  error() << "'" << identifier << "' expected to have at least one argument"
1173  << eom;
1174  throw 0;
1175  }
1176 
1177  codet fence(ID_fence);
1178 
1179  for(const auto &argument : arguments)
1180  fence.set(get_string_constant(argument), true);
1181 
1182  dest.add(goto_programt::make_other(fence, function.source_location()));
1183  }
1184  else if(identifier=="__builtin_prefetch")
1185  {
1186  // does nothing
1187  }
1188  else if(identifier=="__builtin_unreachable")
1189  {
1190  // says something like UNREACHABLE;
1191  }
1192  else if(identifier==ID_gcc_builtin_va_arg)
1193  {
1194  // This does two things.
1195  // 1) Return value of argument.
1196  // This is just dereferencing.
1197  // 2) Move list pointer to next argument.
1198  // This is just an increment.
1199 
1200  if(arguments.size()!=1)
1201  {
1202  error().source_location=function.find_source_location();
1203  error() << "'" << identifier << "' expected to have one argument" << eom;
1204  throw 0;
1205  }
1206 
1207  exprt list_arg=make_va_list(arguments[0]);
1208 
1209  if(lhs.is_not_nil())
1210  {
1211  exprt list_arg_cast = list_arg;
1212  if(
1213  list_arg.type().id() == ID_pointer &&
1214  to_pointer_type(list_arg.type()).base_type().id() == ID_empty)
1215  {
1216  list_arg_cast =
1218  }
1219 
1220  typet t=pointer_type(lhs.type());
1221  dereference_exprt rhs{
1222  typecast_exprt{dereference_exprt{std::move(list_arg_cast)}, t}};
1223  rhs.add_source_location()=function.source_location();
1224  dest.add(
1225  goto_programt::make_assignment(lhs, rhs, function.source_location()));
1226  }
1227 
1228  code_assignt assign{
1229  list_arg, plus_exprt{list_arg, from_integer(1, pointer_diff_type())}};
1230  assign.rhs().set(
1231  ID_C_va_arg_type, to_code_type(function.type()).return_type());
1233  std::move(assign), function.source_location()));
1234  }
1235  else if(identifier=="__builtin_va_copy")
1236  {
1237  if(arguments.size()!=2)
1238  {
1239  error().source_location=function.find_source_location();
1240  error() << "'" << identifier << "' expected to have two arguments" << eom;
1241  throw 0;
1242  }
1243 
1244  exprt dest_expr=make_va_list(arguments[0]);
1245  const typecast_exprt src_expr(arguments[1], dest_expr.type());
1246 
1247  if(!is_assignable(dest_expr))
1248  {
1250  error() << "va_copy argument expected to be lvalue" << eom;
1251  throw 0;
1252  }
1253 
1255  dest_expr, src_expr, function.source_location()));
1256  }
1257  else if(identifier == "__builtin_va_start" || identifier == "__va_start")
1258  {
1259  // Set the list argument to be the address of the
1260  // parameter argument.
1261  if(arguments.size()!=2)
1262  {
1263  error().source_location=function.find_source_location();
1264  error() << "'" << identifier << "' expected to have two arguments" << eom;
1265  throw 0;
1266  }
1267 
1268  exprt dest_expr=make_va_list(arguments[0]);
1269 
1270  if(!is_assignable(dest_expr))
1271  {
1273  error() << "va_start argument expected to be lvalue" << eom;
1274  throw 0;
1275  }
1276 
1277  if(
1278  dest_expr.type().id() == ID_pointer &&
1279  to_pointer_type(dest_expr.type()).base_type().id() == ID_empty)
1280  {
1281  dest_expr =
1283  }
1284 
1285  side_effect_exprt rhs{
1286  ID_va_start, dest_expr.type(), function.source_location()};
1287  rhs.add_to_operands(
1288  typecast_exprt{address_of_exprt{arguments[1]}, dest_expr.type()});
1289 
1291  std::move(dest_expr), std::move(rhs), function.source_location()));
1292  }
1293  else if(identifier=="__builtin_va_end")
1294  {
1295  // Invalidates the argument. We do so by setting it to NULL.
1296  if(arguments.size()!=1)
1297  {
1298  error().source_location=function.find_source_location();
1299  error() << "'" << identifier << "' expected to have one argument" << eom;
1300  throw 0;
1301  }
1302 
1303  exprt dest_expr=make_va_list(arguments[0]);
1304 
1305  if(!is_assignable(dest_expr))
1306  {
1308  error() << "va_end argument expected to be lvalue" << eom;
1309  throw 0;
1310  }
1311 
1312  // our __builtin_va_list is a pointer
1313  if(dest_expr.type().id() == ID_pointer)
1314  {
1315  const auto zero =
1316  zero_initializer(dest_expr.type(), function.source_location(), ns);
1317  CHECK_RETURN(zero.has_value());
1319  dest_expr, *zero, function.source_location()));
1320  }
1321  }
1322  else if(
1323  identifier == "__builtin_isgreater" ||
1324  identifier == "__builtin_isgreaterequal" ||
1325  identifier == "__builtin_isless" || identifier == "__builtin_islessequal" ||
1326  identifier == "__builtin_islessgreater" ||
1327  identifier == "__builtin_isunordered")
1328  {
1329  // these support two double or two float arguments; we call the
1330  // appropriate internal version
1331  if(arguments.size()!=2 ||
1332  (arguments[0].type()!=double_type() &&
1333  arguments[0].type()!=float_type()) ||
1334  (arguments[1].type()!=double_type() &&
1335  arguments[1].type()!=float_type()))
1336  {
1337  error().source_location=function.find_source_location();
1338  error() << "'" << identifier
1339  << "' expected to have two float/double arguments" << eom;
1340  throw 0;
1341  }
1342 
1343  exprt::operandst new_arguments=arguments;
1344 
1345  bool use_double=arguments[0].type()==double_type();
1346  if(arguments[0].type()!=arguments[1].type())
1347  {
1348  if(use_double)
1349  {
1350  new_arguments[1] =
1351  typecast_exprt(new_arguments[1], arguments[0].type());
1352  }
1353  else
1354  {
1355  new_arguments[0] =
1356  typecast_exprt(new_arguments[0], arguments[1].type());
1357  use_double=true;
1358  }
1359  }
1360 
1361  code_typet f_type=to_code_type(function.type());
1362  f_type.remove_ellipsis();
1363  const typet &a_t=new_arguments[0].type();
1364  f_type.parameters()=
1366 
1367  // replace __builtin_ by CPROVER_PREFIX
1368  std::string name=CPROVER_PREFIX+id2string(identifier).substr(10);
1369  // append d or f for double/float
1370  name+=use_double?'d':'f';
1371 
1372  symbol_exprt new_function=function;
1373  new_function.set_identifier(name);
1374  new_function.type()=f_type;
1375 
1376  code_function_callt function_call(lhs, new_function, new_arguments);
1377  function_call.add_source_location()=function.source_location();
1378 
1379  if(!symbol_table.has_symbol(name))
1380  {
1381  symbolt new_symbol;
1382  new_symbol.base_name=name;
1383  new_symbol.name=name;
1384  new_symbol.type=f_type;
1385  new_symbol.location=function.source_location();
1386  symbol_table.add(new_symbol);
1387  }
1388 
1389  copy(function_call, FUNCTION_CALL, dest);
1390  }
1391  else
1392  {
1393  do_function_call_symbol(*symbol);
1394 
1395  // insert function call
1396  code_function_callt function_call(lhs, function, arguments);
1397  function_call.add_source_location()=function.source_location();
1398 
1399  copy(function_call, FUNCTION_CALL, dest);
1400  }
1401 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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
exprt make_va_list(const exprt &expr)
floatbv_typet float_type()
Definition: c_types.cpp:195
unsignedbv_typet size_type()
Definition: c_types.cpp:68
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:238
bitvector_typet char_type()
Definition: c_types.cpp:124
bitvector_typet c_index_type()
Definition: c_types.cpp:16
floatbv_typet double_type()
Definition: c_types.cpp:203
Operator to return the address of an object.
Definition: pointer_expr.h:361
Arrays with given size.
Definition: std_types.h:763
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
const exprt & size() const
Definition: std_types.h:790
The Boolean type.
Definition: std_types.h:36
The type of C enums.
Definition: c_types.h:217
const memberst & members() const
Definition: c_types.h:255
std::vector< c_enum_membert > memberst
Definition: c_types.h:253
A codet representing an assignment in the program.
codet representation of a function call statement.
A codet representing the declaration that an input of a particular description has a value which corr...
A codet representing the declaration that an output of a particular description has a value which cor...
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:541
const typet & return_type() const
Definition: std_types.h:645
void remove_ellipsis()
Definition: std_types.h:640
const parameterst & parameters() const
Definition: std_types.h:655
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op0()
Definition: expr.h:99
void set_statement(const irep_idt &statement)
Definition: std_code_base.h:60
A constant literal expression.
Definition: std_expr.h:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The empty type.
Definition: std_types.h:51
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
std::vector< exprt > operandst
Definition: expr.h:56
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:114
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2865
Application of (mathematical) function.
void do_havoc_slice(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
symbol_table_baset & symbol_table
void do_input(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_array_op(const irep_idt &id, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
irep_idt get_string_constant(const exprt &expr)
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
void do_prob_coin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
void do_atomic_end(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
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...
virtual void do_function_call_symbol(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
add function calls to function queue for later processing
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
void do_output(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void cpp_new_initializer(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
builds a goto program for object initialization after new
void do_printf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
exprt get_array_argument(const exprt &src)
void do_scanf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void do_atomic_begin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
static void replace_new_object(const exprt &object, exprt &dest)
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void do_prob_uniform(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:934
instructionst::iterator targett
Definition: goto_program.h:592
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:698
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:975
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:964
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:922
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:942
Array index operator.
Definition: std_expr.h:1328
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
bool is_not_nil() const
Definition: irep.h:380
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
A type for mathematical functions (do not confuse with functions/methods in code)
std::vector< typet > domaint
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The plus expression Associativity is not specified.
Definition: std_expr.h:914
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
A base class for a predicate that indicates that an address range is ok to read or write or both.
Definition: pointer_expr.h:734
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
An expression containing a side effect.
Definition: std_code.h:1450
const irep_idt & get_statement() const
Definition: std_code.h:1472
Expression to hold a symbol (variable)
Definition: std_expr.h:80
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:104
const irep_idt & get_identifier() const
Definition: std_expr.h:109
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt value
Initial value of symbol.
Definition: symbol.h:34
const typet & subtype() const
Definition: type.h:156
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const source_locationt & source_location() const
Definition: type.h:74
source_locationt & add_source_location()
Definition: type.h:79
const exprt & op1() const =delete
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition: expr_util.cpp:21
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:216
Deprecated expression utility functions.
format_token_listt parse_format_string(const std::string &arg_string)
optionalt< typet > get_type(const format_tokent &token)
Format String Parser.
std::list< format_tokent > format_token_listt
Program Transformation.
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ASSIGN
Definition: goto_program.h:46
@ OTHER
Definition: goto_program.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes for 'mathematical' expressions.
Mathematical types.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
exprt object_size(const exprt &pointer)
constant_exprt from_rational(const rationalt &a)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const codet & to_code(const exprt &expr)
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
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
Author: Diffblue Ltd.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177