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/message.h>
20 #include <util/std_expr.h>
21 #include <util/std_code.h>
22 #include <util/symbol_table.h>
23 
27 
29  const exprt &what,
30  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:
59  symbol_tablet &_symbol_table,
60  message_handlert &_message_handler):
61  messaget(_message_handler),
62  symbol_table(_symbol_table),
63  ns(_symbol_table)
64  {
65  }
66 
67  void operator()(goto_programt &dest);
68  void operator()(goto_functionst &dest);
69 
70 protected:
73 
74  void make_type(exprt &dest, const typet &type)
75  {
76  if(ns.follow(dest.type())!=ns.follow(type))
77  dest.make_typecast(type);
78  }
79 
82 
83  // strings
84  void do_sprintf(
85  goto_programt &dest,
87  code_function_callt &call);
88  void do_snprintf(
89  goto_programt &dest,
91  code_function_callt &call);
92  void do_strcat(
93  goto_programt &dest,
95  code_function_callt &call);
96  void do_strncmp(
97  goto_programt &dest,
99  code_function_callt &call);
100  void do_strchr(
101  goto_programt &dest,
103  code_function_callt &call);
104  void do_strrchr(
105  goto_programt &dest,
107  code_function_callt &call);
108  void do_strstr(
109  goto_programt &dest,
111  code_function_callt &call);
112  void do_strtok(
113  goto_programt &dest,
115  code_function_callt &call);
116  void do_strerror(
117  goto_programt &dest,
119  code_function_callt &call);
120  void do_fscanf(
121  goto_programt &dest,
123  code_function_callt &call);
124 
126  goto_programt &dest,
128  const code_function_callt::argumentst &arguments,
129  std::size_t format_string_inx,
130  std::size_t argument_start_inx,
131  const std::string &function_name);
132 
134  goto_programt &dest,
136  const code_function_callt::argumentst &arguments,
137  std::size_t format_string_inx,
138  std::size_t argument_start_inx,
139  const std::string &function_name);
140 
141  bool is_string_type(const typet &t) const
142  {
143  return
144  (t.id()==ID_pointer || t.id()==ID_array) &&
145  (t.subtype().id()==ID_signedbv || t.subtype().id()==ID_unsignedbv) &&
146  (to_bitvector_type(t.subtype()).get_width()==config.ansi_c.char_width);
147  }
148 
149  void invalidate_buffer(
150  goto_programt &dest,
152  const exprt &buffer,
153  const typet &buf_type,
154  const mp_integer &limit);
155 };
156 
158  symbol_tablet &symbol_table,
160  goto_programt &dest)
161 {
164 }
165 
167  symbol_tablet &symbol_table,
169  goto_functionst &dest)
170 {
173 }
174 
176  goto_modelt &goto_model,
178 {
180  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 
197 {
199  instrument(dest, it);
200 }
201 
203  goto_programt &dest,
205 {
206  switch(it->type)
207  {
208  case ASSIGN:
209  break;
210 
211  case FUNCTION_CALL:
212  do_function_call(dest, it);
213  break;
214 
215  default:
216  {
217  }
218  }
219 }
220 
222  goto_programt &dest,
223  goto_programt::targett target)
224 {
225  code_function_callt &call=
226  to_code_function_call(target->code);
227  exprt &function=call.function();
228  // const exprt &lhs=call.lhs();
229 
230  if(function.id()==ID_symbol)
231  {
232  const irep_idt &identifier=
233  to_symbol_expr(function).get_identifier();
234 
235  if(identifier=="strcoll")
236  {
237  }
238  else if(identifier=="strncmp")
239  do_strncmp(dest, target, call);
240  else if(identifier=="strxfrm")
241  {
242  }
243  else if(identifier=="strchr")
244  do_strchr(dest, target, call);
245  else if(identifier=="strcspn")
246  {
247  }
248  else if(identifier=="strpbrk")
249  {
250  }
251  else if(identifier=="strrchr")
252  do_strrchr(dest, target, call);
253  else if(identifier=="strspn")
254  {
255  }
256  else if(identifier=="strerror")
257  do_strerror(dest, target, call);
258  else if(identifier=="strstr")
259  do_strstr(dest, target, call);
260  else if(identifier=="strtok")
261  do_strtok(dest, target, call);
262  else if(identifier=="sprintf")
263  do_sprintf(dest, target, call);
264  else if(identifier=="snprintf")
265  do_snprintf(dest, target, call);
266  else if(identifier=="fscanf")
267  do_fscanf(dest, target, call);
268 
269  remove_skip(dest);
270  }
271 }
272 
274  goto_programt &dest,
275  goto_programt::targett target,
276  code_function_callt &call)
277 {
278  const code_function_callt::argumentst &arguments=call.arguments();
279 
280  if(arguments.size()<2)
281  {
282  error().source_location=target->source_location;
283  error() << "sprintf expected to have two or more arguments" << eom;
284  throw 0;
285  }
286 
287  goto_programt tmp;
288 
289  goto_programt::targett assertion=tmp.add_instruction();
290  assertion->source_location=target->source_location;
291  assertion->source_location.set_property_class("string");
292  assertion->source_location.set_comment("sprintf buffer overflow");
293 
294  // in the abstract model, we have to report a
295  // (possibly false) positive here
296  assertion->make_assertion(false_exprt());
297 
298  do_format_string_read(tmp, target, arguments, 1, 2, "sprintf");
299 
300  if(call.lhs().is_not_nil())
301  {
302  goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
303  return_assignment->source_location=target->source_location;
304 
305  exprt rhs =
307 
308  return_assignment->code=code_assignt(call.lhs(), rhs);
309  }
310 
311  target->make_skip();
312  dest.insert_before_swap(target, tmp);
313 }
314 
316  goto_programt &dest,
317  goto_programt::targett target,
318  code_function_callt &call)
319 {
320  const code_function_callt::argumentst &arguments=call.arguments();
321 
322  if(arguments.size()<3)
323  {
324  error().source_location=target->source_location;
325  error() << "snprintf expected to have three or more arguments"
326  << eom;
327  throw 0;
328  }
329 
330  goto_programt tmp;
331 
332  goto_programt::targett assertion=tmp.add_instruction();
333  assertion->source_location=target->source_location;
334  assertion->source_location.set_property_class("string");
335  assertion->source_location.set_comment("snprintf buffer overflow");
336 
337  exprt bufsize=buffer_size(arguments[0]);
338  assertion->make_assertion(
339  binary_relation_exprt(bufsize, ID_ge, arguments[1]));
340 
341  do_format_string_read(tmp, target, arguments, 2, 3, "snprintf");
342 
343  if(call.lhs().is_not_nil())
344  {
345  goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
346  return_assignment->source_location=target->source_location;
347 
348  exprt rhs =
350 
351  return_assignment->code=code_assignt(call.lhs(), rhs);
352  }
353 
354  target->make_skip();
355  dest.insert_before_swap(target, tmp);
356 }
357 
359  goto_programt &dest,
360  goto_programt::targett target,
361  code_function_callt &call)
362 {
363  const code_function_callt::argumentst &arguments=call.arguments();
364 
365  if(arguments.size()<2)
366  {
367  error().source_location=target->source_location;
368  error() << "fscanf expected to have two or more arguments" << eom;
369  throw 0;
370  }
371 
372  goto_programt tmp;
373 
374  do_format_string_write(tmp, target, arguments, 1, 2, "fscanf");
375 
376  if(call.lhs().is_not_nil())
377  {
378  goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
379  return_assignment->source_location=target->source_location;
380 
381  exprt rhs =
383 
384  return_assignment->code=code_assignt(call.lhs(), rhs);
385  }
386 
387  target->make_skip();
388  dest.insert_before_swap(target, tmp);
389 }
390 
392  goto_programt &dest,
394  const code_function_callt::argumentst &arguments,
395  std::size_t format_string_inx,
396  std::size_t argument_start_inx,
397  const std::string &function_name)
398 {
399  const exprt &format_arg=arguments[format_string_inx];
400 
401  if(format_arg.id()==ID_address_of &&
402  format_arg.op0().id()==ID_index &&
403  format_arg.op0().op0().id()==ID_string_constant)
404  {
405  format_token_listt token_list=
406  parse_format_string(format_arg.op0().op0().get_string(ID_value));
407 
408  std::size_t args=0;
409 
410  for(const auto &token : token_list)
411  {
412  if(token.type==format_tokent::token_typet::STRING)
413  {
414  const exprt &arg=arguments[argument_start_inx+args];
415  const typet &arg_type=ns.follow(arg.type());
416 
417  if(arg.id()!=ID_string_constant) // we don't need to check constants
418  {
419  goto_programt::targett assertion=dest.add_instruction();
420  assertion->source_location=target->source_location;
421  assertion->source_location.set_property_class("string");
422  std::string comment("zero-termination of string argument of ");
423  comment += function_name;
424  assertion->source_location.set_comment(comment);
425 
426  exprt temp(arg);
427 
428  if(arg_type.id()!=ID_pointer)
429  {
430  index_exprt index;
431  index.array()=temp;
432  index.index()=from_integer(0, index_type());
433  index.type()=arg_type.subtype();
434  temp=address_of_exprt(index);
435  }
436 
437  assertion->make_assertion(is_zero_string(temp));
438  }
439  }
440 
441  if(token.type!=format_tokent::token_typet::TEXT &&
442  token.type!=format_tokent::token_typet::UNKNOWN) args++;
443 
444  if(find(
445  token.flags.begin(),
446  token.flags.end(),
448  token.flags.end())
449  args++; // just eat the additional argument
450  }
451  }
452  else // non-const format string
453  {
454  goto_programt::targett format_ass=dest.add_instruction();
455  format_ass->make_assertion(is_zero_string(arguments[1]));
456  format_ass->source_location=target->source_location;
457  format_ass->source_location.set_property_class("string");
458  std::string comment("zero-termination of format string of ");
459  comment += function_name;
460  format_ass->source_location.set_comment(comment);
461 
462  for(std::size_t i=2; i<arguments.size(); i++)
463  {
464  const exprt &arg=arguments[i];
465  const typet &arg_type=ns.follow(arguments[i].type());
466 
467  if(arguments[i].id()!=ID_string_constant &&
468  is_string_type(arg_type))
469  {
470  goto_programt::targett assertion=dest.add_instruction();
471  assertion->source_location=target->source_location;
472  assertion->source_location.set_property_class("string");
473  std::string comment("zero-termination of string argument of ");
474  comment += function_name;
475  assertion->source_location.set_comment(comment);
476 
477  exprt temp(arg);
478 
479  if(arg_type.id()!=ID_pointer)
480  {
481  index_exprt index;
482  index.array()=temp;
483  index.index()=from_integer(0, index_type());
484  index.type()=arg_type.subtype();
485  temp=address_of_exprt(index);
486  }
487 
488  assertion->make_assertion(is_zero_string(temp));
489  }
490  }
491  }
492 }
493 
495  goto_programt &dest,
497  const code_function_callt::argumentst &arguments,
498  std::size_t format_string_inx,
499  std::size_t argument_start_inx,
500  const std::string &function_name)
501 {
502  const exprt &format_arg=arguments[format_string_inx];
503 
504  if(format_arg.id()==ID_address_of &&
505  format_arg.op0().id()==ID_index &&
506  format_arg.op0().op0().id()==ID_string_constant) // constant format
507  {
508  format_token_listt token_list=
509  parse_format_string(format_arg.op0().op0().get_string(ID_value));
510 
511  std::size_t args=0;
512 
513  for(const auto &token : token_list)
514  {
515  if(find(
516  token.flags.begin(),
517  token.flags.end(),
519  token.flags.end())
520  continue; // asterisk means `ignore this'
521 
522  switch(token.type)
523  {
525  {
526  const exprt &argument=arguments[argument_start_inx+args];
527  const typet &arg_type=ns.follow(argument.type());
528 
529  goto_programt::targett assertion=dest.add_instruction();
530  assertion->source_location=target->source_location;
531  assertion->source_location.set_property_class("string");
532  std::string comment("format string buffer overflow in ");
533  comment += function_name;
534  assertion->source_location.set_comment(comment);
535 
536  if(token.field_width!=0)
537  {
538  exprt fwidth=from_integer(token.field_width, unsigned_int_type());
540  const plus_exprt fw_1(fwidth, one); // +1 for 0-char
541 
542  exprt fw_lt_bs;
543 
544  if(arg_type.id()==ID_pointer)
545  fw_lt_bs=
546  binary_relation_exprt(fw_1, ID_le, buffer_size(argument));
547  else
548  {
549  const index_exprt index(
550  argument, from_integer(0, unsigned_int_type()));
551  address_of_exprt aof(index);
552  fw_lt_bs=binary_relation_exprt(fw_1, ID_le, buffer_size(aof));
553  }
554 
555  assertion->make_assertion(fw_lt_bs);
556  }
557  else
558  {
559  // this is a possible overflow.
560  assertion->make_assertion(false_exprt());
561  }
562 
563  // now kill the contents
565  dest, target, argument, arg_type, token.field_width);
566 
567  args++;
568  break;
569  }
572  {
573  // nothing
574  break;
575  }
576  default: // everything else
577  {
578  const exprt &argument=arguments[argument_start_inx+args];
579  const typet &arg_type=ns.follow(argument.type());
580 
582  assignment->source_location=target->source_location;
583 
584  const dereference_exprt lhs(argument, arg_type.subtype());
585 
586  side_effect_expr_nondett rhs(lhs.type(), target->source_location);
587 
588  assignment->code=code_assignt(lhs, rhs);
589 
590  args++;
591  break;
592  }
593  }
594  }
595  }
596  else // non-const format string
597  {
598  for(std::size_t i=argument_start_inx; i<arguments.size(); i++)
599  {
600  const typet &arg_type=ns.follow(arguments[i].type());
601 
602  // Note: is_string_type() is a `good guess' here. Actually
603  // any of the pointers could point into an array. But it
604  // would suck if we had to invalidate all variables.
605  // Luckily this case isn't needed too often.
606  if(is_string_type(arg_type))
607  {
608  goto_programt::targett assertion=dest.add_instruction();
609  assertion->source_location=target->source_location;
610  assertion->source_location.set_property_class("string");
611  std::string comment("format string buffer overflow in ");
612  comment += function_name;
613  assertion->source_location.set_comment(comment);
614 
615  // as we don't know any field width for the %s that
616  // should be here during runtime, we just report a
617  // possibly false positive
618  assertion->make_assertion(false_exprt());
619 
620  invalidate_buffer(dest, target, arguments[i], arg_type, 0);
621  }
622  else
623  {
625  assignment->source_location=target->source_location;
626 
627  dereference_exprt lhs(arguments[i], arg_type.subtype());
628 
629  side_effect_expr_nondett rhs(lhs.type(), target->source_location);
630 
631  assignment->code=code_assignt(lhs, rhs);
632  }
633  }
634  }
635 }
636 
638  goto_programt &,
641 {
642 }
643 
645  goto_programt &dest,
646  goto_programt::targett target,
647  code_function_callt &call)
648 {
649  const code_function_callt::argumentst &arguments=call.arguments();
650 
651  if(arguments.size()!=2)
652  {
653  error().source_location=target->source_location;
654  error() << "strchr expected to have two arguments" << eom;
655  throw 0;
656  }
657 
658  goto_programt tmp;
659 
660  goto_programt::targett assertion=tmp.add_instruction();
661  assertion->make_assertion(is_zero_string(arguments[0]));
662  assertion->source_location=target->source_location;
663  assertion->source_location.set_property_class("string");
664  assertion->source_location.set_comment(
665  "zero-termination of string argument of strchr");
666 
667  target->make_skip();
668  dest.insert_before_swap(target, tmp);
669 }
670 
672  goto_programt &dest,
673  goto_programt::targett target,
674  code_function_callt &call)
675 {
676  const code_function_callt::argumentst &arguments=call.arguments();
677 
678  if(arguments.size()!=2)
679  {
680  error().source_location=target->source_location;
681  error() << "strrchr expected to have two arguments" << eom;
682  throw 0;
683  }
684 
685  goto_programt tmp;
686 
687  goto_programt::targett assertion=tmp.add_instruction();
688  assertion->make_assertion(is_zero_string(arguments[0]));
689  assertion->source_location=target->source_location;
690  assertion->source_location.set_property_class("string");
691  assertion->source_location.set_comment(
692  "zero-termination of string argument of strrchr");
693 
694  target->make_skip();
695  dest.insert_before_swap(target, tmp);
696 }
697 
699  goto_programt &dest,
700  goto_programt::targett target,
701  code_function_callt &call)
702 {
703  const code_function_callt::argumentst &arguments=call.arguments();
704 
705  if(arguments.size()!=2)
706  {
707  error().source_location=target->source_location;
708  error() << "strstr expected to have two arguments" << eom;
709  throw 0;
710  }
711 
712  goto_programt tmp;
713 
714  goto_programt::targett assertion0=tmp.add_instruction();
715  assertion0->make_assertion(is_zero_string(arguments[0]));
716  assertion0->source_location=target->source_location;
717  assertion0->source_location.set_property_class("string");
718  assertion0->source_location.set_comment(
719  "zero-termination of 1st string argument of strstr");
720 
721  goto_programt::targett assertion1=tmp.add_instruction();
722  assertion1->make_assertion(is_zero_string(arguments[1]));
723  assertion1->source_location=target->source_location;
724  assertion1->source_location.set_property_class("string");
725  assertion1->source_location.set_comment(
726  "zero-termination of 2nd string argument of strstr");
727 
728  target->make_skip();
729  dest.insert_before_swap(target, tmp);
730 }
731 
733  goto_programt &dest,
734  goto_programt::targett target,
735  code_function_callt &call)
736 {
737  const code_function_callt::argumentst &arguments=call.arguments();
738 
739  if(arguments.size()!=2)
740  {
741  error().source_location=target->source_location;
742  error() << "strtok expected to have two arguments" << eom;
743  throw 0;
744  }
745 
746  goto_programt tmp;
747 
748  goto_programt::targett assertion0=tmp.add_instruction();
749  assertion0->make_assertion(is_zero_string(arguments[0]));
750  assertion0->source_location=target->source_location;
751  assertion0->source_location.set_property_class("string");
752  assertion0->source_location.set_comment(
753  "zero-termination of 1st string argument of strtok");
754 
755  goto_programt::targett assertion1=tmp.add_instruction();
756  assertion1->make_assertion(is_zero_string(arguments[1]));
757  assertion1->source_location=target->source_location;
758  assertion1->source_location.set_property_class("string");
759  assertion1->source_location.set_comment(
760  "zero-termination of 2nd string argument of strtok");
761 
762  target->make_skip();
763  dest.insert_before_swap(target, tmp);
764 }
765 
767  goto_programt &dest,
769  code_function_callt &call)
770 {
771  if(call.lhs().is_nil())
772  {
773  it->make_skip();
774  return;
775  }
776 
777  irep_idt identifier_buf="__strerror_buffer";
778  irep_idt identifier_size="__strerror_buffer_size";
779 
780  if(symbol_table.symbols.find(identifier_buf)==symbol_table.symbols.end())
781  {
782  symbolt new_symbol_size;
783  new_symbol_size.base_name="__strerror_buffer_size";
784  new_symbol_size.pretty_name=new_symbol_size.base_name;
785  new_symbol_size.name=identifier_size;
786  new_symbol_size.mode=ID_C;
787  new_symbol_size.type=size_type();
788  new_symbol_size.is_state_var=true;
789  new_symbol_size.is_lvalue=true;
790  new_symbol_size.is_static_lifetime=true;
791 
792  array_typet type(char_type(), new_symbol_size.symbol_expr());
793  symbolt new_symbol_buf;
794  new_symbol_buf.mode=ID_C;
795  new_symbol_buf.type=type;
796  new_symbol_buf.is_state_var=true;
797  new_symbol_buf.is_lvalue=true;
798  new_symbol_buf.is_static_lifetime=true;
799  new_symbol_buf.base_name="__strerror_buffer";
800  new_symbol_buf.pretty_name=new_symbol_buf.base_name;
801  new_symbol_buf.name=new_symbol_buf.base_name;
802 
803  symbol_table.insert(std::move(new_symbol_buf));
804  symbol_table.insert(std::move(new_symbol_size));
805  }
806 
807  const symbolt &symbol_size=ns.lookup(identifier_size);
808  const symbolt &symbol_buf=ns.lookup(identifier_buf);
809 
810  goto_programt tmp;
811 
812  {
814  exprt nondet_size =
816 
817  assignment1->code=code_assignt(symbol_size.symbol_expr(), nondet_size);
818  assignment1->source_location=it->source_location;
819 
820  goto_programt::targett assumption1=tmp.add_instruction();
821 
822  assumption1->make_assumption(
824  symbol_size.symbol_expr(),
825  ID_notequal,
826  from_integer(0, symbol_size.type)));
827 
828  assumption1->source_location=it->source_location;
829  }
830 
831  // return a pointer to some magic buffer
832  index_exprt index(
833  symbol_buf.symbol_expr(),
834  from_integer(0, index_type()),
835  char_type());
836 
837  address_of_exprt ptr(index);
838 
839  // make that zero-terminated
840  {
842  assignment2->code=code_assignt(is_zero_string(ptr, true), true_exprt());
843  assignment2->source_location=it->source_location;
844  }
845 
846  // assign address
847  {
849  exprt rhs=ptr;
850  make_type(rhs, call.lhs().type());
851  assignment3->code=code_assignt(call.lhs(), rhs);
852  assignment3->source_location=it->source_location;
853  }
854 
855  it->make_skip();
856  dest.insert_before_swap(it, tmp);
857 }
858 
860  goto_programt &dest,
862  const exprt &buffer,
863  const typet &buf_type,
864  const mp_integer &limit)
865 {
866  irep_idt cntr_id="string_instrumentation::$counter";
867 
868  if(symbol_table.symbols.find(cntr_id)==symbol_table.symbols.end())
869  {
870  symbolt new_symbol;
871  new_symbol.base_name="$counter";
872  new_symbol.pretty_name=new_symbol.base_name;
873  new_symbol.name=cntr_id;
874  new_symbol.mode=ID_C;
875  new_symbol.type=size_type();
876  new_symbol.is_state_var=true;
877  new_symbol.is_lvalue=true;
878  new_symbol.is_static_lifetime=true;
879 
880  symbol_table.insert(std::move(new_symbol));
881  }
882 
883  const symbolt &cntr_sym=ns.lookup(cntr_id);
884 
885  // create a loop that runs over the buffer
886  // and invalidates every element
887 
889  init->source_location=target->source_location;
890  init->code=
891  code_assignt(cntr_sym.symbol_expr(), from_integer(0, cntr_sym.type));
892 
894  check->source_location=target->source_location;
895 
897  invalidate->source_location=target->source_location;
898 
900  increment->source_location=target->source_location;
901 
902  const plus_exprt plus(
903  cntr_sym.symbol_expr(), from_integer(1, unsigned_int_type()));
904 
905  increment->code=code_assignt(cntr_sym.symbol_expr(), plus);
906 
908  back->source_location=target->source_location;
909  back->make_goto(check);
910  back->guard=true_exprt();
911 
913  exit->source_location=target->source_location;
914  exit->make_skip();
915 
916  exprt cnt_bs, bufp;
917 
918  if(buf_type.id()==ID_pointer)
919  bufp=buffer;
920  else
921  {
922  index_exprt index;
923  index.array()=buffer;
924  index.index()=from_integer(0, index_type());
925  index.type()=buf_type.subtype();
926  bufp=address_of_exprt(index);
927  }
928 
929  const plus_exprt b_plus_i(bufp, cntr_sym.symbol_expr());
930  const dereference_exprt deref(b_plus_i, buf_type.subtype());
931 
932  check->make_goto(exit);
933 
934  if(limit==0)
935  check->guard=
937  cntr_sym.symbol_expr(),
938  ID_ge,
939  buffer_size(bufp));
940  else
941  check->guard=
943  cntr_sym.symbol_expr(),
944  ID_gt,
945  from_integer(limit, unsigned_int_type()));
946 
947  const side_effect_expr_nondett nondet(
948  buf_type.subtype(), target->source_location);
949  invalidate->code=code_assignt(deref, nondet);
950 }
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
void do_strchr(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
struct configt::ansi_ct ansi_c
BigInt mp_integer
Definition: mp_arith.h:22
string_instrumentationt(symbol_tablet &_symbol_table, message_handlert &_message_handler)
void invalidate_buffer(goto_programt &dest, goto_programt::const_targett target, const exprt &buffer, const typet &buf_type, const mp_integer &limit)
bool is_nil() const
Definition: irep.h:172
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
bool is_not_nil() const
Definition: irep.h:173
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:441
format_token_listt parse_format_string(const std::string &arg_string)
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)
exprt & op0()
Definition: expr.h:72
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1159
irep_idt mode
Language mode.
Definition: symbol.h:52
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
const irep_idt & get_identifier() const
Definition: std_expr.h:128
bool is_string_type(const typet &t) const
void do_strrchr(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
void do_strtok(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
void do_strerror(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
Format String Parser.
void do_strncmp(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
function_mapt function_map
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:55
typet & type()
Definition: expr.h:56
exprt::operandst argumentst
Definition: std_code.h:888
unsignedbv_typet size_type()
Definition: c_types.cpp:58
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
String Abstraction.
configt config
Definition: config.cpp:23
std::size_t char_width
Definition: config.h:33
exprt is_zero_string(const exprt &what, bool write)
bool is_static_lifetime
Definition: symbol.h:67
const irep_idt & id() const
Definition: irep.h:259
Symbol Table + CFG.
void string_instrumentation(symbol_tablet &symbol_table, message_handlert &message_handler, goto_programt &dest)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
void do_strcat(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
The boolean constant true.
Definition: std_expr.h:4486
argumentst & arguments()
Definition: std_code.h:890
instructionst::iterator targett
Definition: goto_program.h:397
source_locationt source_location
Definition: message.h:214
Operator to dereference a pointer.
Definition: std_expr.h:3282
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
void operator()(goto_programt &dest)
instructionst::const_iterator const_targett
Definition: goto_program.h:398
mstreamt & error() const
Definition: message.h:302
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void instrument(goto_programt &dest, goto_programt::targett it)
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1340
A function call.
Definition: std_code.h:858
The plus expression.
Definition: std_expr.h:893
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
exprt zero_string_length(const exprt &what, bool write)
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
void do_fscanf(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
Operator to return the address of an object.
Definition: std_expr.h:3168
const symbolst & symbols
void do_snprintf(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
The boolean constant false.
Definition: std_expr.h:4497
void do_sprintf(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
const source_locationt & source_location() const
Definition: type.h:97
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
typet type
Type of symbol.
Definition: symbol.h:34
exprt & index()
Definition: std_expr.h:1496
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 make_type(exprt &dest, const typet &type)
exprt & function()
Definition: std_code.h:878
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
bool is_state_var
Definition: symbol.h:63
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
const source_locationt & source_location() const
Definition: expr.h:125
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
std::list< format_tokent > format_token_listt
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
arrays with given size
Definition: std_types.h:1013
void do_function_call(goto_programt &dest, goto_programt::targett it)
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
const typet & subtype() const
Definition: type.h:33
Program Transformation.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt & array()
Definition: std_expr.h:1486
void make_typecast(const typet &_type)
Definition: expr.cpp:84
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bitvector_typet char_type()
Definition: c_types.cpp:114
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
void do_strstr(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
Assignment.
Definition: std_code.h:196
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
exprt buffer_size(const exprt &what)
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909
A generic base class for expressions that are predicates, i.e., boolean-typed.
Definition: std_expr.h:578
bool is_lvalue
Definition: symbol.h:68
array index operator
Definition: std_expr.h:1462