frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:00:07Zhttps://git.frama-c.com/pub/frama-c/-/issues/355Cast on funspec not considering typedef2021-02-22T13:00:07ZDillon ParienteCast on funspec not considering typedefID0001518:
**This issue was created automatically from Mantis Issue 1518. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001518:
**This issue was created automatically from Mantis Issue 1518. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001518 | Frama-C | Kernel | public | 2013-10-25 | 2017-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
[STANCE]
The following code:
/* Generated by Frama-C */
struct rr;
typedef struct rr rr;
struct apf;
struct rr {
struct apf *of ;
};
typedef struct apf apf;
struct apf {
apf *next ;
rr *r ;
};
/*@ requires r->of == ((void *)0); */
static apf *f(rr *r)
{
apf *__retres;
__retres = r->of;
return __retres;
}
analyzed by:
frama-c -no-unicode cast.c -ocode cast2.c -print ; frama-c -no-unicode cast2.c
generates an error:
cast2.c:13:[kernel] user error: unexpected token 'apf'
[kernel] user error: skipping file "cast2.c" that has errors.
[kernel] Frama-C aborted: invalid user input.https://git.frama-c.com/pub/frama-c/-/issues/356Axiomatic is recompiled when using severalprocesses2021-02-22T13:00:08ZJens GerlachAxiomatic is recompiled when using severalprocessesID0001685:
**This issue was created automatically from Mantis Issue 1685. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001685:
**This issue was created automatically from Mantis Issue 1685. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001685 | Frama-C | Plug-in > wp | public | 2014-03-12 | 2017-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **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 :
When verifying with alt-ergo and coq the file Axiomatic seems to be compiled again and again.
As far as I understood, alt-ergo seems to kill the coq process.
### Steps To Reproduce :
In fact, I noticed this problem in Neon.https://git.frama-c.com/pub/frama-c/-/issues/359Provide an option to run Coq from Frama-C2021-02-22T13:00:10ZJens GerlachProvide an option to run Coq from Frama-CID0001686:
**This issue was created automatically from Mantis Issue 1686. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001686:
**This issue was created automatically from Mantis Issue 1686. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001686 | Frama-C | Plug-in > wp | public | 2014-03-12 | 2017-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
When proving external Coq-lemma for WP it might be interesting to run Coq from Frama-C, e.g.,
frama-c -wp-coq Foo.vhttps://git.frama-c.com/pub/frama-c/-/issues/361Warning depens on type of volatile variable2021-02-22T13:00:14Zmantis-gitlab-migrationWarning depens on type of volatile variableID0002281:
**This issue was created automatically from Mantis Issue 2281. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002281:
**This issue was created automatically from Mantis Issue 2281. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002281 | Frama-C | Plug-in > Eva | public | 2017-02-15 | 2017-03-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Cygwin | **OS** | Windows 7 | **OS Version** | x64 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-C generates warnings in depend on signed or unsigned volatile variable.
### Steps To Reproduce :
Run EVA analysis for attached file.
## Attachments
- [test_volatile.c](/uploads/dc40a5352e3d5a758e7adc2754d4b4d4/test_volatile.c)https://git.frama-c.com/pub/frama-c/-/issues/362More precise deps when calldeps computation2021-02-22T13:00:15Zmantis-gitlab-migrationMore precise deps when calldeps computationID0001633:
**This issue was created automatically from Mantis Issue 1633. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001633:
**This issue was created automatically from Mantis Issue 1633. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001633 | Frama-C | Plug-in > from | public | 2014-01-27 | 2017-03-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | suspended |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When both -calldeps (for precise computation) and -deps (for the synthesis) options are used, it would be great to use to calldeps results to produce the deps. For instance, in the example below, f is called only once, and its calldeps are precise, but the deps merge all the deps from the 'inc' function. One would expect deps and calldeps to be the same when there is only one call to a function.
### Additional Information :
Results:
from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function inc:
X FROM X; Y; p (and SELF)
Y FROM X; Y; p (and SELF)
[from] Function f:
X FROM X; Y (and SELF)
Y FROM X; Y (and SELF)
[from] Function main:
X FROM X; Y (and SELF)
Y FROM X; Y (and SELF)
[from] ====== END OF DEPENDENCIES ======
[from] ====== DISPLAYING CALLWISE DEPENDENCIES ======
[from] call to inc at calldeps.c:3 (by f):
Y FROM Y; p
[from] call to inc at calldeps.c:4 (by main):
X FROM X; p
[from] call to f at calldeps.c:4 (by main):
Y FROM Y
[from] entry point:
X FROM X
Y FROM Y
[from] ====== END OF CALLWISE DEPENDENCIES ======
### Steps To Reproduce :
Example:
int X, Y;
void inc (int * p) { (*p)++; }
void f (void) { inc (&Y); }
void main (void) { inc (&X); f (); }
$ frama-c -deps -calldeps calldeps.chttps://git.frama-c.com/pub/frama-c/-/issues/363suggest to report column number for warnings2021-02-22T13:00:16ZJochen Burghardtsuggest to report column number for warningsID0002268:
**This issue was created automatically from Mantis Issue 2268. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002268:
**This issue was created automatically from Mantis Issue 2268. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002268 | Frama-C | Plug-in > Eva | public | 2017-01-09 | 2017-03-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | won't fix |
| **Priority** | low | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | xubuntu | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I suggest to print the column number in addition to the line number at each warning of the value analysis' batch (i.e. non-gui) version. This feature could be made on/off-switchable via a command line option. I guess it is easy to implement.
The interest in this information is motivated by an attempt to compare warning counts for (e.g.) "out of bounds read" between Frama-C and Polyspace. The latter aggregates all warnings referring to the same code location into a single one. Obtaining comparable counts from Frama-C can be done by appropriate postprocessing of its stdout stream. However, Frama-C warnings that refer to the same line, but different columns, shouldn't be joined into a single one, since Polyspace e.g. emits and counts 2 warnings for the code "a = b[i] + c[i]" when both array accesses may be out of bounds. Having both line and column number in Frama-C warnings would allow one to exactly duplicate the counting method of Polyspace.
## Attachments
- [patch-column.diff](/uploads/2d64aea8191ef7073bf8e7905a8f859a/patch-column.diff)https://git.frama-c.com/pub/frama-c/-/issues/376Assertion failure when unrolling types of struct members2021-02-22T13:00:35ZKostyantyn VorobyovAssertion failure when unrolling types of struct membersID0002191:
**This issue was created automatically from Mantis Issue 2191. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002191:
**This issue was created automatically from Mantis Issue 2191. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002191 | Frama-C | Plug-in > E-ACSL | public | 2015-12-04 | 2017-01-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | Frama-C 14-Silicon |
### Description :
/* The following program leads to a failure of an assertion in translate.ml. The failure seems to be due to E-ACSL inability to determine the type of the term _G[0].str. */
struct ST {
char *str;
int num;
};
struct ST _G[] = {
{
.str = "Struct_G[0]",
.num = 99
},
{
.str = "Struct_G[1]",
.num = 147
}
};
int main(int argc, char **argv) {
/*@ assert \valid_read(_G[0].str); */
return 0;
}https://git.frama-c.com/pub/frama-c/-/issues/378Incorrect code generation with gmp2021-02-22T13:00:41ZKostyantyn VorobyovIncorrect code generation with gmpID0002231:
**This issue was created automatically from Mantis Issue 2231. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002231:
**This issue was created automatically from Mantis Issue 2231. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002231 | Frama-C | Plug-in > E-ACSL | public | 2016-06-14 | 2017-01-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | X86-64 | **OS** | Linux | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | Frama-C Aluminium | **Fixed in Version** | Frama-C 14-Silicon |
### Description :
In some tricky cases involving multiple casts gmp-generated code is incorrect which leads to segmentation faults due to improper use of gmp library.
For instance, in the example (see attached file) the following code is generated:
unsigned long __gen_e_acsl_cast;
mpz_t __gen_e_acsl__2;
...
__gmpz_sub(__gen_e_acsl_sub,(__mpz_struct const *)__gen_e_acsl_cast,
(__mpz_struct const *)(__gen_e_acsl__2));
This results in a segmentation fault because __gmpz_sub expects a mpz_t, not an integer.
### Steps To Reproduce :
The attached file is instrumented with E-ACSL, compiled and executed
## Attachments
- [mcf_slice.c](/uploads/7444bfe912aba62ff524eae88fda8095/mcf_slice.c)https://git.frama-c.com/pub/frama-c/-/issues/379The disproportion between block sizes and caption sizes on a callgrath.2021-02-22T13:00:42Zmantis-gitlab-migrationThe disproportion between block sizes and caption sizes on a callgrath.ID0002273:
**This issue was created automatically from Mantis Issue 2273. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002273:
**This issue was created automatically from Mantis Issue 2273. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002273 | Frama-C | Graphical User Interface | public | 2017-01-17 | 2017-01-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Max P. | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Cygwin | **OS** | Windows 7 | **OS Version** | x64 SP1 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Callgraph looks as on attached screenshot.
### Additional Information :
After the first callgraph opening the warning is generated:
(frama-c-gui.exe:8512): Pango-WARNING **: couldn't load font "Times-Roman Not-Rotated 14", falling back to "Sans Not-Rotated 14", expect ugly output.
### Steps To Reproduce :
In GUI select command "Show callgraph".
## Attachments
- ![Global_view_2](/uploads/1b6b6f23c7eca80972a9107e1c51f3b8/Global_view_2.png)https://git.frama-c.com/pub/frama-c/-/issues/384coq 8.5: cannot find Memory.v2021-02-22T13:00:50ZJens Gerlachcoq 8.5: cannot find Memory.vID0002208:
**This issue was created automatically from Mantis Issue 2208. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002208:
**This issue was created automatically from Mantis Issue 2208. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002208 | Frama-C | Plug-in > wp | public | 2016-02-11 | 2017-01-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
After updating my Frama-C installation through opam to coq.8.5 and why3.0.86.3 I observe the following error. When compiling the attached file with
coqc -R /Users/jens/.opam/system/share/frama-c/wp/coqwp -as "" WP_basics.v
I receive the following error message:
File "./WP_basics.v", line 3, characters 15-21:
Error: Unable to locate library Memory.
With coq.8.4.6 and earlier I did not observe this error.
### Additional Information :
The path '/Users/jens/.opam/system/share/frama-c' points to my Frama-C share.
ls -l /Users/jens/.opam/system/share/frama-c/wp/coqwp/Memory.v
produces
-rw-r--r-- 1 jens staff 10160 11 Feb 10:38 /Users/jens/.opam/system/share/frama-c/wp/coqwp/Memory.v
## Attachments
- [WP_basics.v](/uploads/e9bbf929a84471fcc0ca1d0a5755739b/WP_basics.v)https://git.frama-c.com/pub/frama-c/-/issues/391wrong example code in value analysis manual, p.35, for message " invalid LHS ...2021-02-22T13:01:00ZJochen Burghardtwrong example code in value analysis manual, p.35, for message " invalid LHS operand for left shift"ID0002257:
**This issue was created automatically from Mantis Issue 2257. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002257:
**This issue was created automatically from Mantis Issue 2257. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002257 | Frama-C | Documentation > manuals | public | 2016-11-21 | 2016-12-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
p.35 (top) of the value analysis manual shows the code from the attached file "lshift_orig.c". However, "frama-c -val lshift_orig.c" does not emit the warning "invalid LHS operand for left shift. assert 0 <= x;" shown in the manual. In fact, x is only written, not read, by the code.
Probably, the code should be like that in file "lshift_new.c". Frama-C emits "lshift_new.c:3:[kernel] warning: invalid LHS operand for left shift. assert 0 ≤ c;" and "lshift_new.c:3:[kernel] warning: signed overflow. assert c<<1 ≤ 2147483647;" when run on that code.
## Attachments
- [lshift_orig.c](/uploads/9b6afc5859b3e4388c1acb15b8dff279/lshift_orig.c)
- [lshift_new.c](/uploads/7fe660e193a41e27c2f9254530e5e91d/lshift_new.c)https://git.frama-c.com/pub/frama-c/-/issues/393Ocaml 4.04.0 build error2021-02-22T13:01:03Zmantis-gitlab-migrationOcaml 4.04.0 build errorID0002255:
**This issue was created automatically from Mantis Issue 2255. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002255:
**This issue was created automatically from Mantis Issue 2255. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002255 | Frama-C | Kernel | public | 2016-11-09 | 2016-12-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jamesjer | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux | **OS Version** | 4.8.6 |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Building with ocaml 4.04.0 fails:
File "src/kernel_services/plugin_entry_points/db.ml", line 1:
Error: The implementation src/kernel_services/plugin_entry_points/db.ml
does not match the interface src/kernel_services/plugin_entry_points/db.cmi:
...
In module Properties.Interp.To_zone:
Values do not match:
val mk_ctx_func_contrat : (Cil_types.kernel_function -> '_a) ref
is not included in
val mk_ctx_func_contrat :
(Cil_types.kernel_function -> state_opt:bool option -> t_ctx) ref
File "src/kernel_services/plugin_entry_points/db.ml", line 1074, characters 10-29:
Actual declaration
### Additional Information :
See https://bugzilla.redhat.com/show_bug.cgi?id=1392552 for the original report, by Richard W. M. Jones. He supplied a patch which, he says, "fixes compilation, but is generally a bit of a hack. Upstream probably will want to make their own better fix." That patch is attached.
### Steps To Reproduce :
Build with Frama-C Aluminium with ocaml 4.04.0 on an x86_64 Linux machine.
## Attachments
- [frama-c-ocaml-4-04.patch](/uploads/caa49c7fec70d631bd0e90ee7a61dc61/frama-c-ocaml-4-04.patch)https://git.frama-c.com/pub/frama-c/-/issues/394Frama-C is unsound when employing both alt-ergo and cvc42021-02-22T13:01:06ZJochen BurghardtFrama-C is unsound when employing both alt-ergo and cvc4ID0002237:
**This issue was created automatically from Mantis Issue 2237. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002237:
**This issue was created automatically from Mantis Issue 2237. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002237 | Frama-C | Plug-in > wp | public | 2016-06-30 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | xubuntu |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-out out -wp-prover alt-ergo -wp-prover cvc4 bug.c" on the attached file "bug.c" proves both lemmas, although they are both obviously false. A look at file "lemma_Two_Alt-Ergo.mlw" shows that Alt-ergo proved in fact One==>Two, while a look at file "Axiomatic.why" indicates that cvc4 proved in fact Two==>One.
Apparently, the order of lemmas is reversed when piping through "why" - the output generated for coq amounts to "prove One" and "prove One==>Two", similar to that for Alt-ergo.
The problem disappeared when the type of the bound variable "x" was changed to "integer".
## Attachments
- [bug.c](/uploads/4c15388a22c29202e6cb9736f3dc73c9/bug.c)
- [lemma_Two_Alt-Ergo.mlw](/uploads/f03a7de730f37671825be7aed7c67b57/lemma_Two_Alt-Ergo.mlw)
- [Axiomatic.why](/uploads/1dcfeb3bf5a2935354dd3cae6d5c5e0a/Axiomatic.why)
- [0001-WP-Fix-definition-order.patch](/uploads/58c12a1488d50b4d416869447762e3e4/0001-WP-Fix-definition-order.patch)https://git.frama-c.com/pub/frama-c/-/issues/396Compiling on Windows (cygwin) fails2021-02-22T13:01:11Zmantis-gitlab-migrationCompiling on Windows (cygwin) failsID0002247:
**This issue was created automatically from Mantis Issue 2247. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002247:
**This issue was created automatically from Mantis Issue 2247. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002247 | Frama-C | Documentation > manuals | public | 2016-10-01 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vlad | **Assigned To** | maroneze | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Windows | **OS Version** | 7 |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Windows installation fails when building frama-c as described here: https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:compiling_from_source
<pre>
$ OPAMYES=yes opam depext -i frama-c
# Detecting depexts using flags: x86 mswindows win32 cygwinports
# The following system packages are needed:
# - gmp
# - gtk2.0
# - gtksourceview2.0
# - libgnomecanvas2
# - pkg-config
installed:gmp
installed:gtk2.0
installed:gtksourceview2.0
installed:libgnomecanvas2
installed:pkg-config
# All required OS packages found.
# Now letting OPAM install the packages
The following actions will be performed:
∗ install frama-c-base 20160501 [required by frama-c]
Why3 can be used by the WP plug-in for running additional automatic solvers
Coq can be used with the WP plug-in for proving interactively proof obligations
∗ install frama-c 20160501
Alt-Ergo Graphical Interface can be used by the WP plug-in
===== ∗ 2 =====
=-=- Gathering sources =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
[frama-c-base: sh] Command started
[frama-c-base: ./configure] Command started
[frama-c-base: make all] Command started
[ERROR] The compilation of frama-c-base failed at "make
FRAMAC_TOP_SRCDIR=C:/Users/User/AppData/Roaming/SPB_Data/.opam/4.02.3+mingw32/build/frama-c-base.20160501
all".
[frama-c-base: sh] Command started
[frama-c-base: ./configure] Command started
[frama-c-base: make uninstall] Command started
[frama-c-base: rm] Command started
#=== ERROR while compiling frama-c-base.20160501 ==============================#
# opam-version 1.3.0~dev (98188f141dbeb429258f2b2c00f6240d0af02b84)
# os win32
# command make FRAMAC_TOP_SRCDIR=C:/Users/User/AppData/Roaming/SPB_Data/.opam/4.02.3+mingw32/build/frama-c-base.20160501 all
### stdout ###
# [...]
### stderr ###
# 4 shift/reduce conflicts.
# 7 shift/reduce conflicts.
# src/libraries/utils/c_bindings.c:1:0: warning: -fPIC ignored for target (all code is position independent)
# /**************************************************************************/
# ^
# src/libraries/utils/c_bindings.c:28:27: fatal error: caml/mlvalues.h: No such file or directory
# compilation terminated.
# make: *** [Makefile:882: src/libraries/utils/c_bindings.o] Error 1
=-=- Error report -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
The following actions were aborted
∗ install frama-c 20160501
The following actions failed
λ build frama-c-base 20160501
No changes have been performed
</pre>https://git.frama-c.com/pub/frama-c/-/issues/397Switch statements seem to be unsound2021-02-22T13:01:13Zmantis-gitlab-migrationSwitch statements seem to be unsoundID0002246:
**This issue was created automatically from Mantis Issue 2246. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002246:
**This issue was created automatically from Mantis Issue 2246. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002246 | Frama-C | Plug-in > wp | public | 2016-08-19 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ghulette | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Linux | **OS Version** | Ubuntu 16.04 |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
// Run the following to see the problem:
// $ frama-c -wp -wp-rte bad.c
//
// Frama-C does not detect the error in the ensures condition. You
// can cause WP to report the error by commenting out the case 0 line,
// or by passing the -simplify-cfg option. Maybe a problem with
// switch statements?
int x;
/*@
requires x != 1;
assigns x;
ensures x != 1;
*/
void bad (int e) {
switch (e) {
case 0: break;
case 1: x = 1; break;
}
}
### Additional Information :
$ frama-c --version
Aluminium-20160501
### Steps To Reproduce :
See comments in description.
## Attachments
- [bad.c](/uploads/c873fd1a6a052a79d2354129467bc6fe/bad.c)https://git.frama-c.com/pub/frama-c/-/issues/399expression "b--3" accepted in ACSL (interpreted as "b - -3"), but not in C2021-02-22T13:01:16ZJochen Burghardtexpression "b--3" accepted in ACSL (interpreted as "b - -3"), but not in CID0002240:
**This issue was created automatically from Mantis Issue 2240. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002240:
**This issue was created automatically from Mantis Issue 2240. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002240 | Frama-C | Kernel > ACSL implementation | public | 2016-07-28 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp aaa.c" on the attached program gives no syntax error, and reports 1/1 goals proven, although the right-hand side expression in line 7 is invalid. Uncommenting line 6, which contains the same expression in C, results in a syntax error, as expected.
## Attachments
- [aaa.c](/uploads/6a6a5f3ec88892032d6934c50957a697/aaa.c)https://git.frama-c.com/pub/frama-c/-/issues/401Annotation wrongly displayed as checked (green bullet) whereas it is false, w...2021-02-22T13:01:21Zmantis-gitlab-migrationAnnotation wrongly displayed as checked (green bullet) whereas it is false, when using the option -rte on command line.ID0002258:
**This issue was created automatically from Mantis Issue 2258. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002258:
**This issue was created automatically from Mantis Issue 2258. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002258 | Frama-C | Plug-in > RTE | public | 2016-11-24 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | julien-cohen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | PC | **OS** | Linux Ubuntu | **OS Version** | 16.04 LTS |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I have a program with an incorrect acces outside an array. When lauching frama-c-gui with no options and value analysis, the out-of-bounds access is detected and the corresponding annotation is displayed with an orange bullet. When using the -rte option, two annotations are displayed (for the lower and upper bound of the array), and a green bullet is displayed for both (which is not correct).
/*@ assert rte: index_bound: 0 ≤ cpt; */
/*@ assert rte: index_bound: cpt < 5; */
The console says :
tableau_erreur.c:11:[value] Assertion 'rte,index_bound' got status valid.
### Additional Information :
Posted on http://stackoverflow.com/questions/40763614/unsound-behavior-with-rte-option-in-magnesium/40766174#40766174 .
There are two screen captures there. Someone (anol) replied and gave additional information (see the post).
### Steps To Reproduce :
Here is my program :
int main(){
int t[5] = {1,2,3,4,5};
int cpt =0 ;
int tmp ;
while (cpt<10){
tmp = getchar() ;
if ( t[cpt] > tmp )
{ return 1 ; }
cpt++ ;
}
return 10 ;
}
The problem occurs when launching frama-c-gui -rte and the calue analysis on this program.https://git.frama-c.com/pub/frama-c/-/issues/403workaround for coq-8.5.1 issue?2021-02-22T13:01:28ZJochen Burghardtworkaround for coq-8.5.1 issue?ID0002233:
**This issue was created automatically from Mantis Issue 2233. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002233:
**This issue was created automatically from Mantis Issue 2233. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002233 | Frama-C | Plug-in > wp | public | 2016-06-16 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | none | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Aluminium-20160501 | **OS** | xubuntu16.04 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
We ran the command
frama-c-gui -cpp-extra-args='-I.' -pp-annot -no-unicode -wp -wp-rte -wp-script wp0.script -wp-model Typed+ref -wp-prop AdjacentDifferenceInverse -wp-coq-timeout 5 -wp-prover coq -wp-par 1 -wp-out adjacent_difference_inverse.wp adi.c
on the attached file "adi.c", using the attached Coq-script "wp0.script".
The goal isn't proven, and when manually starting the Coq Ide, it complains:
Error: The reference Q_UnchangedSection was not found in the current
environment.
However, the lemma "UnchangedSection" is present in lines 28-33 of file "adi.c", and a "Hypothesis Q_UnchangedSection" is present in lines 33-36 of the generated file "adjacent_difference_inverse.wp/typed_ref/Axiomatic.v", which is included in line 33 of file "adjacent_difference_inverse.wp/typed_ref/lemma_AdjacentDifferenceInverse_Coq.v" (i.e. of the file shown in the Coq Ide).
For these reasons, we believe that the behavior is a Coq-8.5.1 problem, not a Frama-c problem. Moreover, the same files cause no problems when Coq-8.5.1 is replaced by Coq-8.4.6.
Nevertheless, in an e-mail to Jens, Loic encouraged us to report the issue here, since Frama-C might provide a workaround for it.
## Attachments
- [adi.c](/uploads/c4c8150d300c94e05ae4078a54bb0388/adi.c)
- [wp0.script](/uploads/7a7bb805cc9c8332faccefd8ebe42e5d/wp0.script)
- [Axiomatic.v](/uploads/9ab08c5dc84284dc5f8412c7ddc95f09/Axiomatic.v)
- [lemma_AdjacentDifferenceInverse_Coq.v](/uploads/d61593407465c9df0f749dc04240e6ea/lemma_AdjacentDifferenceInverse_Coq.v)
- [adi.script](/uploads/9ab0f4bd54640d060c2292833e1bcd01/adi.script)https://git.frama-c.com/pub/frama-c/-/issues/404Unterminated comment while generating division-by-zero assertion2021-02-22T13:01:31ZKostyantyn VorobyovUnterminated comment while generating division-by-zero assertionID0002250:
**This issue was created automatically from Mantis Issue 2250. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002250:
**This issue was created automatically from Mantis Issue 2250. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002250 | Frama-C | Kernel | public | 2016-10-13 | 2016-12-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kvorobyov | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Gentoo | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | Frama-C 14-Silicon | **Fixed in Version** | - |
### Description :
For the following code snippet:
...
ret = dividend / *p;
...
RTE generates annotation:
/*@ assert rte: signed_overflow: dividend/*p ≤ 2147483647; */
The above leads to unterminated comment preprocessing error
### Steps To Reproduce :
frama-c -rte -then -print
of the following program:
int zero_division_006_gbl_divisor = 0;
void zero_division_006 () {
int dividend = 1000;
int *p;
int ret;
p = &zero_division_006_gbl_divisor;
ret = dividend / *p;
}
int main(int argc, const char **argv) {
zero_division_006();
return 0;
}
## Attachments
- [a.c](/uploads/fac19dff3e17847ea3277c0a8c3c3fbf/a.c)https://git.frama-c.com/pub/frama-c/-/issues/415Error in use of polyId in the 1.10 grammar2021-02-22T13:01:49ZDavid CokError in use of polyId in the 1.10 grammarID0002212:
**This issue was created automatically from Mantis Issue 2212. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002212:
**This issue was created automatically from Mantis Issue 2212. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002212 | Frama-C | Documentation > ACSL | public | 2016-02-25 | 2016-07-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | patrick | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | - |
### Description :
The 1.10 ACSL grammar defines a poly-id as a combination of a simple id, optional label-binders and optional type-var-binders. This is correct for the many places that a poly-id is used as part of a declaration. However, poly-id is also used as a term - either as a standalone variable or as the function name in a function application. Here it is a **use** of the identifier, so the contents of the type list are type expressions (as in Fig. 2.12), not type variable binders. Similarly the labels are instances of labels (including label literals such as Here), and not binders. (The comment about binders also applies to the predicate application production in Fig. 2.2). Something like a poly-id-use is needed:
poly-id-use ::= id ( { label-use ( , label-use )* } )? ( < type-expr (, type-expr )* > )?
where
label-use ::= id | label-literal
label-literal ::= Here | Pre | ...