frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T12:57:18Zhttps://git.frama-c.com/pub/frama-c/-/issues/246WP is not able to validate a statically declared structure followed by a memset2021-02-22T12:57:18ZPatricia MouyWP is not able to validate a statically declared structure followed by a memsetID0002387:
**This issue was created automatically from Mantis Issue 2387. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002387:
**This issue was created automatically from Mantis Issue 2387. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002387 | Frama-C | Plug-in > wp | public | 2018-07-11 | 2018-09-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pmo | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 16-Sulfur | **Target Version** | - | **Fixed in Version** | - |
### Description :
By using a clean way to declare the structure, WP fails to validate the structure but by using a "dirty" way, it works !
#include <string.h>
typedef struct {
int i;
float f;
} stest;
void notclean_but_valid() {
char b[sizeof(stest)];
stest *s = b;
memset(s, 0, sizeof(stest));
}
void clean_but_invalid() {
stest s;
memset(&s, 0, sizeof(stest));
}
### Steps To Reproduce :
frama-c -wp-model typed_cast_ref -wp struc.chttps://git.frama-c.com/pub/frama-c/-/issues/259Invalid sizeof(struct) calculation in Sulfur2021-02-22T12:57:43Zmantis-gitlab-migrationInvalid sizeof(struct) calculation in SulfurID0002344:
**This issue was created automatically from Mantis Issue 2344. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002344:
**This issue was created automatically from Mantis Issue 2344. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002344 | Frama-C | Plug-in > wp | public | 2018-01-19 | 2018-07-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abustany | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | x86_64 | **OS** | Linux | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
FramaC version: Sulfur-20171101 (cannot select it in BTS because of #0002343)
With the following C code:
-------------------------------
#include <stdint.h>
#include <string.h>
typedef struct {
uint8_t a;
uint8_t b;
uint8_t c;
uint16_t d;
uint16_t e;
uint16_t f;
char g[4086];
uint16_t h;
} message_t;
/*@ requires \valid(msg);
@*/
void reset_message(message_t *msg) {
memset(msg, 0, sizeof(message_t));
}
-------------------------------
Running: frama-c -wp -wp-fct reset_message -wp-rte -wp-print err.c
produces the following unprovable goal:
-------------------------------
Assume {
(* Heap *)
Have: (region(msg_0.base) <= 0) /\ linked(Malloc_0) /\ sconst(Mchar_0).
(* Pre-condition *)
Have: valid_rw(Malloc_0, msg_0, 4093).
}
Prove: valid_rw(Malloc_0, shift_sint8(w, 0), 4098).
-------------------------------
Using the Typed+cast model doesn't help.
I'm not really sure how the size of the struct is computed (with regard to alignment or padding), but somehow two different parts of the code seem to disagree here.https://git.frama-c.com/pub/frama-c/-/issues/261WP: internal error: only the kernel should set the status of property assumes2021-02-22T12:57:46Zmantis-gitlab-migrationWP: internal error: only the kernel should set the status of property assumesID0002383:
**This issue was created automatically from Mantis Issue 2383. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002383:
**This issue was created automatically from Mantis Issue 2383. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002383 | Frama-C | Plug-in > wp | public | 2018-07-04 | 2018-07-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | evdenis | **Assigned To** | correnson | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C 17-Chlorine |
### Description :
Example:
<pre>
int test(void)
{
int a = 1;
/*@ behavior ok:
assumes a > 0;
ensures \true;
*/
return 3;
}
</pre>
Command:
<pre>
frama-c -wp test.c
</pre>
Log:
<pre>
[wp] [CFG] Goal test_stmt_ok_post : Valid (Unreachable)
[wp] [CFG] Goal test_stmt_ok_assume : Valid (Unreachable)
[kernel] failure: only the kernel should set the status of property assumes
a > 0
[kernel] Current source was: test.c:1
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 568, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 939, characters 6-44
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 562, characters 9-16
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 565, characters 9-16
Called from file "src/kernel_services/ast_data/property_status.ml", line 538, characters 4-109
Called from file "src/kernel_services/ast_data/property_status.ml" (inlined), line 551, characters 42-80
Called from file "src/plugins/wp/wpAnnot.ml", line 81, characters 4-71
Called from file "list.ml", line 85, characters 12-15
Called from file "list.ml", line 85, characters 12-15
Called from file "src/plugins/wp/wpAnnot.ml", line 1243, characters 10-38
Called from file "src/plugins/wp/wpAnnot.ml", line 1258, characters 12-28
Called from file "src/plugins/wp/wpAnnot.ml", line 1271, characters 16-68
Called from file "src/plugins/wp/Generator.ml", line 108, characters 4-67
Called from file "map.ml", line 270, characters 20-25
Called from file "src/plugins/wp/Generator.ml", line 136, characters 4-39
Called from file "src/plugins/wp/register.ml", line 654, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 41-48
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "queue.ml", line 105, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Frama-C aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
</pre>
## Attachments
- [test.c](/uploads/2597c1f73c5b7b83511f003173086460/test.c)https://git.frama-c.com/pub/frama-c/-/issues/347type of float parameter changed unexpectedly to double2021-02-22T12:59:54Zmantis-gitlab-migrationtype of float parameter changed unexpectedly to doubleID0002283:
**This issue was created automatically from Mantis Issue 2283. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002283:
**This issue was created automatically from Mantis Issue 2283. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002283 | Frama-C | Plug-in > wp | public | 2017-02-24 | 2017-05-31 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | widc | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | 16.04 LTS |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | Frama-C 15-Phosphorus |
### Description :
Current source was: sgn.c:4
The full backtrace is:
Raised at file "hashtbl.ml", line 328, characters 23-32
Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
Frama-C aborted: internal error.
Your Frama-C version is Silicon-20161101.
From the floating_point.ml the following message is reported:
Could not parse floating point number "-0x1.0000000000000p0"
The code in the main pane shows:
float sgn(float u)
...
if ((double)u > 0.0) {
...
### Additional Information :
Quick solution would be appreciated.
### Steps To Reproduce :
C code of sgn.c :
/*@
ensures A: \result == 1.0 || \result == 0.0 || \result == -1.0 ;
*/
float sgn(float u)
{
float p; /* return value */
if (u > 0.0) {
p = 1.0;
} else if (u < 0.0) {
p = -1.0;
} else {
p = 0.0;
}
return p;
}
1. Run:
frama-c-gui sgn.c
2. Select the post-condition
3. In context menu - Prove property by WP
(When the three "float" strings in the above code are changed to "double", the tool works fine, no error is reported.)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/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/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/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/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/494missing lower bound of ACSL operator ".." not detected by Magnesium2021-02-22T13:04:01ZJochen Burghardtmissing lower bound of ACSL operator ".." not detected by MagnesiumID0002230:
**This issue was created automatically from Mantis Issue 2230. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002230:
**This issue was created automatically from Mantis Issue 2230. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002230 | Frama-C | Plug-in > wp | public | 2016-06-13 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | suspended |
| **Priority** | none | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Magnesium | **OS** | xubuntu-14.04 | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
The Frama-C Magnesium parser didn't complain about the missing lower bound of "..".
The Frama-C Aluminium parser does find the syntax error (in fact, this was the way we detected it).
We therefore intend this issue not as a bug report, but merely as another regression test on future Frama-C releases. There is nothing to be fixed now.
## Attachments
- [486.c](/uploads/3fc4fdf16d4ecfe42871670515e0ef32/486.c)
- [max_element.c](/uploads/c5be5280ef02a12d06e4b53b840cb0b9/max_element.c)https://git.frama-c.com/pub/frama-c/-/issues/501coq fails to compile Cint because Zbits is not found2021-02-22T13:04:18Zmantis-gitlab-migrationcoq fails to compile Cint because Zbits is not foundID0002155:
**This issue was created automatically from Mantis Issue 2155. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002155:
**This issue was created automatically from Mantis Issue 2155. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002155 | Frama-C | Plug-in > wp | public | 2015-09-02 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
As described in https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2014-March/004380.html, I get the same error message that Cint can't be compiled because Zbits isn't compiled yet.
I'm getting this on a Debian system.
I attached a patch based on the mail that seems to fix the issue for me.
## Attachments
- [wp.driver.patch](/uploads/a497ab58ae4dc3b1ac4220b14fafbd1d/wp.driver.patch)https://git.frama-c.com/pub/frama-c/-/issues/504Reals are bad encoded for coq2021-02-22T13:04:23Zmantis-gitlab-migrationReals are bad encoded for coqID0002214:
**This issue was created automatically from Mantis Issue 2214. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002214:
**This issue was created automatically from Mantis Issue 2214. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002214 | Frama-C | Plug-in > wp | public | 2016-03-03 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | davyg | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | All | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Magnesium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
The definition of real_base(Qedlib) in the coq exporter of wp is incorrect :
There is :
Definition real_base e a n :=
match n with
| 0 => 1%R
| Zpos n => (a * pow e (Pos.to_nat n))%R
| Zneg n => (a / pow e (Pos.to_nat n))%R
end.
in stead of
Definition real_base e a n :=
match n with
| 0 => a
| Zpos n => (a * pow e (Pos.to_nat n))%R
| Zneg n => (a / pow e (Pos.to_nat n))%R
end.
### Steps To Reproduce :
I think that any coq proof you try to prove with wp containing real constant should have the errorhttps://git.frama-c.com/pub/frama-c/-/issues/522provide option "-wp-lemma"2021-02-22T13:04:45ZJens Gerlachprovide option "-wp-lemma"ID0002202:
**This issue was created automatically from Mantis Issue 2202. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002202:
**This issue was created automatically from Mantis Issue 2202. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002202 | Frama-C | Plug-in > wp | public | 2016-01-23 | 2016-02-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
WP has several options to consider only individual functions, properties, or behaviors during verification.
It would be nice if there were an option "-wp-lemma 'name' " which would allow to consider only the names lemma.https://git.frama-c.com/pub/frama-c/-/issues/534memory leak (endless recursion?) caused by erroneous c program2021-02-22T13:05:10ZJochen Burghardtmemory leak (endless recursion?) caused by erroneous c programID0002184:
**This issue was created automatically from Mantis Issue 2184. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002184:
**This issue was created automatically from Mantis Issue 2184. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002184 | Frama-C | Plug-in > wp | public | 2015-11-02 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | 14.04.1-Ubuntu |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
Running "frama-c 10.c" on the attached program causes frama-c to allocate a rapidly increasing amount of memory, until it crashes with the unbuntu-message "Fatal error: out of memory." Apparently, it performs an endless recursion.
The program "10.c" is erroneous and nonsensical, and originates from a "creduce" experiment with a poor test script. However, it may be worth to eliminate the endless recusion, anyway?
## Attachments
- [10.c](/uploads/6b5ba89a77511be850092e7d6514913b/10.c)https://git.frama-c.com/pub/frama-c/-/issues/544assumes clause and labels2021-02-22T13:05:28ZJens Gerlachassumes clause and labelsID0002040:
**This issue was created automatically from Mantis Issue 2040. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002040:
**This issue was created automatically from Mantis Issue 2040. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002040 | Frama-C | Plug-in > wp | public | 2014-12-27 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
My understanding of assumes clauses is that they refer to the pre-state of a function.
The attached example, however, works differently.
The function push_back has two disjoint behaviors that rely on the predicate "full".
The function push_back_twice is only verified if I add the label "Pre"
to the predicate "full" in the assumes clauses of function push_back.
I think this is a bug.
It should not be necessary to add this explicit label.
### Additional Information :
Concerns versions
Neon-20140301
Neon-20140301+dev-stance
I remember that Kim Völlinger had observed the same(?) problem in Oxygen and
that it was fixed in Fluorine.
## Attachments
- [assumes_label.c](/uploads/c4f41bff0222c51c966f982647981368/assumes_label.c)https://git.frama-c.com/pub/frama-c/-/issues/547Incorrect result with X modulo 12021-02-22T13:05:33Zmantis-gitlab-migrationIncorrect result with X modulo 1ID0002141:
**This issue was created automatically from Mantis Issue 2141. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002141:
**This issue was created automatically from Mantis Issue 2141. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002141 | Frama-C | Plug-in > wp | public | 2015-07-01 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
WP concludes that “n % 1 == n”, instead of “n % 1 == 0” where n are integers.
This is only a problem with modulo 1, the correct answer is obtained for other integers, or if n is 0 (0 % 1 == 0).
This can be shown with the following lemmas.
/*@
lemma mod_one_error:
\forall integer i; (i % 1) == i;
*/
> frama-c mod.c -wp -wp-prop=@lemma
[kernel] preprocessing with "gcc -C -E -I. mod.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_lemma_mod_one_error : Valid
[wp] Proved goals: 1 / 1
Qed: 1
/*@
lemma mod_one:
\forall integer i; (i % 1) == 0;
*/
> frama-c mod.c -wp -wp-prop=@lemma
[kernel] preprocessing with "gcc -C -E -I. mod.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_lemma_mod_one : Unknown
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unknown: 1)
I would have expected ‘mod_one_error’ not to validate, and ‘mod_one’ to validate.
The goal generated for mod_one also illustrates the issue.
lemma_mod_one.ergo:
(* ---------------------------------------------------------- *)
(* --- Lemma 'mod_one' --- *)
(* ---------------------------------------------------------- *)
(* --- Global Definitions --- *)
goal lemma_mod_one: forall i : int. 0 = i
This leads to vacuous truths when assuming the correct result. In the example below, wp believes ‘i' is 1, and our assumption leads to the contradictions 1 == 0.
void f1() {
int i = 1 % 1;
//@ assert i == 0;
//@ assert vacuous: \false;
}
> frama-c mod.c -wp
[kernel] preprocessing with "gcc -C -E -I. mod.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_f1_assert_vacuous : Valid
[wp] [Alt-Ergo] Goal typed_f1_assert : Unknown
[wp] Proved goals: 1 / 2
Qed: 1
Alt-Ergo: 0 (unknown: 1)
This behavior was observed in both Neon and Sodium.https://git.frama-c.com/pub/frama-c/-/issues/550Crash with \is_infinite2021-02-22T13:05:39Zmantis-gitlab-migrationCrash with \is_infiniteID0002082:
**This issue was created automatically from Mantis Issue 2082. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002082:
**This issue was created automatically from Mantis Issue 2082. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002082 | Frama-C | Plug-in > wp | public | 2015-02-24 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
Using the built-in \is_infinite causes wp to crash.
This is used in the provided libc specifications (math.h), and a call to these functions will cause a crash.
### Steps To Reproduce :
Create program:
#include <math.h>
/*@
ensures \true;
*/
void main() {
double val = acos(1);
}
Run frama-c, where FRAMA_C_LIBC is .../frama-c-Neon-20140301/share/libc:
frama-c -cpp-extra-args="-I${FRAMA_C_LIBC}" -wp is_infinte_test.c
Get output:
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acos, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acosf, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acosh, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acoshf, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acoshl, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function acosl, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function asin, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function asinf, generating default assigns from the specification
is_infinte_test.c:7:[kernel] warning: No code nor implicit assigns clause for function asinl, generating default assigns from the specification
[wp] warning: No definition for 'memchr' interpreted as reads nothing
[wp] warning: No definition for 'memset' interpreted as reads nothing
[wp] warning: No definition for 'strchr' interpreted as reads nothing
[wp] warning: No definition for 'strcmp' interpreted as reads nothing
[wp] warning: No definition for 'wcscmp' interpreted as reads nothing
[wp] warning: No definition for 'wcslen' interpreted as reads nothing
[wp] warning: No definition for 'wcsncmp' interpreted as reads nothing
[wp] warning: Missing RTE guards
[wp] user error: Builtin \is_infinite(float64) not defined
[wp] failure: Logic '\is_infinite' undefined
[kernel] Current source was: is_infinte_test.c:8
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/wp/LogicCompiler.ml", line 698, characters 20-51
Called from file "src/wp/LogicCompiler.ml", line 758, characters 10-23
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 357, characters 28-51
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 357, characters 28-51
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "list.ml", line 57, characters 20-23
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/cfgWP.ml", line 1069, characters 18-63
Called from file "src/wp/Warning.ml", line 155, characters 14-18
Called from file "src/wp/cfgWP.ml", line 1099, characters 23-207
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/calculus.ml", line 448, characters 14-224
Called from file "src/wp/calculus.ml", line 595, characters 10-57
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 579, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 574, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 699, characters 40-59
Called from file "set.ml", line 288, characters 38-41
Called from file "map.ml", line 169, characters 20-25
Called from file "map.ml", line 169, characters 10-18
Called from file "map.ml", line 169, characters 10-18
Called from file "src/wp/calculus.ml", line 699, characters 4-64
Called from file "src/wp/calculus.ml", line 745, characters 19-51
Called from file "src/wp/cfgWP.ml", line 1382, characters 39-62
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/wp/cfgWP.ml", line 1371, characters 14-837
Called from file "src/wp/Model.ml", line 111, characters 17-20
Re-raised at file "src/wp/Model.ml", line 116, characters 25-28
Called from file "src/wp/Model.ml", line 117, characters 19-36
Called from file "src/wp/register.ml", line 435, characters 17-42
Called from file "src/wp/register.ml", line 574, characters 17-24
Re-raised at file "src/wp/register.ml", line 578, characters 29-31
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 735, characters 2-9
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
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_guidelineshttps://git.frama-c.com/pub/frama-c/-/issues/617deficient axioms2021-02-22T13:07:23ZDavid Cokdeficient axiomsID0002138:
**This issue was created automatically from Mantis Issue 2138. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002138:
**This issue was created automatically from Mantis Issue 2138. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002138 | Frama-C | Plug-in > wp | public | 2015-06-29 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DavidCok | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | Windows | **OS Version** | 7 |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The proof of the following with -WP and alt-ergo fails:
/*@
requires (int)(x+y) == x+y;
ensures \result == x+y;
*/
int f(int x, int y) {
return x+y;
}
On inspecting the intermediate artifacts, we identified the problem as inadequate axioms. Two solutions requiring changes in axioms worked for us.
However, I don't know if either change would have wider ramifications.
1)
axiom is_to_sint32 :
(forall x:int [is_sint32(to_sint32(x))]. is_sint32(to_sint32(x)))
The effect of the triggers in this axiom is simply to allow is_sint32(to_sint32(x)) to be reduced to true. In fact the more common need is to know that to_sint32(x) satisfies is_sint32. The proof above goes through if the trigger is changed to
axiom is_to_sint32 :
(forall x:int [to_sint32(x)]. is_sint32(to_sint32(x)))
2)
axiom id_sint32 :
(forall x:int [to_sint32(x)]. ((((-2147483648) <= x) and
(x < 2147483648)) -> (to_sint32(x) = x)))
This axiom is much more useful if it is written as an equivalence instead of an implication. Doing so also enables the proof of the program above to go through.https://git.frama-c.com/pub/frama-c/-/issues/618Sessions and WP do not interact properly2021-02-22T13:07:24Zmantis-gitlab-migrationSessions and WP do not interact properlyID0002044:
**This issue was created automatically from Mantis Issue 2044. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002044:
**This issue was created automatically from Mantis Issue 2044. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002044 | Frama-C | Plug-in > wp | public | 2015-01-06 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | correnson | **Resolution** | no change required |
| **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 :
Bonjour, quelques problèmes avec le -save et le -load des sessions conjugés avec WP/Why3 et l'option no-let !!!!
1. Si on utilise pas -wp-out les fichiers temporaires de wp sont supprimés et lors du prochain appel de frama-c avec le -load, il se plaint de l'absence des fichiers
2. Si on specifie -wp-out, avec le -load, Frama-C retrouve les fichiers générés mais il ne semble pas retrouver tout ce dont il a besoin.
3. Enfin lors de l'utilisation de coq comme prover lors d'un run (avec -load et -save), au prochain appel avec toujours -load et -save, frama-c appelle systématiquement coq, y compris si on specifie -wp-prover altergo par exemple.
### Steps To Reproduce :
Pour les points 1 et 2:
Par exemple, pour le fichier C suivant:
$ cat essai.c
struct greycounter_mem {_Bool _first; };
/*@ requires \valid(self);
@ ensures ((*self)._first ==1);
@ assigns *self;*/
void greycounter_reset (struct greycounter_mem *self) {
self->_first = 1;;
return;
}
Le script suivant active les différents problemes:
#!bin/bash
src=essai.c
# Error 1: temporary wp folder with no-let option and why3 solver (eg. altergo or CVC4)
frama-c -save session -wp-prop "@ensures" -wp-prover why3:altergo -wp-no-let $src
frama-c -load session -save session -wp-prop "@assigns" $src
# Error 2: no-let with why3:cvc4
frama-c -save session -wp-prop "@ensures" -wp-prover CVC4 $src -wp-no-let -wp-out wp
frama-c -load session -save session -wp-prop "@assigns" $src
# Here it works
frama-c -save session -wp-prop "@ensures" -wp-prover CVC4 $src -wp-out wp
frama-c -load session -save session -wp-prop "@assigns" $src