Closed fleupold closed 5 years ago
Remove pointer arithmetic (e.g(bit*)foo + 3). Instead, pass along the offset (in the example that would be 3) and only use it when a single item is accessed (e.g. foo[i] --> foo[offset + i]).
(bit*)foo + 3
foo[i] --> foo[offset + i]
The reason for that is that pointer arithmetic leads to a constraint explosion in pepper and thus needs to be avoided. For more background see https://github.com/pepper-project/pequin/issues/35.
Remove pointer arithmetic (e.g
(bit*)foo + 3). Instead, pass along the offset (in the example that would be 3) and only use it when a single item is accessed (e.g.foo[i] --> foo[offset + i]).The reason for that is that pointer arithmetic leads to a constraint explosion in pepper and thus needs to be avoided. For more background see https://github.com/pepper-project/pequin/issues/35.