0000381: propagation of \result clauses - Frama-C Bug Tracking System

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

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000381

Frama-C

Plug-in > Eva

public

2010-01-21 17:19

2014-02-12 16:56

Reporter

lalande

Assigned To

pascal

Priority

normal

Severity

feature

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Beryllium-20090901

Target Version

Fixed in Version

Frama-C Boron-20100401

Summary

0000381: propagation of \result clauses

Description

Hello, when discovering Frama-C, I tried to specify some clauses on some functions to specify constraints on the return statement. But it seems that the "ensures" clauses that are "unknown" are not propagated after the analysis of the function. For example: /*@ensures \result >= 0; @ensures \result <= 10; int fonc() { int y = rand(); return y; } int main() { u = fonc(); } gives y in [--;--] u in [--;--] The @assert seems to be propagated, whereas the constraints on \result not. I got a response of one of the developer that says that this is in the TODO list... Is it right ? Best regards, JF Lalande.

Additional Information

Frama-C Beryllium 2009-09-01

Tags

No tags attached.

Attached Files

Relationships

Notes
(0000648) signoles (manager) 2010-01-21 17:36	See also the today thread on Frama-C discuss : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-January/001759.html.

(0000712) pascal (reporter) 2010-02-23 22:49 edited on: 2010-02-23 22:50	Fixing miscellaneous syntax errors in the example, the development versin now produces: [value] Values for function main: u IN [0..10] Note that you can also write 0 <= u <= 10 ; for the post-condition, it is a tad more concise.

Issue History
Date Modified	Username	Field	Change
2010-01-21 17:19	lalande	New Issue
2010-01-21 17:35	signoles	Relationship added	duplicate of 0000074
2010-01-21 17:36	signoles	Note Added: 0000648
2010-01-21 17:36	signoles	Assigned To	=> pascal
2010-01-21 17:36	signoles	Status	new => assigned
2010-01-21 17:36	signoles	Category	kernel => plug-in > value analysis
2010-01-21 17:36	signoles	Additional Information Updated
2010-02-23 22:49	pascal	Note Added: 0000712
2010-02-23 22:50	pascal	Note Edited: 0000712
2010-02-23 22:51	pascal	Status	assigned => resolved
2010-02-23 22:51	pascal	Fixed in Version	=> Frama-C Bore
2010-02-23 22:51	pascal	Resolution	open => fixed
2010-04-13 15:30	signoles	Status	resolved => new
2010-04-13 15:31	signoles	Status	new => closed
2018-01-12 14:26	signoles	Category	Plug-in > value analysis => Plug-in > Eva