Frama-C Bug Tracking System - Frama-C
View Issue Details
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.
Relationships
Attached Filesc label_pointer.c (140) 2020-03-10 07:18
https://bts.frama-c.com/file_download.php?file_id=1346&type=bug

Notes
(0006959)
signoles   
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   
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   
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 ModifiedUsernameFieldChange
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