frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:29:13Zhttps://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/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/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/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/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/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/323Configure step fails on bytecode architectures2021-02-22T12:59:21Zmantis-gitlab-migrationConfigure step fails on bytecode architecturesID0001763:
**This issue was created automatically from Mantis Issue 1763. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001763:
**This issue was created automatically from Mantis Issue 1763. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001763 | Frama-C | Kernel > configure | public | 2014-04-28 | 2017-08-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **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** | - |
### Description :
The configure step fails on pure bytecode architectures with the following message:
checking for /usr/lib/ocaml/ocamlgraph/graph.cmo... yes
configure: OcamlGraph 1.8.5 > 1.8.4 found: should be compatible, but no warranty. Use it at your own risk!
configure: OcamlGraph 1.8.5 is incompatible with Frama-C.
configure: switching to OcamlGraph provided by Frama-C
checking for ocamlgraph... no
checking for ocamlgraph.tar.gz... no
configure: error: cannot find OcamlGraph in the current directory.
Quite strange: would your Frama-C distribution be corrupted?
Anyway:
1. download the latest version from http://ocamlgraph.lri.fr/download
2. install it by './configure && make && make install'
3. rerun ./configure here
make[1]: *** [override_dh_auto_configure] Error 1
It is due to the fact that the script tries to compile a test program linking against the OCamlgraph library in the native case and calls ocamlgraph_error in the bytecode case instead of trying to compile the test program.
In order to make Frama-C build on bytecode architecture, I've disabled that call to ocamlgraph_error.https://git.frama-c.com/pub/frama-c/-/issues/311opam installation of frama-c-base fails2021-02-22T12:59:01Zmantis-gitlab-migrationopam installation of frama-c-base failsID0002331:
**This issue was created automatically from Mantis Issue 2331. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002331:
**This issue was created automatically from Mantis Issue 2331. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002331 | Frama-C | Kernel > Makefile | public | 2017-11-07 | 2017-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | seberoon | **Assigned To** | bobot | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | mac | **OS** | mac os | **OS Version** | 10.11.6 |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | Frama-C 16-Sulfur |
### Description :
Following opam installation instructions at https://frama-c.com/install-phosphorus-20170501.html#installing-frama-c-on-mac-os-x.
All ok up until opam install frama-c-base, which fails:
# File "src/plugins/wp/qed/src/numbers.mll", line 131, characters 18-19:
# Error: This expression has type string but an expression was expected of type
# bytes
This is using a fresh installation of homebrew and opam.
### Additional Information :
Mac OS 10.11.6
Xcode 8.2.1
## Attachments
- [frama-c_install_fail.txt](/uploads/21e1e50e3f88505149e7ba982b3583b9/frama-c_install_fail.txt)https://git.frama-c.com/pub/frama-c/-/issues/150coq and ocaml conflict2021-02-22T12:54:56Zmantis-gitlab-migrationcoq and ocaml conflictID0002372:
**This issue was created automatically from Mantis Issue 2372. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002372:
**This issue was created automatically from Mantis Issue 2372. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002372 | Frama-C | Kernel > configure | public | 2018-03-28 | 2019-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sthudium@mac.com | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Macbook Pro | **OS** | OS X | **OS Version** | 10.3.3 |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | Frama-C 19-Potassium |
### Description :
I cannot install frame-c.
The error report says that the installed version of coq and ocaml conflict with frama-c.
See attached txt file.
## Attachments
- [install_framac_terminal_text.txt](/uploads/a6ff4d5118eff6812fa3d412c905f8fa/install_framac_terminal_text.txt)https://git.frama-c.com/pub/frama-c/-/issues/73Bytecode only compilation fails when linking to stdlib2021-02-22T12:52:37Zmantis-gitlab-migrationBytecode only compilation fails when linking to stdlibID0002378:
**This issue was created automatically from Mantis Issue 2378. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002378:
**This issue was created automatically from Mantis Issue 2378. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002378 | Frama-C | ptests | public | 2018-06-18 | 2020-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | bytecode-only | **OS** | OpenBSD | **OS Version** | 6.3 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium |
### Description :
Compiling bytecode only fails with this error:
ocamlfind ocamlc -I ptests -dtypes -vmthread -g -o bin/ptests.byte unix.cma threads.cma str.cma dynlink.cma ptests/ptests_config.ml ptests/ptests.ml
File "ptests/ptests.ml", line 1:
Error: Required module `Uchar' is unavailable
### Steps To Reproduce :
Compile OCaml >=4.03 without optimizing compilers.
Use this compiler to build frama-c
## Attachments
- [patch-configure_in](/uploads/bf282dbc3c08065b0ff2a13f4fb83464/patch-configure_in)
- [patch-Makefile](/uploads/8465ce62432109e8765f692552e038a5/patch-Makefile)
- [patch-configure_in_2](/uploads/0fc49374e72889fac876d95a3de5dd71/patch-configure_in_2)
- [patch-Makefile_2](/uploads/568208604221bf782f915ed5f2ccf1b0/patch-Makefile_2)
- [patch-Makefile_3](/uploads/c238c03a2a9a0c54e559a994b4448f87/patch-Makefile_3)