Skip to content

Commit 2cfd2f3

Browse files
author
kroening
committed
pointer accesses
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@1049 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
1 parent fbf72f1 commit 2cfd2f3

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

src/pointer-analysis/dereference.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -852,6 +852,15 @@ bool dereferencet::memory_model(
852852
return memory_model_conversion(value, to_type, guard, offset);
853853
}
854854

855+
// we are willing to do the same for pointers
856+
857+
if(from_type.id()==ID_pointer &&
858+
to_type.id()==ID_pointer)
859+
{
860+
if(bv_width(from_type)==bv_width(to_type))
861+
return memory_model_conversion(value, to_type, guard, offset);
862+
}
863+
855864
// otherwise, we will stich it together from bytes
856865

857866
return memory_model_bytes(value, to_type, guard, offset);

0 commit comments

Comments
 (0)