| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0001441 | Frama-C | Kernel | public | 2013-06-04 14:16 | 2014-03-13 15:57 | ||||
| Reporter | Anne | ||||||||
| Assigned To | signoles | ||||||||
| Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C Fluorine-20130501 | ||||||||
| Target Version | Fixed in Version | Frama-C Neon-20140301 | |||||||
| Summary | 0001441: frama-c.toplevel not working anymore | ||||||||
| Description | I 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)). | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
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 ;-). |
|
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... |
|
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. |
|
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 ;-)). |
|
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. |
|
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. |
|
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... |
|
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. |
|
signoles (manager) 2014-02-27 16:45 |
Fix committed to feature/neon-bug-1441 branch. |
|
signoles (manager) 2014-02-27 17:07 |
Fix committed to feature/neon-bug-1441 branch. |
|
signoles (manager) 2014-02-27 17:18 |
Fix committed to stable/neon branch. |
|
Anne (reporter) 2014-02-28 07:57 |
Thank you again ! I'll test that when I'll get the new version. |
| Notes |
| 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 | Source_changeset_attached | => framac feature/neon-bug-1441 4226a0d4 |
| 2014-02-27 16:45 | signoles | Note Added: 0004874 | |
| 2014-02-27 16:45 | signoles | Resolution | open => fixed |
| 2014-02-27 17:07 | signoles | Source_changeset_attached | => framac feature/neon-bug-1441 66969567 |
| 2014-02-27 17:07 | signoles | Note Added: 0004875 | |
| 2014-02-27 17:18 | signoles | Source_changeset_attached | => framac stable/neon 66969567 |
| 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 |
| Issue History |