cprover
string_instrumentation.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String Abstraction
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "string_instrumentation.h"
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/invariant.h>
20 #include <util/pointer_expr.h>
21 #include <util/std_code.h>
22 #include <util/std_expr.h>
23 #include <util/string_constant.h>
24 #include <util/symbol_table.h>
25 
29 
30 predicate_exprt is_zero_string(const exprt &what, bool write)
31 {
32  predicate_exprt result("is_zero_string");
33  result.copy_to_operands(what);
34  result.set("lhs", write);
35  return result;
36 }
37 
39  const exprt &what,
40  bool write)
41 {
42  exprt result("zero_string_length", size_type());
43  result.copy_to_operands(what);
44  result.set("lhs", write);
45  return result;
46 }
47 
48 exprt buffer_size(const exprt &what)
49 {
50  exprt result("buffer_size", size_type());
51  result.copy_to_operands(what);
52  return result;
53 }
54 
56 {
57 public:
58  explicit string_instrumentationt(symbol_tablet &_symbol_table)
59  : symbol_table(_symbol_table), ns(_symbol_table)
60  {
61  }
62 
63  void operator()(goto_programt &dest);
64  void operator()(goto_functionst &dest);
65 
66 protected:
69 
70  void make_type(exprt &dest, const typet &type)
71  {
72  if(ns.follow(dest.type())!=ns.follow(type))
73  dest = typecast_exprt(dest, type);
74  }
75 
78 
79  // strings
80  void do_sprintf(
81  goto_programt &dest,
83  const code_function_callt &);
84  void do_snprintf(
85  goto_programt &dest,
87  const code_function_callt &);
88  void do_strcat(
89  goto_programt &dest,
91  const code_function_callt &);
92  void do_strncmp(
93  goto_programt &dest,
95  const code_function_callt &);
96  void do_strchr(
97  goto_programt &dest,
99  const code_function_callt &);
100  void do_strrchr(
101  goto_programt &dest,
102  goto_programt::targett target,
103  const code_function_callt &);
104  void do_strstr(
105  goto_programt &dest,
106  goto_programt::targett target,
107  const code_function_callt &);
108  void do_strtok(
109  goto_programt &dest,
110  goto_programt::targett target,
111  const code_function_callt &);
112  void do_strerror(
113  goto_programt &dest,
115  const code_function_callt &);
116  void do_fscanf(
117  goto_programt &dest,
118  goto_programt::targett target,
119  const code_function_callt &);
120 
122  goto_programt &dest,
124  const code_function_callt::argumentst &arguments,
125  std::size_t format_string_inx,
126  std::size_t argument_start_inx,
127  const std::string &function_name);
128 
130  goto_programt &dest,
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 
137  bool is_string_type(const typet &t) const
138  {
139  return
140  (t.id()==ID_pointer || t.id()==ID_array) &&
141  (t.subtype().id()==ID_signedbv || t.subtype().id()==ID_unsignedbv) &&
143  }
144 
145  void invalidate_buffer(
146  goto_programt &dest,
148  const exprt &buffer,
149  const typet &buf_type,
150  const mp_integer &limit);
151 };
152 
154  symbol_tablet &symbol_table,
155  goto_programt &dest)
156 {
159 }
160 
162  symbol_tablet &symbol_table,
163  goto_functionst &dest)
164 {
167 }
168 
170 {
172  goto_model.symbol_table,
173  goto_model.goto_functions);
174 }
175 
177 {
178  for(goto_functionst::function_mapt::iterator
179  it=dest.function_map.begin();
180  it!=dest.function_map.end();
181  it++)
182  {
183  (*this)(it->second.body);
184  }
185 }
186 
188 {
190  instrument(dest, it);
191 }
192 
194  goto_programt &dest,
196 {
197  if(it->is_function_call())
198  do_function_call(dest, it);
199 }
200 
202  goto_programt &dest,
203  goto_programt::targett target)
204 {
205  const code_function_callt &call = target->get_function_call();
206  const exprt &function = call.function();
207  // const exprt &lhs=call.lhs();
208 
209  if(function.id()==ID_symbol)
210  {
211  const irep_idt &identifier=
212  to_symbol_expr(function).get_identifier();
213 
214  if(identifier=="strcoll")
215  {
216  }
217  else if(identifier=="strncmp")
218  do_strncmp(dest, target, call);
219  else if(identifier=="strxfrm")
220  {
221  }
222  else if(identifier=="strchr")
223  do_strchr(dest, target, call);
224  else if(identifier=="strcspn")
225  {
226  }
227  else if(identifier=="strpbrk")
228  {
229  }
230  else if(identifier=="strrchr")
231  do_strrchr(dest, target, call);
232  else if(identifier=="strspn")
233  {
234  }
235  else if(identifier=="strerror")
236  do_strerror(dest, target, call);
237  else if(identifier=="strstr")
238  do_strstr(dest, target, call);
239  else if(identifier=="strtok")
240  do_strtok(dest, target, call);
241  else if(identifier=="sprintf")
242  do_sprintf(dest, target, call);
243  else if(identifier=="snprintf")
244  do_snprintf(dest, target, call);
245  else if(identifier=="fscanf")
246  do_fscanf(dest, target, call);
247 
248  remove_skip(dest);
249  }
250 }
251 
253  goto_programt &dest,
254  goto_programt::targett target,
255  const code_function_callt &call)
256 {
257  const code_function_callt::argumentst &arguments=call.arguments();
258 
259  if(arguments.size()<2)
260  {
262  "sprintf expected to have two or more arguments",
263  target->source_location);
264  }
265 
266  goto_programt tmp;
267 
268  // in the abstract model, we have to report a
269  // (possibly false) positive here
270  goto_programt::targett assertion = tmp.add(
272  assertion->source_location.set_property_class("string");
273  assertion->source_location.set_comment("sprintf buffer overflow");
274 
275  do_format_string_read(tmp, target, arguments, 1, 2, "sprintf");
276 
277  if(call.lhs().is_not_nil())
278  {
279  exprt rhs =
281 
282  tmp.add(
283  goto_programt::make_assignment(call.lhs(), rhs, target->source_location));
284  }
285 
286  target->turn_into_skip();
287  dest.insert_before_swap(target, tmp);
288 }
289 
291  goto_programt &dest,
292  goto_programt::targett target,
293  const code_function_callt &call)
294 {
295  const code_function_callt::argumentst &arguments=call.arguments();
296 
297  if(arguments.size()<3)
298  {
300  "snprintf expected to have three or more arguments",
301  target->source_location);
302  }
303 
304  goto_programt tmp;
305 
306  exprt bufsize = buffer_size(arguments[0]);
307 
309  binary_relation_exprt(bufsize, ID_ge, arguments[1]),
310  target->source_location));
311  assertion->source_location.set_property_class("string");
312  assertion->source_location.set_comment("snprintf buffer overflow");
313 
314  do_format_string_read(tmp, target, arguments, 2, 3, "snprintf");
315 
316  if(call.lhs().is_not_nil())
317  {
318  exprt rhs =
320 
321  tmp.add(
322  goto_programt::make_assignment(call.lhs(), rhs, target->source_location));
323  }
324 
325  target->turn_into_skip();
326  dest.insert_before_swap(target, tmp);
327 }
328 
330  goto_programt &dest,
331  goto_programt::targett target,
332  const code_function_callt &call)
333 {
334  const code_function_callt::argumentst &arguments=call.arguments();
335 
336  if(arguments.size()<2)
337  {
339  "fscanf expected to have two or more arguments", target->source_location);
340  }
341 
342  goto_programt tmp;
343 
344  do_format_string_write(tmp, target, arguments, 1, 2, "fscanf");
345 
346  if(call.lhs().is_not_nil())
347  {
348  exprt rhs =
350 
351  tmp.add(
352  goto_programt::make_assignment(call.lhs(), rhs, target->source_location));
353  }
354 
355  target->turn_into_skip();
356  dest.insert_before_swap(target, tmp);
357 }
358 
360  goto_programt &dest,
362  const code_function_callt::argumentst &arguments,
363  std::size_t format_string_inx,
364  std::size_t argument_start_inx,
365  const std::string &function_name)
366 {
367  const exprt &format_arg=arguments[format_string_inx];
368 
369  if(
370  format_arg.id() == ID_address_of &&
371  to_address_of_expr(format_arg).object().id() == ID_index &&
372  to_index_expr(to_address_of_expr(format_arg).object()).array().id() ==
373  ID_string_constant)
374  {
377  to_index_expr(to_address_of_expr(format_arg).object()).array())
378  .get_value()));
379 
380  std::size_t args=0;
381 
382  for(const auto &token : token_list)
383  {
384  if(token.type==format_tokent::token_typet::STRING)
385  {
386  const exprt &arg=arguments[argument_start_inx+args];
387 
388  if(arg.id()!=ID_string_constant) // we don't need to check constants
389  {
390  exprt temp(arg);
391 
392  if(arg.type().id() != ID_pointer)
393  {
394  index_exprt index(temp, from_integer(0, index_type()));
395  temp=address_of_exprt(index);
396  }
397 
398  goto_programt::targett assertion =
400  is_zero_string(temp), target->source_location));
401  assertion->source_location.set_property_class("string");
402  std::string comment("zero-termination of string argument of ");
403  comment += function_name;
404  assertion->source_location.set_comment(comment);
405  }
406  }
407 
408  if(token.type!=format_tokent::token_typet::TEXT &&
409  token.type!=format_tokent::token_typet::UNKNOWN) args++;
410 
411  if(find(
412  token.flags.begin(),
413  token.flags.end(),
415  token.flags.end())
416  args++; // just eat the additional argument
417  }
418  }
419  else // non-const format string
420  {
422  is_zero_string(arguments[1]), target->source_location));
423  format_ass->source_location.set_property_class("string");
424  format_ass->source_location.set_comment(
425  "zero-termination of format string of " + function_name);
426 
427  for(std::size_t i=2; i<arguments.size(); i++)
428  {
429  const exprt &arg=arguments[i];
430 
431  if(arguments[i].id() != ID_string_constant && is_string_type(arg.type()))
432  {
433  exprt temp(arg);
434 
435  if(arg.type().id() != ID_pointer)
436  {
437  index_exprt index(temp, from_integer(0, index_type()));
438  temp=address_of_exprt(index);
439  }
440 
441  goto_programt::targett assertion =
443  is_zero_string(temp), target->source_location));
444  assertion->source_location.set_property_class("string");
445  assertion->source_location.set_comment(
446  "zero-termination of string argument of " + function_name);
447  }
448  }
449  }
450 }
451 
453  goto_programt &dest,
455  const code_function_callt::argumentst &arguments,
456  std::size_t format_string_inx,
457  std::size_t argument_start_inx,
458  const std::string &function_name)
459 {
460  const exprt &format_arg=arguments[format_string_inx];
461 
462  if(
463  format_arg.id() == ID_address_of &&
464  to_address_of_expr(format_arg).object().id() == ID_index &&
465  to_index_expr(to_address_of_expr(format_arg).object()).array().id() ==
466  ID_string_constant) // constant format
467  {
470  to_index_expr(to_address_of_expr(format_arg).object()).array())
471  .get_value()));
472 
473  std::size_t args=0;
474 
475  for(const auto &token : token_list)
476  {
477  if(find(
478  token.flags.begin(),
479  token.flags.end(),
481  token.flags.end())
482  continue; // asterisk means `ignore this'
483 
484  switch(token.type)
485  {
487  {
488  const exprt &argument=arguments[argument_start_inx+args];
489  const typet &arg_type = argument.type();
490 
491  exprt condition;
492 
493  if(token.field_width!=0)
494  {
495  exprt fwidth=from_integer(token.field_width, unsigned_int_type());
497  const plus_exprt fw_1(fwidth, one); // +1 for 0-char
498 
499  exprt fw_lt_bs;
500 
501  if(arg_type.id()==ID_pointer)
502  fw_lt_bs=
503  binary_relation_exprt(fw_1, ID_le, buffer_size(argument));
504  else
505  {
506  const index_exprt index(
507  argument, from_integer(0, unsigned_int_type()));
508  address_of_exprt aof(index);
509  fw_lt_bs=binary_relation_exprt(fw_1, ID_le, buffer_size(aof));
510  }
511 
512  condition = fw_lt_bs;
513  }
514  else
515  {
516  // this is a possible overflow.
517  condition = false_exprt();
518  }
519 
520  goto_programt::targett assertion = dest.add(
521  goto_programt::make_assertion(condition, target->source_location));
522  assertion->source_location.set_property_class("string");
523  std::string comment("format string buffer overflow in ");
524  comment += function_name;
525  assertion->source_location.set_comment(comment);
526 
527  // now kill the contents
529  dest, target, argument, arg_type, token.field_width);
530 
531  args++;
532  break;
533  }
536  {
537  // nothing
538  break;
539  }
544  {
545  const exprt &argument=arguments[argument_start_inx+args];
546  const dereference_exprt lhs{argument};
547 
548  side_effect_expr_nondett rhs(lhs.type(), target->source_location);
549 
550  dest.add(
552 
553  args++;
554  break;
555  }
556  }
557  }
558  }
559  else // non-const format string
560  {
561  for(std::size_t i=argument_start_inx; i<arguments.size(); i++)
562  {
563  const typet &arg_type = arguments[i].type();
564 
565  // Note: is_string_type() is a `good guess' here. Actually
566  // any of the pointers could point into an array. But it
567  // would suck if we had to invalidate all variables.
568  // Luckily this case isn't needed too often.
569  if(is_string_type(arg_type))
570  {
571  // as we don't know any field width for the %s that
572  // should be here during runtime, we just report a
573  // possibly false positive
574  goto_programt::targett assertion =
576  false_exprt(), target->source_location));
577  assertion->source_location.set_property_class("string");
578  std::string comment("format string buffer overflow in ");
579  comment += function_name;
580  assertion->source_location.set_comment(comment);
581 
582  invalidate_buffer(dest, target, arguments[i], arg_type, 0);
583  }
584  else
585  {
586  dereference_exprt lhs{arguments[i]};
587 
588  side_effect_expr_nondett rhs(lhs.type(), target->source_location);
589 
590  dest.add(
592  }
593  }
594  }
595 }
596 
598  goto_programt &,
600  const code_function_callt &)
601 {
602 }
603 
605  goto_programt &dest,
606  goto_programt::targett target,
607  const code_function_callt &call)
608 {
609  const code_function_callt::argumentst &arguments=call.arguments();
610 
611  if(arguments.size()!=2)
612  {
614  "strchr expected to have two arguments", target->source_location);
615  }
616 
617  goto_programt tmp;
618 
620  is_zero_string(arguments[0]), target->source_location));
621  assertion->source_location.set_property_class("string");
622  assertion->source_location.set_comment(
623  "zero-termination of string argument of strchr");
624 
625  target->turn_into_skip();
626  dest.insert_before_swap(target, tmp);
627 }
628 
630  goto_programt &dest,
631  goto_programt::targett target,
632  const code_function_callt &call)
633 {
634  const code_function_callt::argumentst &arguments=call.arguments();
635 
636  if(arguments.size()!=2)
637  {
639  "strrchr expected to have two arguments", target->source_location);
640  }
641 
642  goto_programt tmp;
643 
645  is_zero_string(arguments[0]), target->source_location));
646  assertion->source_location.set_property_class("string");
647  assertion->source_location.set_comment(
648  "zero-termination of string argument of strrchr");
649 
650  target->turn_into_skip();
651  dest.insert_before_swap(target, tmp);
652 }
653 
655  goto_programt &dest,
656  goto_programt::targett target,
657  const code_function_callt &call)
658 {
659  const code_function_callt::argumentst &arguments=call.arguments();
660 
661  if(arguments.size()!=2)
662  {
664  "strstr expected to have two arguments", target->source_location);
665  }
666 
667  goto_programt tmp;
668 
670  is_zero_string(arguments[0]), target->source_location));
671  assertion0->source_location.set_property_class("string");
672  assertion0->source_location.set_comment(
673  "zero-termination of 1st string argument of strstr");
674 
676  is_zero_string(arguments[1]), target->source_location));
677  assertion1->source_location.set_property_class("string");
678  assertion1->source_location.set_comment(
679  "zero-termination of 2nd string argument of strstr");
680 
681  target->turn_into_skip();
682  dest.insert_before_swap(target, tmp);
683 }
684 
686  goto_programt &dest,
687  goto_programt::targett target,
688  const code_function_callt &call)
689 {
690  const code_function_callt::argumentst &arguments=call.arguments();
691 
692  if(arguments.size()!=2)
693  {
695  "strtok expected to have two arguments", target->source_location);
696  }
697 
698  goto_programt tmp;
699 
701  is_zero_string(arguments[0]), target->source_location));
702  assertion0->source_location.set_property_class("string");
703  assertion0->source_location.set_comment(
704  "zero-termination of 1st string argument of strtok");
705 
707  is_zero_string(arguments[1]), target->source_location));
708  assertion1->source_location.set_property_class("string");
709  assertion1->source_location.set_comment(
710  "zero-termination of 2nd string argument of strtok");
711 
712  target->turn_into_skip();
713  dest.insert_before_swap(target, tmp);
714 }
715 
717  goto_programt &dest,
719  const code_function_callt &call)
720 {
721  if(call.lhs().is_nil())
722  {
723  it->turn_into_skip();
724  return;
725  }
726 
727  irep_idt identifier_buf="__strerror_buffer";
728  irep_idt identifier_size="__strerror_buffer_size";
729 
730  if(symbol_table.symbols.find(identifier_buf)==symbol_table.symbols.end())
731  {
732  symbolt new_symbol_size;
733  new_symbol_size.base_name="__strerror_buffer_size";
734  new_symbol_size.pretty_name=new_symbol_size.base_name;
735  new_symbol_size.name=identifier_size;
736  new_symbol_size.mode=ID_C;
737  new_symbol_size.type=size_type();
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;
744  new_symbol_buf.mode=ID_C;
745  new_symbol_buf.type=type;
746  new_symbol_buf.is_state_var=true;
747  new_symbol_buf.is_lvalue=true;
748  new_symbol_buf.is_static_lifetime=true;
749  new_symbol_buf.base_name="__strerror_buffer";
750  new_symbol_buf.pretty_name=new_symbol_buf.base_name;
751  new_symbol_buf.name=new_symbol_buf.base_name;
752 
753  symbol_table.insert(std::move(new_symbol_buf));
754  symbol_table.insert(std::move(new_symbol_size));
755  }
756 
757  const symbolt &symbol_size=ns.lookup(identifier_size);
758  const symbolt &symbol_buf=ns.lookup(identifier_buf);
759 
760  goto_programt tmp;
761 
762  {
763  exprt nondet_size =
766  code_assignt(symbol_size.symbol_expr(), nondet_size),
767  it->source_location));
768 
771  symbol_size.symbol_expr(),
772  ID_notequal,
773  from_integer(0, symbol_size.type)),
774  it->source_location));
775  }
776 
777  // return a pointer to some magic buffer
778  index_exprt index(
779  symbol_buf.symbol_expr(),
780  from_integer(0, index_type()),
781  char_type());
782 
783  address_of_exprt ptr(index);
784 
785  // make that zero-terminated
787  is_zero_string(ptr, true), true_exprt(), it->source_location));
788 
789  // assign address
790  {
791  exprt rhs=ptr;
792  make_type(rhs, call.lhs().type());
794  code_assignt(call.lhs(), rhs), it->source_location));
795  }
796 
797  it->turn_into_skip();
798  dest.insert_before_swap(it, tmp);
799 }
800 
802  goto_programt &dest,
804  const exprt &buffer,
805  const typet &buf_type,
806  const mp_integer &limit)
807 {
808  irep_idt cntr_id="string_instrumentation::$counter";
809 
810  if(symbol_table.symbols.find(cntr_id)==symbol_table.symbols.end())
811  {
812  symbolt new_symbol;
813  new_symbol.base_name="$counter";
814  new_symbol.pretty_name=new_symbol.base_name;
815  new_symbol.name=cntr_id;
816  new_symbol.mode=ID_C;
817  new_symbol.type=size_type();
818  new_symbol.is_state_var=true;
819  new_symbol.is_lvalue=true;
820  new_symbol.is_static_lifetime=true;
821 
822  symbol_table.insert(std::move(new_symbol));
823  }
824 
825  const symbolt &cntr_sym=ns.lookup(cntr_id);
826 
827  // create a loop that runs over the buffer
828  // and invalidates every element
829 
831  cntr_sym.symbol_expr(),
832  from_integer(0, cntr_sym.type),
833  target->source_location));
834 
835  exprt bufp;
836 
837  if(buf_type.id()==ID_pointer)
838  bufp=buffer;
839  else
840  {
841  index_exprt index(
842  buffer, from_integer(0, index_type()), buf_type.subtype());
843  bufp=address_of_exprt(index);
844  }
845 
846  exprt condition;
847 
848  if(limit==0)
849  condition =
850  binary_relation_exprt(cntr_sym.symbol_expr(), ID_ge, buffer_size(bufp));
851  else
852  condition = binary_relation_exprt(
853  cntr_sym.symbol_expr(), ID_gt, from_integer(limit, unsigned_int_type()));
854 
855  goto_programt::targett check = dest.add(
857 
859  static_cast<const codet &>(get_nil_irep()),
860  target->source_location,
861  ASSIGN,
862  nil_exprt(),
863  {}));
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(
873 
875  dest.add(goto_programt::make_skip(target->source_location));
876 
877  check->complete_goto(exit);
878 
879  const plus_exprt b_plus_i(bufp, cntr_sym.symbol_expr());
880  const dereference_exprt deref(b_plus_i, buf_type.subtype());
881 
882  const side_effect_expr_nondett nondet(
883  buf_type.subtype(), target->source_location);
884 
885  invalidate->code=code_assignt(deref, nondet);
886 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bitvector_typet index_type()
Definition: c_types.cpp:16
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
unsignedbv_typet size_type()
Definition: c_types.cpp:58
bitvector_typet char_type()
Definition: c_types.cpp:114
Operator to return the address of an object.
Definition: pointer_expr.h:200
Arrays with given size.
Definition: std_types.h:968
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:675
std::size_t get_width() const
Definition: std_types.h:1048
A codet representing an assignment in the program.
Definition: std_code.h:295
codet representation of a function call statement.
Definition: std_code.h:1215
exprt & function()
Definition: std_code.h:1250
argumentst & arguments()
Definition: std_code.h:1260
exprt::operandst argumentst
Definition: std_code.h:1224
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
struct configt::ansi_ct ansi_c
Operator to dereference a pointer.
Definition: pointer_expr.h:256
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
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:133
const source_locationt & source_location() const
Definition: expr.h:234
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2726
A collection of goto functions.
function_mapt function_map
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.
Definition: goto_program.h:180
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:876
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:577
instructionst::iterator targett
Definition: goto_program.h:550
instructionst::const_iterator const_targett
Definition: goto_program.h:551
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:995
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:822
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:657
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:969
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:864
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:938
Array index operator.
Definition: std_expr.h:1243
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
bool is_nil() const
Definition: irep.h:387
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
The NIL expression.
Definition: std_expr.h:2735
The plus expression Associativity is not specified.
Definition: std_expr.h:831
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:485
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1968
void do_strchr(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
void do_function_call(goto_programt &dest, goto_programt::targett target)
bool is_string_type(const typet &t) const
void do_fscanf(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
void operator()(goto_programt &dest)
void do_strerror(goto_programt &dest, goto_programt::targett it, const code_function_callt &)
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_strrchr(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
void make_type(exprt &dest, const typet &type)
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)
string_instrumentationt(symbol_tablet &_symbol_table)
void instrument(goto_programt &dest, goto_programt::targett it)
void do_snprintf(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
void do_strstr(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
void do_strncmp(goto_programt &dest, goto_programt::targett it, const code_function_callt &)
void do_strtok(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
void do_strcat(goto_programt &dest, goto_programt::targett it, const code_function_callt &)
void invalidate_buffer(goto_programt &dest, goto_programt::const_targett target, const exprt &buffer, const typet &buf_type, const mp_integer &limit)
void do_sprintf(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
const irep_idt & get_identifier() const
Definition: std_expr.h:110
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Definition: symbol_table.h:20
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_static_lifetime
Definition: symbol.h:65
bool is_state_var
Definition: symbol.h:62
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
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
bool is_lvalue
Definition: symbol.h:66
irep_idt mode
Language mode.
Definition: symbol.h:49
The Boolean constant true.
Definition: std_expr.h:2717
Semantic type conversion.
Definition: std_expr.h:1781
The type of an expression, extends irept.
Definition: type.h:28
const source_locationt & source_location() const
Definition: type.h:71
const typet & subtype() const
Definition: type.h:47
configt config
Definition: config.cpp:24
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
Definition: goto_program.h:47
const irept & get_nil_irep()
Definition: irep.cpp:26
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
BigInt mp_integer
Definition: mp_arith.h:19
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:237
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
Program Transformation.
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1096
const string_constantt & to_string_constant(const exprt &expr)
exprt buffer_size(const exprt &what)
predicate_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.
std::size_t char_width
Definition: config.h:114
Author: Diffblue Ltd.