Frama-C Bug Tracking System - Frama-C
View Issue Details
0000606Frama-CKernel > Makefilepublic2010-10-13 22:242010-12-09 19:09
closedno change required 
Frama-C Boron-20100401 
0000606: Don't edit files in make install. Instead, just use all plug-ins in the plugin directory
The current Frama-C architecture makes packaging Frama-C (and anything using it) unnecessarily difficult. Mark Rader and I managed to package "Frama-C" and "Why" for Fedora, but a few minor changes to Frama-C would make it MUCH easier to package and install (and thus update in the future). In particular, please change Frama-C so that adding or removing a plug-in does NOT require any file contents to be changed. Instead, Frama-C should just look at the plug-in directory, and presume that all files in that directory (with the proper extensions) are to be used. That way, to add a plug-in, an installer only needs to add a file to that directory; to remove the plug-in, the installer only needs to remove the files in that directory. This would also require changing the Frama-C "Makefile.dynamic" file so that installation would never modify the file "$(FRAMAC_SHARE)/" or any other file during "make install". The reason is that modern packaging systems (e.g. rpm of Red Hat/Fedora/Novell/SuSE and deb for Debian/Ubuntu) separate the install step into TWO stages. The first one, which does NOT have root privileges, is done by the distributor to create a package; this normally runs "make install DESTDIR=tempdir". The contents of tempdir are then stored in the package. When the user installs the package, that is the second stage, but normally that just copies files and that's it. Thanks!
For more about how to make source releases easy to install, please see: "Releasing Free/Libre/Open Source Software (FLOSS) for Source Installation"
No tags attached.
related to 0000461closed signoles Frama-c-gui doesn't install on bytecode architecture 
child of 0000462closed virgile Makefile.dynamic should not change 
child of 0000528closed signoles Makefile.dynamic should always write to $(DESTDIR) 
Issue History
2010-10-13 22:24dwheelerNew Issue
2010-10-13 22:24dwheelerStatusnew => assigned
2010-10-13 22:24dwheelerAssigned To => signoles
2010-10-14 08:56signolesRelationship addedrelated to 0000462
2010-10-14 08:56signolesRelationship addedrelated to 0000528
2010-10-14 08:56signolesRelationship addedrelated to 0000461
2010-10-14 09:05signolesRelationship deletedrelated to 0000462
2010-10-14 09:05signolesRelationship deletedrelated to 0000528
2010-10-14 09:06signolesRelationship addedchild of 0000462
2010-10-14 09:06signolesRelationship addedchild of 0000528
2010-10-14 09:14signolesNote Added: 0001189
2010-10-14 09:14signolesStatusassigned => feedback
2010-10-16 23:40pascalNote Added: 0001197
2010-12-09 19:09signolesStatusfeedback => closed
2010-12-09 19:09signolesResolutionopen => no change required

2010-10-14 09:14   
The issues about $(FRAMAC_SHARE)/ and DESTDIR have already been reported (respectively task #462 and #528) and resolved. The fixes will be part of the next public release. Another bug related to the install process (task #461) has been fixed. After a quick look at the Frama-C Makefiles, the install process should only create directories and copy files. Do you see any file contents to be changed when adding/removing a plug-in (different than $(FRAMAC_SHARE)/ If any, please report their names. Otherwise, I will close this task. Please feel free to open another task on this BTS if there is anything else which is "bad" in the building process of Frama-C (in a private e-mail, Mark Rader points a specific line containing an echo in Makefile.dynamic in, but I don't know where it is).
2010-10-16 23:40   
Note that the patches that fix bugs 461 and 462 are available from