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'.) ## Attachments - [label_pointer.c](/uploads/ef51b56f81d231eaedc46a0d2aea401e/label_pointer.c)