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#include <util/symbol_table.h>
23
27
28exprt is_zero_string(const exprt &what, bool write)
29{
30 unary_exprt result{"is_zero_string", what, c_bool_type()};
31 result.copy_to_operands(what);
32 result.set("lhs", write);
33 return notequal_exprt{result, from_integer(0, c_bool_type())};
34}
35
37 const exprt &what,
38 bool write)
39{
40 exprt result("zero_string_length", size_type());
41 result.copy_to_operands(what);
42 result.set("lhs", write);
43 return result;
44}
45
47{
48 exprt result("buffer_size", size_type());
49 result.copy_to_operands(what);
50 return result;
51}
52
54{
55public:
60
63
64protected:
67
68 void make_type(exprt &dest, const typet &type)
69 {
70 if(ns.follow(dest.type())!=ns.follow(type))
71 dest = typecast_exprt(dest, type);
72 }
73
76
77 // strings
78 void do_sprintf(
81 const exprt &lhs,
82 const exprt::operandst &arguments);
83 void do_snprintf(
86 const exprt &lhs,
87 const exprt::operandst &arguments);
91 const exprt &lhs,
92 const exprt::operandst &arguments);
93 void do_strncmp(
96 const exprt &lhs,
97 const exprt::operandst &arguments);
98 void do_strchr(
101 const exprt &lhs,
102 const exprt::operandst &arguments);
103 void do_strrchr(
106 const exprt &lhs,
107 const exprt::operandst &arguments);
108 void do_strstr(
111 const exprt &lhs,
112 const exprt::operandst &arguments);
113 void do_strtok(
116 const exprt &lhs,
117 const exprt::operandst &arguments);
118 void do_strerror(
121 const exprt &lhs,
122 const exprt::operandst &arguments);
123 void do_fscanf(
126 const exprt &lhs,
127 const exprt::operandst &arguments);
128
132 const code_function_callt::argumentst &arguments,
133 std::size_t format_string_inx,
134 std::size_t argument_start_inx,
135 const std::string &function_name);
136
140 const code_function_callt::argumentst &arguments,
141 std::size_t format_string_inx,
142 std::size_t argument_start_inx,
143 const std::string &function_name);
144
145 bool is_string_type(const typet &t) const
146 {
147 return (t.id() == ID_pointer || t.id() == ID_array) &&
151 config.ansi_c.char_width);
152 }
153
157 const exprt &buffer,
158 const typet &buf_type,
159 const mp_integer &limit);
160};
161
169
177
179{
181 goto_model.symbol_table,
182 goto_model.goto_functions);
183}
184
186{
187 for(goto_functionst::function_mapt::iterator
188 it=dest.function_map.begin();
189 it!=dest.function_map.end();
190 it++)
191 {
192 (*this)(it->second.body);
193 }
194}
195
201
205{
206 if(it->is_function_call())
208}
209
213{
214 const exprt &lhs = as_const(*target).call_lhs();
215 const exprt &function = as_const(*target).call_function();
216 const auto &arguments = as_const(*target).call_arguments();
217
218 if(function.id()==ID_symbol)
219 {
220 const irep_idt &identifier=
221 to_symbol_expr(function).get_identifier();
222
223 if(identifier=="strcoll")
224 {
225 }
226 else if(identifier=="strncmp")
227 do_strncmp(dest, target, lhs, arguments);
228 else if(identifier=="strxfrm")
229 {
230 }
231 else if(identifier=="strchr")
232 do_strchr(dest, target, lhs, arguments);
233 else if(identifier=="strcspn")
234 {
235 }
236 else if(identifier=="strpbrk")
237 {
238 }
239 else if(identifier=="strrchr")
240 do_strrchr(dest, target, lhs, arguments);
241 else if(identifier=="strspn")
242 {
243 }
244 else if(identifier=="strerror")
245 do_strerror(dest, target, lhs, arguments);
246 else if(identifier=="strstr")
247 do_strstr(dest, target, lhs, arguments);
248 else if(identifier=="strtok")
249 do_strtok(dest, target, lhs, arguments);
250 else if(identifier=="sprintf")
251 do_sprintf(dest, target, lhs, arguments);
252 else if(identifier=="snprintf")
253 do_snprintf(dest, target, lhs, arguments);
254 else if(identifier=="fscanf")
255 do_fscanf(dest, target, lhs, arguments);
256
258 }
259}
260
264 const exprt &lhs,
265 const exprt::operandst &arguments)
266{
267 if(arguments.size()<2)
268 {
270 "sprintf expected to have two or more arguments",
271 target->source_location());
272 }
273
275
276 // in the abstract model, we have to report a
277 // (possibly false) positive here
278 goto_programt::targett assertion = tmp.add(
280 assertion->source_location_nonconst().set_property_class("string");
281 assertion->source_location_nonconst().set_comment("sprintf buffer overflow");
282
283 do_format_string_read(tmp, target, arguments, 1, 2, "sprintf");
284
285 if(lhs.is_not_nil())
286 {
287 exprt rhs = side_effect_expr_nondett(lhs.type(), target->source_location());
288
289 tmp.add(
291 }
292
293 target->turn_into_skip();
294 dest.insert_before_swap(target, tmp);
295}
296
300 const exprt &lhs,
301 const exprt::operandst &arguments)
302{
303 if(arguments.size()<3)
304 {
306 "snprintf expected to have three or more arguments",
307 target->source_location());
308 }
309
311
312 exprt bufsize = buffer_size(arguments[0]);
313
315 binary_relation_exprt(bufsize, ID_ge, arguments[1]),
316 target->source_location()));
317 assertion->source_location_nonconst().set_property_class("string");
318 assertion->source_location_nonconst().set_comment("snprintf buffer overflow");
319
320 do_format_string_read(tmp, target, arguments, 2, 3, "snprintf");
321
322 if(lhs.is_not_nil())
323 {
324 exprt rhs = side_effect_expr_nondett(lhs.type(), target->source_location());
325
326 tmp.add(
328 }
329
330 target->turn_into_skip();
331 dest.insert_before_swap(target, tmp);
332}
333
337 const exprt &lhs,
338 const exprt::operandst &arguments)
339{
340 if(arguments.size()<2)
341 {
343 "fscanf expected to have two or more arguments",
344 target->source_location());
345 }
346
348
349 do_format_string_write(tmp, target, arguments, 1, 2, "fscanf");
350
351 if(lhs.is_not_nil())
352 {
353 exprt rhs = side_effect_expr_nondett(lhs.type(), target->source_location());
354
355 tmp.add(
357 }
358
359 target->turn_into_skip();
360 dest.insert_before_swap(target, tmp);
361}
362
366 const code_function_callt::argumentst &arguments,
367 std::size_t format_string_inx,
368 std::size_t argument_start_inx,
369 const std::string &function_name)
370{
371 const exprt &format_arg=arguments[format_string_inx];
372
373 if(
374 format_arg.id() == ID_address_of &&
375 to_address_of_expr(format_arg).object().id() == ID_index &&
376 to_index_expr(to_address_of_expr(format_arg).object()).array().id() ==
378 {
382 .get_value()));
383
384 std::size_t args=0;
385
386 for(const auto &token : token_list)
387 {
389 {
390 const exprt &arg=arguments[argument_start_inx+args];
391
392 if(arg.id()!=ID_string_constant) // we don't need to check constants
393 {
394 exprt temp(arg);
395
396 if(arg.type().id() != ID_pointer)
397 {
399 temp=address_of_exprt(index);
400 }
401
402 goto_programt::targett assertion =
404 is_zero_string(temp), target->source_location()));
405 assertion->source_location_nonconst().set_property_class("string");
406 std::string comment("zero-termination of string argument of ");
407 comment += function_name;
408 assertion->source_location_nonconst().set_comment(comment);
409 }
410 }
411
412 if(token.type!=format_tokent::token_typet::TEXT &&
413 token.type!=format_tokent::token_typet::UNKNOWN) args++;
414
415 if(find(
416 token.flags.begin(),
417 token.flags.end(),
419 token.flags.end())
420 args++; // just eat the additional argument
421 }
422 }
423 else // non-const format string
424 {
426 is_zero_string(arguments[1]), target->source_location()));
427 format_ass->source_location_nonconst().set_property_class("string");
428 format_ass->source_location_nonconst().set_comment(
429 "zero-termination of format string of " + function_name);
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 {
442 temp=address_of_exprt(index);
443 }
444
445 goto_programt::targett assertion =
447 is_zero_string(temp), target->source_location()));
448 assertion->source_location_nonconst().set_property_class("string");
449 assertion->source_location_nonconst().set_comment(
450 "zero-termination of string argument of " + function_name);
451 }
452 }
453 }
454}
455
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 {
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
504
505 if(arg_type.id()==ID_pointer)
506 fw_lt_bs=
508 else
509 {
510 const index_exprt index(
512 address_of_exprt aof(index);
514 }
515
516 condition = fw_lt_bs;
517 }
518 else
519 {
520 // this is a possible overflow.
521 condition = false_exprt();
522 }
523
524 goto_programt::targett assertion =
526 condition, target->source_location()));
527 assertion->source_location_nonconst().set_property_class("string");
528 std::string comment("format string buffer overflow in ");
529 comment += function_name;
530 assertion->source_location_nonconst().set_comment(comment);
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.
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 goto_programt::targett assertion =
581 false_exprt(), target->source_location()));
582 assertion->source_location_nonconst().set_property_class("string");
583 std::string comment("format string buffer overflow in ");
584 comment += function_name;
585 assertion->source_location_nonconst().set_comment(comment);
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(
597 }
598 }
599 }
600}
601
609
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
623
625 is_zero_string(arguments[0]), target->source_location()));
626 assertion->source_location_nonconst().set_property_class("string");
627 assertion->source_location_nonconst().set_comment(
628 "zero-termination of string argument of strchr");
629
630 target->turn_into_skip();
631 dest.insert_before_swap(target, tmp);
632}
633
637 const exprt &lhs,
638 const exprt::operandst &arguments)
639{
640 if(arguments.size()!=2)
641 {
643 "strrchr expected to have two arguments", target->source_location());
644 }
645
647
649 is_zero_string(arguments[0]), target->source_location()));
650 assertion->source_location_nonconst().set_property_class("string");
651 assertion->source_location_nonconst().set_comment(
652 "zero-termination of string argument of strrchr");
653
654 target->turn_into_skip();
655 dest.insert_before_swap(target, tmp);
656}
657
661 const exprt &lhs,
662 const exprt::operandst &arguments)
663{
664 if(arguments.size()!=2)
665 {
667 "strstr expected to have two arguments", target->source_location());
668 }
669
671
673 is_zero_string(arguments[0]), target->source_location()));
674 assertion0->source_location_nonconst().set_property_class("string");
675 assertion0->source_location_nonconst().set_comment(
676 "zero-termination of 1st string argument of strstr");
677
679 is_zero_string(arguments[1]), target->source_location()));
680 assertion1->source_location_nonconst().set_property_class("string");
681 assertion1->source_location_nonconst().set_comment(
682 "zero-termination of 2nd string argument of strstr");
683
684 target->turn_into_skip();
685 dest.insert_before_swap(target, tmp);
686}
687
691 const exprt &lhs,
692 const exprt::operandst &arguments)
693{
694 if(arguments.size()!=2)
695 {
697 "strtok expected to have two arguments", target->source_location());
698 }
699
701
703 is_zero_string(arguments[0]), target->source_location()));
704 assertion0->source_location_nonconst().set_property_class("string");
705 assertion0->source_location_nonconst().set_comment(
706 "zero-termination of 1st string argument of strtok");
707
709 is_zero_string(arguments[1]), target->source_location()));
710 assertion1->source_location_nonconst().set_property_class("string");
711 assertion1->source_location_nonconst().set_comment(
712 "zero-termination of 2nd string argument of strtok");
713
714 target->turn_into_skip();
715 dest.insert_before_swap(target, tmp);
716}
717
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
734 {
736 new_symbol_size.base_name="__strerror_buffer_size";
737 new_symbol_size.pretty_name=new_symbol_size.base_name;
741 new_symbol_size.is_state_var=true;
742 new_symbol_size.is_lvalue=true;
743 new_symbol_size.is_static_lifetime=true;
744
745 array_typet type(char_type(), new_symbol_size.symbol_expr());
747 new_symbol_buf.mode=ID_C;
748 new_symbol_buf.type=type;
749 new_symbol_buf.is_state_var=true;
750 new_symbol_buf.is_lvalue=true;
751 new_symbol_buf.is_static_lifetime=true;
752 new_symbol_buf.base_name="__strerror_buffer";
753 new_symbol_buf.pretty_name=new_symbol_buf.base_name;
754 new_symbol_buf.name=new_symbol_buf.base_name;
755
758 }
759
762
764
765 {
769 code_assignt(symbol_size.symbol_expr(), nondet_size),
770 it->source_location()));
771
774 symbol_size.symbol_expr(),
776 from_integer(0, symbol_size.type)),
777 it->source_location()));
778 }
779
780 // return a pointer to some magic buffer
781 index_exprt index(
782 symbol_buf.symbol_expr(), from_integer(0, c_index_type()), char_type());
783
784 address_of_exprt ptr(index);
785
786 // make that zero-terminated
788 unary_exprt{"is_zero_string", ptr, c_bool_type()},
790 it->source_location()));
791
792 // assign address
793 {
794 exprt rhs=ptr;
795 make_type(rhs, lhs.type());
797 code_assignt(lhs, rhs), it->source_location()));
798 }
799
800 it->turn_into_skip();
801 dest.insert_before_swap(it, tmp);
802}
803
807 const exprt &buffer,
808 const typet &buf_type,
809 const mp_integer &limit)
810{
811 irep_idt cntr_id="string_instrumentation::$counter";
812
814 {
815 symbolt new_symbol;
816 new_symbol.base_name="$counter";
817 new_symbol.pretty_name=new_symbol.base_name;
818 new_symbol.name=cntr_id;
819 new_symbol.mode=ID_C;
820 new_symbol.type=size_type();
821 new_symbol.is_state_var=true;
822 new_symbol.is_lvalue=true;
823 new_symbol.is_static_lifetime=true;
824
825 symbol_table.insert(std::move(new_symbol));
826 }
827
829
830 // create a loop that runs over the buffer
831 // and invalidates every element
832
834 cntr_sym.symbol_expr(),
835 from_integer(0, cntr_sym.type),
836 target->source_location()));
837
838 exprt bufp;
839
840 if(buf_type.id()==ID_pointer)
841 bufp=buffer;
842 else
843 {
844 index_exprt index(
845 buffer,
847 to_type_with_subtype(buf_type).subtype());
848 bufp=address_of_exprt(index);
849 }
850
851 exprt condition;
852
853 if(limit==0)
854 condition =
856 else
857 condition = binary_relation_exprt(
859
860 goto_programt::targett check = dest.add(
862
864 static_cast<const codet &>(get_nil_irep()),
865 target->source_location(),
866 ASSIGN,
867 nil_exprt(),
868 {}));
869
870 const plus_exprt plus(
871 cntr_sym.symbol_expr(), from_integer(1, unsigned_int_type()));
872
874 cntr_sym.symbol_expr(), plus, target->source_location()));
875
876 dest.add(
878
880 dest.add(goto_programt::make_skip(target->source_location()));
881
882 check->complete_goto(exit);
883
884 const plus_exprt b_plus_i(bufp, cntr_sym.symbol_expr());
885 const dereference_exprt deref(b_plus_i, buf_type.subtype());
886
888 buf_type.subtype(), target->source_location());
889
890 invalidate->code_nonconst() = code_assignt(deref, nondet);
891}
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:54
unsignedbv_typet size_type()
Definition c_types.cpp:68
bitvector_typet char_type()
Definition c_types.cpp:124
typet c_bool_type()
Definition c_types.cpp:118
bitvector_typet c_index_type()
Definition c_types.cpp:16
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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:674
std::size_t get_width() const
Definition std_types.h:864
A codet representing an assignment in the program.
Data structure for representing an arbitrary statement in a 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:37
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:129
typet & type()
Return the type of the expression.
Definition expr.h:82
const source_locationt & source_location() const
Definition expr.h:230
The Boolean constant false.
Definition std_expr.h:2865
A collection of goto functions.
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
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())
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())
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:1328
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().
The NIL expression.
Definition std_expr.h:2874
Disequality.
Definition std_expr.h:1283
The plus expression Associativity is not specified.
Definition std_expr.h:914
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
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)
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)
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)
string_instrumentationt(symbol_tablet &_symbol_table)
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:109
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition symbol.h:28
bool is_static_lifetime
Definition symbol.h:65
bool is_state_var
Definition symbol.h:62
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition symbol.h:52
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
bool is_lvalue
Definition symbol.h:66
irep_idt mode
Language mode.
Definition symbol.h:49
The Boolean constant true.
Definition std_expr.h:2856
const typet & subtype() const
Definition type.h:156
Semantic type conversion.
Definition std_expr.h:1920
The type of an expression, extends irept.
Definition type.h:29
const source_locationt & source_location() const
Definition type.h:74
Generic base class for unary expressions.
Definition std_expr.h:281
configt config
Definition config.cpp:25
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)
@ ASSIGN
const irept & get_nil_irep()
Definition irep.cpp:20
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.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1391
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189
const string_constantt & to_string_constant(const exprt &expr)
exprt buffer_size(const exprt &what)
exprt is_zero_string(const exprt &what, bool write)
void string_instrumentation(symbol_tablet &symbol_table, goto_programt &dest)
exprt zero_string_length(const exprt &what, bool write)
String Abstraction.
Author: Diffblue Ltd.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:177