frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-07-11T15:44:07Zhttps://git.frama-c.com/pub/frama-c/-/issues/2593Build failure if only the eva plugin is selected: -rectypes is required2022-07-11T15:44:07Zfx-cartonBuild failure if only the eva plugin is selected: -rectypes is required### Steps to reproduce the issue
- untar the frama-c-24.0 sources
- configure with: --disable-landmarks --with-no-plugin --enable-gui --enable-callgraph --enable-server --enable-eva
- make
### Expected behaviour
Compilation succeeds
#...### Steps to reproduce the issue
- untar the frama-c-24.0 sources
- configure with: --disable-landmarks --with-no-plugin --enable-gui --enable-callgraph --enable-server --enable-eva
- make
### Expected behaviour
Compilation succeeds
### Actual behaviour
Compilation fails with the following message:
```
Ocamlc src/plugins/value/domains/multidim_domain.cmo
File "src/plugins/value/domains/multidim_domain.ml", line 1:
Error: Invalid import of Abstract_memory, which uses recursive types.
The compilation flag -rectypes is required
make: *** [share/Makefile.generic:78: src/plugins/value/domains/multidim_domain.cmo] Error 2
```
### Contextual information
- Frama-C installation mode: from source
- Frama-C version: 24.0
- Plug-in used: Eva (and dependencies)
- OS name: Linux
- OS version: Gentoo linux
### Additional information (optional)
- With no configure options, it builds fine.
- I've tried to debug the issue, and I think this is caused by having "-rectypes" added to BFLAGS for the rule compiling src/kernel_services/abstract_interp/abstract_memory.mli; which seems to be added as a side effect of the following line in the Makefile:
```
src/kernel_services/abstract_interp/abstract_memory.cmo: BFLAGS += -rectypes
```
For some reason, the dependency tree happens to change between the two configurations (default ./configure and ./configure with the aforementioned options), and in the latter case, the .cmi is a dependency of the .cmo, and thus inherits the local variables including BFLAGS.
- If I run `make src/kernel_services/abstract_interp/abstract_memory.cmi` and then `make`, it builds fine, because in the first make invocation the .cmo is not in the dependency tree, so -rectypes won't be added.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/134Bytecode only build fail with error 1272021-02-22T13:33:25Zmantis-gitlab-migrationBytecode only build fail with error 127ID0002473:
**This issue was created automatically from Mantis Issue 2473. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002473:
**This issue was created automatically from Mantis Issue 2473. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002473 | Frama-C | Kernel > Makefile | public | 2019-08-23 | 2019-08-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | bobot | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 bytecode only | **OS** | OpenBSD | **OS Version** | -current |
| **Product Version** | Frama-C 19-Potassium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-C build fine with native code compilers available, but fails to build
bytecode-only with the following error. I suspect the relevant clue is the _DEP_REDO suffix ?
Generating src/plugins/callgraph/.Makefile.plugin.generated
Generating src/plugins/metrics/.Makefile.plugin.generated
gmake[1]: Entering directory '/usr/obj/pobj/frama-c-19.0/Frama-C-snapshot-19.0'
Ocamldep src/plugins/metrics/.depend
gmake[1]: *** [src/plugins/metrics/.Makefile.plugin.generated:901: src/plugins/metrics/Metrics_DEP_REDO] Error 127
gmake[1]: Leaving directory '/usr/obj/pobj/frama-c-19.0/Frama-C-snapshot-19.0'
Ocamlc src/plugins/aorai/bool3.cmo
gmake: *** [share/Makefile.generic:78: src/plugins/aorai/bool3.cmo] Error 127
### Steps To Reproduce :
Install OCaml without native-code compilers, install dependencies, try to build Frama-C.https://git.frama-c.com/pub/frama-c/-/issues/158build failure due to mangled variable assignment in Makefile2022-09-28T11:02:51Zmantis-gitlab-migrationbuild failure due to mangled variable assignment in MakefileID0002458:
**This issue was created automatically from Mantis Issue 2458. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002458:
**This issue was created automatically from Mantis Issue 2458. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002458 | Frama-C | Kernel > configure | public | 2019-06-20 | 2019-06-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 | **OS** | OpenBSD | **OS Version** | 6.5-current |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
here's the patch:
Index: Makefile.generating
--- Makefile.generating.orig
+++ Makefile.generating
@@ -153,8 +153,8 @@ endif
ifeq ($(HAS_OCAML408),yes)
DYNLINK_INIT=fun () -> ()
FORMAT_STAG=stag
- FORMAT_STRING_OF_STAG=match s with\n\
- | Format.String_tag str -> str\n\
+ FORMAT_STRING_OF_STAG=match s with \
+ | Format.String_tag str -> str \
| _ -> raise (Invalid_argument "unsupported tag extension")
FORMAT_STAG_OF_STRING=Format.String_tag s
else
The \n quoting does not work on GNU make 4.2.1. I get
FORMAT_STRING_OF_STAG='match s withn | Format …`
The GNU make manual recommends to use the 'define' keyword to assign multi-line values to make variables, but why bother? We don't need the linebreaks, do we?Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/157configure does not detect gtksourceview due to wrong path2022-09-28T11:03:51Zmantis-gitlab-migrationconfigure does not detect gtksourceview due to wrong pathID0002457:
**This issue was created automatically from Mantis Issue 2457. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002457:
**This issue was created automatically from Mantis Issue 2457. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002457 | Frama-C | Kernel > configure | public | 2019-06-20 | 2019-06-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 | **OS** | OpenBSD | **OS Version** | 6.5 |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is on 19.0-beta2.
due to looking in the wrong directory, gtksourceview is not found.
Diff can be found in `Additional Information`
### Additional Information :
Index: configure.in
--- configure.in.orig
+++ configure.in
@@ -975,8 +975,8 @@ else
fi
configure_library([GTKSOURCEVIEW],
- [$SOURCEVIEW_PATH/lablgtksourceview2.$LIB_SUFFIX,
- $SOURCEVIEW_PATH/lablgtk3_sourceview3.$LIB_SUFFIX],
+ [$LABLGTKPATH_FOR_CONFIGURE/lablgtksourceview2.$LIB_SUFFIX,
+ $LABLGTKPATH_FOR_CONFIGURE/lablgtk3_sourceview3.$LIB_SUFFIX],
[lablgtksourceview not found],
no)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/160Does not build with OCaml 4.08.02022-09-28T11:03:06Zmantis-gitlab-migrationDoes not build with OCaml 4.08.0ID0002456:
**This issue was created automatically from Mantis Issue 2456. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002456:
**This issue was created automatically from Mantis Issue 2456. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002456 | Frama-C | Kernel > Makefile | public | 2019-06-18 | 2019-06-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | madroach | **Assigned To** | bobot | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | amd64 | **OS** | OpenBSD | **OS Version** | -current |
| **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - |
### Description :
The build fails with OCaml 4.08.0:
Packing /usr/obj/pobj/frama-c-18.0/frama-c-18.0-Argon/lib/plugins/top/Wp.cmo
File "_none_", line 1:
Error: The implementation (obtained by packing)
does not match the interface /usr/obj/pobj/frama-c-18.0/frama-c-18.0-Argon/lib/plugins/top/Wp.mli:
...
In module Cint:
Values do not match:
val is_cint_simplifier : Conditions/1.simplifier
is not included in
val is_cint_simplifier : Conditions/2.simplifier
File "src/plugins/wp/Cint.mli", line 80, characters 0-45:
Expected declaration
File "src/plugins/wp/Cint.mli", line 80, characters 0-45:
Actual declaration
File "_none_", line 1:
Definition of module Conditions/1
File "_none_", line 1:
Definition of module Conditions/2
gmake: *** [src/plugins/wp/.Makefile.plugin.generated:580: /usr/obj/pobj/frama-c-18.0/frama-c-18.0-Argon/lib/plugins/top/Wp.cmo] Error 2
I suspect the problem lies in there being multiple identical Wp.mli files, each declaring the same Conditions module, which OCaml 4.08.0 now does not view as identical.François BobotFrançois Bobothttps://git.frama-c.com/pub/frama-c/-/issues/247Can't compile2021-02-22T13:35:44Zmantis-gitlab-migrationCan't compileID0002391:
**This issue was created automatically from Mantis Issue 2391. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002391:
**This issue was created automatically from Mantis Issue 2391. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002391 | Frama-C | Kernel > Makefile | public | 2018-07-25 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yurichev | **Assigned To** | virgile | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x64 | **OS** | Ubuntu Linux | **OS Version** | 16.04 |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Got this file: https://frama-c.com/download/frama-c-Chlorine-20180502.tar.gz
Unpacked, typed "./configure", then "make" and got:
======================================================================
...
Ocamlc src/libraries/datatype/type.cmi
Ocamlc src/kernel_services/plugin_entry_points/log.cmi
Ocamlc src/libraries/project/project_skeleton.cmi
Ocamlc src/libraries/utils/pretty_utils.cmi
Ocamlc src/libraries/stdlib/integer.cmi
File "src/libraries/stdlib/integer.mli", line 26, characters 9-12:
Error: Unbound module Z
share/Makefile.generic:70: recipe for target 'src/libraries/stdlib/integer.cmi' failed
make: *** [src/libraries/stdlib/integer.cmi] Error 2
======================================================================
## Attachments
- [make_stdout](/uploads/401d9f44f320b484e178a6155274ee0d/make_stdout)
- [make_stderr](/uploads/8ecf375aceb48adc242fde2b25e103a0/make_stderr)
- [config.log](/uploads/cd25941939119614209fbc318815d10f/config.log)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)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/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/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/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/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 Bobothttps://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/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/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/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/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/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)