Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001441Frama-CKernelpublic2013-06-04 14:162014-03-13 15:57
ReporterAnne 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130501 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001441: frama-c.toplevel not working anymore
DescriptionI already reported this in the mailing list, and I understand that you don't have time to fix this, but I open an issue anyway to store some information. I noticed two different problems : (1) $ make top report conflicts (warning 31) about ocaml and frama-c modules Subst and Config. 1a/ Subst seems not used anymore : could be removed ? 1b/ maybe Config could be renamed ? (2) $ bin/toplevel.top -h shows frama-c help. So it seems that this is not an ocaml toplevel. At the end of toplevel_boot.ml, replacing : < Cmdline.catch_toplevel_run ... by > !Db.Toplevel.run (fun () -> ()) and compiling again gives back an ocaml toplevel (but still not fully working because of the module problem (1)).
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0003936)
signoles (manager)
2013-06-04 16:11

About (1): Subst is still used in a CEA's internal plug-in. So it is not removable right now. Renaming is a solution (both for Subst and Config). But renaming Frama-C modules each time OCaml introduces new ones is not doable on the long-term, in particular if we want to tend towards a stable API. We have to find a more stable solution (packing?). About (2): - toplevel_boot.ml is actually automatically generated by Makefile. So it is not so easy to modify a subpart. - One need to clarify which semantics one exactly wants to have for a Frama-C toplevel... As far as I know, you are the only developer who ever used it and even who would like to get a Frama-C toplevel. So there is arguably at least not a strong need from the community nor from any customer to get one ;-).
(0003937)
Anne (reporter)
2013-06-04 16:17

Maybe they don't know that they can have one :-p But of course, I understand your remarks. As I said, I only opened this ticket to remember what I observed. But you can close it if you wish...
(0003938)
signoles (manager)
2013-06-04 17:41

I agree with you: it is worth remembering what has to be done in this direction. So I let this task opened.
(0004486)
signoles (manager)
2014-02-05 10:49

- Subst is no more part of the open source distribution. - There's still the warning about Config, but it seems that the Frama-C one is used: could be considered ok. - the contents of toplevel_boot.ml is now simply: let () = Topdirs.dir_directory Config.libdir So it behaves like a standard OCaml toplevel, but I don't know if it behaves as you expect (still I don't know what it is supposed to do ;-)).
(0004487)
Anne (reporter)
2014-02-05 11:12

Million thanks Julien ! I'll try it as soon as I'll have the last Frama-C version (soon I hope!). To answer about what it is supposed to do: I wrote a small library with some functions to get information about the current project like: - list of called undefined function, - list of statements with indirect calls, - filter reachable statements, - filter uncalled function, - etc. These function are basically wrapping over existing Frama-C functions, but with easier access. I add functions when I need new information. Then, I can load a project, and interactively ask questions to explore it, which is more convenient that to write a script or a plug-in.
(0004488)
signoles (manager)
2014-02-05 11:23

After a quick check, it works. But, since boot.ml is not loaded in the toplevel (otherwise one doesn't get a true OCaml toplevel), few differences may happen with the pretty printer and the exception handler. If it is ok, I'll close this task.
(0004489)
Anne (reporter)
2014-02-05 11:25

I'll tell you as soon as I know, but I guess I first need a fresh version of frama-c to be able to test it...
(0004872)
Anne (reporter)
2014-02-27 15:16

It seems to work... for simple things ! Some initializations are probably still missing, because I get error messages, for instance: %%% !Db.Value.compute ();; [kernel] failure: [Emitter] no hook table for parameter -plevel Exception: Log.AbortFatal "kernel". But anyway: %%% Dynamic.Parameter.Int.get "-plevel" ();; = 200 But most "browsing" functions are working, and that is a lot for me since I don't really need to run Value in a toplevel, do I ? Thank you again.
(0004874)
signoles (manager)
2014-02-27 16:45

Fix committed to feature/neon-bug-1441 branch.
(0004875)
signoles (manager)
2014-02-27 17:07

Fix committed to feature/neon-bug-1441 branch.
(0004876)
signoles (manager)
2014-02-27 17:18

Fix committed to stable/neon branch.
(0004877)
Anne (reporter)
2014-02-28 07:57

Thank you again ! I'll test that when I'll get the new version.

- Issue History
Date Modified Username Field Change
2013-06-04 14:16 Anne New Issue
2013-06-04 15:55 signoles Status new => assigned
2013-06-04 15:55 signoles Assigned To => signoles
2013-06-04 15:55 signoles Status assigned => acknowledged
2013-06-04 16:11 signoles Note Added: 0003936
2013-06-04 16:17 Anne Note Added: 0003937
2013-06-04 17:41 signoles Note Added: 0003938
2014-02-05 10:49 signoles Note Added: 0004486
2014-02-05 10:49 signoles Status acknowledged => feedback
2014-02-05 11:12 Anne Note Added: 0004487
2014-02-05 11:12 Anne Status feedback => assigned
2014-02-05 11:23 signoles Note Added: 0004488
2014-02-05 11:25 Anne Note Added: 0004489
2014-02-27 15:16 Anne Note Added: 0004872
2014-02-27 16:45 signoles Note Added: 0004874
2014-02-27 16:45 signoles Resolution open => fixed
2014-02-27 17:07 signoles Note Added: 0004875
2014-02-27 17:18 signoles Note Added: 0004876
2014-02-28 07:57 Anne Note Added: 0004877
2014-02-28 09:19 signoles Status assigned => resolved
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker