31 result.copy_to_operands(what);
32 result.
set(
"lhs", write);
42 result.
set(
"lhs", write);
135 const std::string &function_name);
143 const std::string &function_name);
187 for(goto_functionst::function_mapt::iterator
188 it=
dest.function_map.begin();
189 it!=
dest.function_map.end();
192 (*this)(it->second.body);
206 if(it->is_function_call())
216 const auto &arguments =
as_const(*target).call_arguments();
223 if(identifier==
"strcoll")
226 else if(identifier==
"strncmp")
228 else if(identifier==
"strxfrm")
231 else if(identifier==
"strchr")
233 else if(identifier==
"strcspn")
236 else if(identifier==
"strpbrk")
239 else if(identifier==
"strrchr")
241 else if(identifier==
"strspn")
244 else if(identifier==
"strerror")
246 else if(identifier==
"strstr")
248 else if(identifier==
"strtok")
250 else if(identifier==
"sprintf")
252 else if(identifier==
"snprintf")
254 else if(identifier==
"fscanf")
267 if(arguments.size()<2)
270 "sprintf expected to have two or more arguments",
271 target->source_location());
280 assertion->source_location_nonconst().set_property_class(
"string");
281 assertion->source_location_nonconst().set_comment(
"sprintf buffer overflow");
293 target->turn_into_skip();
294 dest.insert_before_swap(target,
tmp);
303 if(arguments.size()<3)
306 "snprintf expected to have three or more arguments",
307 target->source_location());
317 assertion->source_location_nonconst().set_property_class(
"string");
318 assertion->source_location_nonconst().set_comment(
"snprintf buffer overflow");
330 target->turn_into_skip();
331 dest.insert_before_swap(target,
tmp);
340 if(arguments.size()<2)
343 "fscanf expected to have two or more arguments",
344 target->source_location());
359 target->turn_into_skip();
360 dest.insert_before_swap(target,
tmp);
369 const std::string &function_name)
405 assertion->source_location_nonconst().set_property_class(
"string");
406 std::string
comment(
"zero-termination of string argument of ");
408 assertion->source_location_nonconst().set_comment(
comment);
427 format_ass->source_location_nonconst().set_property_class(
"string");
428 format_ass->source_location_nonconst().set_comment(
429 "zero-termination of format string of " + function_name);
431 for(std::size_t
i=2;
i<arguments.size();
i++)
433 const exprt &arg=arguments[
i];
448 assertion->source_location_nonconst().set_property_class(
"string");
449 assertion->source_location_nonconst().set_comment(
450 "zero-termination of string argument of " + function_name);
462 const std::string &function_name)
497 if(token.field_width!=0)
527 assertion->source_location_nonconst().set_property_class(
"string");
528 std::string
comment(
"format string buffer overflow in ");
530 assertion->source_location_nonconst().set_comment(
comment);
582 assertion->source_location_nonconst().set_property_class(
"string");
583 std::string
comment(
"format string buffer overflow in ");
585 assertion->source_location_nonconst().set_comment(
comment);
616 if(arguments.size()!=2)
619 "strchr expected to have two arguments", target->source_location());
626 assertion->source_location_nonconst().set_property_class(
"string");
627 assertion->source_location_nonconst().set_comment(
628 "zero-termination of string argument of strchr");
630 target->turn_into_skip();
631 dest.insert_before_swap(target,
tmp);
640 if(arguments.size()!=2)
643 "strrchr expected to have two arguments", target->source_location());
650 assertion->source_location_nonconst().set_property_class(
"string");
651 assertion->source_location_nonconst().set_comment(
652 "zero-termination of string argument of strrchr");
654 target->turn_into_skip();
655 dest.insert_before_swap(target,
tmp);
664 if(arguments.size()!=2)
667 "strstr expected to have two arguments", target->source_location());
674 assertion0->source_location_nonconst().set_property_class(
"string");
675 assertion0->source_location_nonconst().set_comment(
676 "zero-termination of 1st string argument of strstr");
680 assertion1->source_location_nonconst().set_property_class(
"string");
681 assertion1->source_location_nonconst().set_comment(
682 "zero-termination of 2nd string argument of strstr");
684 target->turn_into_skip();
685 dest.insert_before_swap(target,
tmp);
694 if(arguments.size()!=2)
697 "strtok expected to have two arguments", target->source_location());
704 assertion0->source_location_nonconst().set_property_class(
"string");
705 assertion0->source_location_nonconst().set_comment(
706 "zero-termination of 1st string argument of strtok");
710 assertion1->source_location_nonconst().set_property_class(
"string");
711 assertion1->source_location_nonconst().set_comment(
712 "zero-termination of 2nd string argument of strtok");
714 target->turn_into_skip();
715 dest.insert_before_swap(target,
tmp);
726 it->turn_into_skip();
800 it->turn_into_skip();
801 dest.insert_before_swap(it,
tmp);
882 check->complete_goto(exit);
888 buf_type.subtype(), target->source_location());
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()
unsignedbv_typet size_type()
bitvector_typet char_type()
bitvector_typet c_index_type()
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A base class for relations, i.e., binary predicates whose two operands have the same type.
std::size_t get_width() const
A codet representing an assignment in the program.
exprt::operandst argumentst
Data structure for representing an arbitrary statement in a program.
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.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
The Boolean constant false.
A collection of goto functions.
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())
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())
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())
void set(const irep_idt &name, const irep_idt &value)
const irep_idt & id() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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 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)
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)
void do_strncmp(goto_programt &dest, goto_programt::targett it, const exprt &lhs, const exprt::operandst &arguments)
void make_type(exprt &dest, const typet &type)
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)
symbol_tablet & symbol_table
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)
string_instrumentationt(symbol_tablet &_symbol_table)
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
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt pretty_name
Language-specific display name.
irep_idt irep_idt base_name
Name of module the symbol belongs to.
irep_idt mode
Language mode.
The Boolean constant true.
const typet & subtype() const
Semantic type conversion.
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 irept & get_nil_irep()
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 index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const string_constantt & to_string_constant(const exprt &expr)
exprt buffer_size(const exprt &what)
exprt is_zero_string(const exprt &what, bool write)
void string_instrumentation(symbol_tablet &symbol_table, goto_programt &dest)
exprt zero_string_length(const exprt &what, bool write)
const type_with_subtypet & to_type_with_subtype(const typet &type)