frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T13:46:18Z
https://git.frama-c.com/pub/frama-c/-/issues/1929
ACSL builtins
2021-02-22T13:46:18Z
Loïc Correnson
ACSL builtins
ID0000816:
**This issue was created automatically from Mantis Issue 816. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000816:
**This issue was created automatically from Mantis Issue 816. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000816 | Frama-C | Plug-in > wp | public | 2011-05-10 | 2012-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | correnson | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Support for ACSL builtin functions (\max, \abs, \is_finite ...) with their overloaded specifications
https://git.frama-c.com/pub/frama-c/-/issues/1948
addr_eq versus = and <> in generated axioms access_update, access_update_neq
2021-02-22T13:47:03Z
Jochen Burghardt
addr_eq versus = and <> in generated axioms access_update, access_update_neq
ID0001117:
**This issue was created automatically from Mantis Issue 1117. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001117:
**This issue was created automatically from Mantis Issue 1117. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001117 | Frama-C | Plug-in > wp | public | 2012-03-12 | 2012-11-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | pherrmann | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
I ran "frama-c -wp -cpp-command 'gcc -C -E -I.' -pp-annot -wp-rte -wp-proof alt-ergo -no-unicode -wp-warnings -wp-out ./out ftest.c" on the attached program and inspected the generated file "out/store_ftest_post_1_po_ergo.why".
In the proof obligation for c-source line 14, the update operator a[i<-v] is used with e.g. addr_shift(s_0,0) substituted for i. In the axioms access_update and access_update_neq, arguments at position i are compared by built-in equality (and disequality <>).
However, terms starting with "addr_shift" are usually compared by "addr_eq", e.g. in the translation of lemma l.
I suggest to check whether the mentioned axioms should be weakened to:
axiom access_update : (forall a:'a1 farray.(forall i:int.(forall j:int.(forall v:'a1.(addr_eq(i,j) -> a[i<-v][j]=v)))))
axiom access_update_neq : (forall a:'a1 farray.(forall i:int.(forall j:int.(forall v:'a1.((not addr_eq(i,j)) -> (a[i<-v][j]=a[j]))))))
If not, I suggest to check whether addr_eq is in fact the same as =, and to drop the former for sake of simplicity.
## Attachments
- [ftest.c](/uploads/cd05b6376c9c0e2eb054fdb51936c97c/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/1026
Signal -7 and then crashed.
2021-02-22T13:47:19Z
mantis-gitlab-migration
Signal -7 and then crashed.
ID0001602:
**This issue was created automatically from Mantis Issue 1602. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001602:
**This issue was created automatically from Mantis Issue 1602. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001602 | Frama-C | Plug-in > wp | public | 2014-01-15 | 2014-06-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dharma | **Assigned To** | correnson | **Resolution** | unable to reproduce |
| **Priority** | high | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
$ frama-c -wp -wp-rte test_frama.c -wp-fct=myFunc -wp-bhv=basic -main myFunc -lib-entry -wp-timeout=500
[kernel] preprocessing with "gcc -C -E -I. test_frama.c"
[wp] Running WP plugin...
[rte] annotating function myFunc
[wp] Collecting axiomatic usage
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_myFunc_basic_post : Failed
Error: Unix.SIGNAL -7
Any comments?
### Steps To Reproduce :
I used Alt-Ergo 0.95.2. Unfortunately, this code is somewhat complex and cannot disclose here although I would like to share.
## Attachments
- [ApLowAlm.mlw](/uploads/39c448b8eed5e0db531692fb99845956/ApLowAlm.mlw)
https://git.frama-c.com/pub/frama-c/-/issues/109
Crash on loop with global assigns and per-behavior assigns
2021-02-22T13:47:26Z
Boris Yakobowski
Crash on loop with global assigns and per-behavior assigns
ID0002180:
**This issue was created automatically from Mantis Issue 2180. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002180:
**This issue was created automatically from Mantis Issue 2180. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002180 | Frama-C | Plug-in > wp | public | 2015-10-19 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | correnson | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
frama-c -wp crashes on the following program
/*@ behavior foo:
*/
void main(void)
{
int i;
int t[10];
i = 0;
/*@ loop assigns t[0 .. i];
for foo: loop assigns t[0 .. i]; */
while (i < 10) {
t[i] = 0;
i ++;
}
return;
}
https://git.frama-c.com/pub/frama-c/-/issues/1972
Proof obligations of lemma properties
2021-02-22T13:47:37Z
Patrick Baudin
Proof obligations of lemma properties
ID0000895:
**This issue was created automatically from Mantis Issue 895. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000895:
**This issue was created automatically from Mantis Issue 895. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000895 | Frama-C | Plug-in > wp | public | 2011-07-28 | 2012-09-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | correnson | **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 Oxygen-20120901 |
### Description :
Proof obligations of lemma properties are not generated.
Revision: 14360
### Additional Information :
cat test_po_lemma1.c
//@ lemma l: 2 == 1 + 1 ;
//@ ensures p: \true ;
void f (void) {
return ;
}
> frama-c -wp -wp-model Store test_po_lemma1.c -wp-warnings
test_po_lemma1.c:1:[wp] warning: Proof obligation for property 'l' not generated.
https://git.frama-c.com/pub/frama-c/-/issues/1987
unable to prove that comparison-result is 0 or 1: insufficient axiomatization...
2021-02-22T13:48:00Z
Jochen Burghardt
unable to prove that comparison-result is 0 or 1: insufficient axiomatization of eq_int_bool?
ID0001028:
**This issue was created automatically from Mantis Issue 1028. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001028:
**This issue was created automatically from Mantis Issue 1028. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001028 | Frama-C | Plug-in > wp | public | 2011-11-28 | 2012-09-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
The attached program is verified under Jessie (why 2.30), but not under Wp.
Jessie generates two obligations: one for the case a==9 (and \result==1), and another for a!=9 (and \result==0); both are trivial to verify.
In contrast, Wp generates something like ite(eq_int_bool(a,9),1,0)==0 || ite(eq_int_bool(a,9),1,0)==1. I found axioms like ite(true,x,y)==x and ite(false,x,y)==y, however, an axiom about eq_int_bool always returning either true or false seems to be missing.
## Attachments
- [ftest.c](/uploads/96a730b802870b497a4fb76f715f40b4/ftest.c)
- [ite.why](/uploads/d97237421ce7afd76bca35e26fa10a06/ite.why)
https://git.frama-c.com/pub/frama-c/-/issues/107
Information on C type of array is not present (in Coq)
2021-02-22T13:48:11Z
Jens Gerlach
Information on C type of array is not present (in Coq)
ID0002332:
**This issue was created automatically from Mantis Issue 2332. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002332:
**This issue was created automatically from Mantis Issue 2332. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002332 | Frama-C | Plug-in > wp | public | 2017-11-22 | 2019-10-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | Linux, macOS | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the attached file 'array.c' there are two simple predicates 'AllEqual' and 'Constant' that involve int arrays.
There are also two lemmas that relate both predicate.
While it can automatically verified that "Constant" implies "AllEqual" the proof of the "converse" statement fails. When looking at the Coq presentation of "AllEqual" it becomes apparent that Coq only sees an "integer array"; the specific C type (represented by the predicate 'is_sint32') is NOT present at all.
### Additional Information :
The error also occurs in the beta release of Frama-C 16 (Sulfur).
### Steps To Reproduce :
Run the command:
frama-c-gui -no-unicode -wp -wp-prover alt-ergo -wp-prover coq -wp-script 'wp0.script' array.c
## Attachments
- [array.c](/uploads/9ffd5dc713b956ec02a3457ddc3b71c6/array.c)
- [wp0.script](/uploads/eb44100130d8efee641d5565ee82857b/wp0.script)
https://git.frama-c.com/pub/frama-c/-/issues/1999
Bitwise Operators
2021-02-22T13:48:18Z
Loïc Correnson
Bitwise Operators
ID0001108:
**This issue was created automatically from Mantis Issue 1108. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001108:
**This issue was created automatically from Mantis Issue 1108. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001108 | Frama-C | Plug-in > wp | public | 2012-02-29 | 2012-09-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | correnson | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
No correspondance between C-bitwise operations of natural int-model and ACSL-bitwise ones.
Error in translation of (~) in C.
### Additional Information :
Reported on Frama-C Discuss
https://git.frama-c.com/pub/frama-c/-/issues/2018
Upgrading WP causes crash in Jessie
2021-02-22T13:48:53Z
mantis-gitlab-migration
Upgrading WP causes crash in Jessie
ID0001225:
**This issue was created automatically from Mantis Issue 1225. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001225:
**This issue was created automatically from Mantis Issue 1225. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001225 | Frama-C | Plug-in > wp | public | 2012-07-02 | 2012-09-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
I just upgraded WP to 0.5 and I've discovered that Jessie crashes on a file that shouldn't cause any problems:
[kernel] preprocessing with "gcc -C -E -I. -dD test-pc4.c"
[jessie] Starting Jessie translation
[kernel] The full backtrace is:
Called from file "src/project/state_builder.ml", line 439, characters 10-31
Called from file "src/project/project.ml", line 119, characters 28-67
Called from file "hashtbl.ml", line 157, characters 23-35
Called from file "hashtbl.ml", line 161, characters 12-33
Called from file "src/project/project.ml", line 116, characters 6-364
Called from file "list.ml", line 69, characters 12-15
Called from file "src/lib/qstack.ml", line 107, characters 4-23
Called from file "src/kernel/file.ml", line 1376, characters 2-33
Called from file "register.ml", line 96, characters 4-93
Called from file "register.ml", line 290, characters 6-12
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 723, characters 2-9
Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
Unexpected error (File "src/type/datatype.ml", line 98, characters 18-24: Assertion failed).
I called Jessie with frama-c -jessie -jessie-atp=gui -pp-annot. Both why2 and why3 are installed.
Everything works with Jessie after I uninstalled WP-0.5 and reinstalled Nitrogen from scratch.
This is strange since an update of WP should only affect files in src/wp.
https://git.frama-c.com/pub/frama-c/-/issues/2039
WP 0.5 crashes with an Unbound label parameter 'Here'
2021-02-22T13:49:30Z
Mounir Assaf
WP 0.5 crashes with an Unbound label parameter 'Here'
ID0001060:
**This issue was created automatically from Mantis Issue 1060. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001060:
**This issue was created automatically from Mantis Issue 1060. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001060 | Frama-C | Plug-in > wp | public | 2012-01-11 | 2012-06-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Mounir | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
A reproductible bug for the attached example from "ACSL by example". It was proven correctly previously.
[wp] failure: Unbound label parameter 'Here' in predicate or function call
[kernel] The full backtrace is:
Raised at file "register.ml", line 610, characters 27-29
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 723, characters 2-9
Called from file "src/kernel/cmdline.ml", line 200, characters 4-8
## Attachments
- [count.c](/uploads/5d2267bc8572f7408b3f4710096bd854/count.c)
https://git.frama-c.com/pub/frama-c/-/issues/2075
Requires of behaviors lost
2021-02-22T13:50:27Z
Boris Yakobowski
Requires of behaviors lost
ID0001035:
**This issue was created automatically from Mantis Issue 1035. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001035:
**This issue was created automatically from Mantis Issue 1035. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001035 | Frama-C | Plug-in > wp | public | 2011-11-30 | 2012-01-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **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 :
The wp currently loses 'required' clauses attached to a behavior. The example below can be used to test this; the access to *p should be proven valid.
Cmdline : frama-c -wp -wp-rte
/*@ behavior p: assumes x == 1; requires \valid(p);
behavior q: assumes x!= 1;
disjoint behaviors; */
void f(int x, int *p) {
if (x == 1)
*p = 1;
}
https://git.frama-c.com/pub/frama-c/-/issues/2081
Testing example which is OK for Jessie-plugin fails with wp-plugin.
2021-02-22T13:50:32Z
mantis-gitlab-migration
Testing example which is OK for Jessie-plugin fails with wp-plugin.
ID0001054:
**This issue was created automatically from Mantis Issue 1054. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001054:
**This issue was created automatically from Mantis Issue 1054. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001054 | Frama-C | Plug-in > wp | public | 2011-12-16 | 2011-12-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | naveugene | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[Sorry for my English]
I tried to verificate function with Frama-C Carbon + wp plugin + Alt-Ergo:
void set_array (int t[] , int n, int a)
{ for (int i=0; i < n; i++) t[i] = a; }
using Frama-C Boron + jessie plugin + Alt-Ergo all is OK:
"
total : 15
valid : 15 (100%)
"
but using wp:
"
No proofs : 3
Partial proofs : 1
Complete proofs : 3
Total : 7
"
files from "logs" folder (store_set_array_assert_3_rte_log.txt , store_set_array_assert_4_rte_log.txt , store_set_array_post_1_log.txt) are empty.
==================
Why count of "No proofs", "Partial proofs" is not 0? Why logfiles are empty?
(I'm including console output for jessie, wp for my example, and file arr_set_for.c with procedure and ACSL implementation in "arr_set_for.zip".)
### Tags :
jessie, wp
### Additional Information :
The examples from "frama-c-wp-manual.pdf", page 8 (swap1.c, swap 2.c) are OK.
## Attachments
- [arr_set_for.zip](/uploads/0f9a00c0f09c4866ce250f20a557f9f2/arr_set_for.zip)
https://git.frama-c.com/pub/frama-c/-/issues/2105
Problems when using ptests.
2021-02-22T13:51:05Z
Patrick Baudin
Problems when using ptests.
ID0000984:
**This issue was created automatically from Mantis Issue 984. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000984:
**This issue was created automatically from Mantis Issue 984. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000984 | Frama-C | Plug-in > wp | public | 2011-10-12 | 2011-10-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | correnson | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | sometimes |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Using ptests gives alt-ergo files with typing errors which are not there when executing the command given by ptests.
### Additional Information :
cd plugins/wp_bench/CAS_bcl/auto-test
ptests.byte tests/c2fc/auto-test.c
https://git.frama-c.com/pub/frama-c/-/issues/2116
wp-plugin does not generate coq *.v goals.
2021-02-22T13:51:27Z
mantis-gitlab-migration
wp-plugin does not generate coq *.v goals.
ID0000926:
**This issue was created automatically from Mantis Issue 926. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000926:
**This issue was created automatically from Mantis Issue 926. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000926 | Frama-C | Plug-in > wp | public | 2011-08-15 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jessie_user | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Wp plugin for carbon-20110201 does not generate coq proover goals.
In carbon-beta2 there is no such error.
frama-c -wp-help
Plug-in name: WP 0.3
frama-c -version
Version: Carbon-20110201
Ocaml-version: 64 bit, we have not GUI installed.
Example:
frama-c -wp -wp-out wp_longlong -wp-rte test_wp_longlong.c
ls wp_longlong/
store_add_assert_1_rte_body.txt store_add_assert_2_rte_head.txt store_add_post_1_A_body.txt
store_add_assert_1_rte_head.txt store_add_assert_3_rte_body.txt store_add_post_1_A_head.txt
store_add_assert_2_rte_body.txt store_add_assert_3_rte_head.txt store_env1.txt
There are no *.v coq-files.
Example with another options: (-wp-proof coq)
frama-c -wp -wp-out wp_longlong -wp-proof coq -wp-rte test_wp_longlong.c
wp_longlong Directory with goals to prove contains:
ls wp_longlong/
store_add_assert_1_rte_body.txt store_add_assert_2_rte_head.txt store_add_assert_3_rte_log.txt store_env1.txt wp.vo
store_add_assert_1_rte_head.txt store_add_assert_2_rte_log.txt store_add_post_1_A_body.txt store_env1.v
store_add_assert_1_rte_log.txt store_add_assert_3_rte_body.txt store_add_post_1_A_head.txt store_env1.vo
store_add_assert_2_rte_body.txt store_add_assert_3_rte_head.txt store_add_post_1_A_log.txt store_model.vo
There are no coq *.v files, only store_env1.v without goals to proof.
## Attachments
- [test_wp_longlong.c](/uploads/bf9396ba8a1de7309ee14aa87057d065/test_wp_longlong.c)
https://git.frama-c.com/pub/frama-c/-/issues/2117
Wp rises an error in if you use struct and long long type, with wp-rte option
2021-02-22T13:51:29Z
mantis-gitlab-migration
Wp rises an error in if you use struct and long long type, with wp-rte option
ID0000925:
**This issue was created automatically from Mantis Issue 925. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000925:
**This issue was created automatically from Mantis Issue 925. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000925 | Frama-C | Plug-in > wp | public | 2011-08-12 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jessie_user | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Following command with -wp-rte option rises an error.
frama-c -wp -wp-rte -wp-out wp_longlong test_wp_longlong.c
Output:
frama-c -wp -wp-rte -wp-out wp_longlong test_wp_longlong.c
[kernel] preprocessing with "gcc -C -E -I. test_wp_longlong.c"
[rte] annotating function add
[kernel] The full backtrace is:
Raised at file "src/kernel/command.ml", line 42, characters 10-13
Called from file "src/wp/cfgProof.ml", line 125, characters 4-118
Called from file "list.ml", line 69, characters 12-15
Called from file "list.ml", line 69, characters 12-15
Called from file "list.ml", line 69, characters 12-15
Called from file "list.ml", line 69, characters 12-15
Called from file "src/wp/cfgProof.ml", line 223, characters 1-607
Called from file "src/wp/register.ml", line 322, characters 41-57
Called from file "src/wp/register.ml", line 464, characters 3-32
Called from file "src/wp/register.ml", line 533, characters 8-20
Called from file "src/wp/register.ml", line 570, characters 4-18
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 660, characters 2-9
Called from file "src/kernel/cmdline.ml", line 173, characters 4-8
Unexpected error (Failure("int_of_string")).
Please report as 'crash' at http://bts.frama-c.com/
Note that a backtrace alone often does not have information to
understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
Without wp-rte Option ok:
frama-c -wp -wp-out wp_longlong test_wp_longlong.c
[kernel] preprocessing with "gcc -C -E -I. test_wp_longlong.c"
[wp] warning: Missing RTE guards
If you use int type in INTEGER32 structure, then its ok.
### Additional Information :
struct INTEGER32 {
// int value; // Ok
long long value; // Fails
};
typedef struct INTEGER32 int32;
/*@
requires \valid(x) && \valid(y);
*/
void add (int32* x, int32* y){
int32 erg;
erg.value = x->value + y->value;
}
## Attachments
- [test_wp_longlong.c](/uploads/821c2c96e2982d73b22a7f481b578648/test_wp_longlong.c)
https://git.frama-c.com/pub/frama-c/-/issues/2147
Hypothesis missing about pointed datatypes
2021-02-22T13:52:10Z
Patrick Baudin
Hypothesis missing about pointed datatypes
ID0000779:
**This issue was created automatically from Mantis Issue 779. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000779:
**This issue was created automatically from Mantis Issue 779. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000779 | Frama-C | Plug-in > wp | public | 2011-04-08 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | dargaye | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
An hypothesis about the bounds of the pointed data seems to be missing.
The assertion of the given example cannot be proved with WP Carbon beta-2.
file pb_uint8.c
---------------
void f(unsigned char *t) {
//@ assert t[0] < 256;
t[1]=3;
}
command: frama-c-gui -wp -wp-axioms pb_uint8.c
https://git.frama-c.com/pub/frama-c/-/issues/2149
initial value of structures
2021-02-22T13:52:13Z
Patrick Baudin
initial value of structures
ID0000796:
**This issue was created automatically from Mantis Issue 796. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000796:
**This issue was created automatically from Mantis Issue 796. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000796 | Frama-C | Plug-in > wp | public | 2011-04-14 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | dargaye | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
The related PO seems to be probable. Perhaps a problem of axiomatics or triggers for alt-ergo.
### Additional Information :
> frama-c-gui -wp -wp-prop p5 valinit.c -wp-proof alt-ergo
...
[wp] [Alt-Ergo] Goal store_main_post_19_p5 : Timeout
It should be the same problem with -wp-prop p5_bis
## Attachments
- [valinit.c](/uploads/a48ae2216cd53c29a6445737407b4d78/valinit.c)
https://git.frama-c.com/pub/frama-c/-/issues/2203
unprovable po with -split
2021-02-22T13:53:32Z
Stephane Duprat
unprovable po with -split
ID0000642:
**This issue was created automatically from Mantis Issue 642. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000642:
**This issue was created automatically from Mantis Issue 642. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000642 | Frama-C | Plug-in > wp | public | 2010-12-17 | 2011-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sduprat | **Assigned To** | dargaye | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101201-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20110201 |
### Description :
po of VAR2_PANNE seems to unprovable using -wp-split option. No problem without -wp-split for this property.
cmd:
sduprat@vmu3cat03:~/tmp$ frama-c-gui -pp-annot -wp -wp-proof alt-ergo -wp-model Store -wp-par 10 -wp-no-arrays source_combined.c -wp-split
sduprat@vmu3cat03:~/tmp$ frama-c-gui -pp-annot -wp -wp-proof alt-ergo -wp-model Store -wp-par 10 -wp-no-arrays source_combined.c
## Attachments
- [src.tar](/uploads/b9070c9e2c4de1cf8fe05d2f7e865c66/src.tar)
https://git.frama-c.com/pub/frama-c/-/issues/2205
Unexpected error (Stack overflow) during WP
2021-02-22T13:53:36Z
Benjamin Monate
Unexpected error (Stack overflow) during WP
ID0000665:
**This issue was created automatically from Mantis Issue 665. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000665:
**This issue was created automatically from Mantis Issue 665. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000665 | Frama-C | Plug-in > wp | public | 2011-01-10 | 2011-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | monate | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | Frama-C Carbon-20110201 | **Fixed in Version** | Frama-C Carbon-20110201 |
### Description :
On this file (inspired by bts#654):
frama-c.byte -wp -wp-proof alt-ergo 654.c
crashes with a stack overflow.
===========
typedef unsigned long u64;
struct range {
u64 start;
u64 end;
};
#define min(a,b) ((a < b) ? a : b)
#define max(a,b) ((a > b) ? a : b)
int add_range(struct range *range, int az, int nr_range, u64 start, u64 end);
int add_range_with_merge(struct range *range, int az, int nr_range,
u64 start, u64 end);
void subtract_range(struct range *range, int az, u64 start, u64 end);
/*@ predicate isSorted(struct range* ranges, integer length) =
@ length <= 1 ||
@ (\forall integer idx; 0 <= idx < length-1 ==> ranges[idx].start <= ranges[idx + 1].start);
@
@ logic integer appears{L}(struct range* ranges, integer length, integer istart, integer iend) =
@ length <= 0
@ ? 0
@ : (istart == ranges[0].start && iend == ranges[0].end)
@ ? 1 + appears(ranges + 1, length - 1, istart, iend)
@ : appears(ranges + 1, length - 1, istart, iend);
@*/
/*@ requires az >= 0;
@ requires \valid(range+ (0..az-1));
@
@ assigns *(range+ (0..az-1));
@
@ ensures \forall integer i; 0 <= i < az ==>
@ appears(range, az, range[i].start, range[i].end) == \old(appears(range, az, range[i].start, range[i].end));
@ ensures isSorted(range, az);
@*/
void sort(struct range *range, int az) ;
/*@ logic integer nemptyCount{L}(struct range* ranges, integer length) =
@ length <= 0
@ ? 0
@ : ranges[0].end == 0
@ ? nemptyCount(ranges + 1, length - 1)
@ : 1 + nemptyCount(ranges + 1, length - 1);
@
@ logic integer emptyCount{L}(struct range* ranges, integer length) =
@ length - nemptyCount(ranges, length);
@*/
/*@ requires az >= 0;
@ requires \valid(range+ (0..az-1));
@
@ assigns *(range+ (0..az-1));
@
@ ensures \result == nemptyCount(range, az);
@ ensures isSorted(range, \result);
@ ensures \forall integer i; 0 <= i < \result ==>
@ appears(range, \result, range[i].start, range[i].end) == \old(appears(range, az, range[i].start, range[i].end));
@*/
int clean_range(struct range *range, int az)
{
int i, j, k = az - 1, nr_range = az;
/*@
@
@ loop invariant 0 <= i <= k;
@ loop invariant emptyCount(range, i) == 0;
@ loop invariant emptyCount(range, az) == \at(emptyCount(range, az), Pre);
@ loop invariant az-1-emptyCount(range, az) <= k <= az-1;
@ loop invariant \forall integer idx; (0 <= idx < az) &&
@ \at(range[idx].end != 0, Pre) ==>
@ appears(range, az, \at(range[idx].start, Pre), \at(range[idx].end, Pre))
@ == \at(appears(range, az, \at(range[idx].start, Pre), \at(range[idx].end, Pre)), Pre);
loop variant k - i;
@*/
for (i = 0; i < k; i++) {
if (range[i].end)
continue;
/*@
@
@ loop invariant i <= j <= k;
@ loop invariant \forall integer idx; j < idx < az ==> range[idx].end == 0;
loop variant j;
@*/
for (j = k; j > i; j--) {
if (range[j].end) {
k = j;
break;
}
}
if (j == i)
break;
range[i].start = range[k].start;
range[i].end = range[k].end;
range[k].start = 0;
range[k].end = 0;
k--;
}
/*@
@
@ loop invariant 0 <= i <= emptyCount(range, az);
loop variant i;
@*/
/* count it */
for (i = 0; i < az; i++) {
if (!range[i].end) {
nr_range = i;
break;
}
}
/*@ assert nr_range == emptyCount(range, az);
@*/
sort(range,nr_range);
return nr_range;
}
https://git.frama-c.com/pub/frama-c/-/issues/2206
warning: Degenerated goal
2021-02-22T13:53:39Z
Stephane Duprat
warning: Degenerated goal
ID0000662:
**This issue was created automatically from Mantis Issue 662. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000662:
**This issue was created automatically from Mantis Issue 662. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000662 | Frama-C | Plug-in > wp | public | 2011-01-07 | 2011-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sduprat | **Assigned To** | dargaye | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | Frama-C Carbon-20110201 | **Fixed in Version** | Frama-C Carbon-20110201 |
### Description :
warning degenerated goal is raised with this source example containing unions.
ensures are unproved.
### Additional Information :
frama-c -wp -pp-annot -wp-model Store -wp-proof alt-ergo -wp-split *.c
[wp] warning: Degenerated goal store_f1_post_5_P1 (1 warning)
[wp] warning: Degenerated goal store_f1_post_6_P2 (2 warnings)
[wp] warning: Degenerated goal store_f1_post_7_P3 (3 warnings)
[wp] [Alt-Ergo] Goal store_f1_post_7_P3 : Unknown
[wp] [Alt-Ergo] Goal store_f1_post_6_P2 : Unknown
[wp] [Alt-Ergo] Goal store_f1_post_5_P1 : Unknown
## Attachments
- [source.c](/uploads/ebf0295e683ad2e585cd469c5f85bf51/source.c)