2021-03-05 08:16 CET
  

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 Files
  • c file icon label_pointer.c (140 bytes) 2020-03-10 07:18 - 
    /*@
  requires 0 < n;
  requires \valid(a + (0..n-1));
*/
void foo(int* a, int n)
{
   int m = 0;
   //@ assert a[m] == \at(a[m],Here);
}
    c file icon label_pointer.c (140 bytes) 2020-03-10 07:18 +

-Relationships
+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 );
...
}
+Notes

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