check for accesses to locals that are out-of-scope
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3099 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
parent
d66468eb66
commit
f1b0d2e0c5
|
@ -1,4 +1,4 @@
|
|||
KNOWNBUG
|
||||
CORE
|
||||
main.c
|
||||
--pointer-check
|
||||
^EXIT=10$
|
||||
|
|
|
@ -11,6 +11,7 @@ Date: March 2013
|
|||
#ifndef CPROVER_DIRTY_H
|
||||
#define CPROVER_DIRTY_H
|
||||
|
||||
#include <util/std_expr.h>
|
||||
#include <goto-programs/goto_functions.h>
|
||||
|
||||
class dirtyt
|
||||
|
@ -24,11 +25,22 @@ public:
|
|||
}
|
||||
|
||||
void output(std::ostream &out) const;
|
||||
|
||||
bool is_dirty(const irep_idt &id) const
|
||||
|
||||
// will go away, use below
|
||||
inline bool is_dirty(const irep_idt &id) const
|
||||
{
|
||||
return dirty.find(id)!=dirty.end();
|
||||
}
|
||||
|
||||
inline bool operator()(const irep_idt &id) const
|
||||
{
|
||||
return dirty.find(id)!=dirty.end();
|
||||
}
|
||||
|
||||
inline bool operator()(const symbol_exprt &expr) const
|
||||
{
|
||||
return operator()(expr.get_identifier());
|
||||
}
|
||||
|
||||
protected:
|
||||
void build(const goto_functiont &goto_function);
|
||||
|
|
|
@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/guard.h>
|
||||
#include <util/base_type.h>
|
||||
#include <util/pointer_predicates.h>
|
||||
#include <util/cprover_prefix.h>
|
||||
|
||||
#include "local_may_alias.h"
|
||||
#include "goto_check.h"
|
||||
|
@ -831,18 +832,22 @@ void goto_checkt::pointer_validity_check(
|
|||
#else
|
||||
|
||||
std::set<exprt> alias_set=local_may_alias->get(t, pointer);
|
||||
|
||||
bool may_use_offset=local_may_alias->may_use_offset(t, pointer);
|
||||
bool aliases_unknown=alias_set.find(exprt(ID_unknown))!=alias_set.end();
|
||||
bool aliases_dynamic_object=alias_set.find(exprt(ID_dynamic_object))!=alias_set.end();
|
||||
bool aliases_null_object=alias_set.find(exprt(ID_null_object))!=alias_set.end();
|
||||
|
||||
bool aliases_other_object=false;
|
||||
|
||||
for(std::set<exprt>::const_iterator it=alias_set.begin();
|
||||
it!=alias_set.end();
|
||||
it++)
|
||||
if(it->id()!=ID_unknown && it->id()!=ID_dynamic_object && it->id()!=ID_null_object)
|
||||
if(it->id()!=ID_unknown &&
|
||||
it->id()!=ID_dynamic_object &&
|
||||
it->id()!=ID_null_object)
|
||||
{
|
||||
aliases_other_object=true;
|
||||
}
|
||||
|
||||
const typet &dereference_type=pointer_type.subtype();
|
||||
|
||||
|
@ -875,6 +880,15 @@ void goto_checkt::pointer_validity_check(
|
|||
expr,
|
||||
guard);
|
||||
|
||||
if(aliases_unknown || aliases_other_object)
|
||||
add_guarded_claim(
|
||||
not_exprt(dead_object(pointer, ns)),
|
||||
"dereference failure: dead object",
|
||||
"pointer dereference",
|
||||
expr.find_location(),
|
||||
expr,
|
||||
guard);
|
||||
|
||||
if(enable_bounds_check && may_use_offset)
|
||||
{
|
||||
if(aliases_unknown || aliases_dynamic_object)
|
||||
|
@ -1388,6 +1402,28 @@ void goto_checkt::goto_check(goto_functiont &goto_function)
|
|||
if(!enable_assumptions)
|
||||
i.type=SKIP;
|
||||
}
|
||||
else if(i.is_dead())
|
||||
{
|
||||
if(enable_pointer_check)
|
||||
{
|
||||
assert(i.code.operands().size()==1);
|
||||
const symbol_exprt &variable=to_symbol_expr(i.code.op0());
|
||||
|
||||
// is it dirty?
|
||||
if(local_may_alias->dirty(variable))
|
||||
{
|
||||
// need to mark the dead variable as dead
|
||||
goto_programt::targett t=new_code.add_instruction(ASSIGN);
|
||||
exprt address_of_expr=address_of_exprt(variable);
|
||||
exprt lhs=symbol_expr(ns.lookup(CPROVER_PREFIX "dead_object"));
|
||||
exprt rhs=if_exprt(
|
||||
side_effect_expr_nondett(bool_typet()), address_of_expr, lhs, lhs.type());
|
||||
t->location=i.location;
|
||||
t->code=code_assignt(lhs, rhs);
|
||||
t->code.location()=i.location;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
for(goto_programt::instructionst::iterator
|
||||
i_it=new_code.instructions.begin();
|
||||
|
|
|
@ -111,6 +111,26 @@ exprt deallocated(const exprt &pointer, const namespacet &ns)
|
|||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: dead_object
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
exprt dead_object(const exprt &pointer, const namespacet &ns)
|
||||
{
|
||||
// we check __CPROVER_dead_object!
|
||||
const symbolt &deallocated_symbol=ns.lookup(CPROVER_PREFIX "dead_object");
|
||||
|
||||
return same_object(pointer, deallocated_symbol.symbol_expr());
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: dynamic_size
|
||||
|
||||
Inputs:
|
||||
|
|
|
@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
|
||||
exprt same_object(const exprt &p1, const exprt &p2);
|
||||
exprt deallocated(const exprt &pointer, const namespacet &ns);
|
||||
exprt dead_object(const exprt &pointer, const namespacet &ns);
|
||||
exprt dynamic_size(const namespacet &ns);
|
||||
exprt malloc_object(const exprt &pointer, const namespacet &ns);
|
||||
exprt object_size(const exprt &pointer);
|
||||
|
|
Loading…
Reference in New Issue