|Anonymous | Login | Signup for a new account||2018-12-10 10:58 CET|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0001128||Frama-C||Kernel > Makefile||public||2012-03-22 08:24||2014-02-12 16:53|
|Priority||normal||Severity||feature||Reproducibility||have not tried|
|Product Version||Frama-C Nitrogen-20111001|
|Target Version||Fixed in Version||Frama-C Oxygen-20120901|
|Summary||0001128: Install frama-c.top|
|Description||At the moment, [make install] provides [frama-c], [frama-c.byte], [frama-c-gui] and [frama-c-gui].|
It would be great if it could also install [frama-c-top] from [bin/toplevel.top].
|Tags||No tags attached.|
I'm not sure that this debugging tool is really useful whenever Frama-C is installed since you can simply use the '-load-script' option to test something.
Furthermore there are two issues related to src/toplevel/toplevel_topdirs.ml (which bin/toplevel.top depends on):
1) this file is out-of-date
2) this file only works from a subdirectory of the Frama-C source (like 'bin').
I find it useful to have an interactive tool in order to prepare some scripts.
1) that's true. I had to add some [Toplevel_topdirs.add_top] in an init.ml file,
and then call [frama-c-Nitrogen-20111001/bin/toplevel.top -init init.ml]
2) well, it seems to work from other places since I do it ;-)
In case you are interested, the missing directories are :
(from Dillon on the mailing list a long time ago)
Ok: I didn't understand your (2) before because I was using:
and this is working from anywhere. But I have just realized that you cannot move toplevel.top to another place. I guess that is what you meant.
So I just do :
ln -s /path/to/frama-c-Nitrogen-20111001/bin/toplevel.top $FRAMAC_BINDIR/frama-c-top
And this is working (but you cannot remove the frama-c-Nitrogen-20111001 of course !)
|That's the point :). And your 'ln -s' partial solution does not work at all for binary package: Linux maintainers of Frama-C packages will hate us if we implement this solution ;-).|
Ok: I understand. I can do my "ln -s" myself ;-)
Just keep providing the 'top' target : I find it very useful...
What do you thing about adding:
let _ = Topdirs.dir_directory Config.libdir
Wouldn't it work ?
|At least if I replace all my [Toplevel_topdirs.add_top] by [Topdirs.dir_directory Config.libdir], it is working.|
I confirm that if I copy bin/toplevel.top into /usr/local/bin/frama-c-top,
I can run frama-c-top from anywhere and use it normally as soon as I begin by :
Of course, I cannot use [Config.libdir] at that point since it doesn't find Config yet, but then I can do:
and then load my plugins !
This is only an information : you can do whatever you want with it ;-)
Actually, with Nitrogen, if you do 'make top' before 'make install', bin/toplevel.top is installed and is then called 'frama-c.toplevel'.
I just improve it in order to:
- include all directories as you suggest (by using Config.libdir)
- be able to call project-related function (like Ast.get). It was not possible yet.
Is it enough for you?
Well, I don't even remember what the problem was since I finally managed to make everything work as I wished...
Thanks for the toplevel installation !
I would have been very sad to lose the toplevel in a future version.
Having a look at my files, I just remember that there is still a small problem with an error message when loading some file. In my ocamlinit,
I have :
XXX is a plug-in and XXXapi defines its API, so it uses XXX.
I get an error message :
[kernel] warning: cannot load plug-in `XXX' (plug-in not found).
but everything is working fine. I think that this is because XXX is loaded, but Frama-C Dynamic system doesn't know it.
I also tried to use Dynamic.load_module, but it SIGSEGV (Signal -10).
This is really a minor problem since everything is working well, but it might interest you.
Otherwise, you can close this task.
Using [Dynamic.load_module] (without any #load instruction) does not crash on my computer, as you can see below.
julien@is006613:~/frama-c$ FRAMAC_LIB=lib/fc ./bin/toplevel.top
Objective Caml version 3.12.1
# Dynamic.load_module "lib/plugins/Aorai.cmo";;
- : unit = ()
# let f = Dynamic.get ~plugin:"Aorai" "run" (Datatype.func Datatype.unit Datatype.unit);;
val f : unit -> unit = <fun>
# f ();;
[aorai] Welcome to the Aorai plugin
[aorai] user error: Error. File 'dummy.i' not found.
[aorai] user error: Error. File '' : invalid LTL file name.
[aorai] user error: Error. File '' not found.
[aorai] user error: Generation stopped.
- : unit = ()
|2012-03-22 08:24||Anne||New Issue|
|2012-03-22 08:24||Anne||Status||new => assigned|
|2012-03-22 08:24||Anne||Assigned To||=> signoles|
|2012-03-22 09:53||signoles||Note Added: 0002787|
|2012-03-22 10:05||Anne||Note Added: 0002788|
|2012-03-22 10:09||signoles||Status||assigned => acknowledged|
|2012-03-22 10:39||Anne||Note Added: 0002789|
|2012-03-29 15:06||Anne||Note Added: 0002806|
|2012-03-29 15:20||signoles||Note Added: 0002807|
|2012-03-29 15:52||Anne||Note Added: 0002808|
|2012-03-29 16:05||Anne||Note Added: 0002809|
|2012-03-29 16:12||Anne||Note Added: 0002810|
|2012-03-29 16:23||Anne||Note Added: 0002811|
|2012-09-10 16:13||signoles||Note Added: 0003436|
|2012-09-10 16:13||signoles||Status||acknowledged => feedback|
|2012-09-10 17:27||Anne||Note Added: 0003438|
|2012-09-11 14:14||signoles||Note Added: 0003441|
|2012-09-11 14:14||signoles||Status||feedback => resolved|
|2012-09-11 14:14||signoles||Resolution||open => fixed|
|2012-09-19 17:15||signoles||Fixed in Version||=> Frama-C Oxygen-20120901|
|2012-09-19 17:16||signoles||Status||resolved => closed|
|Copyright © 2000 - 2018 MantisBT Team|