View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002500 | Frama-C | Kernel > ACSL implementation | public | 2020-03-10 07:18 | 2020-03-20 15:09 | ||||
Reporter | jens | ||||||||
Assigned To | signoles | ||||||||
Priority | high | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | no change required | ||||||
Platform | OS | linux, macOS | OS Version | ||||||
Product Version | Frama-C 20-Calcium | ||||||||
Target Version | Fixed in Version | ||||||||
Summary | 0002500: unbound logic variable warning for local variable | ||||||||
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'.) | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
signoles (manager) 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. |
jens (reporter) 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. |
correnson (manager) 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 ); ... } |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2020-03-10 07:18 | jens | New Issue | |
2020-03-10 07:18 | jens | Status | new => assigned |
2020-03-10 07:18 | jens | Assigned To | => correnson |
2020-03-10 07:18 | jens | File Added: label_pointer.c | |
2020-03-11 17:40 | signoles | Category | Plug-in > wp => Kernel > ACSL implementation |
2020-03-11 17:40 | signoles | Assigned To | correnson => signoles |
2020-03-11 17:41 | signoles | Note Added: 0006959 | |
2020-03-11 17:41 | signoles | Status | assigned => closed |
2020-03-11 17:41 | signoles | Resolution | open => no change required |
2020-03-11 17:48 | jens | Note Added: 0006960 | |
2020-03-11 17:48 | jens | Status | closed => feedback |
2020-03-11 17:48 | jens | Resolution | no change required => reopened |
2020-03-16 12:29 | correnson | Note Added: 0006961 | |
2020-03-16 12:30 | correnson | Status | feedback => resolved |
2020-03-16 12:30 | correnson | Resolution | reopened => no change required |
2020-03-20 15:09 | signoles | Status | resolved => closed |