Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001128Frama-CKernel > Makefilepublic2012-03-22 08:242014-02-12 16:53
Assigned Tosignoles 
PrioritynormalSeverityfeatureReproducibilityhave not tried
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001128: Install
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/].
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
signoles (manager)
2012-03-22 09:53

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/ (which bin/ 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)
2012-03-22 10:05

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 file, and then call [frama-c-Nitrogen-20111001/bin/ -init] 2) well, it seems to work from other places since I do it ;-)
Anne (reporter)
2012-03-22 10:39

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)
2012-03-29 15:06

Ok: I didn't understand your (2) before because I was using: /path/to/frama-c-Nitrogen-20111001/bin/ and this is working from anywhere. But I have just realized that you cannot move to another place. I guess that is what you meant. So I just do : ln -s /path/to/frama-c-Nitrogen-20111001/bin/ $FRAMAC_BINDIR/frama-c-top And this is working (but you cannot remove the frama-c-Nitrogen-20111001 of course !)
signoles (manager)
2012-03-29 15:20

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)
2012-03-29 15:52

Ok: I understand. I can do my "ln -s" myself ;-) Just keep providing the 'top' target : I find it very useful... Thanks!
Anne (reporter)
2012-03-29 16:05

What do you thing about adding: let _ = Topdirs.dir_directory Config.libdir Wouldn't it work ?
Anne (reporter)
2012-03-29 16:12

At least if I replace all my [Toplevel_topdirs.add_top] by [Topdirs.dir_directory Config.libdir], it is working.
Anne (reporter)
2012-03-29 16:23

I confirm that if I copy bin/ 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)
2012-09-10 16:13

Actually, with Nitrogen, if you do 'make top' before 'make install', bin/ 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)
2012-09-10 17:27

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)
2012-09-11 14:14

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/ 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 = # 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 Checkin
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 - 2020 MantisBT Team
Powered by Mantis Bugtracker