cprover
Loading...
Searching...
No Matches
string_instrumentation.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: String Abstraction
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#include <algorithm>
15
16#include <util/arith_tools.h>
17#include <util/c_types.h>
18#include <util/config.h>
19#include <util/pointer_expr.h>
20#include <util/std_code.h>
22
26
27exprt is_zero_string(const exprt &what, bool write)
28{
29 unary_exprt result{"is_zero_string", what, c_bool_type()};
30 result.copy_to_operands(what);
31 result.set("lhs", write);
32 return notequal_exprt{result, from_integer(0, c_bool_type())};
33}
34
36 const exprt &what,
37 bool write)
38{
39 exprt result("zero_string_length", size_type());
40 result.copy_to_operands(what);
41 result.set("lhs", write);
42 return result;
43}
44
46{
47 exprt result("buffer_size", size_type());
48 result.copy_to_operands(what);
49 return result;
50}
51
53{
54public:
56 : symbol_table(_symbol_table), ns(_symbol_table)
57 {
58 }
59
60 void operator()(goto_programt &dest);
61 void operator()(goto_functionst &dest);
62
63protected:
66
67 void make_type(exprt &dest, const typet &type)
68 {
69 if(ns.follow(dest.type())!=ns.follow(type))
70 dest = typecast_exprt(dest, type);
71 }
72
75
76 // strings
77 void do_sprintf(
78 goto_programt &dest,
80 const exprt &lhs,
81 const exprt::operandst &arguments);
82 void do_snprintf(
83 goto_programt &dest,
85 const exprt &lhs,
86 const exprt::operandst &arguments);
88 goto_programt &dest,
90 const exprt &lhs,
91 const exprt::operandst &arguments);
92 void do_strncmp(
93 goto_programt &dest,
95 const exprt &lhs,
96 const exprt::operandst &arguments);
97 void do_strchr(
98 goto_programt &dest,
100 const exprt &lhs,
101 const exprt::operandst &arguments);
102 void do_strrchr(
103 goto_programt &dest,
105 const exprt &lhs,
106 const exprt::operandst &arguments);
107 void do_strstr(
108 goto_programt &dest,
110 const exprt &lhs,
111 const exprt::operandst &arguments);
112 void do_strtok(
113 goto_programt &dest,
115 const exprt &lhs,
116 const exprt::operandst &arguments);
117 void do_strerror(
118 goto_programt &dest,
120 const exprt &lhs,
121 const exprt::operandst &arguments);
122 void do_fscanf(
123 goto_programt &dest,
125 const exprt &lhs,
126 const exprt::operandst &arguments);
127
129 goto_programt &dest,
131 const code_function_callt::argumentst &arguments,
132 std::size_t format_string_inx,
133 std::size_t argument_start_inx,
134 const std::string &function_name);
135
137 goto_programt &dest,
139 const code_function_callt::argumentst &arguments,
140 std::size_t format_string_inx,
141 std::size_t argument_start_inx,
142 const std::string &function_name);
143
144 bool is_string_type(const typet &t) const
145 {
146 return (t.id() == ID_pointer || t.id() == ID_array) &&
147 (to_type_with_subtype(t).subtype().id() == ID_signedbv ||
148 to_type_with_subtype(t).subtype().id() == ID_unsignedbv) &&
151 }
152
154 goto_programt &dest,
156 const exprt &buffer,
157 const typet &buf_type,
158 const mp_integer &limit);
159};
160
168
176
178{
180 goto_model.symbol_table,
181 goto_model.goto_functions);
182}
183
185{
186 for(goto_functionst::function_mapt::iterator
187 it=dest.function_map.begin();
188 it!=dest.function_map.end();
189 it++)
190 {
191 (*this)(it->second.body);
192 }
193}
194
200
202 goto_programt &dest,
204{
205 if(it->is_function_call())
206 do_function_call(dest, it);
207}
208
210 goto_programt &dest,
212{
213 const exprt &lhs = as_const(*target).call_lhs();
214 const exprt &function = as_const(*target).call_function();
215 const auto &arguments = as_const(*target).call_arguments();
216
217 if(function.id()==ID_symbol)
218 {
219 const irep_idt &identifier=
220 to_symbol_expr(function).get_identifier();
221
222 if(identifier=="strcoll")
223 {
224 }
225 else if(identifier=="strncmp")
226 do_strncmp(dest, target, lhs, arguments);
227 else if(identifier=="strxfrm")
228 {
229 }
230 else if(identifier=="strchr")
231 do_strchr(dest, target, lhs, arguments);
232 else if(identifier=="strcspn")
233 {
234 }
235 else if(identifier=="strpbrk")
236 {
237 }
238 else if(identifier=="strrchr")
239 do_strrchr(dest, target, lhs, arguments);
240 else if(identifier=="strspn")
241 {
242 }
243 else if(identifier=="strerror")
244 do_strerror(dest, target, lhs, arguments);
245 else if(identifier=="strstr")
246 do_strstr(dest, target, lhs, arguments);
247 else if(identifier=="strtok")
248 do_strtok(dest, target, lhs, arguments);
249 else if(identifier=="sprintf")
250 do_sprintf(dest, target, lhs, arguments);
251 else if(identifier=="snprintf")
252 do_snprintf(dest, target, lhs, arguments);
253 else if(identifier == "fscanf" || identifier == "__isoc99_fscanf")
254 do_fscanf(dest, target, lhs, arguments);
255
256 remove_skip(dest);
257 }
258}
259
261 goto_programt &dest,
263 const exprt &lhs,
264 const exprt::operandst &arguments)
265{
266 if(arguments.size()<2)
267 {
269 "sprintf expected to have two or more arguments",
270 target->source_location());
271 }
272
273 goto_programt tmp;
274
275 // in the abstract model, we have to report a
276 // (possibly false) positive here
277 source_locationt annotated_location = target->source_location();
278 annotated_location.set_property_class("string");
279 annotated_location.set_comment("sprintf buffer overflow");
280 tmp.add(goto_programt::make_assertion(false_exprt(), annotated_location));
281
282 do_format_string_read(tmp, target, arguments, 1, 2, "sprintf");
283
284 if(lhs.is_not_nil())
285 {
286 exprt rhs = side_effect_expr_nondett(lhs.type(), target->source_location());
287
288 tmp.add(
289 goto_programt::make_assignment(lhs, rhs, target->source_location()));
290 }
291
292 target->turn_into_skip();
293 dest.insert_before_swap(target, tmp);
294}
295
297 goto_programt &dest,
299 const exprt &lhs,
300 const exprt::operandst &arguments)
301{
302 if(arguments.size()<3)
303 {
305 "snprintf expected to have three or more arguments",
306 target->source_location());
307 }
308
309 goto_programt tmp;
310
311 exprt bufsize = buffer_size(arguments[0]);
312
313 source_locationt annotated_location = target->source_location();
314 annotated_location.set_property_class("string");
315 annotated_location.set_comment("snprintf buffer overflow");
317 binary_relation_exprt(bufsize, ID_ge, arguments[1]), annotated_location));
318
319 do_format_string_read(tmp, target, arguments, 2, 3, "snprintf");
320
321 if(lhs.is_not_nil())
322 {
323 exprt rhs = side_effect_expr_nondett(lhs.type(), target->source_location());
324
325 tmp.add(
326 goto_programt::make_assignment(lhs, rhs, target->source_location()));
327 }
328
329 target->turn_into_skip();
330 dest.insert_before_swap(target, tmp);
331}
332
334 goto_programt &dest,
336 const exprt &lhs,
337 const exprt::operandst &arguments)
338{
339 if(arguments.size()<2)
340 {
342 "fscanf expected to have two or more arguments",
343 target->source_location());
344 }
345
346 goto_programt tmp;
347
348 do_format_string_write(tmp, target, arguments, 1, 2, "fscanf");
349
350 if(lhs.is_not_nil())
351 {
352 exprt rhs = side_effect_expr_nondett(lhs.type(), target->source_location());
353
354 tmp.add(
355 goto_programt::make_assignment(lhs, rhs, target->source_location()));
356 }
357
358 target->turn_into_skip();
359 dest.insert_before_swap(target, tmp);
360}
361
363 goto_programt &dest,
365 const code_function_callt::argumentst &arguments,
366 std::size_t format_string_inx,
367 std::size_t argument_start_inx,
368 const std::string &function_name)
369{
370 const exprt &format_arg=arguments[format_string_inx];
371
372 if(
373 format_arg.id() == ID_address_of &&
374 to_address_of_expr(format_arg).object().id() == ID_index &&
375 to_index_expr(to_address_of_expr(format_arg).object()).array().id() ==
376 ID_string_constant)
377 {
380 to_index_expr(to_address_of_expr(format_arg).object()).array())
381 .get_value()));
382
383 std::size_t args=0;
384
385 for(const auto &token : token_list)
386 {
388 {
389 const exprt &arg=arguments[argument_start_inx+args];
390
391 if(arg.id()!=ID_string_constant) // we don't need to check constants
392 {
393 exprt temp(arg);
394
395 if(arg.type().id() != ID_pointer)
396 {
397 index_exprt index(temp, from_integer(0, c_index_type()));
398 temp=address_of_exprt(index);
399 }
400
401 source_locationt annotated_location = target->source_location();
402 annotated_location.set_property_class("string");
403 std::string comment("zero-termination of string argument of ");
404 comment += function_name;
405 annotated_location.set_comment(comment);
407 is_zero_string(temp), annotated_location));
408 }
409 }
410
411 if(token.type!=format_tokent::token_typet::TEXT &&
412 token.type!=format_tokent::token_typet::UNKNOWN) args++;
413
414 if(find(
415 token.flags.begin(),
416 token.flags.end(),
418 token.flags.end())
419 args++; // just eat the additional argument
420 }
421 }
422 else // non-const format string
423 {
424 source_locationt annotated_location = target->source_location();
425 annotated_location.set_property_class("string");
426 annotated_location.set_comment(
427 "zero-termination of format string of " + function_name);
429 is_zero_string(arguments[1]), annotated_location));
430
431 for(std::size_t i=2; i<arguments.size(); i++)
432 {
433 const exprt &arg=arguments[i];
434
435 if(arguments[i].id() != ID_string_constant && is_string_type(arg.type()))
436 {
437 exprt temp(arg);
438
439 if(arg.type().id() != ID_pointer)
440 {
441 index_exprt index(temp, from_integer(0, c_index_type()));
442 temp=address_of_exprt(index);
443 }
444
445 source_locationt annotated_location = target->source_location();
446 annotated_location.set_property_class("string");
447 annotated_location.set_comment(
448 "zero-termination of string argument of " + function_name);
450 is_zero_string(temp), annotated_location));
451 }
452 }
453 }
454}
455
457 goto_programt &dest,
459 const code_function_callt::argumentst &arguments,
460 std::size_t format_string_inx,
461 std::size_t argument_start_inx,
462 const std::string &function_name)
463{
464 const exprt &format_arg=arguments[format_string_inx];
465
466 if(
467 format_arg.id() == ID_address_of &&
468 to_address_of_expr(format_arg).object().id() == ID_index &&
469 to_index_expr(to_address_of_expr(format_arg).object()).array().id() ==
470 ID_string_constant) // constant format
471 {
474 to_index_expr(to_address_of_expr(format_arg).object()).array())
475 .get_value()));
476
477 std::size_t args=0;
478
479 for(const auto &token : token_list)
480 {
481 if(find(
482 token.flags.begin(),
483 token.flags.end(),
485 token.flags.end())
486 continue; // asterisk means `ignore this'
487
488 switch(token.type)
489 {
491 {
492 const exprt &argument=arguments[argument_start_inx+args];
493 const typet &arg_type = argument.type();
494
495 exprt condition;
496
497 if(token.field_width!=0)
498 {
499 exprt fwidth=from_integer(token.field_width, unsigned_int_type());
501 const plus_exprt fw_1(fwidth, one); // +1 for 0-char
502
503 exprt fw_lt_bs;
504
505 if(arg_type.id()==ID_pointer)
506 fw_lt_bs=
507 binary_relation_exprt(fw_1, ID_le, buffer_size(argument));
508 else
509 {
510 const index_exprt index(
511 argument, from_integer(0, unsigned_int_type()));
512 address_of_exprt aof(index);
513 fw_lt_bs=binary_relation_exprt(fw_1, ID_le, buffer_size(aof));
514 }
515
516 condition = fw_lt_bs;
517 }
518 else
519 {
520 // this is a possible overflow.
521 condition = false_exprt();
522 }
523
524 source_locationt annotated_location = target->source_location();
525 annotated_location.set_property_class("string");
526 std::string comment("format string buffer overflow in ");
527 comment += function_name;
528 annotated_location.set_comment(comment);
529 dest.add(
530 goto_programt::make_assertion(condition, annotated_location));
531
532 // now kill the contents
534 dest, target, argument, arg_type, token.field_width);
535
536 args++;
537 break;
538 }
541 {
542 // nothing
543 break;
544 }
549 {
550 const exprt &argument=arguments[argument_start_inx+args];
551 const dereference_exprt lhs{argument};
552
553 side_effect_expr_nondett rhs(lhs.type(), target->source_location());
554
556 lhs, rhs, target->source_location()));
557
558 args++;
559 break;
560 }
561 }
562 }
563 }
564 else // non-const format string
565 {
566 for(std::size_t i=argument_start_inx; i<arguments.size(); i++)
567 {
568 const typet &arg_type = arguments[i].type();
569
570 // Note: is_string_type() is a `good guess' here. Actually
571 // any of the pointers could point into an array. But it
572 // would suck if we had to invalidate all variables.
573 // Luckily this case isn't needed too often.
574 if(is_string_type(arg_type))
575 {
576 // as we don't know any field width for the %s that
577 // should be here during runtime, we just report a
578 // possibly false positive
579 source_locationt annotated_location = target->source_location();
580 annotated_location.set_property_class("string");
581 std::string comment("format string buffer overflow in ");
582 comment += function_name;
583 annotated_location.set_comment(comment);
584 dest.add(
585 goto_programt::make_assertion(false_exprt(), annotated_location));
586
587 invalidate_buffer(dest, target, arguments[i], arg_type, 0);
588 }
589 else
590 {
591 dereference_exprt lhs{arguments[i]};
592
593 side_effect_expr_nondett rhs(lhs.type(), target->source_location());
594
595 dest.add(
596 goto_programt::make_assignment(lhs, rhs, target->source_location()));
597 }
598 }
599 }
600}
601
609
611 goto_programt &dest,
613 const exprt &lhs,
614 const exprt::operandst &arguments)
615{
616 if(arguments.size()!=2)
617 {
619 "strchr expected to have two arguments", target->source_location());
620 }
621
622 source_locationt annotated_location = target->source_location();
623 annotated_location.set_property_class("string");
624 annotated_location.set_comment(
625 "zero-termination of string argument of strchr");
627 is_zero_string(arguments[0]), annotated_location);
628
629 target->turn_into_skip();
630 dest.insert_before_swap(target, assertion);
631}
632
634 goto_programt &dest,
636 const exprt &lhs,
637 const exprt::operandst &arguments)
638{
639 if(arguments.size()!=2)
640 {
642 "strrchr expected to have two arguments", target->source_location());
643 }
644
645 source_locationt annotated_location = target->source_location();
646 annotated_location.set_property_class("string");
647 annotated_location.set_comment(
648 "zero-termination of string argument of strrchr");
650 is_zero_string(arguments[0]), annotated_location);
651
652 target->turn_into_skip();
653 dest.insert_before_swap(target, assertion);
654}
655
657 goto_programt &dest,
659 const exprt &lhs,
660 const exprt::operandst &arguments)
661{
662 if(arguments.size()!=2)
663 {
665 "strstr expected to have two arguments", target->source_location());
666 }
667
668 goto_programt tmp;
669
670 source_locationt annotated_location = target->source_location();
671 annotated_location.set_property_class("string");
672 annotated_location.set_comment(
673 "zero-termination of 1st string argument of strstr");
675 is_zero_string(arguments[0]), annotated_location));
676
677 annotated_location.set_property_class("string");
678 annotated_location.set_comment(
679 "zero-termination of 2nd string argument of strstr");
681 is_zero_string(arguments[1]), annotated_location));
682
683 target->turn_into_skip();
684 dest.insert_before_swap(target, tmp);
685}
686
688 goto_programt &dest,
690 const exprt &lhs,
691 const exprt::operandst &arguments)
692{
693 if(arguments.size()!=2)
694 {
696 "strtok expected to have two arguments", target->source_location());
697 }
698
699 goto_programt tmp;
700
701 source_locationt annotated_location = target->source_location();
702 annotated_location.set_property_class("string");
703 annotated_location.set_comment(
704 "zero-termination of 1st string argument of strtok");
706 is_zero_string(arguments[0]), annotated_location));
707
708 annotated_location.set_property_class("string");
709 annotated_location.set_comment(
710 "zero-termination of 2nd string argument of strtok");
712 is_zero_string(arguments[1]), annotated_location));
713
714 target->turn_into_skip();
715 dest.insert_before_swap(target, tmp);
716}
717
719 goto_programt &dest,
721 const exprt &lhs,
722 const exprt::operandst &arguments)
723{
724 if(lhs.is_nil())
725 {
726 it->turn_into_skip();
727 return;
728 }
729
730 irep_idt identifier_buf="__strerror_buffer";
731 irep_idt identifier_size="__strerror_buffer_size";
732
733 if(symbol_table.symbols.find(identifier_buf)==symbol_table.symbols.end())
734 {
735 symbolt new_symbol_size{identifier_size, size_type(), ID_C};
736 new_symbol_size.base_name = identifier_size;
737 new_symbol_size.pretty_name=new_symbol_size.base_name;
738 new_symbol_size.is_state_var=true;
739 new_symbol_size.is_lvalue=true;
740 new_symbol_size.is_static_lifetime=true;
741
742 array_typet type(char_type(), new_symbol_size.symbol_expr());
743 symbolt new_symbol_buf{identifier_buf, type, ID_C};
744 new_symbol_buf.is_state_var=true;
745 new_symbol_buf.is_lvalue=true;
746 new_symbol_buf.is_static_lifetime=true;
747 new_symbol_buf.base_name = identifier_buf;
748 new_symbol_buf.pretty_name=new_symbol_buf.base_name;
749
750 symbol_table.insert(std::move(new_symbol_buf));
751 symbol_table.insert(std::move(new_symbol_size));
752 }
753
754 const symbolt &symbol_size=ns.lookup(identifier_size);
755 const symbolt &symbol_buf=ns.lookup(identifier_buf);
756
757 goto_programt tmp;
758
759 {
760 exprt nondet_size =
761 side_effect_expr_nondett(size_type(), it->source_location());
763 code_assignt(symbol_size.symbol_expr(), nondet_size),
764 it->source_location()));
765
768 symbol_size.symbol_expr(),
769 ID_notequal,
770 from_integer(0, symbol_size.type)),
771 it->source_location()));
772 }
773
774 // return a pointer to some magic buffer
775 index_exprt index(
776 symbol_buf.symbol_expr(), from_integer(0, c_index_type()), char_type());
777
778 address_of_exprt ptr(index);
779
780 // make that zero-terminated
782 unary_exprt{"is_zero_string", ptr, c_bool_type()},
784 it->source_location()));
785
786 // assign address
787 {
788 exprt rhs=ptr;
789 make_type(rhs, lhs.type());
791 code_assignt(lhs, rhs), it->source_location()));
792 }
793
794 it->turn_into_skip();
795 dest.insert_before_swap(it, tmp);
796}
797
799 goto_programt &dest,
801 const exprt &buffer,
802 const typet &buf_type,
803 const mp_integer &limit)
804{
805 irep_idt cntr_id="string_instrumentation::$counter";
806
807 if(symbol_table.symbols.find(cntr_id)==symbol_table.symbols.end())
808 {
809 symbolt new_symbol{cntr_id, size_type(), ID_C};
810 new_symbol.base_name="$counter";
811 new_symbol.pretty_name=new_symbol.base_name;
812 new_symbol.is_state_var=true;
813 new_symbol.is_lvalue=true;
814 new_symbol.is_static_lifetime=true;
815
816 symbol_table.insert(std::move(new_symbol));
817 }
818
819 const symbolt &cntr_sym=ns.lookup(cntr_id);
820
821 // create a loop that runs over the buffer
822 // and invalidates every element
823
825 cntr_sym.symbol_expr(),
826 from_integer(0, cntr_sym.type),
827 target->source_location()));
828
829 exprt bufp;
830
831 if(buf_type.id()==ID_pointer)
832 bufp=buffer;
833 else
834 {
835 index_exprt index(
836 buffer,
838 to_type_with_subtype(buf_type).subtype());
839 bufp=address_of_exprt(index);
840 }
841
842 exprt condition;
843
844 if(limit==0)
845 condition =
846 binary_relation_exprt(cntr_sym.symbol_expr(), ID_ge, buffer_size(bufp));
847 else
848 condition = binary_relation_exprt(
849 cntr_sym.symbol_expr(), ID_gt, from_integer(limit, unsigned_int_type()));
850
851 goto_programt::targett check = dest.add(
852 goto_programt::make_incomplete_goto(condition, target->source_location()));
853
854 const plus_exprt b_plus_i(bufp, cntr_sym.symbol_expr());
855 const dereference_exprt deref(
856 b_plus_i, to_type_with_subtype(buf_type).subtype());
857
858 const side_effect_expr_nondett nondet(
859 to_type_with_subtype(buf_type).subtype(), target->source_location());
860
861 // invalidate
862 dest.add(
863 goto_programt::make_assignment(deref, nondet, target->source_location()));
864
865 const plus_exprt plus(
866 cntr_sym.symbol_expr(), from_integer(1, unsigned_int_type()));
867
869 cntr_sym.symbol_expr(), plus, target->source_location()));
870
871 dest.add(
872 goto_programt::make_goto(check, true_exprt(), target->source_location()));
873
875 dest.add(goto_programt::make_skip(target->source_location()));
876
877 check->complete_goto(exit);
878}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:41
unsignedbv_typet size_type()
Definition c_types.cpp:55
bitvector_typet char_type()
Definition c_types.cpp:111
typet c_bool_type()
Definition c_types.cpp:105
bitvector_typet c_index_type()
Definition c_types.cpp:16
Operator to return the address of an object.
Arrays with given size.
Definition std_types.h:763
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
std::size_t get_width() const
Definition std_types.h:876
A goto_instruction_codet representing an assignment in the program.
struct configt::ansi_ct ansi_c
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
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
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
The Boolean constant false.
Definition std_expr.h:3017
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
This class represents an instruction in the GOTO intermediate representation.
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())
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
instructionst::iterator targett
instructionst::const_iterator const_targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Array index operator.
Definition std_expr.h:1410
Thrown when we can't handle something in an input source file.
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:420
bool is_not_nil() const
Definition irep.h:380
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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().
Disequality.
Definition std_expr.h:1365
The plus expression Associativity is not specified.
Definition std_expr.h:947
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
void do_strtok(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
void do_function_call(goto_programt &dest, goto_programt::targett target)
bool is_string_type(const typet &t) const
void operator()(goto_programt &dest)
void do_snprintf(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
string_instrumentationt(symbol_table_baset &_symbol_table)
void do_format_string_read(goto_programt &dest, goto_programt::const_targett target, const code_function_callt::argumentst &arguments, std::size_t format_string_inx, std::size_t argument_start_inx, const std::string &function_name)
symbol_table_baset & symbol_table
void do_strncmp(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt::operandst &arguments)
void make_type(exprt &dest, const typet &type)
void do_sprintf(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
void do_strstr(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
void do_strerror(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt::operandst &arguments)
void do_format_string_write(goto_programt &dest, goto_programt::const_targett target, const code_function_callt::argumentst &arguments, std::size_t format_string_inx, std::size_t argument_start_inx, const std::string &function_name)
void do_fscanf(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
void instrument(goto_programt &dest, goto_programt::targett it)
void do_strcat(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt::operandst &arguments)
void do_strrchr(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
void invalidate_buffer(goto_programt &dest, goto_programt::const_targett target, const exprt &buffer, const typet &buf_type, const mp_integer &limit)
void do_strchr(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
const irep_idt & get_identifier() const
Definition std_expr.h:142
The symbol table base class interface.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
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
The Boolean constant true.
Definition std_expr.h:3008
const typet & subtype() const
Definition type.h:154
Semantic type conversion.
Definition std_expr.h:2017
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:314
format_token_listt parse_format_string(const std::string &arg_string)
Format String Parser.
std::list< format_tokent > format_token_listt
Symbol Table + CFG.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
BigInt mp_integer
Definition smt_terms.h:18
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const string_constantt & to_string_constant(const exprt &expr)
void string_instrumentation(symbol_table_baset &symbol_table, goto_programt &dest)
exprt buffer_size(const exprt &what)
exprt is_zero_string(const exprt &what, bool write)
exprt zero_string_length(const exprt &what, bool write)
String Abstraction.
std::size_t char_width
Definition config.h:137
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:175