Frama-C Bug Tracking System - Frama-C
View Issue Details
0002500Frama-CKernel > ACSL implementationpublic2020-03-10 07:182020-03-20 15:09
closedno change required 
linux, macOS
Frama-C 20-Calcium 
0002500: unbound logic variable warning for local variable
When processing the following lines /*@ requires 0 < n; requires \valid(a + (0..n-1)); */ void foo(int* a, int n) { int m = 0; //@ assert a[m] == \at(a[m],Pre); } with 'frama-c -wp label_pointer.c ', I obtain the following error message for the assertion. [kernel] Parsing label_pointer.c (with preprocessing) [kernel:annot-error] label_pointer.c:9: Warning: unbound logic variable m. Ignoring code annotation [kernel] User Error: warning annot-error treated as fatal error. [kernel] User Error: stopping on file "label_pointer.c" that has errors. Add '-kernel-msg-key pp' for preprocessing command. [kernel] Frama-C aborted: invalid user input. To me this looks like a bug or am I missing something crucial here? (The message does NOT appear when 'Pre' is replaced by 'Here'.)
No tags attached.
c label_pointer.c (140) 2020-03-10 07:18
Issue History
2020-03-10 07:18jensNew Issue
2020-03-10 07:18jensStatusnew => assigned
2020-03-10 07:18jensAssigned To => correnson
2020-03-10 07:18jensFile Added: label_pointer.c
2020-03-11 17:40signolesCategoryPlug-in > wp => Kernel > ACSL implementation
2020-03-11 17:40signolesAssigned Tocorrenson => signoles
2020-03-11 17:41signolesNote Added: 0006959
2020-03-11 17:41signolesStatusassigned => closed
2020-03-11 17:41signolesResolutionopen => no change required
2020-03-11 17:48jensNote Added: 0006960
2020-03-11 17:48jensStatusclosed => feedback
2020-03-11 17:48jensResolutionno change required => reopened
2020-03-16 12:29corrensonNote Added: 0006961
2020-03-16 12:30corrensonStatusfeedback => resolved
2020-03-16 12:30corrensonResolutionreopened => no change required
2020-03-20 15:09signolesStatusresolved => closed

2020-03-11 17:41   
The pre-state of a function (corresponding to Pre) is a program point in which the locals do not exist (but the formals do exist). Therefore \at(m, Pre) is meaningless in your example.
2020-03-11 17:48   
Sure, 'm' is local and '\at(m,Pre)' does not make sense. However, I am using 'm' as an index to the array argument 'a'. To me the assertion "assert a[m] == \at(a[m],Pre)" makes sense.
2020-03-16 12:29   
No it does not make sense, since Pre label is by definition *before* the function body is beginning. However, you can add a label just after its declaration to solve the problem. void foo(...) { int m ; A: ... \at( a[m] , A ); ... }