frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:02:38Zhttps://git.frama-c.com/pub/frama-c/-/issues/443Implementation <-> Documentation Inconsistency2021-02-22T13:02:38Zmantis-gitlab-migrationImplementation <-> Documentation InconsistencyID0000595:
**This issue was created automatically from Mantis Issue 595. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000595:
**This issue was created automatically from Mantis Issue 595. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000595 | Frama-C | Documentation | public | 2010-10-04 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kalyan | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | Frama-C Carbon-20101201-beta1 | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
I see that the Plug-in development guide is not accurate (or consistent with the implementation, if I should put it this way). It makes it difficult for beginners to work with plugin-development, especially using visitors. For example, Section 4.14.3 (Action Performed) and compare it with the implementation, you don't see any DoChildrenPost () and you don't see any JustCopyPost () in the guide. It would be great if you update the plugin-development guide as and when you make changes in the implementation.https://git.frama-c.com/pub/frama-c/-/issues/442Patch for Cross Compiling OCaml-3.12.0(for arm-linux)2021-02-22T13:02:37Zmantis-gitlab-migrationPatch for Cross Compiling OCaml-3.12.0(for arm-linux)ID0000631:
**This issue was created automatically from Mantis Issue 631. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000631:
**This issue was created automatically from Mantis Issue 631. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000631 | Frama-C | Documentation | public | 2010-11-25 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Frank-Chen | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The patch I am uploading is from Eric Cooper(ecc@cmu.edu,http://www.cs.cmu.edu/~ecc/).He sent it to me a month ago.With the patch , I succeeded in making a OCaml-cross-compiler-3.12.0(with a new EABI based arm-linux-gcc-4.3.2),and when I used it to cross-compile mldonkey-3.0.2,mlnet was also generated successfully(you have to configrue with "./configure --enable-ocamlver=3.12.0 --host=arm-linux" and build some .o files with the "compile_by_hand.sh" I am also uploading).But Because this OCaml-cross-compiler-3.12 seems to only support the new EABI but my target machine just supports the old ABI(and the gcc cross compiler of my machine just supports soft float-point), I can't run it on my target machine and don't know whether the mlnet can run perfectly in a new EABI based machine.So I 'd like to upload the patch here and all of you can test it.Maybe someone who want to do a cross-compiling will find it useful.
By the way ,does this kind of version of OCaml which supports soft float-point and the Old ABI(not the new EABI) exist?It seems that OCaml 3.12 adds soft float-point and EABI support together,but I just need soft float-point and the Old ABI.
Best Regards!
Frank-Chen
## Attachments
- [cross-compiler-for-arm-target.patch](/uploads/068b76e2937191decde9dec773884cdf/cross-compiler-for-arm-target.patch)
- [README.cross](/uploads/a9a7684367b4eb08069863d3e15f62c1/README.cross)
- [compile_by_hand.sh](/uploads/cf6e415fcbf8a46c91bdd530c9b04203/compile_by_hand.sh)https://git.frama-c.com/pub/frama-c/-/issues/441mismatch between configure check and INSTALL requirements for ocamlgraph version2021-02-22T14:00:33ZJulien Signolesmismatch between configure check and INSTALL requirements for ocamlgraph versionID0000757:
**This issue was created automatically from Mantis Issue 757. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000757:
**This issue was created automatically from Mantis Issue 757. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000757 | Frama-C | Documentation | public | 2011-03-17 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
configure checks an exact version number for ocamlgraph, while INSTALL says >=.
### Additional Information :
Don't know what is the best thing to do:
- allowing >= is better, but requires that ocamlgraph is stable enough (forward compatibility). Not sure that it is the case yet :-(.
- allowing only = is simpler, but much less flexible for users.https://git.frama-c.com/pub/frama-c/-/issues/440cannot deal with many files2021-02-22T13:38:02Zmantis-gitlab-migrationcannot deal with many filesID0000778:
**This issue was created automatically from Mantis Issue 778. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000778:
**This issue was created automatically from Mantis Issue 778. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000778 | Frama-C | Documentation | public | 2011-04-08 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | njucslzh | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | block | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I have many files which are in a project to analysis , it always cannot correctly preprocess them. Errors as follow:
[gui] warning: Frama-C images not found. Is FRAMAC_SHARE correctly set?
[kernel] preprocessing with "gcc -C -E -I. /home/lzh/cvs-1.11.4/src/zlib.c"
[kernel] user error: failed to run: gcc -C -E -I. -o '/tmp/zlib.c788cad.i' '/home/lzh/cvs-1.11.4/src/zlib.c'
you may set the CPP environment variable to select the proper preprocessor command or use the option "-cpp-command".
[kernel] user error: skipping file "/home/lzh/cvs-1.11.4/src/zlib.c" that has errors.
### Additional Information :
For toy program with two or three simply files, I just change c files to i files directly , it works well. But in practical , this don't work. Can you show me how to preprocess and merge the Source Code files? It is described too little in user manual .https://git.frama-c.com/pub/frama-c/-/issues/437gui and doc2021-02-22T13:57:53ZMuriel Rogergui and docID0001014:
**This issue was created automatically from Mantis Issue 1014. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001014:
**This issue was created automatically from Mantis Issue 1014. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001014 | Frama-C | Documentation | public | 2011-11-10 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | muriel | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
generation of documentation (via make doc) has permanently fail when gui is not installed :
File "src/occurrence/register_gui.ml", line 23, characters 0-18:
Error: Unbound module Pretty_source
1 error(s) encounteredhttps://git.frama-c.com/pub/frama-c/-/issues/436Cute boolean options too cute for their own good2021-02-22T13:02:29ZPascal CuoqCute boolean options too cute for their own goodID0001085:
**This issue was created automatically from Mantis Issue 1085. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001085:
**This issue was created automatically from Mantis Issue 1085. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001085 | Frama-C | Documentation | public | 2012-02-08 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
$ bin/toplevel.opt -kernel-help
Description: General options provided by the Frama-C kernel
Most options of the form '-option-name' and without any parameter
have an opposite with the name '-no-option-name'.
***** LIST OF AVAILABLE OPTIONS:
*** ANALYSIS OPTIONS
...
-safe-arrays for arrays that are fields inside structs, assume that
accesses are in bounds (set by default)
...
There is no way to know that the option to unset this option is -unsafe-arrayshttps://git.frama-c.com/pub/frama-c/-/issues/433Fraunhofer FIRST -> Fraunhofer FOKUS2021-02-22T13:02:21ZJens GerlachFraunhofer FIRST -> Fraunhofer FOKUSID0001334:
**This issue was created automatically from Mantis Issue 1334. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001334:
**This issue was created automatically from Mantis Issue 1334. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001334 | Frama-C | Documentation | public | 2012-12-17 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
Fraunhofer FIRST has been merged into Fraunhofer FOKUS.
Please change URL on http://frama-c.com/wp.html to
www.fokus.fraunhofer.dehttps://git.frama-c.com/pub/frama-c/-/issues/432new link to ACSL by Example2021-02-22T13:02:20ZJens Gerlachnew link to ACSL by ExampleID0001335:
**This issue was created automatically from Mantis Issue 1335. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001335:
**This issue was created automatically from Mantis Issue 1335. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001335 | Frama-C | Documentation | public | 2012-12-17 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
Due to the merge of Fraunhofer FIRST with Fraunhofer FOKUS there is a new URL for the "ACSL by Example" documents.
I suggest to add the new URL
http://www.fokus.fraunhofer.de/de/quest/_download_quest/_projekte/acsl_by_example.pdf
on
http://frama-c.com/wp.htmlhttps://git.frama-c.com/pub/frama-c/-/issues/430suggest to mention in acsl manual that \valid shouldn't be applied to functio...2021-02-22T13:37:44ZJochen Burghardtsuggest to mention in acsl manual that \valid shouldn't be applied to function pointersID0001367:
**This issue was created automatically from Mantis Issue 1367. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001367:
**This issue was created automatically from Mantis Issue 1367. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001367 | Frama-C | Documentation > ACSL | public | 2013-02-14 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
Running "frama-c -val ftest.c" on the attached program reports an unsatisfied precondition in line 4, where \valid has been applied to a pointer to the function foo().
From that behavior, I guess that \valid mustn't be applied to function pointers in general.
However, the acsl manual (acsl.pdf) says on p.54: "\valid applies to a set of terms (see Section 2.3.4) of some pointer type."
An apprioriate restriction to non-function-pointers could be added here.
## Attachments
- [ftest.c](/uploads/c71026e5e16313bc3e6a7391145d1eee/ftest.c)https://git.frama-c.com/pub/frama-c/-/issues/429Namespace through packs - packing frama-c cmx into a cmxa2022-09-28T11:09:00Zmantis-gitlab-migrationNamespace through packs - packing frama-c cmx into a cmxaID0002163:
**This issue was created automatically from Mantis Issue 2163. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002163:
**This issue was created automatically from Mantis Issue 2163. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002163 | Frama-C | Kernel | public | 2015-09-16 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | bobot | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
It would be great if you could add an extra -for-pack FramaC to each byte/native code file compilation.
A way to do it, is to call the makefile with
FRAMAC_USER_FLAGS="-for-pack FramaC" make
But the Makefile.plugin has to be modified to name its pack FramaC.PLUGIN_NAME
This would enable the construction of a packed framaC.cmx and then a library framaC.cmxa.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/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/425Creating a pointer to a local causes valid pointers above it to lose thier va...2021-04-15T08:03:30Zmantis-gitlab-migrationCreating a pointer to a local causes valid pointers above it to lose thier valid statusID0002234:
**This issue was created automatically from Mantis Issue 2234. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002234:
**This issue was created automatically from Mantis Issue 2234. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002234 | Frama-C | Plug-in > wp | public | 2016-06-21 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jrobbins | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Pointers that are \valid lose their status as \valid if there is code below it that assigns to a pointer. This only seems to happen when the pointer in question is wrapped in a struct.
### Additional Information :
Tested on Aluminum on a Linux machine.
### Steps To Reproduce :
== file bug.c:
struct s {
int* ptr;
};
/*@
requires \valid(t.ptr);
@*/
void foo(struct s t) {
//@ assert \valid(t.ptr);
int a;
int* x = &a;
}
== Run command:
frama-c bug.c -wp
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_foo_assert : Unknown (51ms)
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unknown: 1)
== File fixed.c:
struct s {
int* ptr;
};
/*@
requires \valid(t.ptr);
@*/
void foo(struct s t) {
//@ assert \valid(t.ptr);
int a;
int* x; // = &a;
}
== Run command:
frama-c bug.c -wp
== Output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing bug.c (with preprocessing)
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] Proved goals: 1 / 1
Qed: 1Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/424Add remark about additional axioms for read clauses2022-09-08T08:56:38ZJens GerlachAdd remark about additional axioms for read clausesID0001698:
**This issue was created automatically from Mantis Issue 1698. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001698:
**This issue was created automatically from Mantis Issue 1698. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001698 | Frama-C | Documentation > ACSL | public | 2014-03-14 | 2016-06-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | patrick | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
As long as WP does not generate foot prints for reads clauses of axiomatic declarations (see
https://bts.frama-c.com/view.php?id=1693), it might be helpful for users to understand, that it is their responsibility to formulate additional axioms/lemmas to express the foot print.
This could be added to Section 2.6.10 of
"ACSL Version 1.8 Implementation in Neon-20140301".https://git.frama-c.com/pub/frama-c/-/issues/423empty class instance as method argument leads to user error2021-02-22T14:01:31ZJochen Burghardtempty class instance as method argument leads to user errorID0001951:
**This issue was created automatically from Mantis Issue 1951. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001951:
**This issue was created automatically from Mantis Issue 1951. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001951 | Frama-Clang | Plug-in > Eva | public | 2014-11-03 | 2016-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubunto-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
calling "frama-c -val 116.cpp" eventually leads to a user error:
[value] Done for function foo::Ctor
116.cpp:10:[value] user error: Function argument __fc_tmp_0 has unknown size. Aborting
[kernel] Plug-in value aborted: invalid user input.
The error message disappears if either
1) a variable (e.g. "int v;" after line 3) is declared inside class "foo",
2) the call "f.cat(f);" is omitted in line 10, or
3) the argument type of "cat" is changed to "int" in line 5 and "f" is replaced by "0" in line 10.
Apparently, the "f" in line 10 somehow causes an empty struct to be generated, which is not properly accepted.
## Attachments
- [116.cpp](/uploads/81a0fbdbba99b70ad2ddefa6b4bf3272/116.cpp)https://git.frama-c.com/pub/frama-c/-/issues/422suggest to suppress "Neither code nor specification" warning for __builtin_va...2021-02-22T13:37:15ZJochen Burghardtsuggest to suppress "Neither code nor specification" warning for __builtin_va_startID0001368:
**This issue was created automatically from Mantis Issue 1368. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001368:
**This issue was created automatically from Mantis Issue 1368. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001368 | Frama-C | Kernel | public | 2013-02-14 | 2016-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | valentin.perrelle | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
Running "frama-c -val ftest.c" on the attached program results in a "[kernel] warning: Neither code nor specification for function __builtin_va_start, generating default assigns from the prototype".
However,
(1) it is impossible to provide a fully general definition of that function;
(2) providing a special version adapted to our example results in a declaration-mismatch error, (which disappears when the name is changed to e.g. "__builtin_va_star2", so the name "__builtin_va_start" is in fact known to Frama-C).
I suggest to suppress the former warning "Neither code nor specification..." for __builtin_va_start(), and similar for va_end(), etc.
## Attachments
- [ftest.c](/uploads/e9165646a4e7b8fd718d1b64bea5964e/ftest.c)https://git.frama-c.com/pub/frama-c/-/issues/420Log message when plevel is used in logic needed2021-02-22T13:02:00ZPascal CuoqLog message when plevel is used in logic neededID0001674:
**This issue was created automatically from Mantis Issue 1674. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001674:
**This issue was created automatically from Mantis Issue 1674. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001674 | Frama-C | Plug-in > Eva | public | 2014-03-05 | 2016-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | low | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Program:
extern int Frama_C_entropy_source;
/*@ requires \valid(p + (0 .. l-1));
assigns p[0 .. l-1] \from Frama_C_entropy_source;
assigns Frama_C_entropy_source \from Frama_C_entropy_source;
ensures \initialized(p + (0 .. l-1));
*/
void mu(char *p, unsigned l);
main(){
int a[48], b[53];
mu(&a, sizeof a);
mu(&b, sizeof b);
}
$ frama-c -val ~/t.c
Obtained result:
...
[value] computing for function mu <- main.
Called from /Users/pascal/t.c:12.
[value] using specification for function mu
/Users/pascal/t.c:3:[value] Function mu: precondition got status valid.
[value] Done for function mu
[value] computing for function mu <- main.
Called from /Users/pascal/t.c:13.
[value] Done for function mu
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
a[0..47] ∈ [--..--]
b[0..52] ∈ [--..--] or UNINITIALIZED
Wished result:
Warning: more than 200 locations to reduce. Approximating. See option -plevel.https://git.frama-c.com/pub/frama-c/-/issues/419No convenient way to specify shared library functions as assigns clauses2021-02-22T13:37:09ZPascal CuoqNo convenient way to specify shared library functions as assigns clausesID0001479:
**This issue was created automatically from Mantis Issue 1479. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001479:
**This issue was created automatically from Mantis Issue 1479. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001479 | Frama-C | Kernel > ACSL implementation | public | 2013-09-05 | 2016-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | low | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Shared libraries functions store their entire state in a struct, in a pattern similar to that of the attached code.
It would be convenient to have a way to specify that while *ctx_p is computed \from *ctx_p, the pointer field(s) are used only by address and should not pollute the integer fields.
Currently:
$ ~/ppc/bin/toplevel.opt -val modular.c
…
[value] Values at end of function main:
ctx ? {{ garbled mix of &{ctx} (origin: Misaligned {modular.c:21}) }}
y ? {{ garbled mix of &{ctx} (origin: Misaligned {modular.c:21}) }}
## Attachments
- [modular.c](/uploads/d23c0d7f1d7d0eef2b867422055b0869/modular.c)https://git.frama-c.com/pub/frama-c/-/issues/418Cil does not reject incorrect initializers2021-02-22T13:37:05ZBoris YakobowskiCil does not reject incorrect initializersID0000936:
**This issue was created automatically from Mantis Issue 936. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000936:
**This issue was created automatically from Mantis Issue 936. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000936 | Frama-C | Kernel | public | 2011-08-24 | 2016-07-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Cil should reject the initializers of the following program
int x = 1;
int y = x ^ 0;
int main () {
return y;
}
### Additional Information :
(Code such as
const int x = 1;
const int y = x ^ 0;
has seen been seen in the wild. An option that would force Cil to give a warning instead of an error in this case would be nice.)https://git.frama-c.com/pub/frama-c/-/issues/416Ocamlfind cannod be found2021-02-22T13:01:51Zmantis-gitlab-migrationOcamlfind cannod be foundID0002238:
**This issue was created automatically from Mantis Issue 2238. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002238:
**This issue was created automatically from Mantis Issue 2238. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002238 | Frama-C | Kernel | public | 2016-07-05 | 2016-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | alx | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux Fedora | **OS Version** | 24 |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-C crashes when run on a system without ocamlfind with Unexpected error.
### Additional Information :
I run frama-c precisely as
/usr/bin/frama-c -wp -wp-prop="-@assigns" -wp-model "Typed+cast" -wp-rte -wp-gen -wp-proof why3 -cpp-command="gcc -C -E -D_FRAMAC_ -I. -I./libc/" -wp-why-lib why-libs/MemoryAdd.why -wp-out checker_proofs envmap_base.c
[kernel] Current source was: :0
The full backtrace is:
Raised at file "pervasives.ml", line 30, characters 22-33
Called from file "findlib.ml", line 150, characters 10-151
Called from file "src/kernel_services/plugin_entry_points/dynamic.ml", line 292, characters 4-47
Called from file "src/kernel_services/plugin_entry_points/kernel.ml", line 598, characters 4-44
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 831, characters 2-22
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (Failure("Config file not found - neither /etc/ocamlfind.conf nor the directory /etc/ocamlfind.conf.d")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Aluminium-20160501.
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_reporting_guidelines
### Steps To Reproduce :
1. Reinstall packet ocaml-findlib.x86_64 and delete directories
/etc/ocamlfind.conf
/etc/ocamlfind.conf.d"
2. Try to run frama-c on a file