frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T14:01:52Zhttps://git.frama-c.com/pub/frama-c/-/issues/571WP crashes on generation of PO for assigns clause (assertion failure in MemVa...2021-02-22T14:01:52ZVirgile PrevostoWP crashes on generation of PO for assigns clause (assertion failure in MemVar.ml)ID0002126:
**This issue was created automatically from Mantis Issue 2126. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002126:
**This issue was created automatically from Mantis Issue 2126. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002126 | Frama-C | Plug-in > wp | public | 2015-06-02 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Magnesium |
### Description :
On the example source below, frama-c -wp reduced.i crashes with the following error:
File "src/wp/MemVar.ml", line 491, characters 54-60: Assertion failed
Apparently (by inferring why the offending function in MemVar got called), the p1+0 in the assigns for fn1 leads WP to think that p1 should be instantiated with an array (in particular, if you remove the +0, everything is fine).
-- reduced.i
/*@ assigns *(p1); */
int fn1(char *p1);
/*@
assigns \nothing;
*/
void fn2(void) {
char pcr_index;
fn1(&pcr_index);
}https://git.frama-c.com/pub/frama-c/-/issues/749Frama-C/WP "forgets" a proven assertion2021-02-22T14:02:03ZJens GerlachFrama-C/WP "forgets" a proven assertionID0001751:
**This issue was created automatically from Mantis Issue 1751. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001751:
**This issue was created automatically from Mantis Issue 1751. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001751 | Frama-C | Plug-in > wp | public | 2014-04-11 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | patrick | **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 Sodium |
### Description :
In the following function
void strange_after_shift(unsigned int x)
{
unsigned int y = x & 1;
//@ assert y == 0 || y == 1;
//@ assert 0 <= y <= 1;
}
the first assertion is discharged by Qed but the second assertion (which should also hold)
is not discharged with Alt-Ergo.
Moreover, when I try to prove it with Coq, then I cannot see any hypothesis that represents the first assertion.
## Attachments
- [strange_after_shift.c](/uploads/bb5449fe82a2bd2c11222cda38be2a40/strange_after_shift.c)https://git.frama-c.com/pub/frama-c/-/issues/787Frama-C/WP fails to discharge simple bit operation for small integer types2021-02-22T14:02:03ZJens GerlachFrama-C/WP fails to discharge simple bit operation for small integer typesID0001750:
**This issue was created automatically from Mantis Issue 1750. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001750:
**This issue was created automatically from Mantis Issue 1750. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001750 | Frama-C | Plug-in > wp | public | 2014-04-11 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
In the attached file there are for simple functions that computes
b = a & 1;
//@ assert b == 0 || b == 1;
where a and b are of type
unsigned char, unsigned short, unsigned int and unsigned long.
Only for the types unsigned int and unsigned long cab WP (in fact QED) discharge the assertion.
Both alt-ergo and CVC4 fail on unsigned char and unsigned short.
I would be very nice if Frama-C/WP could handle the other cases automatically as well.
## Attachments
- [bit_and.c](/uploads/20b02acd0e271df19fbcab361092552a/bit_and.c)https://git.frama-c.com/pub/frama-c/-/issues/754Frame Validity2021-02-22T14:02:04ZLoïc CorrensonFrame ValidityID0001828:
**This issue was created automatically from Mantis Issue 1828. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001828:
**This issue was created automatically from Mantis Issue 1828. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001828 | Frama-C | Plug-in > wp | public | 2014-07-08 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | correnson | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
//@ requires \valid(one);
void f(int *one){
int two;
//@ assert one != &two;
}
int *zero;
//@ requires \valid(zero) && \valid(one);
void frame(int *one, int arg){
int two;
//@ assert formal: \separated(one,&arg,&two);
//@ assert global: \separated(zero,&arg,&two);
}
## Attachments
- [bts1828_frame.i](/uploads/75bda1142495f914b1db21ba625d707e/bts1828_frame.i)https://git.frama-c.com/pub/frama-c/-/issues/765Status of POs: the word "interruped" should be "interrupted"2021-02-22T14:02:05ZRichard BonichonStatus of POs: the word "interruped" should be "interrupted"ID0001930:
**This issue was created automatically from Mantis Issue 1930. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001930:
**This issue was created automatically from Mantis Issue 1930. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001930 | Frama-C | Plug-in > wp | public | 2014-09-26 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rbonichon | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | low | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
The standard output of wp displays "interruped" instead of "interrupted".
The change should occur in src/wp/register.ml
At the same time, the "mutable interruped" field should be changed to "interrupted"https://git.frama-c.com/pub/frama-c/-/issues/753typo in wp output: "interruped"-->"interrupted"2021-02-22T14:02:05ZJochen Burghardttypo in wp output: "interruped"-->"interrupted"ID0001832:
**This issue was created automatically from Mantis Issue 1832. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001832:
**This issue was created automatically from Mantis Issue 1832. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001832 | Frama-C | Plug-in > wp | public | 2014-07-14 | 2015-03-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | trivial | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
Complete output was:
frama-c -wp-prover alt-ergo,cvc4 -wp -wp-rte gui01.c
[kernel] preprocessing with "gcc -C -E -I. gui01.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_main_assert : Unknown
[wp] [cvc4] Goal typed_main_assert : Timeout
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unknown: 1)
cvc4: 0 (interruped: 1)https://git.frama-c.com/pub/frama-c/-/issues/1029short int to float assertion not proved2021-02-22T14:02:32Zmantis-gitlab-migrationshort int to float assertion not provedID0001653:
**This issue was created automatically from Mantis Issue 1653. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001653:
**This issue was created automatically from Mantis Issue 1653. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001653 | Frama-C | Plug-in > wp | public | 2014-02-24 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 64 bit |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Wonder why this assertion is not provable even though it is a valid one.
#include <limits.h>
/*@ requires x != 0;
assigns \nothing;
*/
void assert(int x);
int main()
{
float f = SHRT_MAX;
short int i = f;
assert(i == SHRT_MAX);
}
### Steps To Reproduce :
[formal_verification]$ frama-c -wp -wp-rte float_to_short_int_max_2.c -pp-annot [kernel] preprocessing with "gcc -C -E -I. -dD float_to_short_int_max_2.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int_2 : Valid (4ms) [wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int : Valid (8ms) [wp] [Alt-Ergo] Goal typed_main_call_assert_pre : Unknownhttps://git.frama-c.com/pub/frama-c/-/issues/1030int to double - assert not verified2021-02-22T14:02:32Zmantis-gitlab-migrationint to double - assert not verifiedID0001651:
**This issue was created automatically from Mantis Issue 1651. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001651:
**This issue was created automatically from Mantis Issue 1651. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001651 | Frama-C | Plug-in > wp | public | 2014-02-24 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | 64 bit |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
For this below program, the assert should be valid I think but the WP is not proving it.
#include <limits.h>
/*@ requires x != 0;
assigns \nothing;
*/
void assert(int x);
int main()
{
double f = INT_MAX;
int i = f;
assert(i == INT_MAX);
return 0;
}
### Additional Information :
The regular C assert was able to prove when I run the a.out after compiling the wrong (commenting the ACSL's assert).
### Steps To Reproduce :
[formal_verification]$ frama-c -wp -wp-rte double_to_int_max_2.c -pp-annot [kernel] preprocessing with "gcc -C -E -I. -dD double_to_int_max_2.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int_2 : Valid (4ms) [wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int : Valid (12ms) [wp] [Alt-Ergo] Goal typed_main_call_assert_pre : Unknown (1s)https://git.frama-c.com/pub/frama-c/-/issues/1031WP: Assertion not proved -> conversion from float to int issue?2021-02-22T14:02:32Zmantis-gitlab-migrationWP: Assertion not proved -> conversion from float to int issue?ID0001655:
**This issue was created automatically from Mantis Issue 1655. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001655:
**This issue was created automatically from Mantis Issue 1655. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001655 | Frama-C | Plug-in > wp | public | 2014-02-27 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Ubuntu | **OS** | Linux | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm using Frama-C for my course at UMD. Found it pretty helpful.
I tried this puzzle, but cannot get WP to prove the assertion, which is true.
I ran through the GDB and found that the value of i is INT_MIN, satisfying the assert.
#include <limits.h>
/*@ requires x != 0;
assigns \nothing;
*/
void assert(int x);
int main()
{
float f = INT_MAX;
int i = f;
assert(i == INT_MIN);
return 0;
}
### Steps To Reproduce :
[formal_verification]$ frama-c -wp -wp-rte float_to_int_assert.c
[kernel] preprocessing with "gcc -C -E -I. float_to_int_assert.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function main
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int_2 : Valid (8ms)
[wp] [Alt-Ergo] Goal typed_main_assert_rte_float_to_int : Valid (12ms)
[wp] [Alt-Ergo] Goal typed_main_call_assert_pre : Unknown
## Attachments
- [int_of_real_why3.diff](/uploads/3aadceb64f4a89ae445498f3e92952de/int_of_real_why3.diff)
- [floats_and_ints.diff](/uploads/b4984e6711b9343f82562f3dd284f08a/floats_and_ints.diff)https://git.frama-c.com/pub/frama-c/-/issues/1191WP ignores some goal2021-02-22T14:02:45Zmantis-gitlab-migrationWP ignores some goalID0001588:
**This issue was created automatically from Mantis Issue 1588. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001588:
**This issue was created automatically from Mantis Issue 1588. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001588 | Frama-C | Plug-in > wp | public | 2013-12-20 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
On this example, WP ignore some of the goals. There should be 3 goals, but :
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_f_loop_inv_l1_2_established : Valid
Loop invariant preservation and assertion are ignore.
### Additional Information :
I simplified the example as much as possible, but it seems that the number of statements is important to reproduce the problem 8-/
### Steps To Reproduce :
frama-c wp.c -wp
## Attachments
- [wp.c](/uploads/f296e3e3d81e278bf5e25179c5d16e29/wp.c)https://git.frama-c.com/pub/frama-c/-/issues/1719axiom ignored because of label, but no label is present in axiom.2021-02-22T14:03:37ZFabrice Derepasaxiom ignored because of label, but no label is present in axiom.ID0000576:
**This issue was created automatically from Mantis Issue 576. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000576:
**This issue was created automatically from Mantis Issue 576. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000576 | Frama-C | Plug-in > wp | public | 2010-08-26 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | derepas | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
svn release id is 'r9704'.
I have the following code in file ex.c:
/*@
@ axiomatic MyAxio {
@ logic integer my_super_fun (char * x,char * y);
@ axiom my_super_axiom_1: \forall char* x; \forall char* y;
@ (*(x+0)==*(y+0)) ==> my_super_fun(x,y);
@ axiom my_super_axiom_2: \forall char * x; \forall char * y;
@ (x[0]==y[0]) ==> my_super_fun(x,y);
@ }
@*/
int main (char *x, char *y) {
//@ assert my_super_fun (x,y);
return 0;
}
Launching the wp on this code yields :
> frama-c -wp -wp-out why_dir ex.c
[kernel] preprocessing with "gcc -C -E -I. ex.c"
ex.c:11:[wp] warning: Ignoring axiom my_super_axiom_2 (because of labels)
ex.c:11:[wp] warning: Ignoring axiom my_super_axiom_1 (because of labels)
But it seems to me that there are no labels in these axioms.https://git.frama-c.com/pub/frama-c/-/issues/2055Why prover unable to validate few ASCL Annotations2021-02-22T14:04:11Zmantis-gitlab-migrationWhy prover unable to validate few ASCL AnnotationsID0001163:
**This issue was created automatically from Mantis Issue 1163. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001163:
**This issue was created automatically from Mantis Issue 1163. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001163 | Frama-C | Plug-in > wp | public | 2012-04-16 | 2012-04-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nmuller | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
<<< Expected Behaviour: >>>
The objective of the C program is to find the absolute value of the difference between two floating point values and to prove that the difference in either way is equal i.e (|A-B| == |B-A|), the value of A ranges from (-25.0 < A < 25.0) and the value of B ranges from (-53.5 < B < 53.5), the important criteria that must was taken is that (7 < |A-B| < 28.5),the program uses several asserstions and loop annotations in the ACSL inside the C source code,
<<< Actual Behaviour: >>>
When the C program is called by the gWhy to verify the VC's , we encountered some problems, by using the provers ( Alt-ergo, Simplify,CVC3 & Gappa) we were not able to validate all the VC's , as a common we had 2 VC's which are not validated by all the provers, which is quite suprising, the reason is that , if we look into the ACSL annotations, we could see that there is use of similar kind of two statements is the following lines, and the provers are able to validated those VC's which are of the same type of declarations and same way of usage,the question here is why are the provers not able to prove those two lines of annotations but could prove them in the next few lines but with different variables ?
<<< Prover Peformances >>>
-----------------------------------------------------------------------
S.N Prover Percent Total Valid Invalid Unknown TimeOut Failure
-----------------------------------------------------------------------
1. Alt-ergo 97% 73 71 0 0 2 0
2. Simplify 92% 73 67 0 0 6 0
3. CVC3 97% 73 71 0 0 0 2
4. Gappa 89% 73 65 0 8 0 0
-----------------------------------------------------------------------
- The time was even changed from 10 sec to 300 sec inorder to see if the impact of timeout may resolve but the results remained unchanged.
### Additional Information :
- The time was even changed from 10 sec to 300 sec inorder to see if the impact of timeout may resolve but the results remained unchanged.
All the four provers are having trouble in validating the 2 Particular VC's, they are
1. assertion - line 22
2. loop invariant preserved - line 16
## Attachments
- [abs_new_BTS.zip](/uploads/00f1b4d159b363e5fe2e537d417dbe4b/abs_new_BTS.zip)https://git.frama-c.com/pub/frama-c/-/issues/2134alt-ergo version managment2021-02-22T14:04:18Zmantis-gitlab-migrationalt-ergo version managmentID0000641:
**This issue was created automatically from Mantis Issue 641. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000641:
**This issue was created automatically from Mantis Issue 641. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000641 | Frama-C | Plug-in > wp | public | 2010-12-16 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dargaye | **Assigned To** | dargaye | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | Frama-C Nitrogen-20111001 | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
When the alt-ergo version is 0.91.x and the -wp-no-arrays option isn't set,
find a way to catch the alt-ergo error outputhttps://git.frama-c.com/pub/frama-c/-/issues/2197Issue INSTALL guidance that alt-ergo has to be up-to-date (0.92 apparently)2021-02-22T14:04:18ZHolger BlasumIssue INSTALL guidance that alt-ergo has to be up-to-date (0.92 apparently)ID0000640:
**This issue was created automatically from Mantis Issue 640. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000640:
**This issue was created automatically from Mantis Issue 640. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000640 | Frama-C | Plug-in > wp | public | 2010-12-16 | 2011-05-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | holgerblasum | **Assigned To** | dargaye | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101201-beta1 | **Target Version** | Frama-C Nitrogen-20111001 | **Fixed in Version** | - |
### Description :
This might a bit too picky but in case it is useful for the new release ...
When I updated to the new release first I hadn't updated alt-ergo (it's fine with 0.92.2 but not with 0.91). Others will run into that too ... Simply point out that dependency in the release notes ("INSTALL" in the root is where I would look). Below is output generated from alt-ergo 0.92.2; 0.91; 0.9.
$ alt-ergo -version Alt-Ergo 0.92.2
$ frama-c -wp -proof alt-ergo swap.c swap1.c
[kernel] warning: cannot load 2 plug-ins (incompatible with Carbon-20101201-b1).
Aorai;
Jessie
[kernel] preprocessing with "gcc -C -E -I. swap.c"
[kernel] preprocessing with "gcc -C -E -I. swap1.c"
[wp] warning: Missing RTE guards
[wp] [Alt-Ergo] Goal store_swap_post_2_B : Valid
[wp] [Alt-Ergo] Goal store_swap_post_1_A : Valid
$ alt-ergo -version
Alt-Ergo 0.91
$ frama-c -wp -wp-proof alt-ergo swap.c swap1.c
[kernel] warning: cannot load 2 plug-ins (incompatible with Carbon-20101201-beta1).
Aorai;
Jessie
[kernel] preprocessing with "gcc -C -E -I. swap.c"
[kernel] preprocessing with "gcc -C -E -I. swap1.c"
[wp] warning: Missing RTE guards
alt-ergo -arrays /tmp/store_swap_post_2_B0f5276.why
File "/tmp/store_swap_post_2_B0f5276.why", line 298, characters 3-4:syntax error
[wp] [Alt-Ergo] Goal store_swap_post_2_B : Failed
File "/tmp/store_swap_post_1_Add7b47.why", line 298, characters 3-4:syntax error
[wp] [Alt-Ergo] Goal store_swap_post_1_A : Failed
$ alt-ergo -version
Alt-Ergo 0.9
$ frama-c -wp -wp-proof alt-ergo swap.c swap1.c
[kernel] warning: cannot load 2 plug-ins (incompatible with Carbon-20101201-beta1).
Aorai;
Jessie
[kernel] preprocessing with "gcc -C -E -I. swap.c"
[kernel] preprocessing with "gcc -C -E -I. swap1.c"
[wp] warning: Missing RTE guards
alt-ergo -arrays /tmp/store_swap_post_2_B5e2f18.why
[wp] [Alt-Ergo] Goal store_swap_post_2_B : Failed
[wp] [Alt-Ergo] Goal store_swap_post_1_A : Failedhttps://git.frama-c.com/pub/frama-c/-/issues/622normalization of "assigns" in statement contract doens't cope with introduced...2021-03-30T07:28:00ZJochen Burghardtnormalization of "assigns" in statement contract doens't cope with introduced auxiliary variablesID0002102:
**This issue was created automatically from Mantis Issue 2102. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002102:
**This issue was created automatically from Mantis Issue 2102. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002102 | Frama-Clang | Plug-in > wp | public | 2015-04-09 | 2015-06-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | sometimes |
| **Platform** | Sodium-20150201 (opam) | **OS** | xubuntu14.04 | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp 468.c" on the attached program generates an unprovable obligation (viz. "false" in Alt-Ergo's .mlw file) for the "assert" (statement contract) in line 7.
Running "frama-c-gui -wp 468.c" shows that the code normalization introduced an auxiliary variable "tmp", which is assigned, too (cf. attached image "468.gif"). However the "assigns" clause wasn't extended accordingly; so in the normalized version, the statement contract is indeed false.
A workaround, found by our student Timon Lapawczyk, is to enclose the statement in line 8 into braces, which makes the contract refer to a compound statement with "tmp" a hidden variable inside it. In this case, the statement contract is proven without problems.
## Attachments
- [468.c](/uploads/3ffd2a021e987a1ea908721495c6fa87/468.c)
- ![468](/uploads/5d29ccc3dc630b3c4df7845d74ead155/468.gif)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2548Error: Unbound value Why3.Whyconf.load_default_config_if_needed2021-04-13T17:49:41ZQixError: Unbound value Why3.Whyconf.load_default_config_if_needed
Before submitting the issue, please confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [ ] the issue has not yet been reported on our old
[BTS](htt...
Before submitting the issue, please confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [ ] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*); **(Can't tell; getting a database connection error)**
- [ ] you installed Frama-C as prescribed in the [instructions](INSTALL.md). **(Not exactly; I'm building from source within a Dockerfile)**
# Contextual information
- Frama-C installation mode: from source
- Frama-C version: c4d10fb975d443e3c40289843fae89c424b54e63
- Plug-in used: WP
- OS name: Debian Buster
- OS version: 20210326 (10.8)
# Steps to reproduce the issue
Dockerfile:
```Dockerfile
FROM debian:buster-20210326 AS base
RUN apt update -y
RUN apt install -y gnupg2 wget apt-transport-https ca-certificates
RUN wget -O - https://apt.llvm.org/llvm-snapshot.gpg.key | apt-key add -
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb http://apt.llvm.org/buster/ llvm-toolchain-buster main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb-src http://apt.llvm.org/buster/ llvm-toolchain-buster main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb http://apt.llvm.org/buster/ llvm-toolchain-buster-12 main\""
RUN bash -c "cat >> /etc/apt/sources.list <<< \"deb-src http://apt.llvm.org/buster/ llvm-toolchain-buster-12 main\""
RUN cat /etc/apt/sources.list
RUN apt update -y
RUN apt install -y clang-12 lld-12 grub-common ninja-build git libssl-dev libgmp-dev pkg-config make m4 unzip tar bzip2 gcc g++ autoconf zlib1g-dev time
RUN cc --version
RUN c++ --version
WORKDIR /opam
RUN wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh
RUN echo "/opam" | sh install.sh --no-backup
ENV PATH="/opam:/opam/bin:${PATH}"
RUN opam --version
RUN time opam init -y --disable-sandboxing --jobs=1
RUN time opam install -y depext ocamlfind ocamlgraph zarith yojson why3.1.4.0 alt-ergo.2.4.0
ENV PATH="/root/.opam/default/bin:${PATH}"
RUN why3 --version
RUN why3 config detect
ARG FRAMAC_REF=c4d10fb975d443e3c40289843fae89c424b54e63
WORKDIR /framac
RUN git init .
RUN git remote add origin https://git.frama-c.com/pub/frama-c.git
RUN git fetch origin ${FRAMAC_REF}
RUN git checkout ${FRAMAC_REF}
RUN autoconf
RUN ./configure
RUN make -j4
RUN make install
RUN frama-c --version; echo
```
# Expected behaviour
Should build to completion.
# Actual behaviour
```
File "src/plugins/wp/Why3Provers.ml", line 31, characters 19-61:
31 | let config = Why3.Whyconf.load_default_config_if_needed config in
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound value Why3.Whyconf.load_default_config_if_needed
make: *** [share/Makefile.generic:78: src/plugins/wp/Why3Provers.cmo] Error 2
make: *** Waiting for unfinished jobs....
The command '/bin/sh -c make -j4' returned a non-zero code: 2
```
---
Some context: Trying to verify a new toy OS and having a bunch of issues since I can't use the standard C library that ships with Frama-C (as there is no C library available in this environment) so I've ended up copying the axiomatic clauses from the `__fc_xxx.h` headers directly.
I saw on StackOverflow that a few bugs that seemed to be affecting me were recently patched on master but not yet released, so I spun up a Dockerfile in order to try to see if any of the verification could be fixed by trying it with the latest head.
However, it doesn't seem to be working - much less getting even simple programs to verify correctly :/ Hence why I'm trying to update everything to latest to see if I can't get _any_ verification to work.
Anyway this is the latest issue I've hit trying to get everything up to date.
Note that there is a lot of stuff in there that isn't directly related to this bug - this is a stripped down Dockerfile, and there is a bunch of extra stuff that comes after this step that I removed to keep things small.https://git.frama-c.com/pub/frama-c/-/issues/41Z3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems2021-04-13T17:49:41ZJens GerlachZ3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems**I updated the title after figuring out a solution**
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [x] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- ...**I updated the title after figuring out a solution**
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [x] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
- [x] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *22.0-beta (Titanium)*
- Plug-in used: *WP*
- OS name: *Xubuntu*
- OS version: *Ubuntu 20.04.1 LTS*
*Please add specific information deemed relevant with regard to this issue.*
I am able to use the options `-wp-prover Alt-Ergo -wp-prover native:coq ` with *ACSL by Example*.
However when using either `-wp-prover Z3` or `-wp-prover z3` I receive the following error message.
(Note that `z3` (4.8.6) has been installed and that it has been successfully registered with `why3 config --full-config`)
```
[kernel] Parsing find.c (with preprocessing)
[rte] annotating function find
[wp] User Error: Prover 'z3' not found in why3.conf
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 25 goals scheduled
[wp] Proved goals: 25 / 25
Qed: 16 (2ms-6ms-20ms)
Alt-Ergo 2.3.3: 9 (5ms-12ms) (87)
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.
```
Similar with `CVC4` and `cvc4`.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/102alt-ergo support in Frama-C 20 beta2021-04-14T07:30:38ZJens Gerlachalt-ergo support in Frama-C 20 betaID0002484:
**This issue was created automatically from Mantis Issue 2484. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002484:
**This issue was created automatically from Mantis Issue 2484. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002484 | Frama-C | Plug-in > wp | public | 2019-11-08 | 2019-11-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | Linux | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
This is a hint to (better) describe the transition from using alt-ergo in Frama-C 19 and 20.
If it is already described, then I apologize.
In Frama-C 19 and before one uses
-wp-prover alt-ergo for the native interface and
-wp-prover why3:alt-ergo for the Why3 interface
In Frama-C 20 the respective options are
-wp-prover native:alt-ergo for the native interface and
-wp-prover alt-ergo
I propose that it is described with other things in a short transition document.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1858Range verification in 2D-array fails2021-04-14T15:17:07ZAllan BlanchardRange verification in 2D-array failsID0001428:
**This issue was created automatically from Mantis Issue 1428. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001428:
**This issue was created automatically from Mantis Issue 1428. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001428 | Frama-C | Plug-in > wp | public | 2013-05-24 | 2013-05-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Allan Blanchard | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Just consider this little example :
void func(){
int a[5][5];
// This works :
//@ assert \valid(a[0 .. 4]);
//@ assert \valid(&a[0 .. 4][0 .. 4]);
// OK :
//@ assert \valid(&a[0][0 .. 4]);
//@ assert \valid(&a[1][0]); //works with 1, 2, 3, 4 but
//@ assert \valid(&a[1][0 .. 4]); //does not
}Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1816do { ... } while (0) pattern causes wp to fail2021-04-14T15:31:18Zmantis-gitlab-migrationdo { ... } while (0) pattern causes wp to failID0001281:
**This issue was created automatically from Mantis Issue 1281. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001281:
**This issue was created automatically from Mantis Issue 1281. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001281 | Frama-C | Plug-in > wp | public | 2012-10-15 | 2014-02-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sjw | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The pattern do { ... } while (0) is used in a number of standard headers
to allow pre-processor macros to introduce a scope and still look like
a statement (you can put a semi-colon after them). This translates to
something like while(1) { ...; break; } as in the following
/*@ requires \valid(x);
@ ensures \result == 0; */
int foo(int *x) {
/* loop invariant 0 == 0; */
while( 1 ) {
*x = 0;
break;
}
return *x;
}
which fails with
$ frama-c -wp do_while_test.c
[kernel] preprocessing with "gcc -C -E -I. do_while_test.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
do_while_test.c:6:[wp] warning: calculus failed on strategy
for 'foo', behavior 'default!', all properties, both assigns or not because
unsupported non-natural loop without invariant property. (abort)
[wp] 0 goal scheduled
It looks like the unconditional break (i.e., the results of optimising
if (!0) break; from the translation of the 'do') causes the cil2cfg pass
to throw out some loop edges, causing the above error.Loïc CorrensonLoïc Correnson