cprover
Loading...
Searching...
No Matches
builtin_functions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Program Transformation
4
5Author: 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>
18#include <util/expr_util.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
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 {
44 error() << "'" << identifier << "' expected to have two arguments" << eom;
45 throw 0;
46 }
47
48 if(lhs.is_nil())
49 {
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 {
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 {
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 {
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 {
91 error() << "error converting operands" << eom;
92 throw 0;
93 }
94
95 if(lb > ub)
96 {
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 {
122 error() << "'" << identifier << "' expected to have two arguments" << eom;
123 throw 0;
124 }
125
126 if(lhs.is_nil())
127 {
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 {
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 {
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 {
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 {
168 error() << "error converting operands" << eom;
169 throw 0;
170 }
171
172 if(num-den > mp_integer(0))
173 {
175 error() << "probability has to be smaller than 1" << eom;
176 throw 0;
177 }
178
179 if(den == mp_integer(0))
180 {
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
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 {
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(
262 tmp_symbol.symbol_expr(),
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(
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
311}
312
314 const exprt &function,
315 const exprt::operandst &arguments,
316 goto_programt &dest)
317{
318 if(arguments.size()<2)
319 {
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 {
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 {
359 error() << "atomic_begin takes no arguments" << eom;
360 throw 0;
361 }
362
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 {
382 error() << "atomic_end takes no arguments" << eom;
383 throw 0;
384 }
385
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
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 {
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 {
741 error() << "error: function '" << identifier << "' not found" << eom;
742 throw 0;
743 }
744
745 if(symbol->type.id()!=ID_code)
746 {
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 {
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 {
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 {
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 {
802 error() << "'" << identifier << "' expected to have no arguments" << eom;
803 throw 0;
804 }
805
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 {
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 {
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 {
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 {
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 {
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 {
909 error() << "'" << identifier << "' expected to have one argument" << eom;
910 throw 0;
911 }
912
913 if(lhs.is_not_nil())
914 {
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 {
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 {
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 {
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 {
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()};
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 {
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(
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 {
1120 error() << "'" << identifier << "' expected to have four arguments"
1121 << eom;
1122 throw 0;
1123 }
1124
1125 goto_programt::targett t = dest.add(
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 {
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(
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 {
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 {
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());
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 {
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 {
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
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 {
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 {
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 exprt & size() const
Definition: std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
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:542
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
void remove_ellipsis()
Definition: std_types.h:640
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
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
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
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
void add_pragma(const irep_idt &pragma)
static bool is_built_in(const std::string &s)
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
source_locationt & add_source_location()
Definition: type.h:79
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.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:216
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition: expr_util.cpp:21
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 address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
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 index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
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 constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
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