smackers
False alarm when the integer encoding is wrapped integer
Consider the following program (a C version of test/rust/array.rs),
#include "smack.h"
#include <stdlib.h>
int main() {
int* arr = (int*)malloc(3*sizeof(int));
unsigned long long idx = __VERIFIER_nondet_unsigned_long_long();
assume(arr[0] < 4);
assume(arr[1] < 5);
assume(arr[2] < 6);
assume(idx < 3);
assert(arr[idx] <= 5);
}
SMACK verifies it when the default integer encoding is used while reports an error when wrapped integer is used. This is because idx can get a value -2**64 which satisfies the assumptions ($ule.i64(idx, -1) && $uge.i64(idx, 0)) in __VERIFIER_nondet_unsigned_long_long. However, arr[-2**64] is clearly uninitialized and thus leads to an error.
One possible solution is to wrap the arguments of the pointer arithmetic using the $tos function.
Sorry, but what should be the expected outcome of verifying this program? Thx!
Sorry, but what should be the expected outcome of verifying this program? Thx!
It should be verified.