Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000606Frama-CKernel > Makefilepublic2010-10-13 22:242010-12-09 19:09
Assigned Tosignoles 
StatusclosedResolutionno change required 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in Version 
Summary0000606: Don't edit files in make install. Instead, just use all plug-ins in the plugin directory
DescriptionThe 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!
Additional Information For more about how to make source releases easy to install, please see: "Releasing Free/Libre/Open Source Software (FLOSS) for Source Installation"
TagsNo tags attached.
Attached Files

- Relationships
related to 0000461closedsignoles Frama-c-gui doesn't install on bytecode architecture 
child of 0000462closedvirgile Makefile.dynamic should not change 
child of 0000528closedsignoles Makefile.dynamic should always write to $(DESTDIR) 

-  Notes
signoles (manager)
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).
pascal (reporter)
2010-10-16 23:40

Note that the patches that fix bugs 461 and 462 are available from

- Issue History
Date Modified Username Field Change
2010-10-13 22:24 dwheeler New Issue
2010-10-13 22:24 dwheeler Status new => assigned
2010-10-13 22:24 dwheeler Assigned To => signoles
2010-10-14 08:56 signoles Relationship added related to 0000462
2010-10-14 08:56 signoles Relationship added related to 0000528
2010-10-14 08:56 signoles Relationship added related to 0000461
2010-10-14 09:05 signoles Relationship deleted related to 0000462
2010-10-14 09:05 signoles Relationship deleted related to 0000528
2010-10-14 09:06 signoles Relationship added child of 0000462
2010-10-14 09:06 signoles Relationship added child of 0000528
2010-10-14 09:14 signoles Note Added: 0001189
2010-10-14 09:14 signoles Status assigned => feedback
2010-10-16 23:40 pascal Note Added: 0001197
2010-12-09 19:09 signoles Status feedback => closed
2010-12-09 19:09 signoles Resolution open => no change required

Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker