|Anonymous | Login | Signup for a new account||2019-06-20 12:22 CEST|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0001441||Frama-C||Kernel||public||2013-06-04 14:16||2014-03-13 15:57|
|Priority||normal||Severity||minor||Reproducibility||have not tried|
|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 ...
> !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.|
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?).
- 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 ;-).
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...
|I agree with you: it is worth remembering what has to be done in this direction. So I let this task opened.|
- 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 ;-)).
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,
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.
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.
|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...|
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".
%%% Dynamic.Parameter.Int.get "-plevel" ();;
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.
|Fix committed to feature/neon-bug-1441 branch.|
|Fix committed to feature/neon-bug-1441 branch.|
|Fix committed to stable/neon branch.|
|Thank you again ! I'll test that when I'll get the new version.|
|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|