2021-02-27 11:02 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001128Frama-CKernel > Makefilepublic2014-02-12 16:53
Assigned Tosignoles 
PrioritynormalSeverityfeatureReproducibilityhave not tried
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001128: Install frama-c.top
DescriptionAt 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].
TagsNo tags attached.
Attached Files




signoles (manager)

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


Anne (reporter)

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


Anne (reporter)

In case you are interested, the missing directories are :

Toplevel_topdirs.add_top "cil/ocamlutil";;
Toplevel_topdirs.add_top "cil/src";;
Toplevel_topdirs.add_top "cil/src/ext";;
Toplevel_topdirs.add_top "cil/src/frontc";;
Toplevel_topdirs.add_top "cil/src/logic";;
Toplevel_topdirs.add_top "external";;
Toplevel_topdirs.add_top "lib/fc";;

(from Dillon on the mailing list a long time ago)


Anne (reporter)

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


signoles (manager)

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


Anne (reporter)

Ok: I understand. I can do my "ln -s" myself ;-)
Just keep providing the 'top' target : I find it very useful...


Anne (reporter)

What do you thing about adding:
let _ = Topdirs.dir_directory Config.libdir

Wouldn't it work ?


Anne (reporter)

At least if I replace all my [Toplevel_topdirs.add_top] by [Topdirs.dir_directory Config.libdir], it is working.


Anne (reporter)

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 :
#directory "/usr/local/lib/frama-c";;

Of course, I cannot use [Config.libdir] at that point since it doesn't find Config yet, but then I can do:
Topdirs.dir_directory Config.plugin_dir;;
and then load my plugins !

This is only an information : you can do whatever you want with it ;-)


signoles (manager)

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?


Anne (reporter)

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 :
#load "XXX.cmo";
#load "XXXapi.cmo";

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.


signoles (manager)

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

-Issue History
Date Modified Username Field Change
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 16:15 svn
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
2013-12-19 01:11 signoles Source_changeset_attached => framac master 44a398e2
2014-02-12 16:53 signoles Source_changeset_attached => framac stable/neon 44a398e2
+Issue History