replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Use a known constant offset when dereferencing

This commit is contained in:
Michael Tautschnig 2017-01-06 23:57:30 +00:00 committed by Michael Tautschnig
parent c507ccfd00
commit cc659c9689
1 changed files with 5 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/pointer-analysis/value_set_dereference.cpp
View File

@ -559,7 +559,11 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
result.value=o.root_object();
// this is relative to the root object
const exprt offset=pointer_offset(pointer_expr);
exprt offset;
if(o.offset().id()==ID_unknown)
offset=pointer_offset(pointer_expr);
else
offset=o.offset();
if(memory_model(result.value, dereference_type, tmp_guard, offset))
{