Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000071Frama-CPlug-in > jessiepublic2009-04-30 14:322010-12-09 19:19
Reporterbobot 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Beryllium-20090902 
Summary0000071: labels are not correctly translated in jessie+why
DescriptionAn 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 Informationframa-c release 5186
TagsNo 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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker