Closed dz333 closed 1 year ago
This is the same as #15 except for arrays.
For any arrays with sequential type and dependent labels,
For each index, i in the bounds of the array, we must generate a check similar to #15.
i
For example, assume all of the assignments to array arr are: [ arr[x] -> {a}, arr[y] -> {b} ]
arr
[ arr[x] -> {a}, arr[y] -> {b} ]
Then we must prove: forall i in {0...len-1}. if !((i == x && a) or (i == y && b)) then L(arr[i]) flows to L(next arr[i])
forall i in {0...len-1}. if !((i == x && a) or (i == y && b)) then L(arr[i]) flows to L(next arr[i])
We can statically generate 1 check for each possible i (This will probably help out z3 rather than adding another forall).
forall
Completed!
dz333
commented
1 year ago dz333
commented
1 year ago
This is the same as #15 except for arrays.
For any arrays with sequential type and dependent labels,
For each index,
iin the bounds of the array, we must generate a check similar to #15.For example, assume all of the assignments to array
arrare:[ arr[x] -> {a}, arr[y] -> {b} ]Then we must prove:
forall i in {0...len-1}. if !((i == x && a) or (i == y && b)) then L(arr[i]) flows to L(next arr[i])We can statically generate 1 check for each possible
i(This will probably help out z3 rather than adding anotherforall).