Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002162Frama-CKernel > Makefilepublic2015-09-16 10:002016-06-21 15:39
Reporterploc 
Assigned Tobobot 
PrioritynormalSeverityminorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002162: Compilation of kernel native cmx is messed up with plugin makefile
DescriptionThe include mechanism of plugin makefiles impact the oflags of the kernel compilation.

For example, the compilation flags of cmx for plugin is enriched with a -for-pack pluginname.

When one compiles frama-c classicaly, with VERBOSEMALE=yes make, one obtains:

ocamlopt ..... -for-pack Aorai structural_descr.ml
and same for a lot of .ml files of the kernel such as external/unmarshal.ml, src/type/type.ml ...

A (not so nice) workaround is to compile first those cmx without call to any dynamic plugin and then the main call:

# kernel only
EXTERNAL_PLUGINS="" VERBOSEMAKE=yes FRAMAC_USER_FLAGS="-for-pack FramaC" GEN_BUCKX_CFLAGS="-fPIC" make

# remaining uncompiled plugins
VERBOSEMAKE=yes FRAMAC_USER_FLAGS="-for-pack FramaC" GEN_BUCKX_CFLAGS="-fPIC" make

# install
sudo make install


Interestingly, removing such cmx compiled incorrectly with -for-pack Aorai, and asking to compile it again, triggers the correct rule:

#frama-c-Sodium-20150201$ rm src/type/structural_descr.cmx

#frama-c-Sodium-20150201$ VERBOSEMAKE=yes make src/type/structural_descr.cmx

It returns:

ocamlopt.opt -c -w +a-3-4-6-9-41-44-45-48 -annot -bin-annot -g -I src/misc -I
src/ai -I src/memory_state -I src/toplevel -I src/slicing_types -I src/pdg_types
-I src/kernel -I src/logic -I src/lib -I src/printer -I src/project -I src/type
-I src/buckx -I src/gui -I external -I cil/src -I cil/src/ext -I cil/src/frontc
-I cil/src/logic -I cil/ocamlutil -I
/home/ploc/Local/src/frama-c/frama-c-Sodium-20150201/lib/plugins -I lib -I
/home/ploc/.opam/4.01.0/lib/ocamlgraph -I /home/ploc/.opam/4.01.0/lib/zarith
-compact src/type/structural_descr.ml

Strange, n'est ce pas?
TagsNo tags attached.
Attached Files

- Relationships
related to 0002163assignedbobot Namespace through packs - packing frama-c cmx into a cmxa 

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2015-09-16 10:00 ploc New Issue
2015-09-16 10:00 ploc Status new => assigned
2015-09-16 10:00 ploc Assigned To => signoles
2015-09-16 11:04 signoles Relationship added related to 0002163
2015-10-21 19:48 signoles Status assigned => confirmed
2016-06-21 15:39 signoles Assigned To signoles => bobot
2016-06-21 15:39 signoles Status confirmed => assigned


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker