32 result.
set(
"lhs", write);
42 result.
set(
"lhs", write);
127 unsigned format_string_inx,
128 unsigned argument_start_inx,
129 const std::string &function_name);
135 unsigned format_string_inx,
136 unsigned argument_start_inx,
137 const std::string &function_name);
142 (t.
id()==ID_pointer || t.
id()==ID_array) &&
151 const typet &buf_type,
175 for(goto_functionst::function_mapt::iterator
180 (*this)(it->second.body);
218 if(
function.
id()==ID_symbol)
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")
268 if(arguments.size()<2)
271 error() <<
"sprintf expected to have two or more arguments" <<
eom;
278 assertion->source_location=target->source_location;
279 assertion->source_location.set_property_class(
"string");
280 assertion->source_location.set_comment(
"sprintf buffer overflow");
291 return_assignment->source_location=target->source_location;
310 if(arguments.size()<3)
313 error() <<
"snprintf expected to have three or more arguments" 321 assertion->source_location=target->source_location;
322 assertion->source_location.set_property_class(
"string");
323 assertion->source_location.set_comment(
"snprintf buffer overflow");
326 assertion->make_assertion(
334 return_assignment->source_location=target->source_location;
353 if(arguments.size()<2)
356 error() <<
"fscanf expected to have two or more arguments" <<
eom;
367 return_assignment->source_location=target->source_location;
383 unsigned format_string_inx,
384 unsigned argument_start_inx,
385 const std::string &function_name)
387 const exprt &format_arg=arguments[format_string_inx];
389 if(format_arg.
id()==ID_address_of &&
390 format_arg.
op0().
id()==ID_index &&
391 format_arg.
op0().
op0().
id()==ID_string_constant)
398 for(
const auto &token : token_list)
402 const exprt &arg=arguments[argument_start_inx+args];
405 if(arg.
id()!=ID_string_constant)
408 assertion->source_location=target->source_location;
409 assertion->source_location.set_property_class(
"string");
410 std::string
comment(
"zero-termination of string argument of ");
412 assertion->source_location.set_comment(
comment);
416 if(arg_type.
id()!=ID_pointer)
444 format_ass->source_location=target->source_location;
445 format_ass->source_location.set_property_class(
"string");
446 std::string
comment(
"zero-termination of format string of ");
448 format_ass->source_location.set_comment(
comment);
450 for(
unsigned i=2; i<arguments.size(); i++)
452 const exprt &arg=arguments[i];
455 if(arguments[i].
id()!=ID_string_constant &&
459 assertion->source_location=target->source_location;
460 assertion->source_location.set_property_class(
"string");
461 std::string
comment(
"zero-termination of string argument of ");
463 assertion->source_location.set_comment(
comment);
467 if(arg_type.
id()!=ID_pointer)
486 unsigned format_string_inx,
487 unsigned argument_start_inx,
488 const std::string &function_name)
490 const exprt &format_arg=arguments[format_string_inx];
492 if(format_arg.
id()==ID_address_of &&
493 format_arg.
op0().
id()==ID_index &&
494 format_arg.
op0().
op0().
id()==ID_string_constant)
501 for(
const auto &token : token_list)
514 const exprt &argument=arguments[argument_start_inx+args];
518 assertion->source_location=target->source_location;
519 assertion->source_location.set_property_class(
"string");
520 std::string
comment(
"format string buffer overflow in ");
522 assertion->source_location.set_comment(
comment);
524 if(token.field_width!=0)
534 if(arg_type.
id()==ID_pointer)
540 index.
array()=argument;
546 assertion->make_assertion(fw_lt_bs);
556 dest, target, argument, arg_type, token.field_width);
569 const exprt &argument=arguments[argument_start_inx+args];
573 assignment->source_location=target->source_location;
591 for(
unsigned i=argument_start_inx; i<arguments.size(); i++)
602 assertion->source_location=target->source_location;
603 assertion->source_location.set_property_class(
"string");
604 std::string
comment(
"format string buffer overflow in ");
606 assertion->source_location.set_comment(
comment);
618 assignment->source_location=target->source_location;
646 if(arguments.size()!=2)
649 error() <<
"strchr expected to have two arguments" <<
eom;
657 assertion->source_location=target->source_location;
658 assertion->source_location.set_property_class(
"string");
659 assertion->source_location.set_comment(
660 "zero-termination of string argument of strchr");
673 if(arguments.size()!=2)
676 error() <<
"strrchr expected to have two arguments" <<
eom;
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 error() <<
"strstr expected to have two arguments" <<
eom;
711 assertion0->source_location=target->source_location;
712 assertion0->source_location.set_property_class(
"string");
713 assertion0->source_location.set_comment(
714 "zero-termination of 1st string argument of strstr");
718 assertion1->source_location=target->source_location;
719 assertion1->source_location.set_property_class(
"string");
720 assertion1->source_location.set_comment(
721 "zero-termination of 2nd string argument of strstr");
734 if(arguments.size()!=2)
737 error() <<
"strtok expected to have two arguments" <<
eom;
745 assertion0->source_location=target->source_location;
746 assertion0->source_location.set_property_class(
"string");
747 assertion0->source_location.set_comment(
748 "zero-termination of 1st string argument of strtok");
752 assertion1->source_location=target->source_location;
753 assertion1->source_location.set_property_class(
"string");
754 assertion1->source_location.set_comment(
755 "zero-termination of 2nd string argument of strtok");
772 irep_idt identifier_buf=
"__strerror_buffer";
773 irep_idt identifier_size=
"__strerror_buffer_size";
778 new_symbol_size.
base_name=
"__strerror_buffer_size";
780 new_symbol_size.
name=identifier_size;
781 new_symbol_size.
mode=ID_C;
791 new_symbol_buf.
mode=ID_C;
792 new_symbol_buf.
type=type;
796 new_symbol_buf.
base_name=
"__strerror_buffer";
818 assumption1->make_assumption(
824 assumption1->source_location=it->source_location;
839 assignment2->source_location=it->source_location;
859 const typet &buf_type,
862 irep_idt cntr_id=
"string_instrumentation::$counter";
869 new_symbol.
name=cntr_id;
870 new_symbol.
mode=ID_C;
885 init->source_location=target->source_location;
890 check->source_location=target->source_location;
893 invalidate->source_location=target->source_location;
896 increment->source_location=target->source_location;
905 back->source_location=target->source_location;
906 back->make_goto(check);
910 exit->source_location=target->source_location;
915 if(buf_type.
id()==ID_pointer)
920 index.
array()=buffer;
930 deref.copy_to_operands(b_plus_i);
932 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)
const typet & follow(const typet &src) const
struct configt::ansi_ct ansi_c
void update()
Update all indices.
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
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)
targett add_instruction()
Adds an instruction at the end.
symbol_tablet & symbol_table
A generic base class for relations, i.e., binary predicates.
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 move_to_operands(exprt &expr)
void do_strncmp(goto_programt &dest, goto_programt::targett it, code_function_callt &call)
irep_idt pretty_name
Language-specific display name.
exprt::operandst argumentst
unsignedbv_typet size_type()
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)
instructionst::const_iterator const_targett
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.
void do_format_string_write(goto_programt &dest, goto_programt::const_targett target, const code_function_callt::argumentst &arguments, unsigned format_string_inx, unsigned argument_start_inx, const std::string &function_name)
source_locationt source_location
API to expression classes.
void operator()(goto_programt &dest)
void instrument(goto_programt &dest, goto_programt::targett it)
A side effect that returns a non-deterministically chosen value.
const exprt & size() const
exprt zero_string_length(const exprt &what, bool write)
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.
function_mapt function_map
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
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 specialization of goto_program_templatet over goto programs in which instructions have codet type...
typet type
Type of symbol.
void make_type(exprt &dest, const typet &type)
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const source_locationt & source_location() const
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
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)
const typet & subtype() const
void make_typecast(const typet &_type)
void do_format_string_read(goto_programt &dest, goto_programt::const_targett target, const code_function_callt::argumentst &arguments, unsigned format_string_inx, unsigned argument_start_inx, const std::string &function_name)
bitvector_typet char_type()
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)
const code_function_callt & to_code_function_call(const codet &code)
A generic base class for expressions that are predicates, i.e., boolean-typed.
instructionst::iterator targett
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.