unbound logic variable warning for local variable
ID0002500: This issue was created automatically from Mantis Issue 2500. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002500 | Frama-C | Kernel > ACSL implementation | public | 2020-03-10 | 2020-03-20 |
| Reporter | jens | Assigned To | signoles | Resolution | no change required |
| Priority | high | Severity | major | Reproducibility | always |
| Platform | - | OS | linux, macOS | OS Version | - |
| Product Version | Frama-C 20-Calcium | Target Version | - | Fixed in Version | - |
Description :
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'.)