frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-05-10T17:02:04Zhttps://git.frama-c.com/pub/frama-c/-/issues/1260Dynamic plugin doc2023-05-10T17:02:04Zmantis-gitlab-migrationDynamic plugin docID0000754:
**This issue was created automatically from Mantis Issue 754. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000754:
**This issue was created automatically from Mantis Issue 754. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000754 | Frama-C | Kernel > Makefile | public | 2011-03-16 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C Nitrogen-20111001 | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
The command : make xxx_DOC (where xxx is a dynamic plugin name) fails with the message :
Pas de règle pour fabriquer la cible « /kernel-doc.ocamldoc »
This is because $(DOC_DIR) is not defined, which seems normal (I far as I know, the compilation of dynamic plugin refers to the installed files, not to the source repository).
The easiest fix would probably be that a plugin internal documentation doesn't depend on the kernel documentation...https://git.frama-c.com/pub/frama-c/-/issues/1252the input file should be the first argument to ptests2023-04-21T13:20:33ZJulien Signolesthe input file should be the first argument to ptestsID0000736:
**This issue was created automatically from Mantis Issue 736. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000736:
**This issue was created automatically from Mantis Issue 736. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000736 | Frama-C | ptests | public | 2011-02-23 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | high | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
all in the title... Required in order to use -then* in tests.https://git.frama-c.com/pub/frama-c/-/issues/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/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/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/427Path for 'make install-doc-code' for external plug-in2022-09-28T11:10:32Zmantis-gitlab-migrationPath for 'make install-doc-code' for external plug-inID0001278:
**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 BobotFrançois Bobothttps://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/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/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/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/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/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/1142Configure script's autolocation of local OcamlGraph breaks out of tree builds2021-03-29T13:54:27Zmantis-gitlab-migrationConfigure script's autolocation of local OcamlGraph breaks out of tree buildsID0001454:
**This issue was created automatically from Mantis Issue 1454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001454:
**This issue was created automatically from Mantis Issue 1454. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001454 | Frama-C | Kernel > configure | public | 2013-07-08 | 2014-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sstewartgallus | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I prefer to build my software packages out of tree. My personal arrangement is to have one sources directory, and one builds directory. I would then run my packages configure script inside a subdirectory of the sources directory specifically for that package, and build from there.
It is great that a version of OcamlGraph is distributed with Frama-C but unfortunately the configure script can only find it if the current directory is the source directory, and this breaks out of tree builds.
The problematic line in configure.in appears to be:
AC_CHECK_FILE($OCAMLGRAPH_LOCAL,OCAMLGRAPH_EXISTS=yes)
This line could probable be fixed in multiple ways. There's probably an autoconf macro for looking for a file in the source directory that's better than AC_CHECK_FILE, or one could define OCAMLGRAPH_LOCAL to use the invocation of ./configure to locate the directory it's located in (which would be something like ("$(cd $(dirname $0) && pwd)/ocamlgraph".)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/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/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/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/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/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)