0002500: unbound logic variable warning for local variable

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

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

label_pointer.c [^] (140 bytes) 2020-03-10 07:18 [Show Content] [Hide Content]

/*@
  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);
}

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