Frama-C Bug Tracking System - Frama-C
View Issue Details
0000932Frama-CKernelpublic2011-08-23 16:092014-02-12 16:58
signoles 
signoles 
lowtweakalways
closedfixed 
Frama-C Carbon-20110201 
Frama-C Oxygen-20120901 
0000932: Journalisation of dynamic functions using abstract types does not work
All in the title...
With the attached files, run:

$ frama-c -load-script cpt.ml -load-script use.ml -journal-enable

Then read the generated journal.
For fixing this issue, the journal must generate "let module" in such cases.
No tags attached.
? use.ml (391) 2011-08-23 16:09
https://bts.frama-c.com/file_download.php?file_id=264&type=bug
Issue History
2011-08-23 16:09signolesNew Issue
2011-08-23 16:09signolesStatusnew => assigned
2011-08-23 16:09signolesAssigned To => signoles
2011-08-23 16:09signolesFile Added: use.ml
2011-08-23 16:10signolesNote Added: 0002163
2011-08-23 16:10signolesStatusassigned => confirmed
2012-07-31 11:48svnCheckin
2012-07-31 11:48svnStatusconfirmed => resolved
2012-07-31 11:48svnResolutionopen => fixed
2012-07-31 11:48signolesNote Added: 0003343
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2014-02-12 16:58signolesNote Added: 0004629
2014-02-12 16:58signolesStatusclosed => resolved

Notes
(0002163)
signoles   
2011-08-23 16:10   
Seem not possible to load 2 different files... Here is cpt.ml:

let mk () = ref 0
let incr c = incr c; !c

include Datatype.Make(struct
  (* order of lines below does matter *)
  include Datatype.Serializable_undefined
  include Datatype.Ref(Datatype.Int)
  let name = "Cpt.t"
end)

let mk =
  Dynamic.register
    ~journalize:true
    ~plugin:"Cpt"
    "mk"
    (Datatype.func Datatype.unit ty) mk

let incr =
  Dynamic.register
    ~journalize:true
    ~plugin:"Cpt"
    "incr"
    (Datatype.func ty Datatype.int)
    incr
(0003343)
signoles   
2012-07-31 11:48   
Generating "let module" in journal is pretty cool :).
(0004629)
signoles   
2014-02-12 16:58   
Fix committed to stable/neon branch.