0000071: labels are not correctly translated in jessie+why

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000071

Frama-C

Plug-in > jessie

public

2009-04-30 14:32

2010-12-09 19:19

Reporter

bobot

Assigned To

cmarche

Priority

normal

Severity

major

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 Beryllium-20090902

Summary

0000071: labels are not correctly translated in jessie+why

Description

An example with a label in a ghost (or not) statement, label.c : =============== void myfun(int p){ p = 1; //@ ghost Mylabel: p = 2; //@ assert \at(p,Mylabel)==p-1; } ==================== Why complains about an unbound label. frama-c -jessie-analysis label.c : =================================== [...] File "why/label.why", line 350, characters 30-47: Unbound label 'Mylabel' =================================== In fact the label is defined in the jessie file. label.jc : =================================== unit myfun(int32 p) behavior default: assumes true; ensures (C_4 : true); { { (C_1 : (p = 1)); (Mylabel : ()); (C_2 : (p = 2)); { (assert for default: (C_3 : (\at(p,Mylabel) == (p - 1)))); () }; (return ()) } } ==================================== and in the why file, but perhaps not well scoped. why/label.why : ==================================== let myfun_safety = fun (p : int32) -> { (JC_4: true) } (let mutable_p = ref p in (init: try begin (C_1: (let jessie_1 = (mutable_p := (safe_int32_of_integer_ (1))) in void)); (Mylabel: (let jessie_2 = (mutable_p := (safe_int32_of_integer_ (2))) in void)); [ { } unit reads mutable_p { (JC_9: eq_int(integer_of_int32(mutable_p@Mylabel), sub_int(integer_of_int32(mutable_p), (1)))) } ]; void; (raise Return); (raise Return) end with Return -> void end)) { true } =================================

Additional Information

frama-c release 5186

Tags

No tags attached.

Attached Files

Relationships

Notes
(0000085) cmarche (developer) 2009-05-22 15:44	fixed in jessie tool (translation for jc to why was buggy)

(0000093) bobot (administrator) 2009-05-25 14:55	If an assert precede the label, the label is still not well scoped : label.c : =============== void myfun(int p){ p = 1; //@ assert \true; //@ ghost Mylabel: p = 2; //@ assert \at(p,Mylabel)==p-1; } ================

(0000464) signoles (manager) 2009-10-15 12:26	Fixed in Why 2.21

Issue History
Date Modified	Username	Field	Change
2009-04-30 14:32	bobot	New Issue
2009-04-30 14:59	signoles	Relationship added	duplicate of 0000063
2009-04-30 16:47	monate	Status	new => assigned
2009-04-30 16:47	monate	Assigned To	=> cmarche
2009-05-22 15:44	cmarche	Note Added: 0000085
2009-05-22 15:47	cmarche	Status	assigned => closed
2009-05-22 15:47	cmarche	Resolution	open => fixed
2009-05-25 14:55	bobot	Note Added: 0000093
2009-05-25 14:55	bobot	Status	closed => feedback
2009-05-25 14:55	bobot	Resolution	fixed => reopened
2009-06-05 12:32	cmarche	Status	feedback => acknowledged
2009-10-15 10:40	cmarche	Status	acknowledged => resolved
2009-10-15 12:25	signoles	Status	resolved => closed
2009-10-15 12:25	signoles	Fixed in Version	=> Frama-C Beryllium 2
2009-10-15 12:26	signoles	Note Added: 0000464
2010-12-09 19:19	signoles	Resolution	reopened => fixed