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>
19#include <util/fresh_symbol.h>
22#include <util/pointer_expr.h>
23#include <util/prefix.h>
24#include <util/rational.h>
25#include <util/rational_tools.h>
26#include <util/simplify_expr.h>
27#include <util/symbol.h>
28
30
31#include "format_strings.h"
32
34 const exprt &lhs,
35 const symbol_exprt &function,
36 const exprt::operandst &arguments,
37 goto_programt &dest)
38{
39 const irep_idt &identifier = function.get_identifier();
40
41 // make it a side effect if there is an LHS
42 if(arguments.size()!=2)
43 {
45 error() << "'" << identifier << "' expected to have two arguments" << eom;
46 throw 0;
47 }
48
49 if(lhs.is_nil())
50 {
52 error() << "'" << identifier << "' expected to have LHS" << eom;
53 throw 0;
54 }
55
56 auto rhs =
57 side_effect_exprt("prob_uniform", lhs.type(), function.source_location());
58
59 if(lhs.type().id()!=ID_unsignedbv &&
60 lhs.type().id()!=ID_signedbv)
61 {
63 error() << "'" << identifier << "' expected other type" << eom;
64 throw 0;
65 }
66
67 if(arguments[0].type().id()!=lhs.type().id() ||
68 arguments[1].type().id()!=lhs.type().id())
69 {
71 error() << "'" << identifier
72 << "' expected operands to be of same type as LHS" << eom;
73 throw 0;
74 }
75
76 if(!arguments[0].is_constant() ||
77 !arguments[1].is_constant())
78 {
80 error() << "'" << identifier
81 << "' expected operands to be constant literals" << eom;
82 throw 0;
83 }
84
85 mp_integer lb, ub;
86
87 if(
88 to_integer(to_constant_expr(arguments[0]), lb) ||
89 to_integer(to_constant_expr(arguments[1]), ub))
90 {
92 error() << "error converting operands" << eom;
93 throw 0;
94 }
95
96 if(lb > ub)
97 {
99 error() << "expected lower bound to be smaller or equal to the "
100 << "upper bound" << eom;
101 throw 0;
102 }
103
104 rhs.add_to_operands(exprt{arguments[0]}, exprt{arguments[1]});
105
106 code_assignt assignment(lhs, rhs);
107 assignment.add_source_location()=function.source_location();
108 copy(assignment, ASSIGN, dest);
109}
110
112 const exprt &lhs,
113 const symbol_exprt &function,
114 const exprt::operandst &arguments,
115 goto_programt &dest)
116{
117 const irep_idt &identifier = function.get_identifier();
118
119 // make it a side effect if there is an LHS
120 if(arguments.size()!=2)
121 {
123 error() << "'" << identifier << "' expected to have two arguments" << eom;
124 throw 0;
125 }
126
127 if(lhs.is_nil())
128 {
130 error() << "'" << identifier << "' expected to have LHS" << eom;
131 throw 0;
132 }
133
134 side_effect_exprt rhs("prob_coin", lhs.type(), function.source_location());
135
136 if(lhs.type()!=bool_typet())
137 {
139 error() << "'" << identifier << "' expected bool" << eom;
140 throw 0;
141 }
142
143 if(arguments[0].type().id() != ID_unsignedbv || !arguments[0].is_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(arguments[1].type().id() != ID_unsignedbv || !arguments[1].is_constant())
152 {
154 error() << "'" << identifier << "' expected second operand to be "
155 << "a constant literal of type unsigned long" << eom;
156 throw 0;
157 }
158
159 mp_integer num, den;
160
161 if(
162 to_integer(to_constant_expr(arguments[0]), num) ||
163 to_integer(to_constant_expr(arguments[1]), den))
164 {
166 error() << "error converting operands" << eom;
167 throw 0;
168 }
169
170 if(num-den > mp_integer(0))
171 {
173 error() << "probability has to be smaller than 1" << eom;
174 throw 0;
175 }
176
177 if(den == mp_integer(0))
178 {
180 error() << "denominator may not be zero" << eom;
181 throw 0;
182 }
183
184 rationalt numerator(num), denominator(den);
185 rationalt prob = numerator / denominator;
186
188
189 code_assignt assignment(lhs, rhs);
190 assignment.add_source_location()=function.source_location();
191 copy(assignment, ASSIGN, dest);
192}
193
195 const exprt &lhs,
196 const symbol_exprt &function,
197 const exprt::operandst &arguments,
198 goto_programt &dest)
199{
200 const irep_idt &f_id = function.get_identifier();
201
202 PRECONDITION(f_id == CPROVER_PREFIX "printf");
203
204 codet printf_code(ID_printf, arguments, function.source_location());
205 copy(printf_code, OTHER, dest);
206}
207
209 const exprt &lhs,
210 const symbol_exprt &function,
211 const exprt::operandst &arguments,
212 goto_programt &dest)
213{
214 const irep_idt &f_id = function.get_identifier();
215
216 if(f_id==CPROVER_PREFIX "scanf")
217 {
218 if(arguments.empty())
219 {
221 error() << "scanf takes at least one argument" << eom;
222 throw 0;
223 }
224
225 irep_idt format_string;
226
227 if(!get_string_constant(arguments[0], format_string))
228 {
229 // use our model
230 format_token_listt token_list=
231 parse_format_string(id2string(format_string));
232
233 std::size_t argument_number=1;
234
235 for(const auto &t : token_list)
236 {
237 const auto type = get_type(t);
238
239 if(type.has_value())
240 {
241 if(argument_number<arguments.size())
242 {
243 const typecast_exprt ptr(
244 arguments[argument_number], pointer_type(*type));
245 argument_number++;
246
247 if(type->id() == ID_array)
248 {
249 #if 0
250 // A string. We first need a nondeterministic size.
252 to_array_type(*type).size()=size;
253
254 const symbolt &tmp_symbol=
256 *type, "scanf_string", dest, function.source_location());
257
258 const address_of_exprt rhs(
260 tmp_symbol.symbol_expr(),
262
263 // now use array copy
264 codet array_copy_statement;
265 array_copy_statement.set_statement(ID_array_copy);
266 array_copy_statement.operands().resize(2);
267 array_copy_statement.op0()=ptr;
268\ array_copy_statement.op1()=rhs;
269 array_copy_statement.add_source_location()=
270 function.source_location();
271
272 copy(array_copy_statement, OTHER, dest);
273 #else
274 const index_exprt new_lhs(
276 const side_effect_expr_nondett rhs(
278 function.source_location());
279 code_assignt assign(new_lhs, rhs);
280 assign.add_source_location()=function.source_location();
281 copy(assign, ASSIGN, dest);
282 #endif
283 }
284 else
285 {
286 // make it nondet for now
287 const dereference_exprt new_lhs{ptr};
288 const side_effect_expr_nondett rhs(
289 *type, function.source_location());
290 code_assignt assign(new_lhs, rhs);
291 assign.add_source_location()=function.source_location();
292 copy(assign, ASSIGN, dest);
293 }
294 }
295 }
296 }
297 }
298 else
299 {
300 // we'll just do nothing
301 code_function_callt function_call(lhs, function, arguments);
302 function_call.add_source_location()=function.source_location();
303
304 copy(function_call, FUNCTION_CALL, dest);
305 }
306 }
307 else
309}
310
312 const exprt &function,
313 const exprt::operandst &arguments,
314 goto_programt &dest)
315{
316 if(arguments.size()<2)
317 {
319 error() << "input takes at least two arguments" << eom;
320 throw 0;
321 }
322
323 copy(code_inputt{arguments, function.source_location()}, OTHER, dest);
324}
325
327 const exprt &function,
328 const exprt::operandst &arguments,
329 goto_programt &dest)
330{
331 if(arguments.size()<2)
332 {
334 error() << "output takes at least two arguments" << eom;
335 throw 0;
336 }
337
338 copy(code_outputt{arguments, function.source_location()}, OTHER, dest);
339}
340
342 const exprt &lhs,
343 const symbol_exprt &function,
344 const exprt::operandst &arguments,
345 goto_programt &dest)
346{
347 if(lhs.is_not_nil())
348 {
350 error() << "atomic_begin does not expect an LHS" << eom;
351 throw 0;
352 }
353
354 if(!arguments.empty())
355 {
357 error() << "atomic_begin takes no arguments" << eom;
358 throw 0;
359 }
360
362}
363
365 const exprt &lhs,
366 const symbol_exprt &function,
367 const exprt::operandst &arguments,
368 goto_programt &dest)
369{
370 if(lhs.is_not_nil())
371 {
373 error() << "atomic_end does not expect an LHS" << eom;
374 throw 0;
375 }
376
377 if(!arguments.empty())
378 {
380 error() << "atomic_end takes no arguments" << eom;
381 throw 0;
382 }
383
385}
386
388 const exprt &lhs,
389 const side_effect_exprt &rhs,
390 goto_programt &dest)
391{
392 if(lhs.is_nil())
393 {
395 error() << "do_cpp_new without lhs is yet to be implemented" << eom;
396 throw 0;
397 }
398
399 // build size expression
401 static_cast<const exprt &>(rhs.find(ID_sizeof));
402
403 bool new_array=rhs.get(ID_statement)==ID_cpp_new_array;
404
405 exprt count;
406
407 if(new_array)
408 {
410 static_cast<const exprt &>(rhs.find(ID_size)), object_size.type());
411
412 // might have side-effect
413 clean_expr(count, dest, ID_cpp);
414 }
415
416 exprt tmp_symbol_expr;
417
418 // is this a placement new?
419 if(rhs.operands().empty()) // no, "regular" one
420 {
421 // call __new or __new_array
422 exprt new_symbol=
423 ns.lookup(new_array?"__new_array":"__new").symbol_expr();
424
425 const code_typet &code_type=
426 to_code_type(new_symbol.type());
427
428 const typet &return_type=
429 code_type.return_type();
430
432 code_type.parameters().size() == 1 || code_type.parameters().size() == 2,
433 "new has one or two parameters");
434
435 const symbolt &tmp_symbol =
436 new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
437
438 tmp_symbol_expr=tmp_symbol.symbol_expr();
439
440 code_function_callt new_call(new_symbol);
441 if(new_array)
442 new_call.arguments().push_back(count);
443 new_call.arguments().push_back(object_size);
444 new_call.set(
445 ID_C_cxx_alloc_type, to_type_with_subtype(lhs.type()).subtype());
446 new_call.lhs()=tmp_symbol_expr;
447 new_call.add_source_location()=rhs.source_location();
448
449 convert(new_call, dest, ID_cpp);
450 }
451 else if(rhs.operands().size()==1)
452 {
453 // call __placement_new
454 exprt new_symbol=
455 ns.lookup(
456 new_array?"__placement_new_array":"__placement_new").symbol_expr();
457
458 const code_typet &code_type=
459 to_code_type(new_symbol.type());
460
461 const typet &return_type=code_type.return_type();
462
464 code_type.parameters().size() == 2 || code_type.parameters().size() == 3,
465 "placement new has two or three parameters");
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 const irep_idt &mode)
624{
625 irep_idt identifier = CPROVER_PREFIX "havoc_slice";
626
627 // We disable checks on the generated instructions
628 // because we add our own rw_ok assertion that takes size into account
629 auto source_location = function.find_source_location();
630 source_location.add_pragma("disable:pointer-check");
631 source_location.add_pragma("disable:pointer-overflow-check");
632 source_location.add_pragma("disable:pointer-primitive-check");
633
634 // check # arguments
635 if(arguments.size() != 2)
636 {
637 error().source_location = source_location;
638 error() << "'" << identifier << "' expected to have two arguments" << eom;
639 throw 0;
640 }
641
642 // check argument types
643 if(arguments[0].type().id() != ID_pointer)
644 {
645 error().source_location = source_location;
646 error() << "'" << identifier
647 << "' first argument expected to have `void *` type" << eom;
648 throw 0;
649 }
650
651 if(arguments[1].type().id() != ID_unsignedbv)
652 {
653 error().source_location = source_location;
654 error() << "'" << identifier
655 << "' second argument expected to have `size_t` type" << eom;
656 throw 0;
657 }
658
659 // check nil lhs
660 if(lhs.is_not_nil())
661 {
662 error().source_location = source_location;
663 error() << "'" << identifier << "' not expected to have a LHS" << eom;
664 throw 0;
665 }
666
667 // insert instructions
668 // assert(rw_ok(argument[0], argument[1]));
669 // char nondet_contents[argument[1]];
670 // __CPROVER_array_replace(p, nondet_contents);
671
672 r_or_w_ok_exprt ok_expr(ID_w_ok, arguments[0], arguments[1]);
673 ok_expr.add_source_location() = source_location;
674 source_locationt annotated_location = source_location;
675 annotated_location.set("user-provided", false);
676 annotated_location.set_property_class(ID_assertion);
677 annotated_location.set_comment(
678 "assertion havoc_slice " + from_expr(ns, identifier, ok_expr));
679 dest.add(goto_programt::make_assertion(ok_expr, annotated_location));
680
681 const array_typet array_type(char_type(), simplify_expr(arguments[1], ns));
682
683 const symbolt &nondet_contents =
684 new_tmp_symbol(array_type, "nondet_contents", dest, source_location, mode);
685 const exprt &nondet_contents_expr = address_of_exprt{index_exprt{
686 nondet_contents.symbol_expr(), from_integer(0, c_index_type())}};
687
688 const exprt &arg0 =
691 nondet_contents_expr, pointer_type(empty_typet{}));
692
693 codet array_replace(ID_array_replace, {arg0, arg1}, source_location);
694 dest.add(goto_programt::make_other(array_replace, source_location));
695}
696
700 const exprt &lhs,
701 const symbol_exprt &function,
702 const exprt::operandst &arguments,
703 goto_programt &dest,
704 const irep_idt &mode)
705{
706 const source_locationt &source_location = function.source_location();
707 const auto alloca_type = to_code_type(function.type());
708
709 if(alloca_type.return_type() != pointer_type(void_type()))
710 {
711 error().source_location = source_location;
712 error() << "'alloca' function called, but 'alloca' has not been declared "
713 << "with expected 'void *' return type." << eom;
714 throw 0;
715 }
716 if(
717 alloca_type.parameters().size() != 1 ||
718 alloca_type.parameters()[0].type() != size_type())
719 {
720 error().source_location = source_location;
721 error() << "'alloca' function called, but 'alloca' has not been declared "
722 << "with expected single 'size_t' parameter." << eom;
723 throw 0;
724 }
725
726 exprt new_lhs = lhs;
727
728 // make sure we have a left-hand side to track the allocation even when the
729 // original program did not
730 if(lhs.is_nil())
731 {
732 new_lhs =
734 alloca_type.return_type(), "alloca", dest, source_location, mode)
735 .symbol_expr();
736 }
737
738 // do the actual function call
739 code_function_callt function_call(new_lhs, function, arguments);
740 function_call.add_source_location() = source_location;
741 copy(function_call, FUNCTION_CALL, dest);
742
743 // Don't add instrumentation when we're in alloca (which might in turn call
744 // __builtin_alloca) -- the instrumentation will be done for the call of
745 // alloca. Also, we can only add instrumentation when we're in a function
746 // context.
747 if(
748 function.source_location().get_function() == "alloca" || !targets.prefix ||
750 {
751 return;
752 }
753
754 // create a symbol to eventually (and non-deterministically) mark the
755 // allocation as dead; this symbol has function scope and is initialised to
756 // NULL
757 symbol_exprt this_alloca_ptr =
759 alloca_type.return_type(),
761 "tmp_alloca",
762 source_location,
763 mode,
765 .symbol_expr();
766 goto_programt decl_prg;
767 decl_prg.add(goto_programt::make_decl(this_alloca_ptr, source_location));
769 this_alloca_ptr,
770 null_pointer_exprt{to_pointer_type(this_alloca_ptr.type())},
771 source_location));
773 targets.prefix->instructions.begin(), decl_prg);
774
775 // non-deterministically update this_alloca_ptr
776 if_exprt rhs{
777 side_effect_expr_nondett{bool_typet(), source_location},
778 new_lhs,
779 this_alloca_ptr};
781 this_alloca_ptr, std::move(rhs), source_location));
782
783 // mark pointer to alloca result as dead, unless the alloca result (in
784 // this_alloca_ptr) is still NULL
785 symbol_exprt dead_object_sym =
786 ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
787 exprt alloca_result =
788 typecast_exprt::conditional_cast(this_alloca_ptr, dead_object_sym.type());
789 if_exprt not_null{
791 this_alloca_ptr,
792 null_pointer_exprt{to_pointer_type(this_alloca_ptr.type())}},
793 dead_object_sym,
794 std::move(alloca_result)};
795 auto assign = goto_programt::make_assignment(
796 std::move(dead_object_sym), std::move(not_null), source_location);
798 targets.suffix->instructions.begin(), assign);
800 targets.suffix->instructions.begin(),
801 goto_programt::make_dead(this_alloca_ptr, source_location));
802}
803
806 const exprt &lhs,
807 const symbol_exprt &function,
808 const exprt::operandst &arguments,
809 goto_programt &dest,
810 const irep_idt &mode)
811{
812 if(function.get_bool(ID_C_invalid_object))
813 return; // ignore
814
815 // lookup symbol
816 const irep_idt &identifier=function.get_identifier();
817
818 const symbolt *symbol;
819 if(ns.lookup(identifier, symbol))
820 {
822 error() << "error: function '" << identifier << "' not found" << eom;
823 throw 0;
824 }
825
826 if(symbol->type.id()!=ID_code)
827 {
829 error() << "error: function '" << identifier
830 << "' type mismatch: expected code" << eom;
831 throw 0;
832 }
833
834 // User-provided function definitions always take precedence over built-ins.
835 // Front-ends do not (yet) consistently set ID_C_incomplete, thus also test
836 // whether the symbol actually has some non-nil value (which might be
837 // "compiled").
838 if(!symbol->type.get_bool(ID_C_incomplete) && symbol->value.is_not_nil())
839 {
841
842 // use symbol->symbol_expr() to ensure we use the type from the symbol table
843 code_function_callt function_call(
844 lhs,
845 symbol->symbol_expr().with_source_location<symbol_exprt>(function),
846 arguments);
847 function_call.add_source_location() = function.source_location();
848
849 // remove void-typed assignments, which may have been created when the
850 // front-end was unable to detect them in type checking for a lack of
851 // available declarations
852 if(
853 lhs.is_not_nil() &&
854 to_code_type(symbol->type).return_type().id() == ID_empty)
855 {
856 function_call.lhs().make_nil();
857 }
858
859 copy(function_call, FUNCTION_CALL, dest);
860
861 return;
862 }
863
864 if(identifier == CPROVER_PREFIX "havoc_slice")
865 {
866 do_havoc_slice(lhs, function, arguments, dest, mode);
867 }
868 else if(
869 identifier == CPROVER_PREFIX "assume" || identifier == "__VERIFIER_assume")
870 {
871 if(arguments.size()!=1)
872 {
874 error() << "'" << identifier << "' expected to have one argument" << eom;
875 throw 0;
876 }
877
878 // let's double-check the type of the argument
879 source_locationt annotated_location = function.source_location();
880 annotated_location.set("user-provided", true);
882 typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
883 annotated_location));
884
885 if(lhs.is_not_nil())
886 {
888 error() << identifier << " expected not to have LHS" << eom;
889 throw 0;
890 }
891 }
892 else if(identifier=="__VERIFIER_error")
893 {
894 if(!arguments.empty())
895 {
897 error() << "'" << identifier << "' expected to have no arguments" << eom;
898 throw 0;
899 }
900
901 source_locationt annotated_location = function.source_location();
902 annotated_location.set("user-provided", true);
903 annotated_location.set_property_class(ID_assertion);
904 dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
905
906 if(lhs.is_not_nil())
907 {
909 error() << identifier << " expected not to have LHS" << eom;
910 throw 0;
911 }
912
913 // __VERIFIER_error has abort() semantics, even if no assertions
914 // are being checked
915 annotated_location = function.source_location();
916 annotated_location.set("user-provided", true);
917 dest.add(goto_programt::make_assumption(false_exprt(), annotated_location));
918 dest.instructions.back().labels.push_back("__VERIFIER_abort");
919 }
920 else if(
921 identifier == "assert" &&
923 {
924 if(arguments.size()!=1)
925 {
927 error() << "'" << identifier << "' expected to have one argument" << eom;
928 throw 0;
929 }
930
931 // let's double-check the type of the argument
932 source_locationt annotated_location = function.source_location();
933 annotated_location.set("user-provided", true);
934 annotated_location.set_property_class(ID_assertion);
935 annotated_location.set_comment(
936 "assertion " + from_expr(ns, identifier, arguments.front()));
938 typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
939 annotated_location));
940
941 if(lhs.is_not_nil())
942 {
944 error() << identifier << " expected not to have LHS" << eom;
945 throw 0;
946 }
947 }
948 else if(
949 identifier == CPROVER_PREFIX "assert" ||
950 identifier == CPROVER_PREFIX "precondition" ||
951 identifier == CPROVER_PREFIX "postcondition")
952 {
953 if(arguments.size()!=2)
954 {
956 error() << "'" << identifier << "' expected to have two arguments" << eom;
957 throw 0;
958 }
959
960 bool is_precondition=
961 identifier==CPROVER_PREFIX "precondition";
962 bool is_postcondition = identifier == CPROVER_PREFIX "postcondition";
963
964 const irep_idt description=
965 get_string_constant(arguments[1]);
966
967 // let's double-check the type of the argument
968 source_locationt annotated_location = function.source_location();
969 if(is_precondition)
970 {
971 annotated_location.set_property_class(ID_precondition);
972 }
973 else if(is_postcondition)
974 {
975 annotated_location.set_property_class(ID_postcondition);
976 }
977 else
978 {
979 annotated_location.set(
980 "user-provided", !function.source_location().is_built_in());
981 annotated_location.set_property_class(ID_assertion);
982 }
983
984 annotated_location.set_comment(description);
985
988 annotated_location));
989
990 if(lhs.is_not_nil())
991 {
993 error() << identifier << " expected not to have LHS" << eom;
994 throw 0;
995 }
996 }
997 else if(identifier==CPROVER_PREFIX "havoc_object")
998 {
999 if(arguments.size()!=1)
1000 {
1002 error() << "'" << identifier << "' expected to have one argument" << eom;
1003 throw 0;
1004 }
1005
1006 if(lhs.is_not_nil())
1007 {
1009 error() << identifier << " expected not to have LHS" << eom;
1010 throw 0;
1011 }
1012
1013 codet havoc(ID_havoc_object);
1014 havoc.add_source_location() = function.source_location();
1015 havoc.copy_to_operands(arguments[0]);
1016
1017 dest.add(goto_programt::make_other(havoc, function.source_location()));
1018 }
1019 else if(identifier==CPROVER_PREFIX "printf")
1020 {
1021 do_printf(lhs, function, arguments, dest);
1022 }
1023 else if(identifier==CPROVER_PREFIX "scanf")
1024 {
1025 do_scanf(lhs, function, arguments, dest);
1026 }
1027 else if(identifier==CPROVER_PREFIX "input" ||
1028 identifier=="__CPROVER::input")
1029 {
1030 if(lhs.is_not_nil())
1031 {
1033 error() << identifier << " expected not to have LHS" << eom;
1034 throw 0;
1035 }
1036
1037 do_input(function, arguments, dest);
1038 }
1039 else if(identifier==CPROVER_PREFIX "output" ||
1040 identifier=="__CPROVER::output")
1041 {
1042 if(lhs.is_not_nil())
1043 {
1045 error() << identifier << " expected not to have LHS" << eom;
1046 throw 0;
1047 }
1048
1049 do_output(function, arguments, dest);
1050 }
1051 else if(identifier==CPROVER_PREFIX "atomic_begin" ||
1052 identifier=="__CPROVER::atomic_begin" ||
1053 identifier=="java::org.cprover.CProver.atomicBegin:()V" ||
1054 identifier=="__VERIFIER_atomic_begin")
1055 {
1056 do_atomic_begin(lhs, function, arguments, dest);
1057 }
1058 else if(identifier==CPROVER_PREFIX "atomic_end" ||
1059 identifier=="__CPROVER::atomic_end" ||
1060 identifier=="java::org.cprover.CProver.atomicEnd:()V" ||
1061 identifier=="__VERIFIER_atomic_end")
1062 {
1063 do_atomic_end(lhs, function, arguments, dest);
1064 }
1065 else if(identifier==CPROVER_PREFIX "prob_biased_coin")
1066 {
1067 do_prob_coin(lhs, function, arguments, dest);
1068 }
1069 else if(has_prefix(id2string(identifier), CPROVER_PREFIX "prob_uniform_"))
1070 {
1071 do_prob_uniform(lhs, function, arguments, dest);
1072 }
1073 else if(has_prefix(id2string(identifier), "nondet_") ||
1074 has_prefix(id2string(identifier), "__VERIFIER_nondet_"))
1075 {
1076 // make it a side effect if there is an LHS
1077 if(lhs.is_nil())
1078 return;
1079
1080 exprt rhs;
1081
1082 // We need to special-case for _Bool, which
1083 // can only be 0 or 1.
1084 if(lhs.type().id()==ID_c_bool)
1085 {
1087 rhs.set(ID_C_identifier, identifier);
1088 rhs=typecast_exprt(rhs, lhs.type());
1089 }
1090 else
1091 {
1092 rhs = side_effect_expr_nondett(lhs.type(), function.source_location());
1093 rhs.set(ID_C_identifier, identifier);
1094 }
1095
1096 code_assignt assignment(lhs, rhs);
1097 assignment.add_source_location()=function.source_location();
1098 copy(assignment, ASSIGN, dest);
1099 }
1100 else if(has_prefix(id2string(identifier), CPROVER_PREFIX "uninterpreted_"))
1101 {
1102 // make it a side effect if there is an LHS
1103 if(lhs.is_nil())
1104 return;
1105
1106 if(function.type().get_bool(ID_C_incomplete))
1107 {
1109 error() << "'" << identifier << "' is not declared, "
1110 << "missing type information required to construct call to "
1111 << "uninterpreted function" << eom;
1112 throw 0;
1113 }
1114
1115 const code_typet &function_call_type = to_code_type(function.type());
1117 for(const auto &parameter : function_call_type.parameters())
1118 domain.push_back(parameter.type());
1119 mathematical_function_typet function_type{domain,
1120 function_call_type.return_type()};
1122 symbol_exprt{function.get_identifier(), function_type}, arguments);
1123
1124 code_assignt assignment(lhs, rhs);
1125 assignment.add_source_location()=function.source_location();
1126 copy(assignment, ASSIGN, dest);
1127 }
1128 else if(identifier==CPROVER_PREFIX "array_equal")
1129 {
1130 do_array_op(ID_array_equal, lhs, function, arguments, dest);
1131 }
1132 else if(identifier==CPROVER_PREFIX "array_set")
1133 {
1134 do_array_op(ID_array_set, lhs, function, arguments, dest);
1135 }
1136 else if(identifier==CPROVER_PREFIX "array_copy")
1137 {
1138 do_array_op(ID_array_copy, lhs, function, arguments, dest);
1139 }
1140 else if(identifier==CPROVER_PREFIX "array_replace")
1141 {
1142 do_array_op(ID_array_replace, lhs, function, arguments, dest);
1143 }
1144 else if(identifier=="__assert_fail" ||
1145 identifier=="_assert" ||
1146 identifier=="__assert_c99" ||
1147 identifier=="_wassert")
1148 {
1149 // __assert_fail is Linux
1150 // These take four arguments:
1151 // "expression", "file.c", line, __func__
1152 // klibc has __assert_fail with 3 arguments
1153 // "expression", "file.c", line
1154
1155 // MingW has
1156 // void _assert (const char*, const char*, int);
1157 // with three arguments:
1158 // "expression", "file.c", line
1159
1160 // This has been seen in Solaris 11.
1161 // Signature:
1162 // void __assert_c99(
1163 // const char *desc, const char *file, int line, const char *func);
1164
1165 // _wassert is Windows. The arguments are
1166 // L"expression", L"file.c", line
1167
1168 if(arguments.size()!=4 &&
1169 arguments.size()!=3)
1170 {
1172 error() << "'" << identifier << "' expected to have four arguments"
1173 << eom;
1174 throw 0;
1175 }
1176
1177 const irep_idt description=
1178 "assertion "+id2string(get_string_constant(arguments[0]));
1179
1180 source_locationt annotated_location = function.source_location();
1181 annotated_location.set("user-provided", true);
1182 annotated_location.set_property_class(ID_assertion);
1183 annotated_location.set_comment(description);
1184 dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
1185 // we ignore any LHS
1186 }
1187 else if(identifier=="__assert_rtn" ||
1188 identifier=="__assert")
1189 {
1190 // __assert_rtn has been seen on MacOS;
1191 // __assert is FreeBSD and Solaris 11.
1192 // These take four arguments:
1193 // __func__, "file.c", line, "expression"
1194 // On Solaris 11, it's three arguments:
1195 // "expression", "file", line
1196
1197 irep_idt description;
1198
1199 if(arguments.size()==4)
1200 {
1201 description=
1202 "assertion "+id2string(get_string_constant(arguments[3]));
1203 }
1204 else if(arguments.size()==3)
1205 {
1206 description=
1207 "assertion "+id2string(get_string_constant(arguments[1]));
1208 }
1209 else
1210 {
1212 error() << "'" << identifier << "' expected to have four arguments"
1213 << eom;
1214 throw 0;
1215 }
1216
1217 source_locationt annotated_location = function.source_location();
1218 annotated_location.set("user-provided", true);
1219 annotated_location.set_property_class(ID_assertion);
1220 annotated_location.set_comment(description);
1221 dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
1222 // we ignore any LHS
1223 }
1224 else if(identifier=="__assert_func")
1225 {
1226 // __assert_func is newlib (used by, e.g., cygwin)
1227 // These take four arguments:
1228 // "file.c", line, __func__, "expression"
1229 if(arguments.size()!=4)
1230 {
1232 error() << "'" << identifier << "' expected to have four arguments"
1233 << eom;
1234 throw 0;
1235 }
1236
1237 irep_idt description;
1238 try
1239 {
1240 description="assertion "+id2string(get_string_constant(arguments[3]));
1241 }
1242 catch(int)
1243 {
1244 // we might be building newlib, where __assert_func is passed
1245 // a pointer-typed symbol; the warning will still have been
1246 // printed
1247 description="assertion";
1248 }
1249
1250 source_locationt annotated_location = function.source_location();
1251 annotated_location.set("user-provided", true);
1252 annotated_location.set_property_class(ID_assertion);
1253 annotated_location.set_comment(description);
1254 dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
1255 // we ignore any LHS
1256 }
1257 else if(identifier==CPROVER_PREFIX "fence")
1258 {
1259 if(arguments.empty())
1260 {
1262 error() << "'" << identifier << "' expected to have at least one argument"
1263 << eom;
1264 throw 0;
1265 }
1266
1267 codet fence(ID_fence);
1268
1269 for(const auto &argument : arguments)
1270 fence.set(get_string_constant(argument), true);
1271
1272 dest.add(goto_programt::make_other(fence, function.source_location()));
1273 }
1274 else if(identifier=="__builtin_prefetch")
1275 {
1276 // does nothing
1277 }
1278 else if(identifier=="__builtin_unreachable")
1279 {
1280 // says something like UNREACHABLE;
1281 }
1282 else if(identifier==ID_gcc_builtin_va_arg)
1283 {
1284 // This does two things.
1285 // 1) Return value of argument.
1286 // This is just dereferencing.
1287 // 2) Move list pointer to next argument.
1288 // This is just an increment.
1289
1290 if(arguments.size()!=1)
1291 {
1293 error() << "'" << identifier << "' expected to have one argument" << eom;
1294 throw 0;
1295 }
1296
1297 exprt list_arg=make_va_list(arguments[0]);
1298
1299 if(lhs.is_not_nil())
1300 {
1301 exprt list_arg_cast = list_arg;
1302 if(
1303 list_arg.type().id() == ID_pointer &&
1304 to_pointer_type(list_arg.type()).base_type().id() == ID_empty)
1305 {
1306 list_arg_cast =
1308 }
1309
1310 typet t=pointer_type(lhs.type());
1312 typecast_exprt{dereference_exprt{std::move(list_arg_cast)}, t}};
1313 rhs.add_source_location()=function.source_location();
1314 dest.add(
1315 goto_programt::make_assignment(lhs, rhs, function.source_location()));
1316 }
1317
1318 code_assignt assign{
1319 list_arg, plus_exprt{list_arg, from_integer(1, pointer_diff_type())}};
1320 assign.rhs().set(
1321 ID_C_va_arg_type, to_code_type(function.type()).return_type());
1323 std::move(assign), function.source_location()));
1324 }
1325 else if(identifier=="__builtin_va_copy")
1326 {
1327 if(arguments.size()!=2)
1328 {
1330 error() << "'" << identifier << "' expected to have two arguments" << eom;
1331 throw 0;
1332 }
1333
1334 exprt dest_expr=make_va_list(arguments[0]);
1335 const typecast_exprt src_expr(arguments[1], dest_expr.type());
1336
1337 if(!is_assignable(dest_expr))
1338 {
1340 error() << "va_copy argument expected to be lvalue" << eom;
1341 throw 0;
1342 }
1343
1345 dest_expr, src_expr, function.source_location()));
1346 }
1347 else if(identifier == "__builtin_va_start" || identifier == "__va_start")
1348 {
1349 // Set the list argument to be the address of the
1350 // parameter argument.
1351 if(arguments.size()!=2)
1352 {
1354 error() << "'" << identifier << "' expected to have two arguments" << eom;
1355 throw 0;
1356 }
1357
1358 exprt dest_expr=make_va_list(arguments[0]);
1359
1360 if(!is_assignable(dest_expr))
1361 {
1363 error() << "va_start argument expected to be lvalue" << eom;
1364 throw 0;
1365 }
1366
1367 if(
1368 dest_expr.type().id() == ID_pointer &&
1369 to_pointer_type(dest_expr.type()).base_type().id() == ID_empty)
1370 {
1371 dest_expr =
1373 }
1374
1376 ID_va_start, dest_expr.type(), function.source_location()};
1377 rhs.add_to_operands(
1378 typecast_exprt{address_of_exprt{arguments[1]}, dest_expr.type()});
1379
1381 std::move(dest_expr), std::move(rhs), function.source_location()));
1382 }
1383 else if(identifier=="__builtin_va_end")
1384 {
1385 // Invalidates the argument. We do so by setting it to NULL.
1386 if(arguments.size()!=1)
1387 {
1389 error() << "'" << identifier << "' expected to have one argument" << eom;
1390 throw 0;
1391 }
1392
1393 exprt dest_expr=make_va_list(arguments[0]);
1394
1395 if(!is_assignable(dest_expr))
1396 {
1398 error() << "va_end argument expected to be lvalue" << eom;
1399 throw 0;
1400 }
1401
1402 // our __builtin_va_list is a pointer
1403 if(dest_expr.type().id() == ID_pointer)
1404 {
1405 const auto zero =
1406 zero_initializer(dest_expr.type(), function.source_location(), ns);
1407 CHECK_RETURN(zero.has_value());
1409 dest_expr, *zero, function.source_location()));
1410 }
1411 }
1412 else if(
1413 identifier == "__builtin_isgreater" ||
1414 identifier == "__builtin_isgreaterequal" ||
1415 identifier == "__builtin_isless" || identifier == "__builtin_islessequal" ||
1416 identifier == "__builtin_islessgreater" ||
1417 identifier == "__builtin_isunordered")
1418 {
1419 // these support two double or two float arguments; we call the
1420 // appropriate internal version
1421 if(arguments.size()!=2 ||
1422 (arguments[0].type()!=double_type() &&
1423 arguments[0].type()!=float_type()) ||
1424 (arguments[1].type()!=double_type() &&
1425 arguments[1].type()!=float_type()))
1426 {
1428 error() << "'" << identifier
1429 << "' expected to have two float/double arguments" << eom;
1430 throw 0;
1431 }
1432
1433 exprt::operandst new_arguments=arguments;
1434
1435 bool use_double=arguments[0].type()==double_type();
1436 if(arguments[0].type()!=arguments[1].type())
1437 {
1438 if(use_double)
1439 {
1440 new_arguments[1] =
1441 typecast_exprt(new_arguments[1], arguments[0].type());
1442 }
1443 else
1444 {
1445 new_arguments[0] =
1446 typecast_exprt(new_arguments[0], arguments[1].type());
1447 use_double=true;
1448 }
1449 }
1450
1451 code_typet f_type=to_code_type(function.type());
1452 f_type.remove_ellipsis();
1453 const typet &a_t=new_arguments[0].type();
1454 f_type.parameters()=
1456
1457 // replace __builtin_ by CPROVER_PREFIX
1458 std::string name=CPROVER_PREFIX+id2string(identifier).substr(10);
1459 // append d or f for double/float
1460 name+=use_double?'d':'f';
1461
1463 ns.lookup(name).type == f_type,
1464 "builtin declaration should match constructed type");
1465
1466 symbol_exprt new_function=function;
1467 new_function.set_identifier(name);
1468 new_function.type()=f_type;
1469
1470 code_function_callt function_call(lhs, new_function, new_arguments);
1471 function_call.add_source_location()=function.source_location();
1472
1473 copy(function_call, FUNCTION_CALL, dest);
1474 }
1475 else if(identifier == "alloca" || identifier == "__builtin_alloca")
1476 {
1477 do_alloca(lhs, function, arguments, dest, mode);
1478 }
1479 else
1480 {
1481 do_function_call_symbol(*symbol);
1482
1483 // insert function call
1484 // use symbol->symbol_expr() to ensure we use the type from the symbol table
1485 code_function_callt function_call(
1486 lhs,
1487 symbol->symbol_expr().with_source_location<symbol_exprt>(function),
1488 arguments);
1489 function_call.add_source_location()=function.source_location();
1490
1491 // remove void-typed assignments, which may have been created when the
1492 // front-end was unable to detect them in type checking for a lack of
1493 // available declarations
1494 if(
1495 lhs.is_not_nil() &&
1496 to_code_type(symbol->type).return_type().id() == ID_empty)
1497 {
1498 function_call.lhs().make_nil();
1499 }
1500
1501 copy(function_call, FUNCTION_CALL, dest);
1502 }
1503}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
exprt make_va_list(const exprt &expr)
floatbv_typet float_type()
Definition c_types.cpp:182
unsignedbv_typet size_type()
Definition c_types.cpp:55
empty_typet void_type()
Definition c_types.cpp:250
signedbv_typet signed_int_type()
Definition c_types.cpp:27
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
signedbv_typet pointer_diff_type()
Definition c_types.cpp:225
bitvector_typet char_type()
Definition c_types.cpp:111
bitvector_typet c_index_type()
Definition c_types.cpp:16
floatbv_typet double_type()
Definition c_types.cpp:190
Operator to return the address of an object.
Arrays with given size.
Definition std_types.h:763
const exprt & size() const
Definition std_types.h:796
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:783
The Boolean type.
Definition std_types.h:36
A goto_instruction_codet representing an assignment in the program.
goto_instruction_codet representation of a function call statement.
A goto_instruction_codet representing the declaration that an input of a particular description has a...
A goto_instruction_codet representing the declaration that an output of a particular description has ...
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.
exprt & op0()
Definition expr.h:125
exprt & op1()
Definition expr.h:128
void set_statement(const irep_idt &statement)
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
The empty type.
Definition std_types.h:51
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
std::vector< exprt > operandst
Definition expr.h:58
bool is_one() const
Return whether the expression is a constant representing 1.
Definition expr.cpp:96
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:155
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:223
source_locationt & add_source_location()
Definition expr.h:228
T & with_source_location(const exprt &other) &
Add the source location from other, if it has any.
Definition expr.h:102
The Boolean constant false.
Definition std_expr.h:3017
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)
struct goto_convertt::targetst targets
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)
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_alloca(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
alloca allocates memory that is freed when leaving the function (and not the block,...
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.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
The trinary if-then-else operator.
Definition std_expr.h:2323
Array index operator.
Definition std_expr.h:1410
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
bool is_not_nil() const
Definition irep.h:380
void make_nil()
Definition irep.h:454
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)
source_locationt source_location
Definition message.h:247
mstreamt & error() const
Definition message.h:399
static eomt eom
Definition message.h:297
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
The plus expression Associativity is not specified.
Definition std_expr.h:947
const typet & base_type() const
The type of the data what we point to.
A base class for a predicate that indicates that an address range is ok to read or write or both.
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 set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
const irep_idt & get_function() const
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:113
void set_identifier(const irep_idt &identifier)
Definition std_expr.h:137
const irep_idt & get_identifier() const
Definition std_expr.h:142
Symbol table entry.
Definition symbol.h:28
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
exprt value
Initial value of symbol.
Definition symbol.h:34
const typet & subtype() const
Definition type.h:154
Semantic type conversion.
Definition std_expr.h:2017
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
source_locationt & add_source_location()
Definition type.h:77
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
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition expr_util.cpp:24
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
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
Program Transformation.
@ FUNCTION_CALL
@ ASSIGN
@ OTHER
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.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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:18
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const codet & to_code(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:361
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
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:844
Symbol table entry.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:175