2021-02-24 19:31 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001441Frama-CKernelpublic2014-03-13 15:57
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityhave not tried
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 ...
> !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




signoles (manager)

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)

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)

I agree with you: it is worth remembering what has to be done in this direction. So I let this task opened.


signoles (manager)

- 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)

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)

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)

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)

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)

Fix committed to feature/neon-bug-1441 branch.


signoles (manager)

Fix committed to feature/neon-bug-1441 branch.


signoles (manager)

Fix committed to stable/neon branch.


Anne (reporter)

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 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