Go to the documentation of this file.
33 result.copy_to_operands(what);
34 result.
set(
"lhs", write);
44 result.
set(
"lhs", write);
125 std::size_t format_string_inx,
126 std::size_t argument_start_inx,
127 const std::string &function_name);
133 std::size_t format_string_inx,
134 std::size_t argument_start_inx,
135 const std::string &function_name);
140 (t.
id()==ID_pointer || t.
id()==ID_array) &&
149 const typet &buf_type,
178 for(goto_functionst::function_mapt::iterator
183 (*this)(it->second.body);
197 if(it->is_function_call())
209 if(
function.
id()==ID_symbol)
214 if(identifier==
"strcoll")
217 else if(identifier==
"strncmp")
219 else if(identifier==
"strxfrm")
222 else if(identifier==
"strchr")
224 else if(identifier==
"strcspn")
227 else if(identifier==
"strpbrk")
230 else if(identifier==
"strrchr")
232 else if(identifier==
"strspn")
235 else if(identifier==
"strerror")
237 else if(identifier==
"strstr")
239 else if(identifier==
"strtok")
241 else if(identifier==
"sprintf")
243 else if(identifier==
"snprintf")
245 else if(identifier==
"fscanf")
259 if(arguments.size()<2)
262 "sprintf expected to have two or more arguments",
263 target->source_location);
272 assertion->source_location.set_property_class(
"string");
273 assertion->source_location.set_comment(
"sprintf buffer overflow");
286 target->turn_into_skip();
297 if(arguments.size()<3)
300 "snprintf expected to have three or more arguments",
301 target->source_location);
311 assertion->source_location.set_property_class(
"string");
312 assertion->source_location.set_comment(
"snprintf buffer overflow");
325 target->turn_into_skip();
336 if(arguments.size()<2)
339 "fscanf expected to have two or more arguments", target->source_location);
355 target->turn_into_skip();
363 std::size_t format_string_inx,
364 std::size_t argument_start_inx,
365 const std::string &function_name)
367 const exprt &format_arg=arguments[format_string_inx];
370 format_arg.
id() == ID_address_of &&
382 for(
const auto &token : token_list)
386 const exprt &arg=arguments[argument_start_inx+args];
388 if(arg.
id()!=ID_string_constant)
392 if(arg.
type().
id() != ID_pointer)
401 assertion->source_location.set_property_class(
"string");
402 std::string
comment(
"zero-termination of string argument of ");
404 assertion->source_location.set_comment(
comment);
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);
427 for(std::size_t i=2; i<arguments.size(); i++)
429 const exprt &arg=arguments[i];
435 if(arg.
type().
id() != ID_pointer)
444 assertion->source_location.set_property_class(
"string");
445 assertion->source_location.set_comment(
446 "zero-termination of string argument of " + function_name);
456 std::size_t format_string_inx,
457 std::size_t argument_start_inx,
458 const std::string &function_name)
460 const exprt &format_arg=arguments[format_string_inx];
463 format_arg.
id() == ID_address_of &&
475 for(
const auto &token : token_list)
488 const exprt &argument=arguments[argument_start_inx+args];
493 if(token.field_width!=0)
501 if(arg_type.
id()==ID_pointer)
512 condition = fw_lt_bs;
522 assertion->source_location.set_property_class(
"string");
523 std::string
comment(
"format string buffer overflow in ");
525 assertion->source_location.set_comment(
comment);
529 dest, target, argument, arg_type, token.field_width);
545 const exprt &argument=arguments[argument_start_inx+args];
561 for(std::size_t i=argument_start_inx; i<arguments.size(); i++)
563 const typet &arg_type = arguments[i].type();
577 assertion->source_location.set_property_class(
"string");
578 std::string
comment(
"format string buffer overflow in ");
580 assertion->source_location.set_comment(
comment);
611 if(arguments.size()!=2)
614 "strchr expected to have two arguments", 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");
625 target->turn_into_skip();
636 if(arguments.size()!=2)
639 "strrchr expected to have two arguments", 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");
650 target->turn_into_skip();
661 if(arguments.size()!=2)
664 "strstr expected to have two arguments", 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");
677 assertion1->source_location.set_property_class(
"string");
678 assertion1->source_location.set_comment(
679 "zero-termination of 2nd string argument of strstr");
681 target->turn_into_skip();
692 if(arguments.size()!=2)
695 "strtok expected to have two arguments", 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");
708 assertion1->source_location.set_property_class(
"string");
709 assertion1->source_location.set_comment(
710 "zero-termination of 2nd string argument of strtok");
712 target->turn_into_skip();
723 it->turn_into_skip();
727 irep_idt identifier_buf=
"__strerror_buffer";
728 irep_idt identifier_size=
"__strerror_buffer_size";
733 new_symbol_size.
base_name=
"__strerror_buffer_size";
735 new_symbol_size.
name=identifier_size;
736 new_symbol_size.
mode=ID_C;
744 new_symbol_buf.
mode=ID_C;
745 new_symbol_buf.
type=type;
749 new_symbol_buf.
base_name=
"__strerror_buffer";
799 it->turn_into_skip();
807 const typet &buf_type,
810 irep_idt cntr_id=
"string_instrumentation::$counter";
817 new_symbol.
name=cntr_id;
818 new_symbol.
mode=ID_C;
839 if(buf_type.
id()==ID_pointer)
879 check->complete_goto(exit);
887 invalidate->code_nonconst() =
code_assignt(deref, nondet);
#define Forall_goto_program_instructions(it, program)
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void do_strcat(goto_programt &dest, goto_programt::targett it, const code_function_callt &)
const typet & subtype() const
void do_fscanf(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
void operator()(goto_programt &dest)
The type of an expression, extends irept.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
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)
exprt is_zero_string(const exprt &what, bool write)
typet type
Type of symbol.
Operator to dereference a pointer.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
void do_snprintf(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
void instrument(goto_programt &dest, goto_programt::targett it)
const string_constantt & to_string_constant(const exprt &expr)
targett add(instructiont &&instruction)
Adds a given instruction at the end.
The plus expression Associativity is not specified.
symbol_tablet & symbol_table
Base class for all expressions.
Generic base class for unary expressions.
void do_strstr(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
irep_idt base_name
Base (non-scoped) name.
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)
struct configt::ansi_ct ansi_c
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
function_mapt function_map
bitvector_typet index_type()
string_instrumentationt(symbol_tablet &_symbol_table)
void do_sprintf(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
irep_idt pretty_name
Language-specific display name.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
irep_idt mode
Language mode.
void do_strncmp(goto_programt &dest, goto_programt::targett it, const code_function_callt &)
void string_instrumentation(symbol_tablet &symbol_table, goto_programt &dest)
const std::string & id2string(const irep_idt &d)
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
void do_strtok(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
exprt zero_string_length(const exprt &what, bool write)
const source_locationt & source_location() const
const irep_idt & get_identifier() const
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
API to expression classes for Pointers.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
void do_strrchr(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
unsignedbv_typet unsigned_int_type()
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
exprt::operandst argumentst
The Boolean constant false.
bitvector_typet char_type()
std::size_t get_width() const
A side_effect_exprt that returns a non-deterministically chosen value.
void invalidate_buffer(goto_programt &dest, goto_programt::const_targett target, const exprt &buffer, const typet &buf_type, const mp_integer &limit)
A collection of goto functions.
void do_strchr(goto_programt &dest, goto_programt::targett target, const code_function_callt &)
goto_functionst goto_functions
GOTO functions.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
void set(const irep_namet &name, const irep_idt &value)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
A base class for relations, i.e., binary predicates whose two operands have the same type.
bool is_string_type(const typet &t) const
void do_function_call(goto_programt &dest, goto_programt::targett target)
A generic container class for the GOTO intermediate representation of one function.
void do_strerror(goto_programt &dest, goto_programt::targett it, const code_function_callt &)
exprt buffer_size(const exprt &what)
instructionst::const_iterator const_targett
const irept & get_nil_irep()
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Operator to return the address of an object.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Semantic type conversion.
unsignedbv_typet size_type()
A codet representing an assignment in the program.
The Boolean constant true.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
This class represents an instruction in the GOTO intermediate representation.
API to expression classes.
const source_locationt & source_location() const
symbol_tablet symbol_table
Symbol table.
irep_idt name
The unique identifier.
instructionst::iterator targett
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
void make_type(exprt &dest, const typet &type)
Data structure for representing an arbitrary statement in a program.