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 - 2018 MantisBT Team
Powered by Mantis Bugtracker