Should we define base\_addr and block\_length on null ? about acsl HOT 4 OPEN

@jensgerlach @pbaudin @backtracking for comments

I'd rather leave them undefined (as they are for any invalid pointer), but if they are to be defined, I'd go for \base_addr(\null) == -1, as they are (or were) systems where 0 is a valid numeric address. There aren't any (valid) memory blocks of size 0, thus \block_length(\null) == 0 would be OK.

from acsl.

First point, \base_addr doesn't return a numerical value but a char* pointer:
\base_addr{L}(p): void* -> char*. It cannot be -1, perhaps (char*)-1. It seems to be a better choice than (char*)0:

Looking at the ACSL definition of \offset and \valid_read (in the same section than \base_addr)
the following values are consistent with \valid_read(\null)<==>\false:

• \base_addr(\null) == char*(-1)
• \block_length(\null)==0
• \offset(\null) == 1
  what ever is the positive or null value of sizeof(void*).

Choosing \base_addr(\null) = (char*)0 = \null gives \offset(null)==0. To ensures \valid_read(\null)<==>\false, the following constraint sizeof(void*)>0 has be to true! It is not a good choice to get such a constraint. I won't be able to infer that and rather prefer to keep sizeof(void*) completely undefined.

from acsl.

Any way, as @vprevosto, I'd rather leave these 3 constructs undefined.

from acsl.

So would I (leave undefined). If not, I would strongly vote for not having \base_addr(\null) == char*(-1), as a negative pointer seems like a bad idea.

from acsl.