Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002500Frama-CKernel > ACSL implementationpublic2020-03-10 07:182020-03-20 15:09
Reporterjens 
Assigned Tosignoles 
PriorityhighSeveritymajorReproducibilityalways
StatusclosedResolutionno change required 
PlatformOSlinux, macOSOS Version
Product VersionFrama-C 20-Calcium 
Target VersionFixed in Version 
Summary0002500: unbound logic variable warning for local variable
DescriptionWhen 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'.)
TagsNo tags attached.
Attached Filesc file icon label_pointer.c [^] (140 bytes) 2020-03-10 07:18 [Show Content]

- Relationships

-  Notes
(0006959)
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.
(0006960)
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.
(0006961)
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 ); ... }

- Issue History
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


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker