frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:48:18Zhttps://git.frama-c.com/pub/frama-c/-/issues/1999Bitwise Operators2021-02-22T13:48:18ZLoïc CorrensonBitwise OperatorsID0001108:
**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 Discusshttps://git.frama-c.com/pub/frama-c/-/issues/1987unable to prove that comparison-result is 0 or 1: insufficient axiomatization...2021-02-22T13:48:00ZJochen Burghardtunable 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/1972Proof obligations of lemma properties2021-02-22T13:47:37ZPatrick BaudinProof obligations of lemma propertiesID0000895:
**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/1960Multiple branches to a label/loop entries crashes wp2021-04-15T07:11:39Zmantis-gitlab-migrationMultiple branches to a label/loop entries crashes wpID0001279:
**This issue was created automatically from Mantis Issue 1279. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001279:
**This issue was created automatically from Mantis Issue 1279. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001279 | Frama-C | Plug-in > wp | public | 2012-10-13 | 2012-10-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sjw | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following code:
/*@ ensures \result == x; */
int test(int x)
{
again:
if (x > 10)
goto again;
if (x > 10)
goto again;
return x;
}
gives
$ ~/frama-c/bin/frama-c -wp doublegoto.c
[kernel] preprocessing with "gcc -C -E -I. doublegoto.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] failure: CFG node <loop-1> has 2 successors instead of 1
...
This is caused by the use of a list for loop headers in cil2cfg.ml. The
attached patch fixes this by using a set of nodes.
## Attachments
- [goto.diff](/uploads/7ba7b9828d39e5be247e9fb3e8ba11cb/goto.diff)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1959Printing of function types causes a stack overflow2021-04-14T15:41:22Zmantis-gitlab-migrationPrinting of function types causes a stack overflowID0001280:
**This issue was created automatically from Mantis Issue 1280. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001280:
**This issue was created automatically from Mantis Issue 1280. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001280 | Frama-C | Plug-in > wp | public | 2012-10-13 | 2012-10-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
This occurs when dealing with function pointer types:
in src/wp/fol_formula.ml, pp_ctype, line
477 | TFun _ as t -> Format.fprintf fmt "%a*" (pp_ctype dim) t
causes a stack overflow through the recursion on t. As far as I can
see, this function is only used to inform the user, so anything else would
be OK.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1948addr_eq versus = and <> in generated axioms access_update, access_update_neq2021-02-22T13:47:03ZJochen Burghardtaddr_eq versus = and <> in generated axioms access_update, access_update_neqID0001117:
**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/1929ACSL builtins2021-02-22T13:46:18ZLoïc CorrensonACSL builtinsID0000816:
**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 specificationshttps://git.frama-c.com/pub/frama-c/-/issues/1928Support of \block_length2021-02-22T13:46:17ZPatrick BaudinSupport of \block_lengthID0000903:
**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/1925[wp] failure: not an integer (Blob)2021-04-14T15:42:16Zmantis-gitlab-migration[wp] failure: not an integer (Blob)ID0001332:
**This issue was created automatically from Mantis Issue 1332. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001332:
**This issue was created automatically from Mantis Issue 1332. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001332 | Frama-C | Plug-in > wp | public | 2012-12-15 | 2012-12-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Philippe | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
> cat bar.c
typedef struct S { signed char x[16]; } S;
/*@ axiomatic Y { logic integer Z (S t, integer i, integer j) reads t.x[i..j]; } */
/*@ ensures \result == Z(s, 0, 15); */
int foo(S s) { return 0; }
> frama-c -wp -wp-rte -wp-fct foo bar.c
[kernel] preprocessing with "gcc -C -E -I. bar.c"
[wp] Running WP plugin...
[rte] annotating function foo
[wp] warning: Interpreting reads-definition as expressions rather than tsets
bar.c:6:[wp] failure: not an integer (Blob)
[kernel] The full backtrace is:
Raised at file "src/kernel/log.ml", line 523, characters 30-31
Called from file "src/kernel/log.ml", line 517, characters 9-16
Re-raised at file "src/kernel/log.ml", line 520, characters 15-16
Called from file "src/wp/translate_prop.ml", line 911, characters 16-71
Called from file "src/wp/translate_prop.ml", line 1323, characters 12-33
Called from file "src/wp/translate_prop.ml", line 1579, characters 32-52
Called from file "list.ml", line 69, characters 12-15
Called from file "src/wp/translate_prop.ml", line 1974, characters 14-68
Re-raised at file "src/wp/translate_prop.ml", line 2029, characters 12-15
Called from file "src/wp/translate_prop.ml", line 1827, characters 27-34
Re-raised at file "src/wp/translate_prop.ml", line 1831, characters 43-48
Called from file "src/wp/translate_prop.ml", line 2188, characters 21-56
Called from file "src/wp/translate_prop.ml", line 1570, characters 17-59
Called from file "src/wp/translate_prop.ml", line 1323, characters 12-33
Called from file "src/wp/translate_prop.ml", line 1745, characters 19-38
Called from file "src/wp/translate_prop.ml", line 1707, characters 13-30
Called from file "src/wp/wp_error.ml", line 102, characters 13-20
Re-raised at file "src/wp/wp_error.ml", line 95, characters 20-23
Called from file "src/wp/cfgWeakestPrecondition.ml", line 224, characters 17-33
Called from file "src/wp/cfgWeakestPrecondition.ml", line 154, characters 18-44
Re-raised at file "src/wp/wp_error.ml", line 90, characters 20-23
Called from file "src/wp/cfgWeakestPrecondition.ml", line 165, characters 34-54
Re-raised at file "src/wp/cfgWeakestPrecondition.ml", line 184, characters 14-17
Called from file "src/wp/cfgpropid.ml", line 96, characters 10-20
Re-raised at file "src/wp/cfgpropid.ml", line 100, characters 14-15
Called from file "src/wp/cfgpropid.ml", line 140, characters 12-59
Called from file "list.ml", line 74, characters 24-34
Called from file "src/wp/calculus.ml", line 326, characters 22-64
Called from file "src/wp/calculus.ml", line 336, characters 23-45
Called from file "src/wp/calculus.ml", line 575, characters 20-43
Called from file "src/wp/calculus.ml", line 498, characters 21-42
Called from file "src/wp/calculus.ml", line 548, characters 20-43
Called from file "src/wp/calculus.ml", line 498, characters 21-42
Called from file "src/wp/calculus.ml", line 551, characters 20-43
Called from file "src/wp/calculus.ml", line 498, characters 21-42
Called from file "src/wp/calculus.ml", line 551, characters 20-43
Called from file "src/wp/calculus.ml", line 498, characters 21-42
Called from file "src/wp/calculus.ml", line 541, characters 20-43
Called from file "src/wp/calculus.ml", line 498, characters 21-42
Called from file "src/wp/calculus.ml", line 536, characters 20-43
Called from file "src/wp/calculus.ml", line 498, characters 21-42
Called from file "src/wp/calculus.ml", line 661, characters 40-59
Called from file "set.ml", line 288, characters 38-41
Called from file "set.ml", line 293, characters 37-58
Called from file "set.ml", line 293, characters 42-57
Called from file "set.ml", line 293, characters 42-57
Called from file "src/wp/calculus.ml", line 661, characters 4-64
Called from file "src/wp/calculus.ml", line 708, characters 19-51
Called from file "src/wp/cfgProof.ml", line 238, characters 30-53
Called from file "list.ml", line 69, characters 12-15
Called from file "src/wp/cfgProof.ml", line 228, characters 8-666
Called from file "src/wp/register.ml", line 586, characters 22-41
Called from file "src/wp/register.ml", line 679, characters 17-24
Re-raised at file "src/wp/register.ml", line 683, characters 32-34
Called from file "src/wp/register.ml", line 678, characters 17-24
Re-raised at file "src/wp/register.ml", line 682, characters 29-31
Called from file "src/wp/register.ml", line 678, characters 17-24
Re-raised at file "src/wp/register.ml", line 682, characters 29-31
Called from file "src/wp/register.ml", line 678, characters 17-24
Re-raised at file "src/wp/register.ml", line 682, characters 29-31
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 38, characters 4-20
Called from file "src/kernel/cmdline.ml", line 720, characters 2-9
Called from file "src/kernel/cmdline.ml", line 197, characters 4-8
Plug-in wp aborted: internal error.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1912Post-state of statement spec2021-08-05T09:27:36Zmantis-gitlab-migrationPost-state of statement specID0000765:
**This issue was created automatically from Mantis Issue 765. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000765:
**This issue was created automatically from Mantis Issue 765. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000765 | Frama-C | Plug-in > wp | public | 2011-03-25 | 2013-03-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When there is a [goto] going out of a block, the post-condition should be check at the normal exit of the block (ie. the program point after the '}'). But there is a problem when the [goto] precisely jump to that point...
The CFG for WP should be able to find only the edge coming from the block exit !
### Additional Information :
$ frama-c -wp toto.c -wp-print
Goal store_f_default_for_stmt_2_stmt_post_1:
forall c:int.
is_in_format(sint32_format, c)
-> ( tag_Then:( (c <> 0) -> (let x= 1 in (x = 10)))
and tag_Else:( (c = 0) -> (let x= 10 in (x = 10))))
## Attachments
- [toto.c](/uploads/8feb2b09fab3964d8240b54efa9b2d18/toto.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1900Translation of tsets2021-04-15T14:21:06ZJulien SignolesTranslation of tsetsID0001389:
**This issue was created automatically from Mantis Issue 1389. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001389:
**This issue was created automatically from Mantis Issue 1389. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001389 | Frama-C | Plug-in > wp | public | 2013-04-15 | 2013-04-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Some tsets are not yet properly translated by Wp. Here is an example which expresses that the first n-th indexes of an array are equal to 0 (the ensures clause):
/*@ requires n >= 0;
@ requires \valid(t+(0..n-1));
@ ensures \result != 0 <==> t[0..n-1] == 0;
@ assigns \nothing;
@*/
int all_zeros(int t[], int n);Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1895performance problem about number of fields in structure for struct equality p...2021-02-22T13:45:15ZStephane Dupratperformance problem about number of fields in structure for struct equality propertiesID0001348:
**This issue was created automatically from Mantis Issue 1348. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001348:
**This issue was created automatically from Mantis Issue 1348. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001348 | Frama-C | Plug-in > wp | public | 2013-01-13 | 2013-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sduprat | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
For the same case of assign of struct,
- property about value of the assigned struct are proved for a small number of fields of struct
- same property unproved with a larger struct (11 elts)
### Additional Information :
See example in attached file
cmd:frama-c -wp source.c -wp-timeout 200
## Attachments
- [source.c](/uploads/173d92f48cc304aadbdc2a8a1d8e00ff/source.c)https://git.frama-c.com/pub/frama-c/-/issues/1889proc name in assigns clause causes crash2021-02-22T13:45:07ZJochen Burghardtproc name in assigns clause causes crashID0001293:
**This issue was created automatically from Mantis Issue 1293. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001293:
**This issue was created automatically from Mantis Issue 1293. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001293 | Frama-C | Plug-in > wp | public | 2012-11-01 | 2013-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
Running "frama-c -wp ftest.c >ftest.log 2>&1" on the attached program, and yielding the attached log file, the Kernel reports an unexpected stack overflow. Although referring to a procedure name ("ftest") in an assigns-clause (line 4) is one of the most stupid user-errors that can be made, it should not cause a crash.
## Attachments
- [ftest1.c](/uploads/72c2395da37560c903d6461b8aacc0d0/ftest1.c)
- [ftest.log](/uploads/778e4fe08dfcfd8b7f6f4e51fc23d36f/ftest.log)https://git.frama-c.com/pub/frama-c/-/issues/1888unproven property used in a behavior in Typed model2021-02-22T13:45:06ZStephane Dupratunproven property used in a behavior in Typed modelID0001299:
**This issue was created automatically from Mantis Issue 1299. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001299:
**This issue was created automatically from Mantis Issue 1299. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001299 | Frama-C | Plug-in > wp | public | 2012-11-06 | 2013-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sduprat | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
In the attached example, the b1_P1 property is unproven while the equivalent whithout the use of behavior is well proven.
This is in case if Typed model. In Store, all is proved.
Seeing the generated goals, perhaps a lack of relation between Mint_1 and Mint_0?
Or a problem in my assigns ?
In case of problem, is there any workaround ?
Regards.
Stéphane
### Additional Information :
Used with Alt-Ergo 0.94.
command used :
//frama-c -wp -wp-print -wp-byreference -wp-model Typed report1.c
## Attachments
- [report1.c](/uploads/da31f453d91122223103f2e40c2f63a3/report1.c)https://git.frama-c.com/pub/frama-c/-/issues/1883Wrong WP computation when calling a function with behaviors (assigns problem ?)2021-02-22T13:44:58Zmantis-gitlab-migrationWrong 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/1880undefined (or built-in?) predicate "global" in proof obligation2021-02-22T13:44:52ZJochen Burghardtundefined (or built-in?) predicate "global" in proof obligationID0001037:
**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/1879lemma tacitly ignored in absense of C code2021-02-22T13:44:51ZJochen Burghardtlemma tacitly ignored in absense of C codeID0001038:
**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/1875time too long even with -wp-timeout 12021-02-22T13:44:45ZPatrick Baudintime too long even with -wp-timeout 1ID0000793:
**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/1874initial value of strings2021-02-22T13:44:43ZPatrick Baudininitial value of stringsID0000794:
**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/1871couldn't verify series of struct member initializations2021-02-22T13:44:37ZJochen Burghardtcouldn't verify series of struct member initializationsID0001119:
**This issue was created automatically from Mantis Issue 1119. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001119:
**This issue was created automatically from Mantis Issue 1119. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001119 | Frama-C | Plug-in > wp | public | 2012-03-13 | 2013-04-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 Fluorine-20130401 |
### Description :
Our students Kerstin Hartig and Kim Völlinger observed problems to verify a series of assignments to struct members. Their extensive investigations of code variants and workaround possibilities is the basis for the following issue description.
Running "frama-c -wp -cpp-command 'gcc -C -E -I.' -pp-annot -wp-rte -wp-proof alt-ergo -wp-timeout 99999999 -no-unicode -wp-warnings 001.c", Alt-Ergo's proof attempt for line 25 didn't terminate within reasonable time, although only the effect of a trivial series of 16 initializing assignments was to be verified. That series wasn't unusually long; e.g. the most popular struct _IO_FILE has 21 members (in /usr/include/libio.h on my linux) that all need to be initialized. In contrast to Alt-Ergo, the Simplify prover found a proof within the default time-limit of 10 secs.
Timing the proof attempts for shorter assignment series, we observed the figures in file 001times.gpdat (elapsed time on a 1GHz machine). Plotting them by gnuplot exhibits their super-exponential growth (file 001times.gif). This behavior is reported separately to the Alt-Ergo bts.
Suggestion (A):
In file 00b.c, we omitted encapsulating variables a,...,p into a struct and defined each of them as an own global variable. In that case, Wp optimizes the assignment series such that no proof obligation at all needs to be given to Alt-Ergo. I suggest to consider performing the same optimization for struct fields; I guess this should be admitted by the default Store memory model. For example, in file 00bC.c, only the contents of the ->a fields need to be considered to verify the ensures clauses in lines 45-47.
Suggestion (B):
Trying to find out the reason for Alt-Ergo's runtimes, I found that a proof of non-interference of different struct fields needs the property
x<>y==>addr_shift(s,x)<>addr_shift(s,y),
which can be proven from the right-injectivity of +, the axiom addr_inj2, and the definition of addr_shift:
x <> y
==> offset(s)+x <> offset(s)+y
==> addr(base(s),offset(s)+x) <> addr(base(s),offset(s)+y)
==> addr_shift(s,x) <> addr_shift(s,y)
However, Alt-ergo seems to have problems to draw that conclusion. When I provide it as an additional axiom
axiom a2 : (forall s:int.(forall x:int.(forall y:int.
addr_shift(s,x)=addr_shift(s,y) -> x=y)))
Alt-Ergo verifies 001.c about as fast as Simplify. Hence, as a backup suggestion for those cases where (A) doesn't work or isn't sufficient, that additional axiom could be included in the .why files given to Alt-Ergo. (However, I'm not sure that this won't cause problems in other contexts.)
Alternatively, and as a workaround, that axiom can be user-provided as Acsl:
/*@ axiomatic a1 { axiom a2: \forall int* s; \forall integer x,y;
(int)(&s[x]) == (int)(&s[y]) ==> x == y; } */
This works also with heterogeneous struct field types as e.g. in file ftest.c.
## Attachments
- [001.c](/uploads/ced01d8c7bd463d266beedf3aef2dbaa/001.c)
- [001times.gpdat](/uploads/5ba591e39aa3cc67f30574fd4075ade5/001times.gpdat)
- ![001times](/uploads/26ba4c90f71c3c9e934aa1eb9773755f/001times.gif)
- [00b.c](/uploads/8fd95abdd7f3e8e5f98dd84d4604a7bf/00b.c)
- [00bC.c](/uploads/d157da3e3ac3992ae4a0df1065179be5/00bC.c)
- [ftest.c](/uploads/c8f0a6d35869253d0e0961ec89cb7d6b/ftest.c)