CBMC: /home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/builtin_functions.cpp Source File

CBMC
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>
17#include <util/expr_initializer.h>
18#include <util/expr_util.h>
19#include <util/fresh_symbol.h>
20#include <util/mathematical_expr.h>
21#include <util/mathematical_types.h>
22#include <util/pointer_expr.h>
23#include <util/rational.h>
24#include <util/rational_tools.h>
25#include <util/simplify_expr.h>
26#include <util/symbol.h>
27
28#include <langapi/language_util.h>
29
30#include "destructor.h"
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.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 && lhs.type().id() != ID_signedbv)
60 {
62 error() << "'" << identifier << "' expected other type" << eom;
63 throw 0;
64 }
65
66 if(
67 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() || !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.add_to_operands(exprt{arguments[0]}, exprt{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.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 || !arguments[0].is_constant())
143 {
145 error() << "'" << identifier << "' expected first operand to be "
146 << "a constant literal of type unsigned long" << eom;
147 throw 0;
148 }
149
150 if(arguments[1].type().id() != ID_unsignedbv || !arguments[1].is_constant())
151 {
153 error() << "'" << identifier << "' expected second operand to be "
154 << "a constant literal of type unsigned long" << eom;
155 throw 0;
156 }
157
158 mp_integer num, den;
159
160 if(
161 to_integer(to_constant_expr(arguments[0]), num) ||
162 to_integer(to_constant_expr(arguments[1]), den))
163 {
165 error() << "error converting operands" << eom;
166 throw 0;
167 }
168
169 if(num - den > mp_integer(0))
170 {
172 error() << "probability has to be smaller than 1" << eom;
173 throw 0;
174 }
175
176 if(den == mp_integer(0))
177 {
179 error() << "denominator may not be zero" << eom;
180 throw 0;
181 }
182
183 rationalt numerator(num), denominator(den);
184 rationalt prob = numerator / denominator;
185
187
188 code_assignt assignment(lhs, rhs);
189 assignment.add_source_location() = function.source_location();
190 copy(assignment, ASSIGN, dest);
191}
192
194 const exprt &lhs,
195 const symbol_exprt &function,
196 const exprt::operandst &arguments,
197 goto_programt &dest)
198{
199 const irep_idt &f_id = function.identifier();
200
201 PRECONDITION(f_id == CPROVER_PREFIX "printf");
202
203 codet printf_code(ID_printf, arguments, function.source_location());
204 copy(printf_code, OTHER, dest);
205}
206
208 const exprt &lhs,
209 const symbol_exprt &function,
210 const exprt::operandst &arguments,
211 goto_programt &dest)
212{
213 const irep_idt &f_id = function.identifier();
214
215 if(f_id == CPROVER_PREFIX "scanf")
216 {
217 if(arguments.empty())
218 {
220 error() << "scanf takes at least one argument" << eom;
221 throw 0;
222 }
223
224 irep_idt format_string;
225
226 if(!get_string_constant(arguments[0], format_string))
227 {
228 // use our model
230 parse_format_string(id2string(format_string));
231
232 std::size_t argument_number = 1;
233
234 for(const auto &t : token_list)
235 {
236 const auto type = get_type(t);
237
238 if(type.has_value())
239 {
240 if(argument_number < arguments.size())
241 {
242 const typecast_exprt ptr(
243 arguments[argument_number], pointer_type(*type));
245
246 if(type->id() == ID_array)
247 {
248#if 0
249 // A string. We first need a nondeterministic size.
251 to_array_type(*type).size()=size;
252
253 const symbolt &tmp_symbol=
255 *type, "scanf_string", dest, function.source_location());
256
257 const address_of_exprt rhs(
259 tmp_symbol.symbol_expr(),
261
262 // now use array copy
264 array_copy_statement.set_statement(ID_array_copy);
265 array_copy_statement.operands().resize(2);
266 array_copy_statement.op0()=ptr;
267\ array_copy_statement.op1()=rhs;
268 array_copy_statement.add_source_location()=
269 function.source_location();
270
272#else
273 const index_exprt new_lhs(
275 const side_effect_expr_nondett rhs(
276 to_array_type(*type).element_type(),
277 function.source_location());
278 code_assignt assign(new_lhs, rhs);
279 assign.add_source_location() = function.source_location();
280 copy(assign, ASSIGN, dest);
281#endif
282 }
283 else
284 {
285 // make it nondet for now
286 const dereference_exprt new_lhs{ptr};
287 const side_effect_expr_nondett rhs(
288 *type, function.source_location());
289 code_assignt assign(new_lhs, rhs);
290 assign.add_source_location() = function.source_location();
291 copy(assign, ASSIGN, dest);
292 }
293 }
294 }
295 }
296 }
297 else
298 {
299 // we'll just do nothing
300 code_function_callt function_call(lhs, function, arguments);
301 function_call.add_source_location() = function.source_location();
302
303 copy(function_call, FUNCTION_CALL, dest);
304 }
305 }
306 else
308}
309
311 const exprt &function,
312 const exprt::operandst &arguments,
313 goto_programt &dest)
314{
315 if(arguments.size() < 2)
316 {
318 error() << "input takes at least two arguments" << eom;
319 throw 0;
320 }
321
322 copy(code_inputt{arguments, function.source_location()}, OTHER, dest);
323}
324
326 const exprt &function,
327 const exprt::operandst &arguments,
328 goto_programt &dest)
329{
330 if(arguments.size() < 2)
331 {
333 error() << "output takes at least two arguments" << eom;
334 throw 0;
335 }
336
337 copy(code_outputt{arguments, function.source_location()}, OTHER, dest);
338}
339
341 const exprt &lhs,
342 const symbol_exprt &function,
343 const exprt::operandst &arguments,
344 goto_programt &dest)
345{
346 if(lhs.is_not_nil())
347 {
349 error() << "atomic_begin does not expect an LHS" << eom;
350 throw 0;
351 }
352
353 if(!arguments.empty())
354 {
356 error() << "atomic_begin takes no arguments" << eom;
357 throw 0;
358 }
359
361}
362
364 const exprt &lhs,
365 const symbol_exprt &function,
366 const exprt::operandst &arguments,
367 goto_programt &dest)
368{
369 if(lhs.is_not_nil())
370 {
372 error() << "atomic_end does not expect an LHS" << eom;
373 throw 0;
374 }
375
376 if(!arguments.empty())
377 {
379 error() << "atomic_end takes no arguments" << eom;
380 throw 0;
381 }
382
384}
385
387 const exprt &lhs,
388 const side_effect_exprt &rhs,
389 goto_programt &dest)
390{
391 if(lhs.is_nil())
392 {
394 error() << "do_cpp_new without lhs is yet to be implemented" << eom;
395 throw 0;
396 }
397
398 // build size expression
399 exprt object_size = static_cast<const exprt &>(rhs.find(ID_sizeof));
400
402
403 exprt count;
404 clean_expr_resultt side_effects;
405
406 if(new_array)
407 {
409 static_cast<const exprt &>(rhs.find(ID_size)), object_size.type());
410
411 // might have side-effect
412 side_effects.add(clean_expr(count, ID_cpp));
413 dest.destructive_append(side_effects.side_effects);
414 }
415
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 = to_code_type(new_symbol.type());
426
427 const typet &return_type = code_type.return_type();
428
430 code_type.parameters().size() == 1 || code_type.parameters().size() == 2,
431 "new has one or two parameters");
432
433 const symbolt &tmp_symbol =
434 new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
435
436 tmp_symbol_expr = tmp_symbol.symbol_expr();
437
438 code_function_callt new_call(new_symbol);
439 if(new_array)
440 new_call.arguments().push_back(count);
441 new_call.arguments().push_back(object_size);
442 new_call.set(
445 new_call.add_source_location() = rhs.source_location();
446
447 convert(new_call, dest, ID_cpp);
448 }
449 else if(rhs.operands().size() == 1)
450 {
451 // call __placement_new
452 exprt new_symbol =
453 ns.lookup(new_array ? "__placement_new_array" : "__placement_new")
454 .symbol_expr();
455
456 const code_typet &code_type = to_code_type(new_symbol.type());
457
458 const typet &return_type = code_type.return_type();
459
461 code_type.parameters().size() == 2 || code_type.parameters().size() == 3,
462 "placement new has two or three parameters");
463
464 const symbolt &tmp_symbol =
465 new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
466
467 tmp_symbol_expr = tmp_symbol.symbol_expr();
468
469 code_function_callt new_call(new_symbol);
470 if(new_array)
471 new_call.arguments().push_back(count);
472 new_call.arguments().push_back(object_size);
473 new_call.arguments().push_back(to_unary_expr(rhs).op()); // memory location
474 new_call.set(
477 new_call.add_source_location() = rhs.source_location();
478
479 for(std::size_t i = 0; i < code_type.parameters().size(); i++)
480 {
482 new_call.arguments()[i], code_type.parameters()[i].type());
483 }
484
485 convert(new_call, dest, ID_cpp);
486 }
487 else
488 {
490 error() << "cpp_new expected to have 0 or 1 operands" << eom;
491 throw 0;
492 }
493
495 lhs,
497 rhs.find_source_location()));
498
499 side_effects.add_temporary(to_symbol_expr(tmp_symbol_expr).identifier());
500 destruct_locals(side_effects.temporaries, dest, ns);
501
502 // grab initializer
505
507}
508
511 const exprt &lhs,
512 const side_effect_exprt &rhs,
513 goto_programt &dest)
514{
515 exprt initializer = static_cast<const exprt &>(rhs.find(ID_initializer));
516
517 if(initializer.is_not_nil())
518 {
519 if(rhs.get_statement() == "cpp_new[]")
520 {
521 // build loop
522 }
523 else if(rhs.get_statement() == ID_cpp_new)
524 {
525 // just one object
527 lhs, to_pointer_type(rhs.type()).base_type());
528
529 replace_new_object(deref_lhs, initializer);
530 convert(to_code(initializer), dest, ID_cpp);
531 }
532 else
534 }
535}
536
538{
539 if(src.id() == ID_typecast)
540 return get_array_argument(to_typecast_expr(src).op());
541
542 if(src.id() != ID_address_of)
543 {
545 error() << "expected array-pointer as argument" << eom;
546 throw 0;
547 }
548
549 const auto &address_of_expr = to_address_of_expr(src);
550
551 if(address_of_expr.object().id() != ID_index)
552 {
554 error() << "expected array-element as argument" << eom;
555 throw 0;
556 }
557
558 const auto &index_expr = to_index_expr(address_of_expr.object());
559
560 if(index_expr.array().type().id() != ID_array)
561 {
563 error() << "expected array as argument" << eom;
564 throw 0;
565 }
566
567 return index_expr.array();
568}
569
571 const irep_idt &id,
572 const exprt &lhs,
573 const symbol_exprt &function,
574 const exprt::operandst &arguments,
575 goto_programt &dest)
576{
577 if(arguments.size() != 2)
578 {
580 error() << id << " expects two arguments" << eom;
581 throw 0;
582 }
583
585 array_op_statement.operands() = arguments;
586 array_op_statement.add_source_location() = function.source_location();
587
588 // lhs is only used with array_equal, in all other cases it should be nil (as
589 // they are of type void)
590 if(id == ID_array_equal)
591 array_op_statement.copy_to_operands(lhs);
592
594}
595
596 static exprt make_va_list(const exprt &expr, const namespacet &ns)
597{
598 if(
600 {
601 // aarch64 ABI mandates that va_list has struct type with member names as
602 // specified
603 const auto &components = ns.follow_tag(*struct_tag_type).components();
605 components.size() == 5,
606 "va_list struct type expected to have 5 components");
607 return member_exprt{expr, components.front()};
608 }
609
610 exprt result = skip_typecast(expr);
611
612 // if it's an address of an lvalue, we take that
613 if(result.id() == ID_address_of)
614 {
615 const auto &address_of_expr = to_address_of_expr(result);
616 if(is_assignable(address_of_expr.object()))
617 result = address_of_expr.object();
618 }
619
620 while(result.type().id() == ID_array &&
621 to_array_type(result.type()).size() == 1)
622 {
623 result = index_exprt{result, from_integer(0, c_index_type())};
624 }
625
626 return result;
627}
628
630 const exprt &lhs,
631 const symbol_exprt &function,
632 const exprt::operandst &arguments,
633 goto_programt &dest,
634 const irep_idt &mode)
635{
636 irep_idt identifier = CPROVER_PREFIX "havoc_slice";
637
638 // We disable checks on the generated instructions
639 // because we add our own rw_ok assertion that takes size into account
640 auto source_location = function.find_source_location();
641 source_location.add_pragma("disable:pointer-check");
642 source_location.add_pragma("disable:pointer-overflow-check");
643 source_location.add_pragma("disable:pointer-primitive-check");
644
645 // check # arguments
646 if(arguments.size() != 2)
647 {
648 error().source_location = source_location;
649 error() << "'" << identifier << "' expected to have two arguments" << eom;
650 throw 0;
651 }
652
653 // check argument types
654 if(arguments[0].type().id() != ID_pointer)
655 {
656 error().source_location = source_location;
657 error() << "'" << identifier
658 << "' first argument expected to have `void *` type" << eom;
659 throw 0;
660 }
661
662 if(arguments[1].type().id() != ID_unsignedbv)
663 {
664 error().source_location = source_location;
665 error() << "'" << identifier
666 << "' second argument expected to have `size_t` type" << eom;
667 throw 0;
668 }
669
670 // check nil lhs
671 if(lhs.is_not_nil())
672 {
673 error().source_location = source_location;
674 error() << "'" << identifier << "' not expected to have a LHS" << eom;
675 throw 0;
676 }
677
678 // insert instructions
679 // assert(rw_ok(argument[0], argument[1]));
680 // char nondet_contents[argument[1]];
681 // __CPROVER_array_replace(p, nondet_contents);
682
683 r_or_w_ok_exprt ok_expr(ID_w_ok, arguments[0], arguments[1]);
684 ok_expr.add_source_location() = source_location;
685 source_locationt annotated_location = source_location;
686 annotated_location.set("user-provided", false);
687 annotated_location.set_property_class(ID_assertion);
688 annotated_location.set_comment(
689 "assertion havoc_slice " + from_expr(ns, identifier, ok_expr));
691
692 const array_typet array_type(char_type(), simplify_expr(arguments[1], ns));
693
694 const symbolt &nondet_contents =
695 new_tmp_symbol(array_type, "nondet_contents", dest, source_location, mode);
697 nondet_contents.symbol_expr(), from_integer(0, c_index_type())}};
698
699 const exprt &arg0 =
703
704 codet array_replace(ID_array_replace, {arg0, arg1}, source_location);
705 dest.add(goto_programt::make_other(array_replace, source_location));
706
707 destruct_locals({nondet_contents.name}, dest, ns);
708}
709
713 const exprt &lhs,
714 const symbol_exprt &function,
715 const exprt::operandst &arguments,
716 goto_programt &dest,
717 const irep_idt &mode)
718{
719 const source_locationt &source_location = function.source_location();
720 const auto alloca_type = to_code_type(function.type());
721
722 if(alloca_type.return_type() != pointer_type(void_type()))
723 {
724 error().source_location = source_location;
725 error() << "'alloca' function called, but 'alloca' has not been declared "
726 << "with expected 'void *' return type." << eom;
727 throw 0;
728 }
729 if(
730 alloca_type.parameters().size() != 1 ||
731 alloca_type.parameters()[0].type() != size_type())
732 {
733 error().source_location = source_location;
734 error() << "'alloca' function called, but 'alloca' has not been declared "
735 << "with expected single 'size_t' parameter." << eom;
736 throw 0;
737 }
738
739 exprt new_lhs = lhs;
740
741 // make sure we have a left-hand side to track the allocation even when the
742 // original program did not
743 if(lhs.is_nil())
744 {
745 new_lhs =
747 alloca_type.return_type(), "alloca", dest, source_location, mode)
748 .symbol_expr();
749 }
750
751 // do the actual function call
752 code_function_callt function_call(new_lhs, function, arguments);
753 function_call.add_source_location() = source_location;
754 copy(function_call, FUNCTION_CALL, dest);
755
756 // Don't add instrumentation when we're in alloca (which might in turn call
757 // __builtin_alloca) -- the instrumentation will be done for the call of
758 // alloca. Also, we can only add instrumentation when we're in a function
759 // context.
760 if(
761 function.source_location().get_function() == "alloca" || !targets.prefix ||
762 !targets.suffix)
763 {
764 return;
765 }
766
767 // create a symbol to eventually (and non-deterministically) mark the
768 // allocation as dead; this symbol has function scope and is initialised to
769 // NULL
772 alloca_type.return_type(),
773 id2string(function.source_location().get_function()),
774 "tmp_alloca",
775 source_location,
776 mode,
778 .symbol_expr();
784 source_location));
785 targets.prefix->destructive_insert(
786 targets.prefix->instructions.begin(), decl_prg);
787
788 // non-deterministically update this_alloca_ptr
789 if_exprt rhs{
790 side_effect_expr_nondett{bool_typet(), source_location},
791 new_lhs,
794 this_alloca_ptr, std::move(rhs), source_location));
795
796 if(lhs.is_nil())
797 destruct_locals({to_symbol_expr(new_lhs).identifier()}, dest, ns);
798
799 // mark pointer to alloca result as dead, unless the alloca result (in
800 // this_alloca_ptr) is still NULL
802 ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
810 std::move(alloca_result)};
811 auto assign = goto_programt::make_assignment(
812 std::move(dead_object_sym), std::move(not_null), source_location);
813 targets.suffix->insert_before_swap(
814 targets.suffix->instructions.begin(), assign);
815 targets.suffix->insert_after(
816 targets.suffix->instructions.begin(),
817 goto_programt::make_dead(this_alloca_ptr, source_location));
818}
819
822 const exprt &lhs,
823 const symbol_exprt &function,
824 const exprt::operandst &arguments,
825 goto_programt &dest,
826 const irep_idt &mode)
827{
828 if(function.get_bool(ID_C_invalid_object))
829 return; // ignore
830
831 // lookup symbol
832 const irep_idt &identifier = function.identifier();
833
834 const symbolt *symbol;
835 if(ns.lookup(identifier, symbol))
836 {
838 error() << "function '" << identifier << "' not found" << eom;
839 throw 0;
840 }
841
842 if(symbol->type.id() != ID_code)
843 {
845 error() << "function '" << identifier << "' type mismatch: expected code"
846 << eom;
847 throw 0;
848 }
849
850 // User-provided function definitions always take precedence over built-ins.
851 // Front-ends do not (yet) consistently set ID_C_incomplete, thus also test
852 // whether the symbol actually has some non-nil value (which might be
853 // "compiled").
854 if(!symbol->type.get_bool(ID_C_incomplete) && symbol->value.is_not_nil())
855 {
857
858 // use symbol->symbol_expr() to ensure we use the type from the symbol table
859 code_function_callt function_call(
860 lhs, symbol->symbol_expr().with_source_location(function), arguments);
861 function_call.add_source_location() = function.source_location();
862
863 // remove void-typed assignments, which may have been created when the
864 // front-end was unable to detect them in type checking for a lack of
865 // available declarations
866 if(
867 lhs.is_not_nil() &&
868 to_code_type(symbol->type).return_type().id() == ID_empty)
869 {
870 function_call.lhs().make_nil();
871 }
872
873 copy(function_call, FUNCTION_CALL, dest);
874
875 return;
876 }
877
878 if(identifier == CPROVER_PREFIX "havoc_slice")
879 {
880 do_havoc_slice(lhs, function, arguments, dest, mode);
881 }
882 else if(
883 identifier == CPROVER_PREFIX "assume" || identifier == "__VERIFIER_assume")
884 {
885 if(arguments.size() != 1)
886 {
888 error() << "'" << identifier << "' expected to have one argument" << eom;
889 throw 0;
890 }
891
892 // let's double-check the type of the argument
894 annotated_location.set("user-provided", true);
896 typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
898
899 if(lhs.is_not_nil())
900 {
902 error() << identifier << " expected not to have LHS" << eom;
903 throw 0;
904 }
905 }
906 else if(identifier == "__VERIFIER_error")
907 {
908 if(!arguments.empty())
909 {
911 error() << "'" << identifier << "' expected to have no arguments" << eom;
912 throw 0;
913 }
914
916 annotated_location.set("user-provided", true);
917 annotated_location.set_property_class(ID_assertion);
919
920 if(lhs.is_not_nil())
921 {
923 error() << identifier << " expected not to have LHS" << eom;
924 throw 0;
925 }
926
927 // __VERIFIER_error has abort() semantics, even if no assertions
928 // are being checked
930 annotated_location.set("user-provided", true);
932 dest.instructions.back().labels.push_back("__VERIFIER_abort");
933 }
934 else if(
935 identifier == "assert" &&
936 to_code_type(symbol->type).return_type() == signed_int_type())
937 {
938 if(arguments.size() != 1)
939 {
941 error() << "'" << identifier << "' expected to have one argument" << eom;
942 throw 0;
943 }
944
945 // let's double-check the type of the argument
947 annotated_location.set("user-provided", true);
948 annotated_location.set_property_class(ID_assertion);
949 annotated_location.set_comment(
950 "assertion " + from_expr(ns, identifier, arguments.front()));
952 typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
954
955 if(lhs.is_not_nil())
956 {
958 error() << identifier << " expected not to have LHS" << eom;
959 throw 0;
960 }
961 }
962 else if(
963 identifier == CPROVER_PREFIX "assert" ||
964 identifier == CPROVER_PREFIX "precondition" ||
965 identifier == CPROVER_PREFIX "postcondition")
966 {
967 if(arguments.size() != 2)
968 {
970 error() << "'" << identifier << "' expected to have two arguments" << eom;
971 throw 0;
972 }
973
974 bool is_precondition = identifier == CPROVER_PREFIX "precondition";
975 bool is_postcondition = identifier == CPROVER_PREFIX "postcondition";
976
977 const irep_idt description = get_string_constant(arguments[1]);
978
979 // let's double-check the type of the argument
982 {
983 annotated_location.set_property_class(ID_precondition);
984 }
985 else if(is_postcondition)
986 {
987 annotated_location.set_property_class(ID_postcondition);
988 }
989 else
990 {
992 "user-provided", !function.source_location().is_built_in());
993 annotated_location.set_property_class(ID_assertion);
994 }
995
996 annotated_location.set_comment(description);
997
1001
1002 if(lhs.is_not_nil())
1003 {
1005 error() << identifier << " expected not to have LHS" << eom;
1006 throw 0;
1007 }
1008 }
1009 else if(identifier == CPROVER_PREFIX "havoc_object")
1010 {
1011 if(arguments.size() != 1)
1012 {
1014 error() << "'" << identifier << "' expected to have one argument" << eom;
1015 throw 0;
1016 }
1017
1018 if(lhs.is_not_nil())
1019 {
1021 error() << identifier << " expected not to have LHS" << eom;
1022 throw 0;
1023 }
1024
1025 codet havoc(ID_havoc_object);
1026 havoc.add_source_location() = function.source_location();
1027 havoc.copy_to_operands(arguments[0]);
1028
1029 dest.add(goto_programt::make_other(havoc, function.source_location()));
1030 }
1031 else if(identifier == CPROVER_PREFIX "printf")
1032 {
1033 do_printf(lhs, function, arguments, dest);
1034 }
1035 else if(identifier == CPROVER_PREFIX "scanf")
1036 {
1037 do_scanf(lhs, function, arguments, dest);
1038 }
1039 else if(
1040 identifier == CPROVER_PREFIX "input" || identifier == "__CPROVER::input")
1041 {
1042 if(lhs.is_not_nil())
1043 {
1045 error() << identifier << " expected not to have LHS" << eom;
1046 throw 0;
1047 }
1048
1049 do_input(function, arguments, dest);
1050 }
1051 else if(
1052 identifier == CPROVER_PREFIX "output" || identifier == "__CPROVER::output")
1053 {
1054 if(lhs.is_not_nil())
1055 {
1057 error() << identifier << " expected not to have LHS" << eom;
1058 throw 0;
1059 }
1060
1061 do_output(function, arguments, dest);
1062 }
1063 else if(
1064 identifier == CPROVER_PREFIX "atomic_begin" ||
1065 identifier == "__CPROVER::atomic_begin" ||
1066 identifier == "java::org.cprover.CProver.atomicBegin:()V" ||
1067 identifier == "__VERIFIER_atomic_begin")
1068 {
1069 do_atomic_begin(lhs, function, arguments, dest);
1070 }
1071 else if(
1072 identifier == CPROVER_PREFIX "atomic_end" ||
1073 identifier == "__CPROVER::atomic_end" ||
1074 identifier == "java::org.cprover.CProver.atomicEnd:()V" ||
1075 identifier == "__VERIFIER_atomic_end")
1076 {
1077 do_atomic_end(lhs, function, arguments, dest);
1078 }
1079 else if(identifier == CPROVER_PREFIX "prob_biased_coin")
1080 {
1081 do_prob_coin(lhs, function, arguments, dest);
1082 }
1083 else if(identifier.starts_with(CPROVER_PREFIX "prob_uniform_"))
1084 {
1085 do_prob_uniform(lhs, function, arguments, dest);
1086 }
1087 else if(
1088 identifier.starts_with("nondet_") ||
1089 identifier.starts_with("__VERIFIER_nondet_"))
1090 {
1091 // make it a side effect if there is an LHS
1092 if(lhs.is_nil())
1093 return;
1094
1095 exprt rhs;
1096
1097 // We need to special-case for _Bool, which
1098 // can only be 0 or 1.
1099 if(lhs.type().id() == ID_c_bool)
1100 {
1102 rhs.set(ID_C_identifier, identifier);
1103 rhs = typecast_exprt(rhs, lhs.type());
1104 }
1105 else
1106 {
1107 rhs = side_effect_expr_nondett(lhs.type(), function.source_location());
1108 rhs.set(ID_C_identifier, identifier);
1109 }
1110
1111 code_assignt assignment(lhs, rhs);
1112 assignment.add_source_location() = function.source_location();
1113 copy(assignment, ASSIGN, dest);
1114 }
1115 else if(identifier.starts_with(CPROVER_PREFIX "uninterpreted_"))
1116 {
1117 // make it a side effect if there is an LHS
1118 if(lhs.is_nil())
1119 return;
1120
1121 if(function.type().get_bool(ID_C_incomplete))
1122 {
1124 error() << "'" << identifier << "' is not declared, "
1125 << "missing type information required to construct call to "
1126 << "uninterpreted function" << eom;
1127 throw 0;
1128 }
1129
1130 const code_typet &function_call_type = to_code_type(function.type());
1132 for(const auto &parameter : function_call_type.parameters())
1133 domain.push_back(parameter.type());
1134 mathematical_function_typet function_type{
1135 domain, function_call_type.return_type()};
1137 symbol_exprt{function.identifier(), function_type}, arguments);
1138
1139 code_assignt assignment(lhs, rhs);
1140 assignment.add_source_location() = function.source_location();
1141 copy(assignment, ASSIGN, dest);
1142 }
1143 else if(identifier == CPROVER_PREFIX "array_equal")
1144 {
1145 do_array_op(ID_array_equal, lhs, function, arguments, dest);
1146 }
1147 else if(identifier == CPROVER_PREFIX "array_set")
1148 {
1149 do_array_op(ID_array_set, lhs, function, arguments, dest);
1150 }
1151 else if(identifier == CPROVER_PREFIX "array_copy")
1152 {
1153 do_array_op(ID_array_copy, lhs, function, arguments, dest);
1154 }
1155 else if(identifier == CPROVER_PREFIX "array_replace")
1156 {
1157 do_array_op(ID_array_replace, lhs, function, arguments, dest);
1158 }
1159 else if(
1160 identifier == "__assert_fail" || identifier == "_assert" ||
1161 identifier == "__assert_c99" || identifier == "_wassert")
1162 {
1163 // __assert_fail is Linux
1164 // These take four arguments:
1165 // "expression", "file.c", line, __func__
1166 // klibc has __assert_fail with 3 arguments
1167 // "expression", "file.c", line
1168
1169 // MingW has
1170 // void _assert (const char*, const char*, int);
1171 // with three arguments:
1172 // "expression", "file.c", line
1173
1174 // This has been seen in Solaris 11.
1175 // Signature:
1176 // void __assert_c99(
1177 // const char *desc, const char *file, int line, const char *func);
1178
1179 // _wassert is Windows. The arguments are
1180 // L"expression", L"file.c", line
1181
1182 if(arguments.size() != 4 && arguments.size() != 3)
1183 {
1185 error() << "'" << identifier << "' expected to have four arguments"
1186 << eom;
1187 throw 0;
1188 }
1189
1190 const irep_idt description =
1191 "assertion " + id2string(get_string_constant(arguments[0]));
1192
1194 annotated_location.set("user-provided", true);
1195 annotated_location.set_property_class(ID_assertion);
1196 annotated_location.set_comment(description);
1198 // we ignore any LHS
1199 }
1200 else if(identifier == "__assert_rtn" || identifier == "__assert")
1201 {
1202 // __assert_rtn has been seen on MacOS;
1203 // __assert is FreeBSD and Solaris 11.
1204 // These take four arguments:
1205 // __func__, "file.c", line, "expression"
1206 // On Solaris 11, it's three arguments:
1207 // "expression", "file", line
1208
1209 irep_idt description;
1210
1211 if(arguments.size() == 4)
1212 {
1213 description = "assertion " + id2string(get_string_constant(arguments[3]));
1214 }
1215 else if(arguments.size() == 3)
1216 {
1217 description = "assertion " + id2string(get_string_constant(arguments[1]));
1218 }
1219 else
1220 {
1222 error() << "'" << identifier << "' expected to have four arguments"
1223 << eom;
1224 throw 0;
1225 }
1226
1228 annotated_location.set("user-provided", true);
1229 annotated_location.set_property_class(ID_assertion);
1230 annotated_location.set_comment(description);
1232 // we ignore any LHS
1233 }
1234 else if(
1235 identifier == "__assert_func" || identifier == "__assert2" ||
1236 identifier == "__assert13")
1237 {
1238 // __assert_func is newlib (used by, e.g., cygwin)
1239 // __assert2 is OpenBSD
1240 // __assert13 is NetBSD
1241 // These take four arguments:
1242 // "file.c", line, __func__, "expression"
1243 if(arguments.size() != 4)
1244 {
1246 error() << "'" << identifier << "' expected to have four arguments"
1247 << eom;
1248 throw 0;
1249 }
1250
1251 irep_idt description;
1252 try
1253 {
1254 description = "assertion " + id2string(get_string_constant(arguments[3]));
1255 }
1256 catch(int)
1257 {
1258 // we might be building newlib, where __assert_func is passed
1259 // a pointer-typed symbol; the warning will still have been
1260 // printed
1261 description = "assertion";
1262 }
1263
1265 annotated_location.set("user-provided", true);
1266 annotated_location.set_property_class(ID_assertion);
1267 annotated_location.set_comment(description);
1269 // we ignore any LHS
1270 }
1271 else if(identifier == CPROVER_PREFIX "fence")
1272 {
1273 if(arguments.empty())
1274 {
1276 error() << "'" << identifier << "' expected to have at least one argument"
1277 << eom;
1278 throw 0;
1279 }
1280
1282
1283 for(const auto &argument : arguments)
1285
1287 }
1288 else if(identifier == "__builtin_prefetch")
1289 {
1290 // does nothing
1291 }
1292 else if(identifier == "__builtin_unreachable")
1293 {
1294 // says something like UNREACHABLE;
1295 }
1296 else if(identifier == ID_gcc_builtin_va_arg)
1297 {
1298 // This does two things.
1299 // 1) Return value of argument.
1300 // This is just dereferencing.
1301 // 2) Move list pointer to next argument.
1302 // This is just an increment.
1303
1304 if(arguments.size() != 1)
1305 {
1307 error() << "'" << identifier << "' expected to have one argument" << eom;
1308 throw 0;
1309 }
1310
1311 exprt list_arg = make_va_list(arguments[0], ns);
1312 const bool va_list_is_void_ptr =
1313 list_arg.type().id() == ID_pointer &&
1314 to_pointer_type(list_arg.type()).base_type().id() == ID_empty;
1315
1316 if(lhs.is_not_nil())
1317 {
1320 {
1323 }
1324
1325 typet t = pointer_type(lhs.type());
1328 rhs.add_source_location() = function.source_location();
1329 dest.add(
1330 goto_programt::make_assignment(lhs, rhs, function.source_location()));
1331 }
1332
1334 plus_exprt{
1337 : list_arg),
1339 list_arg.type());
1340 code_assignt assign{list_arg, std::move(list_arg_ptr_arithmetic)};
1341 assign.rhs().set(
1342 ID_C_va_arg_type, to_code_type(function.type()).return_type());
1344 std::move(assign), function.source_location()));
1345 }
1346 else if(identifier == "__builtin_va_copy")
1347 {
1348 if(arguments.size() != 2)
1349 {
1351 error() << "'" << identifier << "' expected to have two arguments" << eom;
1352 throw 0;
1353 }
1354
1355 exprt dest_expr = make_va_list(arguments[0], ns);
1356 const typecast_exprt src_expr(arguments[1], dest_expr.type());
1357
1359 {
1360 error().source_location = dest_expr.find_source_location();
1361 error() << "va_copy argument expected to be lvalue" << eom;
1362 throw 0;
1363 }
1364
1366 dest_expr, src_expr, function.source_location()));
1367 }
1368 else if(identifier == "__builtin_va_start" || identifier == "__va_start")
1369 {
1370 // Set the list argument to be the address of the
1371 // parameter argument.
1372 if(arguments.size() != 2)
1373 {
1375 error() << "'" << identifier << "' expected to have two arguments" << eom;
1376 throw 0;
1377 }
1378
1379 exprt dest_expr = make_va_list(arguments[0], ns);
1380
1382 {
1383 error().source_location = dest_expr.find_source_location();
1384 error() << "va_start argument expected to be lvalue" << eom;
1385 throw 0;
1386 }
1387
1388 if(
1389 dest_expr.type().id() == ID_pointer &&
1390 to_pointer_type(dest_expr.type()).base_type().id() == ID_empty)
1391 {
1392 dest_expr =
1394 }
1395
1397 ID_va_start, dest_expr.type(), function.source_location()};
1398 rhs.add_to_operands(
1399 typecast_exprt{address_of_exprt{arguments[1]}, dest_expr.type()});
1400
1402 std::move(dest_expr), std::move(rhs), function.source_location()));
1403 }
1404 else if(identifier == "__builtin_va_end")
1405 {
1406 // Invalidates the argument. We do so by setting it to NULL.
1407 if(arguments.size() != 1)
1408 {
1410 error() << "'" << identifier << "' expected to have one argument" << eom;
1411 throw 0;
1412 }
1413
1414 exprt dest_expr = make_va_list(arguments[0], ns);
1415
1417 {
1418 error().source_location = dest_expr.find_source_location();
1419 error() << "va_end argument expected to be lvalue" << eom;
1420 throw 0;
1421 }
1422
1423 // our __builtin_va_list is a pointer
1424 if(dest_expr.type().id() == ID_pointer)
1425 {
1426 const auto zero =
1427 zero_initializer(dest_expr.type(), function.source_location(), ns);
1428 CHECK_RETURN(zero.has_value());
1430 dest_expr, *zero, function.source_location()));
1431 }
1432 }
1433 else if(
1434 identifier == "__builtin_isgreater" ||
1435 identifier == "__builtin_isgreaterequal" ||
1436 identifier == "__builtin_isless" || identifier == "__builtin_islessequal" ||
1437 identifier == "__builtin_islessgreater" ||
1438 identifier == "__builtin_isunordered")
1439 {
1440 // these support two double or two float arguments; we call the
1441 // appropriate internal version
1442 if(
1443 arguments.size() != 2 ||
1444 (arguments[0].type() != double_type() &&
1445 arguments[0].type() != float_type()) ||
1446 (arguments[1].type() != double_type() &&
1447 arguments[1].type() != float_type()))
1448 {
1450 error() << "'" << identifier
1451 << "' expected to have two float/double arguments" << eom;
1452 throw 0;
1453 }
1454
1455 exprt::operandst new_arguments = arguments;
1456
1457 bool use_double = arguments[0].type() == double_type();
1458 if(arguments[0].type() != arguments[1].type())
1459 {
1460 if(use_double)
1461 {
1462 new_arguments[1] =
1463 typecast_exprt(new_arguments[1], arguments[0].type());
1464 }
1465 else
1466 {
1467 new_arguments[0] =
1468 typecast_exprt(new_arguments[0], arguments[1].type());
1469 use_double = true;
1470 }
1471 }
1472
1473 code_typet f_type = to_code_type(function.type());
1474 f_type.remove_ellipsis();
1475 const typet &a_t = new_arguments[0].type();
1476 f_type.parameters() =
1478
1479 // replace __builtin_ by CPROVER_PREFIX
1480 std::string name = CPROVER_PREFIX + id2string(identifier).substr(10);
1481 // append d or f for double/float
1482 name += use_double ? 'd' : 'f';
1483
1485 ns.lookup(name).type == f_type,
1486 "builtin declaration should match constructed type");
1487
1488 symbol_exprt new_function = function;
1489 new_function.identifier(name);
1490 new_function.type() = f_type;
1491
1492 code_function_callt function_call(lhs, new_function, new_arguments);
1493 function_call.add_source_location() = function.source_location();
1494
1495 copy(function_call, FUNCTION_CALL, dest);
1496 }
1497 else if(identifier == "alloca" || identifier == "__builtin_alloca")
1498 {
1499 do_alloca(lhs, function, arguments, dest, mode);
1500 }
1501 else
1502 {
1503 do_function_call_symbol(*symbol);
1504
1505 // insert function call
1506 // use symbol->symbol_expr() to ensure we use the type from the symbol table
1507 code_function_callt function_call(
1508 lhs, symbol->symbol_expr().with_source_location(function), arguments);
1509 function_call.add_source_location() = function.source_location();
1510
1511 // remove void-typed assignments, which may have been created when the
1512 // front-end was unable to detect them in type checking for a lack of
1513 // available declarations
1514 if(
1515 lhs.is_not_nil() &&
1516 to_code_type(symbol->type).return_type().id() == ID_empty)
1517 {
1518 function_call.lhs().make_nil();
1519 }
1520
1521 copy(function_call, FUNCTION_CALL, dest);
1522 }
1523}
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.
Definition arith_tools.cpp:21
static exprt make_va_list(const exprt &expr, const namespacet &ns)
floatbv_typet float_type()
Definition c_types.cpp:177
empty_typet void_type()
Definition c_types.cpp:245
signedbv_typet signed_int_type()
Definition c_types.cpp:22
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
signedbv_typet pointer_diff_type()
Definition c_types.cpp:220
bitvector_typet char_type()
Definition c_types.cpp:106
bitvector_typet c_index_type()
Definition c_types.cpp:16
floatbv_typet double_type()
Definition c_types.cpp:185
Operator to return the address of an object.
Definition pointer_expr.h:540
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Arrays with given size.
Definition std_types.h:806
The Boolean type.
Definition std_types.h:35
A goto_instruction_codet representing an assignment in the program.
goto_instruction_codet representation of a function call statement.
exprt & lhs()
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 ...
Definition std_types.h:599
Base type of functions.
Definition std_types.h:582
std::vector< parametert > parameterst
Definition std_types.h:585
Data structure for representing an arbitrary statement in a program.
Definition std_code_base.h:29
Operator to dereference a pointer.
Definition pointer_expr.h:834
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:107
The empty type.
Definition std_types.h:50
Equality.
Definition std_expr.h:1339
Base class for all expressions.
Definition expr.h:57
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:68
std::vector< exprt > operandst
Definition expr.h:59
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:164
typet & type()
Return the type of the expression.
Definition expr.h:85
operandst & operands()
Definition expr.h:95
const source_locationt & source_location() const
Definition expr.h:236
source_locationt & add_source_location()
Definition expr.h:241
The Boolean constant false.
Definition std_expr.h:3135
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 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)
namespacet ns
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)
clean_expr_resultt clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used=true)
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:72
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition goto_program.h:944
instructionst instructions
The list of instructions in the goto program.
Definition goto_program.h:621
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition goto_program.h:970
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition goto_program.h:721
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition goto_program.h:989
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
Definition goto_program.h:956
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition goto_program.h:978
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition goto_program.h:738
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition goto_program.h:963
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition goto_program.h:932
The trinary if-then-else operator.
Definition std_expr.h:2426
Array index operator.
Definition std_expr.h:1431
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
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:412
bool is_not_nil() const
Definition irep.h:372
void make_nil()
Definition irep.h:446
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
A type for mathematical functions (do not confuse with functions/methods in code)
std::vector< typet > domaint
Extract member of struct or union.
Definition std_expr.h:2866
source_locationt source_location
Definition message.h:239
mstreamt & error() const
Definition message.h:401
static eomt eom
Definition message.h:289
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition namespace.cpp:134
The null pointer constant.
Definition pointer_expr.h:909
The plus expression Associativity is not specified.
Definition std_expr.h:1006
A base class for a predicate that indicates that an address range is ok to read or write or both.
Definition pointer_expr.h:920
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
An expression containing a side effect.
Definition std_code.h:1450
const irep_idt & get_statement() const
Definition std_code.h:1472
Expression to hold a symbol (variable)
Definition std_expr.h:132
void identifier(const irep_idt &identifier)
Definition std_expr.h:160
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
Semantic type conversion.
Definition std_expr.h:1995
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2003
The type of an expression, extends irept.
Definition type.h:29
source_locationt & add_source_location()
Definition type.h:77
#define CPROVER_PREFIX
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
Definition destructor.cpp:62
Destructor Calls.
std::optional< 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:188
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)
std::optional< 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
Definition goto_program.h:48
@ ASSIGN
Definition goto_program.h:45
@ OTHER
Definition goto_program.h:36
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
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:577
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition pointer_expr.h:93
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:17
#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:1494
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2024
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:424
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3078
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:221
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:787
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition std_types.h:28
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:887
std::list< irep_idt > temporaries
Identifiers of temporaries introduced while cleaning an expression.
void add(clean_expr_resultt &&other)
void add_temporary(const irep_idt &id)
goto_programt side_effects
Statements implementing side effects of the expression that was subject to cleaning.
Symbol table entry.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208
#define size_type
Definition unistd.c:186

AltStyle によって変換されたページ (->オリジナル) /