Unbound logic variable warning when using .. to specify array length, i.e. \valid(buckets+(0..{x})), when {x} is a global variable

[sabrina-reis]

I wanted to bring this behavior of the ACSL parser to other people's attention. On the whole, whitespace is not an issue for the ACSL parser, so I did not anticipate this issue and I did not see it mentioned in the manual or on the web.

Let's say I have the following C code:

# define NUMBUCKETS 5
uint32_t buckets[NUMBUCKETS];

/*@                                                                                                                                                 
@ requires \valid(buckets+(0..NUMBUCKETS));                                                                     
@*/  
 void init_buckets();

When I run frama-c on this code with -wp, I get the following error:

Warning: unbound logic variable NUMBUCKETS. Ignoring specification of function init_buckets

The issue disappears when I put a space after .. like so:

@ requires \valid(buckets+(0.. NUMBUCKETS));                                                                     

The ACSL manual should probably bring attention to the fact that whitespace is needed for parsing here if you're using a global variable.

[vprevosto]

Thanks for your report.

The issue with NUMBUCKETS is known and might indeed deserve to be reported explicitly in the ACSL manual. Basically, the C preprocessor must treat 0..NUMBUCKETS as a preprocessing number token, as per Section 6.4.8 of the C standard (C11 and C17, but if I'm not mistaken C99 has the same clause), so that it won't see NUMBUCKETS as a separate token.

On the other hand, I don't have any issue with \valid(buckets+(0..1)), at least on a very quick check. Which version of Frama-C are you using? Could you provide a complete example reproducing the problem?

[sabrina-reis]

Thanks for your response, Virgile. I couldn't reproduce the issue with the int literals this morning. I'll edit my report to make clear this is just a problem with global variables. I appreciate your clarification on the origin of this problem and hope that this report helps develop more thorough documentation for ACSL.