33 result.
set(
"lhs", write);
43 result.
set(
"lhs", write);
128 std::size_t format_string_inx,
129 std::size_t argument_start_inx,
130 const std::string &function_name);
136 std::size_t format_string_inx,
137 std::size_t argument_start_inx,
138 const std::string &function_name);
143 (t.
id()==ID_pointer || t.
id()==ID_array) &&
152 const typet &buf_type,
186 for(goto_functionst::function_mapt::iterator
191 (*this)(it->second.body);
229 if(
function.
id()==ID_symbol)
234 if(identifier==
"strcoll")
237 else if(identifier==
"strncmp")
239 else if(identifier==
"strxfrm")
242 else if(identifier==
"strchr")
244 else if(identifier==
"strcspn")
247 else if(identifier==
"strpbrk")
250 else if(identifier==
"strrchr")
252 else if(identifier==
"strspn")
255 else if(identifier==
"strerror")
257 else if(identifier==
"strstr")
259 else if(identifier==
"strtok")
261 else if(identifier==
"sprintf")
263 else if(identifier==
"snprintf")
265 else if(identifier==
"fscanf")
279 if(arguments.size()<2)
282 "sprintf expected to have two or more arguments",
283 target->source_location);
289 assertion->source_location=target->source_location;
290 assertion->source_location.set_property_class(
"string");
291 assertion->source_location.set_comment(
"sprintf buffer overflow");
302 return_assignment->source_location=target->source_location;
321 if(arguments.size()<3)
324 "snprintf expected to have three or more arguments",
325 target->source_location);
331 assertion->source_location=target->source_location;
332 assertion->source_location.set_property_class(
"string");
333 assertion->source_location.set_comment(
"snprintf buffer overflow");
336 assertion->make_assertion(
344 return_assignment->source_location=target->source_location;
363 if(arguments.size()<2)
366 "fscanf expected to have two or more arguments", target->source_location);
376 return_assignment->source_location=target->source_location;
392 std::size_t format_string_inx,
393 std::size_t argument_start_inx,
394 const std::string &function_name)
396 const exprt &format_arg=arguments[format_string_inx];
398 if(format_arg.
id()==ID_address_of &&
399 format_arg.
op0().
id()==ID_index &&
400 format_arg.
op0().
op0().
id()==ID_string_constant)
407 for(
const auto &token : token_list)
411 const exprt &arg=arguments[argument_start_inx+args];
414 if(arg.
id()!=ID_string_constant)
417 assertion->source_location=target->source_location;
418 assertion->source_location.set_property_class(
"string");
419 std::string
comment(
"zero-termination of string argument of ");
421 assertion->source_location.set_comment(
comment);
425 if(arg_type.
id()!=ID_pointer)
453 format_ass->source_location=target->source_location;
454 format_ass->source_location.set_property_class(
"string");
455 std::string
comment(
"zero-termination of format string of ");
457 format_ass->source_location.set_comment(
comment);
459 for(std::size_t i=2; i<arguments.size(); i++)
461 const exprt &arg=arguments[i];
464 if(arguments[i].
id()!=ID_string_constant &&
468 assertion->source_location=target->source_location;
469 assertion->source_location.set_property_class(
"string");
470 std::string
comment(
"zero-termination of string argument of ");
472 assertion->source_location.set_comment(
comment);
476 if(arg_type.
id()!=ID_pointer)
495 std::size_t format_string_inx,
496 std::size_t argument_start_inx,
497 const std::string &function_name)
499 const exprt &format_arg=arguments[format_string_inx];
501 if(format_arg.
id()==ID_address_of &&
502 format_arg.
op0().
id()==ID_index &&
503 format_arg.
op0().
op0().
id()==ID_string_constant)
510 for(
const auto &token : token_list)
523 const exprt &argument=arguments[argument_start_inx+args];
527 assertion->source_location=target->source_location;
528 assertion->source_location.set_property_class(
"string");
529 std::string
comment(
"format string buffer overflow in ");
531 assertion->source_location.set_comment(
comment);
533 if(token.field_width!=0)
541 if(arg_type.
id()==ID_pointer)
552 assertion->make_assertion(fw_lt_bs);
562 dest, target, argument, arg_type, token.field_width);
575 const exprt &argument=arguments[argument_start_inx+args];
579 assignment->source_location=target->source_location;
595 for(std::size_t i=argument_start_inx; i<arguments.size(); i++)
606 assertion->source_location=target->source_location;
607 assertion->source_location.set_property_class(
"string");
608 std::string
comment(
"format string buffer overflow in ");
610 assertion->source_location.set_comment(
comment);
622 assignment->source_location=target->source_location;
648 if(arguments.size()!=2)
651 "strchr expected to have two arguments", target->source_location);
658 assertion->source_location=target->source_location;
659 assertion->source_location.set_property_class(
"string");
660 assertion->source_location.set_comment(
661 "zero-termination of string argument of strchr");
674 if(arguments.size()!=2)
677 "strrchr expected to have two arguments", target->source_location);
684 assertion->source_location=target->source_location;
685 assertion->source_location.set_property_class(
"string");
686 assertion->source_location.set_comment(
687 "zero-termination of string argument of strrchr");
700 if(arguments.size()!=2)
703 "strstr expected to have two arguments", target->source_location);
710 assertion0->source_location=target->source_location;
711 assertion0->source_location.set_property_class(
"string");
712 assertion0->source_location.set_comment(
713 "zero-termination of 1st string argument of strstr");
717 assertion1->source_location=target->source_location;
718 assertion1->source_location.set_property_class(
"string");
719 assertion1->source_location.set_comment(
720 "zero-termination of 2nd string argument of strstr");
733 if(arguments.size()!=2)
736 "strtok expected to have two arguments", target->source_location);
743 assertion0->source_location=target->source_location;
744 assertion0->source_location.set_property_class(
"string");
745 assertion0->source_location.set_comment(
746 "zero-termination of 1st string argument of strtok");
750 assertion1->source_location=target->source_location;
751 assertion1->source_location.set_property_class(
"string");
752 assertion1->source_location.set_comment(
753 "zero-termination of 2nd string argument of strtok");
770 irep_idt identifier_buf=
"__strerror_buffer";
771 irep_idt identifier_size=
"__strerror_buffer_size";
776 new_symbol_size.
base_name=
"__strerror_buffer_size";
778 new_symbol_size.
name=identifier_size;
779 new_symbol_size.
mode=ID_C;
787 new_symbol_buf.
mode=ID_C;
788 new_symbol_buf.
type=type;
792 new_symbol_buf.
base_name=
"__strerror_buffer";
811 assignment1->source_location=it->source_location;
815 assumption1->make_assumption(
821 assumption1->source_location=it->source_location;
836 assignment2->source_location=it->source_location;
845 assignment3->source_location=it->source_location;
856 const typet &buf_type,
859 irep_idt cntr_id=
"string_instrumentation::$counter";
866 new_symbol.
name=cntr_id;
867 new_symbol.
mode=ID_C;
882 init->source_location=target->source_location;
887 check->source_location=target->source_location;
890 invalidate->source_location=target->source_location;
893 increment->source_location=target->source_location;
901 back->source_location=target->source_location;
902 back->make_goto(check);
906 exit->source_location=target->source_location;
911 if(buf_type.
id()==ID_pointer)
916 index.
array()=buffer;
925 check->make_goto(exit);