34 result.
set(
"lhs", write);
44 result.
set(
"lhs", write);
129 std::size_t format_string_inx,
130 std::size_t argument_start_inx,
131 const std::string &function_name);
137 std::size_t format_string_inx,
138 std::size_t argument_start_inx,
139 const std::string &function_name);
144 (t.
id()==ID_pointer || t.
id()==ID_array) &&
153 const typet &buf_type,
187 for(goto_functionst::function_mapt::iterator
192 (*this)(it->second.body);
230 if(
function.
id()==ID_symbol)
235 if(identifier==
"strcoll")
238 else if(identifier==
"strncmp")
240 else if(identifier==
"strxfrm")
243 else if(identifier==
"strchr")
245 else if(identifier==
"strcspn")
248 else if(identifier==
"strpbrk")
251 else if(identifier==
"strrchr")
253 else if(identifier==
"strspn")
256 else if(identifier==
"strerror")
258 else if(identifier==
"strstr")
260 else if(identifier==
"strtok")
262 else if(identifier==
"sprintf")
264 else if(identifier==
"snprintf")
266 else if(identifier==
"fscanf")
280 if(arguments.size()<2)
283 error() <<
"sprintf expected to have two or more arguments" <<
eom;
290 assertion->source_location=target->source_location;
291 assertion->source_location.set_property_class(
"string");
292 assertion->source_location.set_comment(
"sprintf buffer overflow");
303 return_assignment->source_location=target->source_location;
322 if(arguments.size()<3)
325 error() <<
"snprintf expected to have three or more arguments" 333 assertion->source_location=target->source_location;
334 assertion->source_location.set_property_class(
"string");
335 assertion->source_location.set_comment(
"snprintf buffer overflow");
338 assertion->make_assertion(
346 return_assignment->source_location=target->source_location;
365 if(arguments.size()<2)
368 error() <<
"fscanf expected to have two or more arguments" <<
eom;
379 return_assignment->source_location=target->source_location;
395 std::size_t format_string_inx,
396 std::size_t argument_start_inx,
397 const std::string &function_name)
399 const exprt &format_arg=arguments[format_string_inx];
401 if(format_arg.
id()==ID_address_of &&
402 format_arg.
op0().
id()==ID_index &&
403 format_arg.
op0().
op0().
id()==ID_string_constant)
410 for(
const auto &token : token_list)
414 const exprt &arg=arguments[argument_start_inx+args];
417 if(arg.
id()!=ID_string_constant)
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 ");
424 assertion->source_location.set_comment(
comment);
428 if(arg_type.
id()!=ID_pointer)
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 ");
460 format_ass->source_location.set_comment(
comment);
462 for(std::size_t i=2; i<arguments.size(); i++)
464 const exprt &arg=arguments[i];
467 if(arguments[i].
id()!=ID_string_constant &&
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 ");
475 assertion->source_location.set_comment(
comment);
479 if(arg_type.
id()!=ID_pointer)
498 std::size_t format_string_inx,
499 std::size_t argument_start_inx,
500 const std::string &function_name)
502 const exprt &format_arg=arguments[format_string_inx];
504 if(format_arg.
id()==ID_address_of &&
505 format_arg.
op0().
id()==ID_index &&
506 format_arg.
op0().
op0().
id()==ID_string_constant)
513 for(
const auto &token : token_list)
526 const exprt &argument=arguments[argument_start_inx+args];
530 assertion->source_location=target->source_location;
531 assertion->source_location.set_property_class(
"string");
532 std::string
comment(
"format string buffer overflow in ");
534 assertion->source_location.set_comment(
comment);
536 if(token.field_width!=0)
544 if(arg_type.
id()==ID_pointer)
555 assertion->make_assertion(fw_lt_bs);
565 dest, target, argument, arg_type, token.field_width);
578 const exprt &argument=arguments[argument_start_inx+args];
582 assignment->source_location=target->source_location;
599 for(std::size_t i=argument_start_inx; i<arguments.size(); i++)
610 assertion->source_location=target->source_location;
611 assertion->source_location.set_property_class(
"string");
612 std::string
comment(
"format string buffer overflow in ");
614 assertion->source_location.set_comment(
comment);
626 assignment->source_location=target->source_location;
653 if(arguments.size()!=2)
656 error() <<
"strchr expected to have two arguments" <<
eom;
664 assertion->source_location=target->source_location;
665 assertion->source_location.set_property_class(
"string");
666 assertion->source_location.set_comment(
667 "zero-termination of string argument of strchr");
680 if(arguments.size()!=2)
683 error() <<
"strrchr expected to have two arguments" <<
eom;
691 assertion->source_location=target->source_location;
692 assertion->source_location.set_property_class(
"string");
693 assertion->source_location.set_comment(
694 "zero-termination of string argument of strrchr");
707 if(arguments.size()!=2)
710 error() <<
"strstr expected to have two arguments" <<
eom;
718 assertion0->source_location=target->source_location;
719 assertion0->source_location.set_property_class(
"string");
720 assertion0->source_location.set_comment(
721 "zero-termination of 1st string argument of strstr");
725 assertion1->source_location=target->source_location;
726 assertion1->source_location.set_property_class(
"string");
727 assertion1->source_location.set_comment(
728 "zero-termination of 2nd string argument of strstr");
741 if(arguments.size()!=2)
744 error() <<
"strtok expected to have two arguments" <<
eom;
752 assertion0->source_location=target->source_location;
753 assertion0->source_location.set_property_class(
"string");
754 assertion0->source_location.set_comment(
755 "zero-termination of 1st string argument of strtok");
759 assertion1->source_location=target->source_location;
760 assertion1->source_location.set_property_class(
"string");
761 assertion1->source_location.set_comment(
762 "zero-termination of 2nd string argument of strtok");
779 irep_idt identifier_buf=
"__strerror_buffer";
780 irep_idt identifier_size=
"__strerror_buffer_size";
785 new_symbol_size.
base_name=
"__strerror_buffer_size";
787 new_symbol_size.
name=identifier_size;
788 new_symbol_size.
mode=ID_C;
796 new_symbol_buf.
mode=ID_C;
797 new_symbol_buf.type=type;
798 new_symbol_buf.is_state_var=
true;
799 new_symbol_buf.is_lvalue=
true;
800 new_symbol_buf.is_static_lifetime=
true;
801 new_symbol_buf.base_name=
"__strerror_buffer";
802 new_symbol_buf.pretty_name=new_symbol_buf.base_name;
803 new_symbol_buf.name=new_symbol_buf.base_name;
823 assumption1->make_assumption(
829 assumption1->source_location=it->source_location;
844 assignment2->source_location=it->source_location;
864 const typet &buf_type,
867 irep_idt cntr_id=
"string_instrumentation::$counter";
874 new_symbol.
name=cntr_id;
875 new_symbol.
mode=ID_C;
890 init->source_location=target->source_location;
895 check->source_location=target->source_location;
898 invalidate->source_location=target->source_location;
901 increment->source_location=target->source_location;
909 back->source_location=target->source_location;
910 back->make_goto(check);
914 exit->source_location=target->source_location;
919 if(buf_type.
id()==ID_pointer)
924 index.
array()=buffer;
933 check->make_goto(exit);
The type of an expression.
irep_idt name
The unique identifier.
void do_strchr(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
struct configt::ansi_ct ansi_c
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)
symbol_tablet & symbol_table
A generic base class for relations, i.e., binary predicates.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
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)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
irep_idt mode
Language mode.
std::string comment(const rw_set_baset::entryt &entry, bool write)
unsignedbv_typet unsigned_int_type()
void copy_to_operands(const exprt &expr)
const irep_idt & get_identifier() const
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)
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.
exprt::operandst argumentst
unsignedbv_typet size_type()
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static mstreamt & eom(mstreamt &m)
exprt is_zero_string(const exprt &what, bool write)
const irep_idt & id() const
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
void do_strcat(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
The boolean constant true.
instructionst::iterator targett
source_locationt source_location
Operator to dereference a pointer.
API to expression classes.
void operator()(goto_programt &dest)
instructionst::const_iterator const_targett
void instrument(goto_programt &dest, goto_programt::targett it)
A side effect that returns a non-deterministically chosen value.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
exprt zero_string_length(const exprt &what, bool write)
const typet & follow(const typet &) const
bitvector_typet index_type()
void do_fscanf(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
Operator to return the address of an object.
void do_snprintf(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
The boolean constant false.
void do_sprintf(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
A generic container class for the GOTO intermediate representation of one function.
typet type
Type of symbol.
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)
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
const source_locationt & source_location() const
const std::string & get_string(const irep_namet &name) const
source_locationt & add_source_location()
#define Forall_goto_program_instructions(it, program)
void do_function_call(goto_programt &dest, goto_programt::targett it)
goto_programt coverage_criteriont message_handlert & message_handler
const typet & subtype() const
void make_typecast(const typet &_type)
goto_functionst goto_functions
GOTO functions.
bitvector_typet char_type()
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void do_strstr(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
void set(const irep_namet &name, const irep_idt &value)
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)
A generic base class for expressions that are predicates, i.e., boolean-typed.