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/2425share/Makefile.kernel: No such file or directory2021-02-22T14:04:47Zmantis-gitlab-migrationshare/Makefile.kernel: No such file or directoryID0000408:
**This issue was created automatically from Mantis Issue 408. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000408:
**This issue was created automatically from Mantis Issue 408. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000408 | Frama-C | Kernel > Makefile | public | 2010-02-16 | 2010-02-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | javert42 | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
running 'make' gives the following errors:
share/Makefile.dynamic:55: share/Makefile.kernel: No such file or directory
Makefile:1853: .depend: No such file or directory
Copying to lib/dgraph.cmi
cp: cannot stat `ocamlgraph/dgraph/dgraph.cmi': No such file or directory
make: *** [lib/dgraph.cmi] Error 1https://git.frama-c.com/pub/frama-c/-/issues/2424cp: cannot stat `ocamlgraph/dgraph/dgraph.cmi': No such file or directory2021-02-22T14:04:47Zmantis-gitlab-migrationcp: cannot stat `ocamlgraph/dgraph/dgraph.cmi': No such file or directoryID0000409:
**This issue was created automatically from Mantis Issue 409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000409:
**This issue was created automatically from Mantis Issue 409. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000409 | Frama-C | Kernel > Makefile | public | 2010-02-16 | 2010-02-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | javert42 | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c-Beryllium-20090902-why-2.21
Running make gives the following error:
share/Makefile.dynamic:55: share/Makefile.kernel: No such file or directory
Makefile:1853: .depend: No such file or directory
Copying to lib/dgraph.cmi
cp: cannot stat `ocamlgraph/dgraph/dgraph.cmi': No such file or directory
make: *** [lib/dgraph.cmi] Error 1
### Additional Information :
dgraph.cmi does not exist in ocamlgraph/dgraph
dgraph.cmi does not exist anywhere in ocamlgraph.tar.gzhttps://git.frama-c.com/pub/frama-c/-/issues/2394Should not call install-kernel-opt on bytecode architectures2021-02-22T13:58:07Zmantis-gitlab-migrationShould not call install-kernel-opt on bytecode architecturesID0000382:
**This issue was created automatically from Mantis Issue 382. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000382:
**This issue was created automatically from Mantis Issue 382. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000382 | Frama-C | Kernel > Makefile | public | 2010-01-22 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **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 :
The “install” target calls unconditionally “install-kernel-opt” which fails on bytecode-only architectures.
Please find attached a patch to fix this little issue.
Regards,
## Attachments
- [0003-Do-not-install-native-Kernel-modules-on-bytecode-arc.patch](/uploads/52da9ae0daa63b793785cc38cc5ddca7/0003-Do-not-install-native-Kernel-modules-on-bytecode-arc.patch)https://git.frama-c.com/pub/frama-c/-/issues/2353problem to make install the "hello_world"-plugin2021-02-22T13:57:08Zmantis-gitlab-migrationproblem to make install the "hello_world"-pluginID0000582:
**This issue was created automatically from Mantis Issue 582. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000582:
**This issue was created automatically from Mantis Issue 582. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000582 | Frama-C | Kernel > Makefile | public | 2010-09-13 | 2010-09-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | fsd | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I've installed frama-c on ubuntu lucid lynx 10.04
I wanted to make a simple plugin "hello_world" like in the description of the documentation "plugin-developer-Boron-20100401.pdf" with the two files Makefile and hello_world.ml
After copying the sources of the documentation and saving both in the folder /home/jean-pierre/Bureau/ocamldoc/ i started the terminal, went to the folder and wrote "make". the terminal said:
jean-pierre@jean-pierre-laptop:~/Bureau/ocamldoc$ make
/usr/share/frama-c/Makefile.dynamic:180: .depend: Aucun fichier ou dossier de ce type
ocamlc.opt -c -I . -w Ael -warn-error A -annot -g -I /usr/lib/frama-c hello_world.ml
File "hello_world.ml", line 12, characters 14-18:
Warning Z: unused variable name.
File "hello_world.ml", line 3, characters 3-119:
Error: Signature mismatch:
Modules do not match:
sig val name : string val shortname : string val deser : string end
is not included in
sig val name : string val shortname : string val descr : string end
The field `descr' is required but not provided
make: *** [hello_world.cmo] Erreur 2
### Additional Information :
i tried for windows XP with frama-c and cygwin but there are also problems.
any ideas?https://git.frama-c.com/pub/frama-c/-/issues/2336Don't edit files in make install. Instead, just use all plug-ins in the plugi...2021-02-22T14:04:39Zmantis-gitlab-migrationDon't edit files in make install. Instead, just use all plug-ins in the plugin directoryID0000606:
**This issue was created automatically from Mantis Issue 606. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000606:
**This issue was created automatically from Mantis Issue 606. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000606 | Frama-C | Kernel > Makefile | public | 2010-10-13 | 2010-12-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dwheeler | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The current Frama-C architecture makes packaging Frama-C (and anything using it) unnecessarily difficult. Mark Rader and I managed to package "Frama-C" and "Why" for Fedora, but a few minor changes to Frama-C would make it MUCH easier to package and install (and thus update in the future).
In particular, please change Frama-C so that adding or removing a plug-in does NOT require any file contents to be changed. Instead, Frama-C should just look at the plug-in directory, and presume that all files in that directory (with the proper extensions) are to be used. That way, to add a plug-in, an installer only needs to add a file to that directory; to remove the plug-in, the installer only needs to remove the files in that directory.
This would also require changing the Frama-C "Makefile.dynamic" file so that installation would never modify the file "$(FRAMAC_SHARE)/known_plugins.ac"
or any other file during "make install".
The reason is that modern packaging systems (e.g. rpm of Red Hat/Fedora/Novell/SuSE and deb for Debian/Ubuntu) separate the install step into TWO stages. The first one, which does NOT have root privileges, is done by the distributor to create a package; this normally runs "make install DESTDIR=tempdir". The contents of tempdir are then stored in the package.
When the user installs the package, that is the second stage, but normally that just copies files and that's it.
Thanks!
### Additional Information :
For more about how to make source releases easy to install, please see:
"Releasing Free/Libre/Open Source Software (FLOSS) for Source Installation"
http://www.dwheeler.com/essays/releasing-floss-software.htmlhttps://git.frama-c.com/pub/frama-c/-/issues/2294Makefile.dynamic should not change known_plugins.ac2021-02-22T14:04:39Zmantis-gitlab-migrationMakefile.dynamic should not change known_plugins.acID0000462:
**This issue was created automatically from Mantis Issue 462. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000462:
**This issue was created automatically from Mantis Issue 462. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000462 | Frama-C | Kernel > Makefile | public | 2010-04-27 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
I'm not sure whether this is a bug or a feature, but in my understanding, installing an external plugin for Frama-C should not modify the files installed by Frama-C itself.
In this specific case, when the Jessie plugin wants to install, 'Makefile.dynamic' tells to append a line in '/usr/share/frama-c/known_plugins.ac'. If the user doesn't have write access on 'known_plugins.ac', the installation fails. Specifically, this would have lead to a build failure on any Debian build daemon. For now, I've desactivated this "feature" in 'Makefile.dynamic' using the attached patch.
'known_plugins.ac' is used only by the configure scripts of aorai and security_slicing. IMHO, they should rely on the existence of plugin files rather than some text file with (potentially) random content.
## Attachments
- [0005-Don-t-modify-system-files.patch](/uploads/a2a99b05668822004392ce1b153044af/0005-Don-t-modify-system-files.patch)https://git.frama-c.com/pub/frama-c/-/issues/2253Error during plugin compilation2021-02-22T13:54:59Zmantis-gitlab-migrationError during plugin compilationID0000681:
**This issue was created automatically from Mantis Issue 681. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000681:
**This issue was created automatically from Mantis Issue 681. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000681 | Frama-C | Kernel > Makefile | public | 2011-01-21 | 2011-01-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | CFaure | **Assigned To** | signoles | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | block | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I made a custom install of Frama-C with
DESTDIR=/home/faure/frama-c/frama-c-install.
I tries to compile a plugin with a Makefile built as described in the manual.
But I got errors and nothing got compiled.
Then I modified the makefile as described in additional information: I mainly added modified the values of FRAMAC_SHARE and FRAMAC_LIBDIR because the paths where wrong.
The make got further but I finally got a link error:
Linking frama-c-Saferiver.byte
Cannot find file /usr/local/lib/frama-c/boot.cmo
make: *** [frama-c-Saferiver.byte] Error 2
### Additional Information :
# Frama-c should be properly installed with "make install
# before any use of this makefile
DESTDIR=/home/faure/frama-c/frama-c-install
FRAMAC_BIN=$(DESTDIR)/usr/local/bin
FRAMAC_SHARE :=$(shell $(FRAMAC_BIN)/frama-c.byte -print-path)
FRAMAC_LIBDIR :=$(shell $(FRAMAC_BIN)/frama-c.byte -print-libpath)
PLUGIN_NAME = Saferiver
PLUGIN_CMO = register
FRAMAC_SHARE := $(DESTDIR)/$(FRAMAC_SHARE)
FRAMAC_LIBDIR := $(DESTDIR)/$(FRAMAC_LIBDIR)
include $(FRAMAC_SHARE)/Makefile.dynamichttps://git.frama-c.com/pub/frama-c/-/issues/2243lib apron not found in configure2021-02-22T13:54:41Zmantis-gitlab-migrationlib apron not found in configureID0000647:
**This issue was created automatically from Mantis Issue 647. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000647:
**This issue was created automatically from Mantis Issue 647. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000647 | Frama-C | Kernel > configure | public | 2010-12-22 | 2011-02-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jmharang | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20110201 |
### Description :
I build the beta release on a ubuntu 10.04 (LTS) :
Lib Apron not found by configure
..
checking for /usr/local/lib/apron.a... no
checking for /usr/lib/apron.a... no
..
but :
jmharang@po25975:~/src/frama-c/frama-c-Carbon-20101202-beta2$ dpkg -l | grep -i apron
ii libapron 0.9.10-4build1 Runtime libraries for APRON
ii libapron-dev 0.9.10-4build1 An abstract interpretation library
ii libapron-ocaml 0.9.10-4build1 Runtime libraries for APRON
ii libapron-ocaml-dev 0.9.10-4build1 An abstract interpretation library
and :
jmharang@po25975:/usr/lib$ ls -Al libapron*
lrwxrwxrwx 1 root root 13 2010-12-21 17:10 libapron.so -> libapron.so.0
-rw-r--r-- 1 root root 783696 2010-02-24 20:09 libapron.so.0
### Additional Information :
I take a look to configure.in
jmharang@po25975:~/src/frama-c/frama-c-Carbon-20101202-beta2$ grep apron configure.in
# [JS 2009/03/25] apron must be configured before why/jc which uses $HAS_APRON
[/usr/local/lib/apron.a,/usr/lib/apron.a],
[apron not found])
./configure search apron.a and not libapron.a
I patch my configure (sh) to find it and it's seems ok.
In boron (frama-c-Boron-20100401-why-2.24) :
config.log:configure:7525: checking for /usr/local/lib/apron.a
config.log:configure:7550: checking for /usr/lib/apron.a
config.log:ac_cv_file__usr_lib_apron_a=no
config.log:ac_cv_file__usr_local_lib_apron_a=nohttps://git.frama-c.com/pub/frama-c/-/issues/2217Signature mismatch errors while compiling simple "hello world" plug-in2021-02-22T13:54:02Zmantis-gitlab-migrationSignature mismatch errors while compiling simple "hello world" plug-inID0000777:
**This issue was created automatically from Mantis Issue 777. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000777:
**This issue was created automatically from Mantis Issue 777. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000777 | Frama-C | Kernel > Makefile | public | 2011-04-07 | 2011-04-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | njucslzh | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20110201 |
### Description :
ocamlc -c -I . -w Z -warn-error A -annot -g -I "/usr/lib/frama-c" -I /usr/lib/frama-c hello_world.ml
File "hello_world.ml", line 63, characters 5-132:
Error: Signature mismatch:
Modules do not match:
sig val name : string val shortname : string val help : string end
is not included in
sig val name : string val shortname : string val descr : string end
The field `descr' is required but not provided
make: *** [hello_world.cmo] ?? 2
### Additional Information :
OS:Ubuntu 10.10
OCaml:3.11.2
I changed the file /usr/share/frama-c/Makefile.config :
# compilers and others executables
OCAMLC ?=ocamlc
OCAMLOPT ?=ocamlopt
OCAMLDEP ?=ocamldep -slash
OCAMLLEX ?=ocamllex
OCAMLYACC ?=ocamlyacc
OCAMLMKTOP ?=ocamlmktop
OCAMLDOC ?=ocamldoc
OCAMLCP ?=ocamlcphttps://git.frama-c.com/pub/frama-c/-/issues/2048the make errors2021-02-22T13:49:46Zmantis-gitlab-migrationthe make errorsID0001034:
**This issue was created automatically from Mantis Issue 1034. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001034:
**This issue was created automatically from Mantis Issue 1034. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001034 | Frama-C | Kernel > Makefile | public | 2011-11-30 | 2012-05-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | luoting | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I am trying to install frama-c Nitrogen-20111001 in ubuntu10.04 (linux 2.6.32).
Firstly ,./configure
luoting@luoting-desktop:~/frama-c2011/frama-c-Nitrogen-20111001$ ./configure
configure: ******************
configure: * CONFIGURE MAKE *
configure: ******************
checking for make... make
make version is GNU Make 3.81: Good!
configure: *****************************
configure: * CONFIGURE OCAML COMPILERS *
configure: *****************************
checking for ocamlc... ocamlc
OCaml version is 3.11.2: good!
ocaml library path is /usr/local/lib/ocaml
checking for ocamlopt... ocamlopt
checking ocamlopt version and standard library... differs from ocamlc; ocamlopt discarded.
checking for ocamlc.opt... no
configure: *******************************************
configure: * CONFIGURE MANDATORY TOOLS AND LIBRARIES *
configure: *******************************************
checking for ocamldep... ocamldep
checking for ocamldep.opt... no
checking for ocamllex... ocamllex
checking for ocamllex.opt... no
checking for ocamlyacc... ocamlyacc
checking for /usr/local/lib/ocaml/ocamlgraph/graph.cmo... yes
configure: your OcamlGraph version is incompatible with Frama-C.
configure: switching to OcamlGraph provided by Frama-C
checking for ocamlgraph... yes
checking for ocamlgraph.tar.gz... yes
configure: configuring ocamlgraph...
configure: WARNING: lablgnomecanvas not found: the graph editor and view_graph will not be compiled
configure: ******************************************
configure: * CONFIGURE OPTIONAL TOOLS AND LIBRARIES *
configure: ******************************************
checking for ocamldoc... ocamldoc
checking for ocamlmktop... ocamlmktop
checking for otags... no
configure: **********************
configure: * CONFIGURE PLATFORM *
configure: **********************
checking platform... Unix
checking whether performance counters are usable... ok (2928.571 cycles per us)
configure: ***************************
configure: * WISHED FRAMA-C PLUG-INS *
configure: ***************************
checking for src/constant_propagation... yes
semantic_constant_folding... yes
checking for src/from... yes
from_analysis... yes
checking for src/gui... yes
gui... yes
checking for src/impact... yes
impact... yes
checking for src/inout... yes
inout... yes
checking for src/metrics... yes
metrics... yes
checking for src/occurrence... yes
occurrence... yes
checking for src/pdg... yes
pdg... yes
checking for src/postdominators... yes
postdominators... yes
checking for src/rte... yes
rte_annotation... yes
checking for src/scope... yes
scope... yes
checking for src/semantic_callgraph... yes
semantic_callgraph... yes
checking for src/slicing... yes
slicing... yes
checking for src/sparecode... yes
sparecode... yes
checking for src/syntactic_callgraph... yes
syntactic_callgraph... yes
checking for src/users... yes
users... yes
checking for src/value... yes
value_analysis... yes
checking for src/aorai/Makefile.in... yes
aorai... yes
checking for ltl2ba... yes
checking for src/report/Makefile.in... yes
report... yes
checking for src/security_slicing/Makefile.in... yes
security_slicing... yes
checking for src/wp/Makefile.in... yes
wp... yes
checking for why... yes
checking for why-dp... yes
checking for alt-ergo... yes
Fatal error: unknown C primitive `caml_expm1_float'
configure: alt-ergo version is .
configure: alt-ergo's array theory unsupported.
checking for coqc... yes
configure: *******************************************************
configure: * CONFIGURE TOOLS AND LIBRARIES USED BY SOME PLUG-INS *
configure: *******************************************************
checking for /usr/local/lib/ocaml/lablgtk2/lablgtk.cma... yes
checking for /usr/local/lib/ocaml/lablgtk2/lablgtksourceview2.cma... yes
checking for /usr/local/lib/ocaml/lablgtk2/lablgnomecanvas.cma... yes
checking for dot... yes
checking for /usr/local/lib/ocaml/dynlink.cmxa... no
configure: *************************************
configure: * CHECKING FOR PLUG-IN DEPENDENCIES *
configure: *************************************
configure: WARNING: native dynlink unavailable (ocaml 3.11 or higher required)
configure: *********************
configure: * CREATING MAKEFILE *
configure: *********************
configure: creating ./config.status
config.status: creating src/aorai/Makefile
config.status: creating src/report/Makefile
config.status: creating src/security_slicing/Makefile
config.status: creating src/wp/Makefile
config.status: creating cil/ocamlutil/perfcount.c
config.status: creating share/Makefile.config
configure: *******************************
configure: * SUMMARY: PLUG-INS AVAILABLE *
configure: *******************************
configure: semantic_constant_folding: yes
configure: from_analysis: yes
configure: gui: yes
configure: impact: yes
configure: inout: yes
configure: metrics: yes
configure: occurrence: yes
configure: pdg: yes
configure: postdominators: yes
configure: rte_annotation: yes
configure: scope: yes
configure: semantic_callgraph: yes
configure: slicing: yes
configure: sparecode: yes
configure: syntactic_callgraph: yes
configure: users: yes
configure: value_analysis: yes
configure: aorai: yes, static
configure: report: yes, static
configure: security_slicing: yes, static
configure: wp: yes, static
and then $make
luoting@luoting-desktop:~/frama-c2011/frama-c-Nitrogen-20111001$ make
Building ocamlgraph
make[1]: ?????? `/home/luoting/frama-c2011/frama-c-Nitrogen-20111001/ocamlgraph'
sed -e s/VERSION/1.8/ -e s/CMA/graph.cma/ -e s/CMXA/graph.cmxa/ \
META.in > META
rm -f src/version.ml
echo "let version = \""1.8"\"" > src/version.ml
echo "let date = \""`date`"\"" >> src/version.ml
rm -f .depend
ocamldep -slash -I src -I lib -I editor -I view_graph -I dgraph\
lib/*.ml lib/*.mli \
src/*.ml src/*.mli \
editor/*.mli editor/*.ml \
view_graph/*.mli view_graph/*.ml \
dgraph/*.mli dgraph/*.ml > .depend
make[1]:?????? `/home/luoting/frama-c2011/frama-c-Nitrogen-20111001/ocamlgraph'
make[1]: ?????? `/home/luoting/frama-c2011/frama-c-Nitrogen-20111001/ocamlgraph'
ocamlc -c -I src -I lib -g -dtypes src/version.ml
ocamlc -I src -I lib -pack -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/path.cmo src/traverse.cmo src/coloring.cmo src/topological.cmo src/components.cmo src/kruskal.cmo src/flow.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
File "_none_", line 1, characters 0-1:
Error: src/sig.cmi
is not a compiled interface
make[1]: *** [graph.cmo] ?? 2
make[1]:?????? `/home/luoting/frama-c2011/frama-c-Nitrogen-20111001/ocamlgraph'
make: *** [lib/graph.cmi] ?? 2
why?
Thanks!https://git.frama-c.com/pub/frama-c/-/issues/1946Strange problem with FRAMAC_LIB from Makefile.dynamic2021-02-22T13:47:01Zmantis-gitlab-migrationStrange problem with FRAMAC_LIB from Makefile.dynamicID0001305:
**This issue was created automatically from Mantis Issue 1305. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001305:
**This issue was created automatically from Mantis Issue 1305. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001305 | Frama-C | Kernel > Makefile | public | 2012-11-15 | 2012-11-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | signoles | **Resolution** | not fixable |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Sorry for the imprecise title, but I didn't manage to find what the real problem is...
With the attached very simplified Makefile:
$ make -fMake2 debugKo
gives:
[kernel] warning: cannot load plug-in `Report' (file not found). The exact failure is: /home/anne/Project/"/usr/local/lib/frama-c"/plugins/Report.cmxs.
Of course, the problem is there with any plugin (I just chose Report as an example so that you can try it).
After many tests, I found a workaround by setting FRAMAC_LIB (to the same value that it has before !!!), and then:
$ make -fMake2 debugOk
but I really have no idea why it works !!??
## Attachments
- [Make2](/uploads/f5577634f761478c2eca2239e6477ad8/Make2)https://git.frama-c.com/pub/frama-c/-/issues/1867Fatal error: exception Env.Error("C:\Frama-C\lib/pervasives.cmi")2021-04-15T15:18:02Zmantis-gitlab-migrationFatal error: exception Env.Error("C:\Frama-C\lib/pervasives.cmi")ID0001418:
**This issue was created automatically from Mantis Issue 1418. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001418:
**This issue was created automatically from Mantis Issue 1418. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001418 | Frama-C | Kernel > configure | public | 2013-05-09 | 2013-05-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | aogrcs | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I did as the INSTALL file said every time under Cygwin, the configure command always gave me this messag, why?
ThanksVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/1839initialization fails without explicitly setting FRAMAC_SHARE on Windows2021-02-22T13:43:49ZDavid Cokinitialization fails without explicitly setting FRAMAC_SHARE on WindowsID0001460:
**This issue was created automatically from Mantis Issue 1460. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001460:
**This issue was created automatically from Mantis Issue 1460. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001460 | Frama-C | Kernel > Makefile | public | 2013-07-18 | 2013-07-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DavidCok | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I configured, built and installed Frama-C per instructions and using defaults, on a Windows 7 sysmte under Cygwin.
No errors were reported in the process until I tried to run the given examples and my own, at which time this was reported:
test-framac $ frama-c -val pointer.c
[kernel] failure: Cannot find file libc\__fc_builtin_for_normalization.i, needed
for Frama-C initialization. Please check that /usr/local/share/frama-c is the c
orrect share path for Frama-C.
[kernel] Current source was: :0
The full backtrace is:
Raised at file "src/kernel/log.ml", line 523, characters 30-31
Called from file "src/kernel/log.ml", line 517, characters 9-16
Re-raised at file "src/kernel/log.ml", line 520, characters 15-16
Called from file "src/kernel/file.ml", line 170, characters 4-171
Called from file "src/project/project.ml", line 345, characters 12-15
Called from file "src/project/project.ml", line 350, characters 17-22
Re-raised at file "src/project/project.ml", line 350, characters 56-57
Called from file "queue.ml", line 135, characters 6-20
Called from file "src/project/project.ml", line 281, characters 2-21
Called from file "src/project/project.ml", line 292, characters 27-44
Called from file "src/kernel/boot.ml", line 69, characters 17-43
Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
Frama-C aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Fluorine-20130601.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at
:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reportin
g_guidelines
test-framac $
The file /usr/local/share/frama-c/libc/__fc_builtin_for_normalization.i
does indeed exist.
I managed to work around the problem by setting
FRAMAC_SHARE=C:/cygwin/usr/local/share/frama-c
explicitly, though the documentation implies that should be the default.
I suspect some issues with Cygwin vs. Windows paths.https://git.frama-c.com/pub/frama-c/-/issues/1802Install frama-c.top2021-02-22T13:42:33Zmantis-gitlab-migrationInstall frama-c.topID0001128:
**This issue was created automatically from Mantis Issue 1128. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001128:
**This issue was created automatically from Mantis Issue 1128. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001128 | Frama-C | Kernel > Makefile | public | 2012-03-22 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
At the moment, [make install] provides [frama-c], [frama-c.byte], [frama-c-gui] and [frama-c-gui].
It would be great if it could also install [frama-c-top] from [bin/toplevel.top].https://git.frama-c.com/pub/frama-c/-/issues/1779Getting frama-c version through --enable-external2021-02-22T13:41:31ZJulien SignolesGetting frama-c version through --enable-externalID0001070:
**This issue was created automatically from Mantis Issue 1070. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001070:
**This issue was created automatically from Mantis Issue 1070. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001070 | Frama-C | Kernel > configure | public | 2012-01-23 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
In a configure of an external plug-in, it would be useful to check the Frama-C version. A basic solution which would be based on "frama-c -version" is not correct when the configure is called through --enable-external.
### Steps To Reproduce :
At this day, plug-in E-ACSL does this by running frama-c -version.https://git.frama-c.com/pub/frama-c/-/issues/1742actions done with make install -n (svn 10897)2021-02-22T13:39:54ZStephane Dupratactions done with make install -n (svn 10897)ID0000637:
**This issue was created automatically from Mantis Issue 637. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000637:
**This issue was created automatically from Mantis Issue 637. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000637 | Frama-C | Kernel > Makefile | public | 2010-12-13 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sduprat | **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 Carbon-20110201 |
### Description :
Soit un rep d'installation que j'utilise dans la ligne configure et qui est vide au départ :
./configure -prefix <rep-install>
dans l'arborescence frama-c, après avoir fait le make, je fais un "make install -n" et je m'attend à voir la liste des commandes de recopie dans le rep <rep-install> sans que les commandes soient effectuées (option -n).
Enfin, je constate qu'une certaine partie des commandes ont été réalisées avec pour preuve la création du répertoire lib/frama-c dans <rep-install>.
Stéphane
Le 13/12/2010 10:06, BAUDIN Patrick a écrit :
> Bonjour Stéphane,
> Peut-tu être un peu plus explicite sur l'emplacement de ce répertoire lib
> et sur son contenu (avant et après la commande) ?
> Cdlt,
> Patrick
>> Bonjour,
>> J'ai fait un "make install -n" qui a pris un peu de temps.
>> Après vérification, le répertoire lib a été créé dans le répertoire cible,
>> Cdlt,
>> Stéphanehttps://git.frama-c.com/pub/frama-c/-/issues/1704Makefile.dynamic should always write to $(DESTDIR)2021-02-22T14:04:39Zmantis-gitlab-migrationMakefile.dynamic should always write to $(DESTDIR)ID0000528:
**This issue was created automatically from Mantis Issue 528. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000528:
**This issue was created automatically from Mantis Issue 528. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000528 | Frama-C | Kernel > Makefile | public | 2010-07-04 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jonathan-Christofer Demay | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
When a dynamic plugin is being built in a sandbox, the install process should always write to $(DESTDIR).
This is already the case for everything that go into $(BINDIR), but not into $(PLUGIN_INSTALL_DIR)
The attached patch fixes that.
However, the part that updates 'known_plugins.ac' is also a problem for the same reason. I haven't figured out yet what to do with it, so as of now it is just disabled.
## Attachments
- [frama-c-20100401-fix_plugin_install.patch](/uploads/7e04dbc072a4cb1e468f7acf80d06b64/frama-c-20100401-fix_plugin_install.patch)https://git.frama-c.com/pub/frama-c/-/issues/1674.make-ocamlgraph is not needed when using non-local ocamlgraph2021-02-22T13:37:38Zmantis-gitlab-migration.make-ocamlgraph is not needed when using non-local ocamlgraphID0000460:
**This issue was created automatically from Mantis Issue 460. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000460:
**This issue was created automatically from Mantis Issue 460. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000460 | Frama-C | Kernel > Makefile | public | 2010-04-27 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
When using a non-local ocamlgraph (and when I don't have the tarball of ocamlgraph), ".make-ocamlgraph" fails (which is expected), but note that there is no need to unpack ocamlgraph.tar.gz if I'm not going to use it.
Please find attached a patch to fix this issue.
Regards,
--
Mehdi
## Attachments
- [0002-.make-ocamlgraph-no-op-for-non-local-ocamlgraph.patch](/uploads/05d9ef799f99f0326a7dc5be945cb24b/0002-.make-ocamlgraph-no-op-for-non-local-ocamlgraph.patch)https://git.frama-c.com/pub/frama-c/-/issues/1673Frama-c-gui doesn't install on bytecode architecture2021-02-22T14:03:33Zmantis-gitlab-migrationFrama-c-gui doesn't install on bytecode architectureID0000461:
**This issue was created automatically from Mantis Issue 461. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000461:
**This issue was created automatically from Mantis Issue 461. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000461 | Frama-C | Kernel > Makefile | public | 2010-04-27 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
The target 'gui' depends directly on 'bin/viewer.opt$(EXE)' which cannot be built on bytecode-only architecutres. Thus, the build and installation fail.
Furthermore, in /usr/lib/frama-c, there are some .cmx files installed without their implementation (their corresponding .o or .a files). If those files are going to be used to build plugins, then the implementation is needed.
Please find attached a patch that fixes both issues.
Regards,
--
Mehdi
## Attachments
- [0003-Fix-build-on-bytecode-only-architectures.patch](/uploads/fc5f7364e5c068ea30982ccb0e07d0a4/0003-Fix-build-on-bytecode-only-architectures.patch)