Error: block size must be a multiple of size #9

yuzeng2333 · 2022-01-31T17:49:41Z

I am doing a simple experiment with arrays in c. The c code is:

`int vec0[5];

int vec_func(int num) {
vec0[0] = 1;
vec0[1] = 2;
vec0[2] = 3;
vec0[3] = 4;
vec0[4] = 5;

return vec0[num];
}`

And here is the partial code for checking:

`(define (check-vec)
(parameterize ([llvm:current-machine (llvm:make-machine cpp:symbols cpp:globals)])

; symbolic inputs
(define-symbolic num (bitvector 32))

; symbolic result
(define r (cpp:@vec_func num))

(define sol
  (solve
   (begin
     (assume (bvsle num 5))
     (assert (not equal? r 3))
    )
  )
)
sol

))

`
But when I ran the checking, an error is reported:

[assert] ~/serval/serval/lib/memory/mblock.rkt:254 mcell-path: block size (bv #x0000000000000001 64) must be a multiple of size (bv #x0000000000000004 64)

I am writing and reading int from the array, so the block size should be 4 byte. why the error says block size is #x0000000000000001?
It seems the "element-size" in mblock.rkt has some problem: it always returns 1 for the integer array, even though its element type is int.

Update: I just find the same error happens for provided array.c in the test folder.

The text was updated successfully, but these errors were encountered:

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Error: block size must be a multiple of size #9

Error: block size must be a multiple of size #9

Error: block size must be a multiple of size #9

Error: block size must be a multiple of size #9

Comments

Uh oh!