frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T14:03:32Zhttps://git.frama-c.com/pub/frama-c/-/issues/1657RTE compiled even with ./configure --disable-rte2021-02-22T14:03:32ZDillon ParienteRTE compiled even with ./configure --disable-rteID0000398:
**This issue was created automatically from Mantis Issue 398. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000398:
**This issue was created automatically from Mantis Issue 398. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000398 | Frama-C | Kernel > configure | public | 2010-02-06 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Hi,
RTE is compiled even if it is disabled at "configure" time. (ie.: ./configure --disable-rte).
### Additional Information :
Seems to be related to other ./configure issues (e.g. issue 262). Moving it to Kernel -> configure.https://git.frama-c.com/pub/frama-c/-/issues/1622After ./confugure with --disable-all-staff options, make holds2021-02-22T13:36:13ZNikolai KosmatovAfter ./confugure with --disable-all-staff options, make holdsID0000305:
**This issue was created automatically from Mantis Issue 305. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000305:
**This issue was created automatically from Mantis Issue 305. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000305 | Frama-C | Kernel > configure | public | 2009-10-27 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Nikolai_Kosmatov | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
After configuring frama-c with the following options
-----------------------
./configure --disable-constant_propagation --disable-from --disable-gui --disable-impact --disable-inout --disable-ltl_to_acsl --disable-metrics --disable-miel --disable-occurrence --disable-pdg --disable-postdominators --disable-scope --disable-security --disable-semantic_callgraph --disable-slicing --disable-sparecode --disable-syntactic_callgraph --disable-users --disable-value --disable-wp
-----------------------
and trying make or make clean, got the following output :
nk@mypc:~/frama-c$ make
Generating src/lib/dynlink_common_interface.ml
Generating src/kernel/config.ml
Generating ptests/ptests_config.ml
Generating share/Makefile.kernel
Generating .depend
hanging with no visible action on .depend for hours.https://git.frama-c.com/pub/frama-c/-/issues/1472"make clean" does not work when upgrading OCaml2021-02-22T13:32:26Zmantis-gitlab-migration"make clean" does not work when upgrading OCamlID0001343:
**This issue was created automatically from Mantis Issue 1343. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001343:
**This issue was created automatically from Mantis Issue 1343. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001343 | Frama-C | Kernel > Makefile | public | 2013-01-08 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dhekir | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
After upgrading from OCaml 3.12 to 4.00, when trying to run "make clean" on the root of the Frama-C source directory, after having already compiled everything using OCaml 3.12, the makefile tries to run a target related to ocamlgraph before cleaning things, but since there are old .cmi files in its directories (which I wanted to be cleaned as well), it tries instead to build things before cleaning them, which gives annoying error messages:
$ make clean
Building ocamlgraph
make[1]: Entering directory `/local/user/framac/oxygen/ocamlgraph'
ocamlc.opt -I src -I lib -pack -g -o graph.cmo src/sig.cmi src/sig_pack.cmi src/dot_ast.cmi lib/unionfind.cmo lib/heap.cmo lib/bitv.cmo src/version.cmo src/util.cmo src/blocks.cmo src/persistent.cmo src/imperative.cmo src/delaunay.cmo src/builder.cmo src/classic.cmo src/rand.cmo src/oper.cmo src/components.cmo src/path.cmo src/nonnegative.cmo src/traverse.cmo src/coloring.cmo src/topological.cmo src/kruskal.cmo src/flow.cmo src/dominator.cmo src/graphviz.cmo src/gml.cmo src/dot_parser.cmo src/dot_lexer.cmo src/dot.cmo src/pack.cmo src/gmap.cmo src/minsep.cmo src/cliquetree.cmo src/mcs_m.cmo src/md.cmo src/strat.cmo src/fixpoint.cmo src/leaderlist.cmo src/contraction.cmo
File "_none_", line 1:
Error: src/sig.cmi
is not a compiled interface for this version of OCaml.
It seems to be for an older version of OCaml.
make[1]: *** [graph.cmo] Error 2
make[1]: Leaving directory `/local/user/framac/oxygen/ocamlgraph'
make: *** [lib/graph.cmi] Error 2
After manually removing such files, I was able to run "make clean". I believe a minor patch should do it, however it's quite tedious to reproduce the bug: it requires configuring an old OCaml, compiling, then configuring a new OCaml before trying "make clean" again.https://git.frama-c.com/pub/frama-c/-/issues/1391Bad links in generated documentation modules.svg2021-02-22T13:29:37Zmantis-gitlab-migrationBad links in generated documentation modules.svgID0001082:
**This issue was created automatically from Mantis Issue 1082. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001082:
**This issue was created automatically from Mantis Issue 1082. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001082 | Frama-C | Kernel > Makefile | public | 2012-02-06 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
There is an error in [share/Makefile.common] in the rule .dot -> .svg
that makes the links incorrect in the generated SVG.
Solution in line 275:
$(ISED) -e "s/\(digraph .*\)/\1 node [href=\"\\N.html\"];/" $<
should be transformed into:
$(ISED) -e "s/\(digraph .*\)/\1 node [href=\"\\\\N.html\"];/" $<
in order to write "\N.html" instead of "N.html" in the dot file.https://git.frama-c.com/pub/frama-c/-/issues/1378PLUGIN_LINK_GUI_OFLAGS not used ?2021-02-22T13:29:13Zmantis-gitlab-migrationPLUGIN_LINK_GUI_OFLAGS not used ?ID0001145:
**This issue was created automatically from Mantis Issue 1145. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001145:
**This issue was created automatically from Mantis Issue 1145. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001145 | Frama-C | Kernel > Makefile | public | 2012-04-12 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
It seems that the variables PLUGIN_LINK_GUI_BFLAGS and PLUGIN_LINK_GUI_OFLAGS that can be defined in plug-ins Makefile are not used in Makefile.plugin.
In $(TARGET_GUI_CMXS) I managed to change :
$(OCAMLOPT) -o $@ -shared $^
into
$(OCAMLOPT) -o $@ -shared $($(basename $(notdir $@))_OFLAGS) \
$($(basename $(notdir $@))_gui_TARGET_GUI_OFLAGS) \
$^
to make it work in my plug-in,
but I guess that there are other modifications to do...https://git.frama-c.com/pub/frama-c/-/issues/1356Handling error in external plug-in through --enable-external2021-02-22T13:28:33ZJulien SignolesHandling error in external plug-in through --enable-externalID0001069:
**This issue was created automatically from Mantis Issue 1069. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001069:
**This issue was created automatically from Mantis Issue 1069. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001069 | Frama-C | Kernel > configure | public | 2012-01-23 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Running './configure --enable-external=my_plugin_path' does not fail if the configure of the external plug-in fails. Worse the detection of this plug-in succeeds, so 'make' will try to compile it.https://git.frama-c.com/pub/frama-c/-/issues/1260Dynamic plugin doc2023-05-10T17:02:04Zmantis-gitlab-migrationDynamic plugin docID0000754:
**This issue was created automatically from Mantis Issue 754. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000754:
**This issue was created automatically from Mantis Issue 754. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000754 | Frama-C | Kernel > Makefile | public | 2011-03-16 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C Nitrogen-20111001 | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
The command : make xxx_DOC (where xxx is a dynamic plugin name) fails with the message :
Pas de règle pour fabriquer la cible « /kernel-doc.ocamldoc »
This is because $(DOC_DIR) is not defined, which seems normal (I far as I know, the compilation of dynamic plugin refers to the installed files, not to the source repository).
The easiest fix would probably be that a plugin internal documentation doesn't depend on the kernel documentation...https://git.frama-c.com/pub/frama-c/-/issues/1252the input file should be the first argument to ptests2023-04-21T13:20:33ZJulien Signolesthe input file should be the first argument to ptestsID0000736:
**This issue was created automatically from Mantis Issue 736. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000736:
**This issue was created automatically from Mantis Issue 736. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000736 | Frama-C | ptests | public | 2011-02-23 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | high | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
all in the title... Required in order to use -then* in tests.https://git.frama-c.com/pub/frama-c/-/issues/1142Configure script's autolocation of local OcamlGraph breaks out of tree builds2021-03-29T13:54:27Zmantis-gitlab-migrationConfigure script's autolocation of local OcamlGraph breaks out of tree buildsID0001454:
**This issue was created automatically from Mantis Issue 1454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001454:
**This issue was created automatically from Mantis Issue 1454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001454 | Frama-C | Kernel > configure | public | 2013-07-08 | 2014-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sstewartgallus | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I prefer to build my software packages out of tree. My personal arrangement is to have one sources directory, and one builds directory. I would then run my packages configure script inside a subdirectory of the sources directory specifically for that package, and build from there.
It is great that a version of OcamlGraph is distributed with Frama-C but unfortunately the configure script can only find it if the current directory is the source directory, and this breaks out of tree builds.
The problematic line in configure.in appears to be:
AC_CHECK_FILE($OCAMLGRAPH_LOCAL,OCAMLGRAPH_EXISTS=yes)
This line could probable be fixed in multiple ways. There's probably an autoconf macro for looking for a file in the source directory that's better than AC_CHECK_FILE, or one could define OCAMLGRAPH_LOCAL to use the invocation of ./configure to locate the directory it's located in (which would be something like ("$(cd $(dirname $0) && pwd)/ocamlgraph".)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/1114Compiling Wp-Coq library2021-02-22T13:28:53ZDillon ParienteCompiling Wp-Coq libraryID0001690:
**This issue was created automatically from Mantis Issue 1690. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001690:
**This issue was created automatically from Mantis Issue 1690. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001690 | Frama-C | Kernel > Makefile | public | 2014-03-13 | 2014-03-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Windows/Cygwin | **OS** | Win7 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
[STANCE]
In Frama-C Neon 20140301, when performing a 'make':
[...]
Compiling Wp-Coq Library
make[1] : on entre dans le répertoire « /frama-c-Neon-rc3/src/wp/share/coqwp »
coqc -R . -as "" BuiltIn.v
Don't know what to do with ./BuiltIn
Usage: coqtop <options>
...
It seems that in {-R . -as ""} the empty string is not managed as expected under Windows/Cygwin.
This topic was already discussed about the RC3.
This BTS record is open for traceability.
(Using coq 8.4pl3 with binaries pack for Windows)https://git.frama-c.com/pub/frama-c/-/issues/1007Erreur de linkage de librarie ocaml avec des fichier objets2021-02-22T13:17:09Zmantis-gitlab-migrationErreur de linkage de librarie ocaml avec des fichier objetsID0001733:
**This issue was created automatically from Mantis Issue 1733. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001733:
**This issue was created automatically from Mantis Issue 1733. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001733 | Frama-C | Kernel > Makefile | public | 2014-04-05 | 2014-07-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | zuy | **Assigned To** | signoles | **Resolution** | unable to reproduce |
| **Priority** | urgent | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Lorsqu'on fait un makefile pour son plugin en linkant une librairie (cma, cmxa) et non des fichiers objets (cmo) à ce plugin, on se retrouve avec une erreur de pré-reference : Forward reference to Llvm in file.
### Additional Information :
Lorsque le makefile souhaite packager l'ensemble des fichiers objets de frama-c avec ceux du plugins on se retrouve face à un problème lorsque le plugin en question souhaite se linker avec non pas une fichier objet mais une bibliothèque de fichier objet. Autrement dit au lieu de charger un cmo, il souhaite charger un cma.
Il semblerait que le make de frama-c n'ai pas prévu cette possibilité.
L'option -pack de ocamlc qui attend uniquement des fichiers objets pour en créer un nouveau; semble ne pas gérer l'arrivé d'une librairie contenant plusieurs fichier objet parmis les fichiers donnés0.
Dans l'exemple ci-dessous avec llvm.cma.
Plusieurs tentatives tendent à montrer que le problème se trouve là. Des tentatives en utilisant des -for-packs uniquement avant la création de la lib partagé (cmxs) ont échouées ainsi que d'autres pour transformer les fichiers objets (en packageant les objet du frama-c et ceux du plugin) en une librairie cma et l'utiliser pour faire le fichier partagé. Voilà les pistes que j'ai suivi et que j'ai surement mal mené.
Est ce réellement un bug ou une mauvaise utilisation du système de makefile mis en place ?
Exemple:
sh -c 'for f in "$@"; do if test -e $f; then chmod u+w $f; fi done' chmod_rw ./.depend
ocamldep.opt -slash \
-I . -I "/usr/local/lib/frama-c" \
lv.ml llvmRegister.ml llvmPrinter.ml llvmMain.ml lv.mli llvmRegister.mli llvmPrinter.mli llvmMain.mli \
\
> ./.depend
touch FCLlvm_DEP
chmod a-w ./.depend
ocamlc.opt -c -I /usr/local/lib/frama-c/plugins -I . -w +a-4-6-9-41-44-45 -annot -bin-annot -g -I "/usr/local/lib/frama-c" -I /home/jc/.opam/system/lib/llvm lv.ml
File "lv.ml", line 9, characters 6-13:
Warning 26: unused variable f32x4_t.
File "lv.ml", line 10, characters 6-13:
Warning 26: unused variable builder.
File "lv.ml", line 15, characters 6-11:
Warning 26: unused variable d64_t.
ocamlc.opt -c -I /usr/local/lib/frama-c/plugins -I . -w +a-4-6-9-41-44-45 -annot -bin-annot -g -I "/usr/local/lib/frama-c" -I /home/jc/.opam/system/lib/llvm llvmRegister.ml
ocamlc.opt -c -I /usr/local/lib/frama-c/plugins -I . -w +a-4-6-9-41-44-45 -annot -bin-annot -g -I "/usr/local/lib/frama-c" -I /home/jc/.opam/system/lib/llvm llvmPrinter.ml
ocamlc.opt -c -I /usr/local/lib/frama-c/plugins -I . -w +a-4-6-9-41-44-45 -annot -bin-annot -g -I "/usr/local/lib/frama-c" -I /home/jc/.opam/system/lib/llvm llvmMain.ml
ocamlc.opt -o FCLlvm.cmo -I /usr/local/lib/frama-c/plugins -I . -w +a-4-6-9-41-44-45 -annot -bin-annot -g -I "/usr/local/lib/frama-c" -I /home/jc/.opam/system/lib/llvm -pack \
llvm.cma \
./lv.cmo ./llvmRegister.cmo ./llvmPrinter.cmo ./llvmMain.cmo
File "_none_", line 1:
Error: Forward reference to Llvm in file ./lv.cmo
make: *** [FCLlvm.cmo] Erreur 2
### Steps To Reproduce :
Créer un plugin nécessitant une librairie caml. Ici l'exemple concerne le byte code mais l'erreur se produit pour le natif aussi. Faire le make appelant le Makefile.dynamic de frama-c.
Puis faire une make.https://git.frama-c.com/pub/frama-c/-/issues/994make version 4.0 is rejected2021-02-22T14:02:28Zmantis-gitlab-migrationmake version 4.0 is rejectedID0001574:
**This issue was created automatically from Mantis Issue 1574. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001574:
**This issue was created automatically from Mantis Issue 1574. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001574 | Frama-C | Kernel > configure | public | 2013-11-28 | 2014-08-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jowi24 | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
$./configure
configure: ******************
configure: * CONFIGURE MAKE *
configure: ******************
checking for make... make
make version is GNU Make 4.0:
configure: error: unsupported version; GNU Make version 3.81
or higher is required.
### Additional Information :
the following test in configure is buggy:
test "$MAKE_DISTRIB" != GNU -o "$MAKE_MAJOR" -lt 3 -o "$MAKE_MINOR" -lt 81;https://git.frama-c.com/pub/frama-c/-/issues/993Configure fails for GNU Make 4.02023-03-09T10:04:17Zmantis-gitlab-migrationConfigure fails for GNU Make 4.0ID0001903:
**This issue was created automatically from Mantis Issue 1903. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001903:
**This issue was created automatically from Mantis Issue 1903. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001903 | Frama-C | Kernel > configure | public | 2014-07-30 | 2014-08-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Julien_t | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Gnu/linux Debian | **OS Version** | Debian 3.14.12-1 |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
First I should probably say that I use opam to install frama-C.
The configure file test whether the Make version is greater than 3.81 but it check that major version is >= 3 (which is ok) and that minor version is >= 81, which is not the case for the version 4.0
### Additional Information :
test at line 2630 of the configure file should be modified.
### Steps To Reproduce :
./configure in an environment with version 4.0 of GNU Makehttps://git.frama-c.com/pub/frama-c/-/issues/947make install fails when --prefix is the source directory2021-02-22T13:27:47ZMihaela Sighireanumake install fails when --prefix is the source directoryID0001962:
**This issue was created automatically from Mantis Issue 1962. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001962:
**This issue was created automatically from Mantis Issue 1962. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001962 | Frama-C | Kernel > configure | public | 2014-11-12 | 2014-12-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Mihaela Sighireanu | **Assigned To** | signoles | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When the installation prefix is exactly the path to the directory containing the sources of drama-c, the installation fails for pests.opt
### Additional Information :
Message of 'make install' :
install bin/ptests.opt \
"/home/verif/sighirea/Tools-other/frama-c-Neon-20140301/bin"/ptests.opt
install: ‘bin/ptests.opt’ and ‘/home/verif/sighirea/Tools-other/frama-c-Neon-20140301/bin/ptests.opt’ are the same file
make: *** [install] Error 1
### Steps To Reproduce :
./configure --prefix=/path/to/source/dir/frama-c-Neon
make
make installhttps://git.frama-c.com/pub/frama-c/-/issues/909ptest doesn't abort tests for which the command is incorrect2022-09-28T12:10:58ZValentin Perrelleptest doesn't abort tests for which the command is incorrectID0002054:
**This issue was created automatically from Mantis Issue 2054. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002054:
**This issue was created automatically from Mantis Issue 2054. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002054 | Frama-C | ptests | public | 2015-01-22 | 2015-01-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | valentin.perrelle | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
ptest has the following behavior when the command used to invoke frama-c is incorrect. First, the command is executed and the error reported by the shell. ptest continues using a previously generated output for the test. If the previous output was correct, it concludes that all tests passed.
When the command is put directly in the test file, tests update may introduce errors in this command line. It should be reported that the test does not pass due to incorrect command provided.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/790Cannot switch to local version if OCamlgraph is already installed2021-02-22T13:11:55ZRichard BonichonCannot switch to local version if OCamlgraph is already installedID0001770:
**This issue was created automatically from Mantis Issue 1770. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001770:
**This issue was created automatically from Mantis Issue 1770. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001770 | Frama-C | Kernel > configure | public | 2014-05-01 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rbonichon | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
I have OCamlgraph 1.8.5 on my machine, which is apparently incompatible with Frama-C Neon. However, I cannot force a switch to the local version with
./configure --enable-local-ocamlgraph
I am not sure if this option was intended to force the use of the local version.
### Additional Information :
The attached patch forces the use of the local ocamlgraph library when --enable-local-ocamlgraph has been given.
Basically, it encapsulates the search for an external library into a conditional which test the presence of then --enable-local switch.
### Steps To Reproduce :
Install external ocamlgraph library (1.8.5. for example, through opam)
Run ./configure --enable-local-ocamlgraph
VERBOSEMAKE=yes make
should show that the external ocamlgraph library is in the include path whereas the local one is not.
## Attachments
- [configure.in.patch](/uploads/3215b70c71e1e87be58aabb5beabe6f7/configure.in.patch)https://git.frama-c.com/pub/frama-c/-/issues/594Relocable buckx2022-08-09T08:54:52Zmantis-gitlab-migrationRelocable buckxID0002165:
**This issue was created automatically from Mantis Issue 2165. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002165:
**This issue was created automatically from Mantis Issue 2165. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002165 | Frama-C | Kernel > Makefile | public | 2015-09-16 | 2015-09-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | signoles | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Please add, as a default option, the relocation for buckx_c files:
GEN_BUCKX_CFLAGS="-fPIC"https://git.frama-c.com/pub/frama-c/-/issues/510Frama-C upgrade installation not foolproof2022-09-28T11:16:35ZJochen BurghardtFrama-C upgrade installation not foolproofID0002223:
**This issue was created automatically from Mantis Issue 2223. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002223:
**This issue was created automatically from Mantis Issue 2223. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002223 | Frama-C | Kernel > Makefile | public | 2016-04-11 | 2016-05-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | have not tried |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | 14.04.1-Ubuntu |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I tried to follow the file "acslplusplus/frama-c/INSTALL" in order to upgrade Frama-C from version "Sodium-20150201" to the current version in the acslplusplus/frama git repository. The file "install.log" documents my attempts; lines starting with "sh> #" are comments I added subsequently to explain my motives; other lines starting with "sh>" are my command-line inputs; the rest is opam output.
As I've done everything in a newly cloned virtual machine, the state before the first and after the last command-line input is preserved, so if any particular information is needed, let me know, there is a good chance that I can provide it.
## Attachments
- [install.log](/uploads/5806bb58a2b823255e3d21a32e1f9da6/install.log)
- [install_122.log](/uploads/a0a17caf1faf77e9182e02f1c5eb393e/install_122.log)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/488Relocable buckx2021-02-22T14:01:47Zmantis-gitlab-migrationRelocable buckxID0002164:
**This issue was created automatically from Mantis Issue 2164. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002164:
**This issue was created automatically from Mantis Issue 2164. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002164 | Frama-C | Kernel > Makefile | public | 2015-09-16 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
Please add, as a default option, the relocation for buckx_c files:
GEN_BUCKX_CFLAGS="-fPIC"https://git.frama-c.com/pub/frama-c/-/issues/428Compilation of kernel native cmx is messed up with plugin makefile2022-09-28T11:09:13Zmantis-gitlab-migrationCompilation of kernel native cmx is messed up with plugin makefileID0002162:
**This issue was created automatically from Mantis Issue 2162. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002162:
**This issue was created automatically from Mantis Issue 2162. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002162 | Frama-C | Kernel > Makefile | public | 2015-09-16 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | bobot | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
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?François BobotFrançois Bobot