View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | 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 | ||||||
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 |
|
![]() |
|
cmarche (developer) 2009-05-22 15:44 |
fixed in jessie tool (translation for jc to why was buggy) |
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; } ================ |
signoles (manager) 2009-10-15 12:26 |
Fixed in Why 2.21 |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2009-04-30 14:32 | bobot | New Issue | |
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 |