30 result.copy_to_operands(what);
126 std::size_t format_string_inx,
127 std::size_t argument_start_inx,
128 const std::string &function_name);
134 std::size_t format_string_inx,
135 std::size_t argument_start_inx,
136 const std::string &function_name);
140 return (t.
id() == ID_pointer || t.
id() == ID_array) &&
151 const typet &buf_type,
180 for(goto_functionst::function_mapt::iterator
185 (*this)(it->second.body);
199 if(it->is_function_call())
209 const auto &arguments =
as_const(*target).call_arguments();
211 if(
function.
id()==ID_symbol)
216 if(identifier==
"strcoll")
219 else if(identifier==
"strncmp")
221 else if(identifier==
"strxfrm")
224 else if(identifier==
"strchr")
226 else if(identifier==
"strcspn")
229 else if(identifier==
"strpbrk")
232 else if(identifier==
"strrchr")
234 else if(identifier==
"strspn")
237 else if(identifier==
"strerror")
239 else if(identifier==
"strstr")
241 else if(identifier==
"strtok")
243 else if(identifier==
"sprintf")
245 else if(identifier==
"snprintf")
247 else if(identifier ==
"fscanf" || identifier ==
"__isoc99_fscanf")
260 if(arguments.size()<2)
263 "sprintf expected to have two or more arguments",
264 target->source_location());
273 annotated_location.
set_comment(
"sprintf buffer overflow");
286 target->turn_into_skip();
296 if(arguments.size()<3)
299 "snprintf expected to have three or more arguments",
300 target->source_location());
309 annotated_location.
set_comment(
"snprintf buffer overflow");
323 target->turn_into_skip();
333 if(arguments.size()<2)
336 "fscanf expected to have two or more arguments",
337 target->source_location());
352 target->turn_into_skip();
360 std::size_t format_string_inx,
361 std::size_t argument_start_inx,
362 const std::string &function_name)
364 const exprt &format_arg=arguments[format_string_inx];
367 format_arg.
id() == ID_address_of &&
379 for(
const auto &token : token_list)
383 const exprt &arg=arguments[argument_start_inx+args];
385 if(arg.
id()!=ID_string_constant)
389 if(arg.
type().
id() != ID_pointer)
397 std::string
comment(
"zero-termination of string argument of ");
421 "zero-termination of format string of " + function_name);
425 for(std::size_t i=2; i<arguments.size(); i++)
427 const exprt &arg=arguments[i];
433 if(arg.
type().
id() != ID_pointer)
442 "zero-termination of string argument of " + function_name);
454 std::size_t format_string_inx,
455 std::size_t argument_start_inx,
456 const std::string &function_name)
458 const exprt &format_arg=arguments[format_string_inx];
461 format_arg.
id() == ID_address_of &&
473 for(
const auto &token : token_list)
486 const exprt &argument=arguments[argument_start_inx+args];
491 if(token.field_width!=0)
499 if(arg_type.
id()==ID_pointer)
510 condition = fw_lt_bs;
520 std::string
comment(
"format string buffer overflow in ");
528 dest, target, argument, arg_type, token.field_width);
544 const exprt &argument=arguments[argument_start_inx+args];
560 for(std::size_t i=argument_start_inx; i<arguments.size(); i++)
562 const typet &arg_type = arguments[i].type();
575 std::string
comment(
"format string buffer overflow in ");
610 if(arguments.size()!=2)
613 "strchr expected to have two arguments", target->source_location());
619 "zero-termination of string argument of strchr");
623 target->turn_into_skip();
633 if(arguments.size()!=2)
636 "strrchr expected to have two arguments", target->source_location());
642 "zero-termination of string argument of strrchr");
646 target->turn_into_skip();
656 if(arguments.size()!=2)
659 "strstr expected to have two arguments", target->source_location());
667 "zero-termination of 1st string argument of strstr");
673 "zero-termination of 2nd string argument of strstr");
677 target->turn_into_skip();
687 if(arguments.size()!=2)
690 "strtok expected to have two arguments", target->source_location());
698 "zero-termination of 1st string argument of strtok");
704 "zero-termination of 2nd string argument of strtok");
708 target->turn_into_skip();
720 it->turn_into_skip();
724 irep_idt identifier_buf=
"__strerror_buffer";
725 irep_idt identifier_size=
"__strerror_buffer_size";
730 new_symbol_size.base_name = identifier_size;
731 new_symbol_size.pretty_name=new_symbol_size.base_name;
732 new_symbol_size.is_state_var=
true;
733 new_symbol_size.is_lvalue=
true;
734 new_symbol_size.is_static_lifetime=
true;
737 symbolt new_symbol_buf{identifier_buf, type, ID_C};
738 new_symbol_buf.is_state_var=
true;
739 new_symbol_buf.is_lvalue=
true;
740 new_symbol_buf.is_static_lifetime=
true;
741 new_symbol_buf.base_name = identifier_buf;
742 new_symbol_buf.pretty_name=new_symbol_buf.base_name;
787 it->turn_into_skip();
795 const typet &buf_type,
798 irep_idt cntr_id=
"string_instrumentation::$counter";
803 new_symbol.base_name=
"$counter";
804 new_symbol.pretty_name=new_symbol.base_name;
805 new_symbol.is_state_var=
true;
806 new_symbol.is_lvalue=
true;
807 new_symbol.is_static_lifetime=
true;
824 if(buf_type.
id()==ID_pointer)
870 check->complete_goto(
exit);
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
unsignedbv_typet unsigned_int_type()
bitvector_typet char_type()
bitvector_typet c_index_type()
Operator to return the address of an object.
A base class for relations, i.e., binary predicates whose two operands have the same type.
std::size_t get_width() const
A goto_instruction_codet representing an assignment in the program.
exprt::operandst argumentst
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.
Base class for all expressions.
std::vector< exprt > operandst
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
The Boolean constant false.
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
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())
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
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())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
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())
Thrown when we can't handle something in an input source file.
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The plus expression Associativity is not specified.
A side_effect_exprt that returns a non-deterministically chosen value.
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
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)
string_instrumentationt(symbol_table_baset &_symbol_table)
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)
symbol_table_baset & symbol_table
void do_strncmp(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt::operandst &arguments)
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)
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
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
The Boolean constant true.
const typet & subtype() const
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const source_locationt & source_location() const
Generic base class for unary expressions.
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
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
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const string_constantt & to_string_constant(const exprt &expr)
void string_instrumentation(symbol_table_baset &symbol_table, goto_programt &dest)
exprt buffer_size(const exprt &what)
exprt is_zero_string(const exprt &what, bool write)
exprt zero_string_length(const exprt &what, bool write)
const type_with_subtypet & to_type_with_subtype(const typet &type)
ssize_t write(int fildes, const void *buf, size_t nbyte)