frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T13:44:51Z
https://git.frama-c.com/pub/frama-c/-/issues/1879
lemma tacitly ignored in absense of C code
2021-02-22T13:44:51Z
Jochen Burghardt
lemma tacitly ignored in absense of C code
ID0001038:
**This issue was created automatically from Mantis Issue 1038. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001038:
**This issue was created automatically from Mantis Issue 1038. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001038 | Frama-C | Plug-in > wp | public | 2011-12-05 | 2013-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
When running "frama-c -wp -cpp-command 'gcc -C -E -I.' -pp-annot -wp-rte -wp-proof simplify -no-unicode -wp-warnings -wp-out ./out ftest.c" on the attached program, I don't get any warning that no proof obligation is generated for lemma "l".
Such a warning is printed, however, when some C code is added (e.g. uncomment the trivial function definition in line 2 to demonstrate).
## Attachments
- [ftest.c](/uploads/d8414c6f283c53b6f03467f3c19b1747/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/1880
undefined (or built-in?) predicate "global" in proof obligation
2021-02-22T13:44:52Z
Jochen Burghardt
undefined (or built-in?) predicate "global" in proof obligation
ID0001037:
**This issue was created automatically from Mantis Issue 1037. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001037:
**This issue was created automatically from Mantis Issue 1037. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001037 | Frama-C | Plug-in > wp | public | 2011-12-01 | 2013-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **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** | Frama-C Fluorine-20130401 |
### Description :
For the attached program, the only generated proof obligation for Simplify reads
"(FORALL (y_0 ta_0) (IMPLIES (EQ (global ta_0) |@true|) (valid ta_0 y_0 1)))".
However, the predicate "global" does not occur anywhere in the .sx file.
While this need not necessarily be a bug, it looks suspicious.
(I couldn't find out whether "global" is a built-in predicate in Simplify.)
## Attachments
- [ftest.c](/uploads/ec86e21d318d4767cce318229736b3c1/ftest.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/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/2098
suggest to provide FILE,LINE references for proof obligations in WP cmd-line ...
2021-08-05T13:14:10Z
Jochen Burghardt
suggest to provide FILE,LINE references for proof obligations in WP cmd-line output
ID0001011:
**This issue was created automatically from Mantis Issue 1011. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001011:
**This issue was created automatically from Mantis Issue 1011. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001011 | Frama-C | Plug-in > wp | public | 2011-11-04 | 2011-11-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Currently, the command-line (i.e. non-gui) version of WP gives internally-generated names of proof obligations, like e.g.
[wp] [Simplify] Goal store_axiom_pop_of_push_pre31_push_stack_s1 : Valid
[wp] [Simplify] Goal store_axiom_pop_of_push_pre26_pop_stack_s2 : Timeout
In order to support the user in improving his program to get it verified, it should be made clear where an unproven obligation originated from, by providing file name and line number. Although a lot of information can be found in the directory specified with "-wp-out", the FILE,LINE information cannot.
Loïc Correnson
Loïc Correnson
https://git.frama-c.com/pub/frama-c/-/issues/2043
warn on stderr about current restrictions, and list them in WP manual
2021-04-15T07:05:34Z
Jochen Burghardt
warn on stderr about current restrictions, and list them in WP manual
ID0001010:
**This issue was created automatically from Mantis Issue 1010. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001010:
**This issue was created automatically from Mantis Issue 1010. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001010 | Frama-C | Plug-in > wp | public | 2011-11-04 | 2012-06-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When run on a file containing Acsl axioms, WP warns about an implementation restriction.
However, when run on a file containing lemmas, WP just says it won't generate proof obligations for them, without giving any reason. I guess, lemmas aren't currently implemented; in this case, WP should tell this to the user.
Additionally, all current implementations restrictions should be listed in the WP manual. In the current version, neither axioms nor lemmas are mentioned at all.
Loïc Correnson
Loïc Correnson
https://git.frama-c.com/pub/frama-c/-/issues/1883
Wrong WP computation when calling a function with behaviors (assigns problem ?)
2021-02-22T13:44:58Z
mantis-gitlab-migration
Wrong WP computation when calling a function with behaviors (assigns problem ?)
ID0000992:
**This issue was created automatically from Mantis Issue 992. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000992:
**This issue was created automatically from Mantis Issue 992. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000992 | Frama-C | Plug-in > wp | public | 2011-10-20 | 2013-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | high | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
The assert [0==1] is proved Valid in the enclosed example. This is because the proof obligation has an hypothesis [b = b + 1] instead of [b = b' + 1].
This problem appears from rev 15799 which is about [assigns] :
[WP] Warning for missing assigns clauses + better merge of assigns for function calls
### Additional Information :
$ frama-c toto.c -wp -wp-prop F -wp-print -wp-no-simpl
Proof Obligation assert_1_F:
Prover Alt-Ergo returns Valid
Environment: Store_env1
- Assumes Post-condition for 'end' (file toto.c, line 10) of 'add'
- Assumes Post-condition for 'ok' (file toto.c, line 6) of 'add'
+ Proves Assertion 'F' (file toto.c, line 19)
Goal store_f_assert_1_F:
let bound_0 = 0 in
let bound_1 = bound_0 in
((1000 <= bound_1) ->
false) ->
((bound_1 < 1000) ->
(bound_0 = (bound_1+1))) ->
tag_F:(0 = 1)
## Attachments
- [toto.c](/uploads/c4f262c05294a3f59da0f6ac5c7e630f/toto.c)
https://git.frama-c.com/pub/frama-c/-/issues/1358
Wrong [\valid(p)] outside the pointed variable scope
2021-02-22T13:32:33Z
mantis-gitlab-migration
Wrong [\valid(p)] outside the pointed variable scope
ID0000986:
**This issue was created automatically from Mantis Issue 986. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000986:
**This issue was created automatically from Mantis Issue 986. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000986 | Frama-C | Plug-in > wp | public | 2011-10-17 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
The following assertion is said to be true, but it shouldn't :
void main (void) {
int * p;
{ int x;
p = &x;
}
/*@ assert \valid(p); */
}
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/1350
Unexpected label Old in pre : ignored annotation
2021-02-22T13:32:30Z
mantis-gitlab-migration
Unexpected label Old in pre : ignored annotation
ID0000979:
**This issue was created automatically from Mantis Issue 979. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000979:
**This issue was created automatically from Mantis Issue 979. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000979 | Frama-C | Plug-in > wp | public | 2011-10-05 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
A precondition using a user predicate is ignored by wp because of an Old label, but there isn't any label in it :
int bound = 0;
//@ predicate Bok{L} (integer n) = 0 <= bound < n;
/*@ behavior ok:
assumes x > 0;
requires Bok (3);
ensures Bok (5);
assigns bound;
*/
int f (int x);
void g (void) {
int x = f(3);
//@ assert P: bound < 20;
}
The command is : frama-c -wp-fct g -wp-prop P bug.c
The precondition : requires Bok{Pre} (3); gives the same error.
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/1928
Support of \block_length
2021-02-22T13:46:17Z
Patrick Baudin
Support of \block_length
ID0000903:
**This issue was created automatically from Mantis Issue 903. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000903:
**This issue was created automatically from Mantis Issue 903. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000903 | Frama-C | Plug-in > wp | public | 2011-07-29 | 2012-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | low | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Properties containing \block_length construct cannot be proved.
## Attachments
- [ex_block_length.c](/uploads/1148c42420d07616df22e0796c4f17d9/ex_block_length.c)
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/1319
Warning for Axiom: From wp: Overloaded operator User defined axiom
2021-02-22T13:27:13Z
Patrick Baudin
Warning for Axiom: From wp: Overloaded operator User defined axiom
ID0000896:
**This issue was created automatically from Mantis Issue 896. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000896:
**This issue was created automatically from Mantis Issue 896. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000896 | Frama-C | Plug-in > wp | public | 2011-07-28 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Since there is no overloading is the source, the warning message has no sense!
### Additional Information :
> cat file.c
extern int tab[], x;
//@ axiomatic A { axiom ax: 10 < \block_length(tab); }
//@ assigns x;
extern void h(void);
//@ requires r2: x==0; assigns x;
void g() { h(); }
//@ requires r1: x==0;
void f(void) { g(); }
> frama-c -wp
...
file.c:8:[wp] warning: Warning for Axiom ax:
From wp: Overloaded operator User defined axiom ax{L} and User defined axiom ax
{L} not yet implemented
Effect: Ignored user-defined axiom 'ax'
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/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/1874
initial value of strings
2021-02-22T13:44:43Z
Patrick Baudin
initial value of strings
ID0000794:
**This issue was created automatically from Mantis Issue 794. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000794:
**This issue was created automatically from Mantis Issue 794. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000794 | Frama-C | Plug-in > wp | public | 2011-04-14 | 2013-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
WP is unable to proof properties on initial value of a string.
That comes from the uncompleteness of the generated PO; there is nothing about the initial value of the string.
### Additional Information :
> frama-c -wp -wp-prop p0 valinit.c -wp-proof alt-ergo
...
[wp] [Alt-Ergo] Goal store_main_post_9_p0 : Timeout
## Attachments
- [valinit.c](/uploads/eae1e5e251e971c442edd54f99d0c958/valinit.c)
https://git.frama-c.com/pub/frama-c/-/issues/1875
time too long even with -wp-timeout 1
2021-02-22T13:44:45Z
Patrick Baudin
time too long even with -wp-timeout 1
ID0000793:
**This issue was created automatically from Mantis Issue 793. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000793:
**This issue was created automatically from Mantis Issue 793. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000793 | Frama-C | Plug-in > wp | public | 2011-04-13 | 2013-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | dargaye | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
The PO is quickly computed, but the proof seems to take a llong time, but -wp-timeout 1 has no effect.
### Additional Information :
Revision: 12840
> frama-c valinit.c -wp -wp-prop p4 -wp-proof alt-ergo -wp-timeout 1
## Attachments
- [valinit.c](/uploads/05ab51222ebc3b38ef9148915d02e2c8/valinit.c)
https://git.frama-c.com/pub/frama-c/-/issues/1762
initializer completion
2021-02-22T13:40:45Z
Patrick Baudin
initializer completion
ID0000788:
**This issue was created automatically from Mantis Issue 788. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000788:
**This issue was created automatically from Mantis Issue 788. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000788 | Frama-C | Plug-in > wp | public | 2011-04-12 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | dargaye | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
C initialization of globals should be completed by 0.
This is partially done by CIL, since
int t15[15] = {3} ;
int t20[20] = {3} ;
is translated into
int t15[15] = {3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0};
int t20[20] = {3};
So, it can (maybe not for big arrays) be a bug of CIL.
Otherwise, wp should virtually perform this completion.
This is not done by wp 0.3 plug-in
### Additional Information :
This ensures clause should be provable.
int t15[15] = {3} ;
int t20[20] = {3} ;
//@ ensures t20[3]==0;
int main (void) { }