fix for non-byte array byte_extract flattening
This commit is contained in:
parent
0779bbd701
commit
7d78d58028
|
@ -1,4 +1,4 @@
|
||||||
KNOWNBUG
|
CORE
|
||||||
main.c
|
main.c
|
||||||
|
|
||||||
^EXIT=0$
|
^EXIT=0$
|
||||||
|
|
|
@ -0,0 +1,31 @@
|
||||||
|
#include <assert.h>
|
||||||
|
#include <stdlib.h>
|
||||||
|
|
||||||
|
extern int nondet_int();
|
||||||
|
|
||||||
|
int main() {
|
||||||
|
|
||||||
|
int arraylen=nondet_int();
|
||||||
|
|
||||||
|
if(arraylen==3)
|
||||||
|
{
|
||||||
|
int** array_init = malloc(sizeof(int *)*arraylen);
|
||||||
|
|
||||||
|
// mis-align that pointer!
|
||||||
|
char * char_ptr = (char *) array_init;
|
||||||
|
char_ptr++;
|
||||||
|
|
||||||
|
int local_var;
|
||||||
|
|
||||||
|
int **array2=(int**)char_ptr;
|
||||||
|
|
||||||
|
// write
|
||||||
|
array2[0]=&local_var;
|
||||||
|
|
||||||
|
// check
|
||||||
|
int value=*array2[0];
|
||||||
|
|
||||||
|
assert(value==local_var);
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
|
@ -0,0 +1,8 @@
|
||||||
|
CORE
|
||||||
|
main.c
|
||||||
|
|
||||||
|
^EXIT=0$
|
||||||
|
^SIGNAL=0$
|
||||||
|
^VERIFICATION SUCCESSFUL$
|
||||||
|
--
|
||||||
|
^warning: ignoring
|
|
@ -117,7 +117,7 @@ exprt flatten_byte_extract(
|
||||||
for(mp_integer i=0; i<num_elements; ++i)
|
for(mp_integer i=0; i<num_elements; ++i)
|
||||||
{
|
{
|
||||||
// the most significant byte comes first in the concatenation!
|
// the most significant byte comes first in the concatenation!
|
||||||
plus_exprt index(first_index, from_integer(i, offset_type));
|
plus_exprt index(first_index, from_integer(num_elements-i-1, offset_type));
|
||||||
concat.copy_to_operands(index_exprt(root, index));
|
concat.copy_to_operands(index_exprt(root, index));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue