Frama-C Bug Tracking System - Frama-C
View Issue Details
0002162Frama-CKernel > Makefilepublic2015-09-16 10:002016-06-21 15:39
ploc 
bobot 
normalminoralways
assignedopen 
Frama-C Sodium 
 
0002162: Compilation of kernel native cmx is messed up with plugin makefile
The 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?
No tags attached.
related to 0002163assigned bobot Namespace through packs - packing frama-c cmx into a cmxa 
Issue History
2015-09-16 10:00plocNew Issue
2015-09-16 10:00plocStatusnew => assigned
2015-09-16 10:00plocAssigned To => signoles
2015-09-16 11:04signolesRelationship addedrelated to 0002163
2015-10-21 19:48signolesStatusassigned => confirmed
2016-06-21 15:39signolesAssigned Tosignoles => bobot
2016-06-21 15:39signolesStatusconfirmed => assigned

There are no notes attached to this issue.