0000895: Proof obligations of lemma properties

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000895

Frama-C

Plug-in > wp

public

2011-07-28 08:29

2012-09-19 17:16

Reporter

patrick

Assigned To

correnson

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C GIT, precise the release id

Target Version

Fixed in Version

Frama-C Oxygen-20120901

Summary

0000895: Proof obligations of lemma properties

Description

Proof obligations of lemma properties are not generated.

Revision: 14360

Additional Information

cat test_po_lemma1.c
//@ lemma l: 2 == 1 + 1 ;
//@ ensures p: \true ;
void f (void) {
return ;
}

> frama-c -wp -wp-model Store test_po_lemma1.c -wp-warnings
test_po_lemma1.c:1:[wp] warning: Proof obligation for property 'l' not generated.

Tags

No tags attached.

Attached Files

Relationships

Notes
(0003252) correnson (manager) 2012-07-06 15:18	Fixed for Typed model (other models will be deprecated soon).

Issue History
Date Modified	Username	Field	Change
2011-07-28 08:29	patrick	New Issue
2011-07-28 08:29	patrick	Status	new => assigned
2011-07-28 08:29	patrick	Assigned To	=> correnson
2012-07-06 15:18	correnson	Note Added: 0003252
2012-07-06 15:18	correnson	Status	assigned => resolved
2012-07-06 15:18	correnson	Resolution	open => fixed
2012-09-19 17:15	signoles	Fixed in Version	=> Frama-C Oxygen-20120901
2012-09-19 17:16	signoles	Status	resolved => closed