Skip to content

Fixes to pointer handling in goto_rw [depends-on: #2646] #748

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 3 commits into from
Closed

Fixes to pointer handling in goto_rw [depends-on: #2646] #748

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
55d45a0
Test actually works fine, no bug known here
tautschnig Feb 27, 2018
1b65ef9
Revert "Fixed some array and pointer reads\writes not appearing"
tautschnig Nov 29, 2016
33c9f89
goto_rw: treat dereference failure as a read/write of __CPROVER_memory
tautschnig Feb 27, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion regression/goto-instrument/slice19/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG
CORE
main.c
--full-slice
^EXIT=0$
Expand Down
14 changes: 14 additions & 0 deletions regression/goto-instrument/slice24/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
#include <assert.h>
#include <stdlib.h>

static void f(int* x) { *x = 5; }
static void g(int *x) { assert(*x == 5); }

int main(int argc, char** argv) {

int *x = (int*)malloc(sizeof(int));
f(x);
g(x);

return 0;
}
6 changes: 6 additions & 0 deletions regression/goto-instrument/slice24/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
CORE
main.c
--full-slice --add-library
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
24 changes: 14 additions & 10 deletions src/analyses/goto_rw.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -127,8 +127,11 @@ void rw_range_sett::get_objects_dereference(
{
const exprt &pointer=deref.pointer();
get_objects_rec(get_modet::READ, pointer);
if(mode!=get_modet::READ)
get_objects_rec(mode, pointer);

// we don't have points-to information, dereferencing will yield some
// in-memory object
const symbolt &memory_symbol = ns.lookup(CPROVER_PREFIX "memory");
get_objects_rec(mode, memory_symbol.symbol_expr(), -1, size);
}

void rw_range_sett::get_objects_byte_extract(
Expand Down Expand Up @@ -413,14 +416,13 @@ void rw_range_sett::get_objects_typecast(

void rw_range_sett::get_objects_address_of(const exprt &object)
{
if(object.id()==ID_string_constant ||
if(object.id()==ID_symbol ||
object.id()==ID_string_constant ||
object.id()==ID_label ||
object.id()==ID_array ||
object.id()=="NULL-object")
// constant, nothing to do
return;
else if(object.id()==ID_symbol)
get_objects_rec(get_modet::READ, object);
else if(object.id()==ID_dereference)
get_objects_rec(get_modet::READ, object);
else if(object.id()==ID_index)
Expand Down Expand Up @@ -563,11 +565,6 @@ void rw_range_sett::get_objects_rec(
{
// dereferencing may yield some weird ones, ignore these
}
else if(mode==get_modet::LHS_W)
{
forall_operands(it, expr)
get_objects_rec(mode, *it);
}
else
throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled";
}
Expand Down Expand Up @@ -620,6 +617,13 @@ void rw_range_set_value_sett::get_objects_dereference(
if(object.is_not_nil() &&
!value_set_dereferencet::has_dereference(object))
get_objects_rec(mode, object, range_start, new_size);
else
{
// we don't have sufficient points-to information, dereferencing will yield
// some in-memory object
const symbolt &memory_symbol = ns.lookup(CPROVER_PREFIX "memory");
get_objects_rec(mode, memory_symbol.symbol_expr(), -1, size);
}
}

void guarded_range_domaint::output(
Expand Down