Byte offset to array index translation must use array type
When dereferencing a void* pointer, the dereferenced type would always be considered compatible with the underlying object type. Nevertheless they are not actually the same. If the object was an array and the byte offset non-zero, the use of void* would yield the wrong index. The correct way to compute the index is using the actual (array) object type. Fixes: #1857
This commit is contained in:
parent
f4fb09948a
commit
9df769a466
|
@ -0,0 +1,18 @@
|
||||||
|
#include <assert.h>
|
||||||
|
#include <string.h>
|
||||||
|
|
||||||
|
int main()
|
||||||
|
{
|
||||||
|
int A[3] = {1, 2, 3};
|
||||||
|
int *p = A;
|
||||||
|
int v1, v2;
|
||||||
|
|
||||||
|
memcpy(&v1, p, sizeof(int));
|
||||||
|
++p;
|
||||||
|
memcpy(&v2, p, sizeof(int));
|
||||||
|
|
||||||
|
assert(v1 == 1);
|
||||||
|
assert(v2 == 2);
|
||||||
|
|
||||||
|
return 0;
|
||||||
|
}
|
|
@ -0,0 +1,8 @@
|
||||||
|
CORE
|
||||||
|
main.c
|
||||||
|
|
||||||
|
^EXIT=0$
|
||||||
|
^SIGNAL=0$
|
||||||
|
^VERIFICATION SUCCESSFUL$
|
||||||
|
--
|
||||||
|
^warning: ignoring
|
|
@ -508,10 +508,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
|
||||||
exprt adjusted_offset;
|
exprt adjusted_offset;
|
||||||
|
|
||||||
// are we doing a byte?
|
// are we doing a byte?
|
||||||
mp_integer element_size=
|
mp_integer element_size =
|
||||||
dereference_type.id()==ID_empty?
|
pointer_offset_size(root_object_type.subtype(), ns);
|
||||||
pointer_offset_size(char_type(), ns):
|
|
||||||
pointer_offset_size(dereference_type, ns);
|
|
||||||
|
|
||||||
if(element_size==1)
|
if(element_size==1)
|
||||||
{
|
{
|
||||||
|
@ -520,7 +518,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
|
||||||
}
|
}
|
||||||
else if(element_size<=0)
|
else if(element_size<=0)
|
||||||
{
|
{
|
||||||
throw "unknown or invalid type size of:\n"+dereference_type.pretty();
|
throw "unknown or invalid type size of:\n" +
|
||||||
|
root_object_type.subtype().pretty();
|
||||||
}
|
}
|
||||||
else
|
else
|
||||||
{
|
{
|
||||||
|
|
Loading…
Reference in New Issue