frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2022-09-28T11:10:32Z
https://git.frama-c.com/pub/frama-c/-/issues/427
Path for 'make install-doc-code' for external plug-in
2022-09-28T11:10:32Z
mantis-gitlab-migration
Path for 'make install-doc-code' for external plug-in
ID0001278:
**This issue was created automatically from Mantis Issue 1278. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001278:
**This issue was created automatically from Mantis Issue 1278. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001278 | Frama-C | Kernel > Makefile | public | 2012-09-26 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | bobot | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I do `make install-doc-code` for my XXX plug-in, it installs the documentation in `/usr/local/share/frama-c/doc/XXX` instead of `/usr/local/share/frama-c/doc/code/XXX` like the other plug-ins. So the links to Frama-C documentation are broken.
François Bobot
François Bobot
https://git.frama-c.com/pub/frama-c/-/issues/323
Configure step fails on bytecode architectures
2021-02-22T12:59:21Z
mantis-gitlab-migration
Configure step fails on bytecode architectures
ID0001763:
**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/311
opam installation of frama-c-base fails
2021-02-22T12:59:01Z
mantis-gitlab-migration
opam installation of frama-c-base fails
ID0002331:
**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/247
Can't compile
2021-02-22T13:35:44Z
mantis-gitlab-migration
Can't compile
ID0002391:
**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/160
Does not build with OCaml 4.08.0
2022-09-28T11:03:06Z
mantis-gitlab-migration
Does not build with OCaml 4.08.0
ID0002456:
**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 Bobot
François Bobot
https://git.frama-c.com/pub/frama-c/-/issues/158
build failure due to mangled variable assignment in Makefile
2022-09-28T11:02:51Z
mantis-gitlab-migration
build failure due to mangled variable assignment in Makefile
ID0002458:
**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 Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/157
configure does not detect gtksourceview due to wrong path
2022-09-28T11:03:51Z
mantis-gitlab-migration
configure does not detect gtksourceview due to wrong path
ID0002457:
**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 Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/150
coq and ocaml conflict
2021-02-22T12:54:56Z
mantis-gitlab-migration
coq and ocaml conflict
ID0002372:
**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/134
Bytecode only build fail with error 127
2021-02-22T13:33:25Z
mantis-gitlab-migration
Bytecode only build fail with error 127
ID0002473:
**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/73
Bytecode only compilation fails when linking to stdlib
2021-02-22T12:52:37Z
mantis-gitlab-migration
Bytecode only compilation fails when linking to stdlib
ID0002378:
**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)