Skip to content

Commit 2a977f6

Browse files
author
Daniel Kroening
committed
do big-endian arrays with flatten_byte_extract
1 parent d00dee3 commit 2a977f6

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

src/solvers/flattening/flatten_byte_operators.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,10 @@ exprt flatten_byte_extract(
117117
for(mp_integer i=0; i<num_elements; ++i)
118118
{
119119
// the most significant byte comes first in the concatenation!
120-
plus_exprt index(first_index, from_integer(num_elements-i-1, offset_type));
120+
mp_integer index_offset=
121+
little_endian?(num_elements-i-1):i;
122+
123+
plus_exprt index(first_index, from_integer(index_offset, offset_type));
121124
concat.copy_to_operands(index_exprt(root, index));
122125
}
123126

0 commit comments

Comments
 (0)