0001353: ACSL label LoopEntry not handled by WP

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001353

Frama-C

Plug-in > wp

public

2013-01-30 16:58

2014-03-13 15:57

Reporter

Anne

Assigned To

correnson

Priority

normal

Severity

minor

Reproducibility

have not tried

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Oxygen-20120901

Target Version

Fixed in Version

Frama-C Neon-20140301

Summary

0001353: ACSL label LoopEntry not handled by WP

Description

As said in the title, the ACSL label LoopEntry seems to be not handled by WP but it is accepted by the kernel.
Using the -wp-warnings option I got warnings like :
- Warning: Generalization of un-labeled values
Reason: Some labels may escape the control flow
but it took me some time to understand the problem.

In the example below, changing LoopEntry by L in the loop invariant makes it work.

BTW, in the example below, it doesn't work either when removing the first (c++;) statement !

Additional Information

int G;
//@ requires G == 0; ensures G == 0;
void f (int c) {
  c++;
  L: //@ loop invariant G == \at (G, LoopEntry);
  while (c) c++;
}

Tags

No tags attached.

Attached Files

Relationships

Notes
(0004562) correnson (manager) 2014-02-12 16:57	Fix committed to stable/neon branch.

Issue History
Date Modified	Username	Field	Change
2013-01-30 16:58	Anne	New Issue
2013-01-30 16:58	Anne	Status	new => assigned
2013-01-30 16:58	Anne	Assigned To	=> correnson
2013-07-26 14:49	svn	Checkin
2013-07-29 14:49	virgile	Relationship added	related to 0001462
2013-07-29 14:59	virgile	Relationship deleted	related to 0001462
2013-07-30 17:46	svn	Checkin
2013-07-30 17:46	svn	Status	assigned => resolved
2013-07-30 17:46	svn	Resolution	open => fixed
2014-02-12 16:57	correnson	Note Added: 0004562
2014-03-13 15:56	signoles	Fixed in Version	=> Frama-C Neon-20140301
2014-03-13 15:57	signoles	Status	resolved => closed