0001670: WP ignores some goals when 'initialized' is used in hypotheses

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

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001670

Frama-C

Plug-in > wp

public

2014-03-04 09:36

2015-03-17 22:17

Reporter

Anne

Assigned To

correnson

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Target Version

Fixed in Version

Frama-C Sodium

Summary

0001670: WP ignores some goals when 'initialized' is used in hypotheses

Description

The message:

[wp] warning: Allocable, Freeable, Valid_read, Fresh and Initialized not yet implemented

is perfectly clear, but I would have expected that annotations using these predicates would have been ignored. Instead of that, proof obligations of other annotations simply disappear.

Steps To Reproduce

Example:
/*@ requires r1: \initialized(Y+(0 .. 99));
    assigns X[0..99];
    ensures X[0] == Y[0];
*/
void cp( int *X, int *Y );

void f (int *A, int *B) {
  cp(B, A);
  /*@ assert a1: A[0] == B[0]; */
}

Without the 'requires' property, the assertion is proved:
$ frama-c -wp test.c -wp-prop a1
...
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_f_assert_a1 : Valid
[wp] Proved goals: 1 / 1
     Qed: 1

With the 'requires' property, the assertion is not even scheduled as a goal:
$ frama-c -wp test.c -wp-prop a1
...
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0

Tags

No tags attached.

Attached Files

Relationships

Notes
(0005180) correnson (manager) 2014-06-02 15:38	Fix committed to master branch.

Issue History
Date Modified	Username	Field	Change
2014-03-04 09:36	Anne	New Issue
2014-03-04 09:36	Anne	Status	new => assigned
2014-03-04 09:36	Anne	Assigned To	=> correnson
2014-06-02 15:38	correnson	Note Added: 0005180
2014-06-02 15:38	correnson	Status	assigned => resolved
2014-06-02 15:38	correnson	Resolution	open => fixed
2015-03-17 22:17	signoles	Fixed in Version	=> Frama-C Sodium
2015-03-17 22:17	signoles	Status	resolved => closed