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;
789 new_symbol_buf.is_state_var=
true;
790 new_symbol_buf.is_lvalue=
true;
791 new_symbol_buf.is_static_lifetime=
true;
792 new_symbol_buf.base_name=
"__strerror_buffer";
793 new_symbol_buf.pretty_name=new_symbol_buf.base_name;
794 new_symbol_buf.name=new_symbol_buf.base_name;
815 assumption1->make_assumption(
821 assumption1->source_location=it->source_location;
836 assignment2->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);
The type of an expression, extends irept.
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
predicate_exprt is_zero_string(const exprt &what, bool write)
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 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 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)
Copy the given argument to the end of exprt's operands.
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.
typet & type()
Return the type of the expression.
exprt::operandst argumentst
unsignedbv_typet size_type()
symbol_tablet symbol_table
Symbol table.
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
Operator to dereference a pointer.
API to expression classes.
void operator()(goto_programt &dest)
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void instrument(goto_programt &dest, goto_programt::targett it)
A side_effect_exprt that returns a non-deterministically chosen value.
codet representation of a function call statement.
The plus expression Associativity is not specified.
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
exprt zero_string_length(const exprt &what, bool write)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Class that provides messages with a built-in verbosity 'level'.
bitvector_typet index_type()
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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)
const source_locationt & source_location() const
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
#define Forall_goto_program_instructions(it, program)
void do_function_call(goto_programt &dest, goto_programt::targett it)
const typet & subtype() const
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
goto_functionst goto_functions
GOTO functions.
bitvector_typet char_type()
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void do_strstr(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
A codet representing an assignment in the program.
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 base class for expressions that are predicates, i.e., Boolean-typed.