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.