Skip to content

GitLab

  • Menu
Projects Groups Snippets
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2332

Closed
Open
Created Apr 30, 2009 by François Bobot@bobotOwner

labels are not correctly translated in jessie+why

ID0000071: This issue was created automatically from Mantis Issue 71. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000071 Frama-C Plug-in > jessie public 2009-04-30 2010-12-09
Reporter bobot Assigned To cmarche Resolution fixed
Priority normal Severity major Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C GIT, precise the release id Target Version - Fixed in Version Frama-C Beryllium-20090902

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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking