frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-08-05T08:49:16Zhttps://git.frama-c.com/pub/frama-c/-/issues/3[wp] shall use per-behaviour assigns at call sites2021-08-05T08:49:16ZNikolai Kosmatov[wp] shall use per-behaviour assigns at call sites# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *20.0 (Calcium)* (as reported by `frama-c -version`)
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *19.10*
*Please add specific information deemed...# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *20.0 (Calcium)* (as reported by `frama-c -version`)
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *19.10*
*Please add specific information deemed relevant with regard to this issue.*
# Steps to reproduce the issue
frama-c-gui -wp behavior_assigns.c
*Please indicate here steps to follow which reproduce the issue.*
See the attached file for a minimal example. [behavior_assigns.c](/uploads/b4eaee1cce8750d4749d64794e79883c/behavior_assigns.c)
# Expected behaviour
The assigns clause of caller can be proved.
# Actual behaviour
The assigns clause of caller is not proved.
The assigns clauses specific for particular behaviors in a callee cannot be used in the caller
under specific conditions falling into such behavior(s) to prove a more restrictive assigns clause
in the caller, rather than the most general assigns taking into account all behaviors of the callee.
# Fix ideas
Obvious workarounds include additional postconditions, that make the specifications more complex and
make the proof with WP less powerful. Matching the callee's behaviors to prove stronger assigns clauses
in the caller could be helpful.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1002assigns clause appears unprovable2021-08-05T08:49:01ZJens Gerlachassigns clause appears unprovableID0001638:
**This issue was created automatically from Mantis Issue 1638. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001638:
**This issue was created automatically from Mantis Issue 1638. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001638 | Frama-C | Plug-in > wp | public | 2014-02-01 | 2014-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | urgent | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
It appears that assigns clauses of functions that modify an array cannot be verified at all.
I attach a simple example of a function set_zero that sets all elements of an array to zero (file set_zero.c).
Attached is also an attempt to prove the assigns clause with Coq (see file wp0.script).
I do not see how from
0 <= n
0 < i
one can conclude
i <= n
Please, correct me if I am totally missing something.
### Additional Information :
Here is my proof attempt for the assigns clause:
Proof.
forward.
remember a_0 as a.
remember n_0 as n.
remember i_0 as i.
remember Mint_0 as M0.
remember Mint_1 as M1.
cut (i <= n).
auto with zarith.
assert(less_equal: 0 <= n).
assumption.
apply Zle_lt_or_eq in less_equal.
rewrite or_comm in less_equal.
destruct less_equal as [equal | less].
(* case equal *)
rewrite <- equal.
assert (~(i <= 0)).
auto with zarith.
contradict H7.
(* what now ? *)
Qed.
## Attachments
- [set_zero.c](/uploads/d5f6e570e7a4f9c0940b3c3d3b58509b/set_zero.c)
- [pb_assigns.c](/uploads/d4c0f6b7c5581fe712fd29c93c5cf800/pb_assigns.c) <- now verified.Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/1018assigns, loop assigns and loop invariant2021-08-05T08:48:53ZVirgile Prevostoassigns, loop assigns and loop invariantID0001461:
**This issue was created automatically from Mantis Issue 1461. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001461:
**This issue was created automatically from Mantis Issue 1461. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001461 | Frama-C | Plug-in > wp | public | 2013-07-24 | 2014-06-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the following (admittedly contrived) example, the assigns of g is not proved by WP (in fact it is reduced to false by Qed), although it is correct from ACSL semantics: as long as the loop invariant states that x still has its old value, the fact that it is mentioned in the loop assigns should not impede its absence in the assigns.
--- test.c
```
int x;
/*@ assigns \nothing; */
int g() {
/*@ loop assigns i,x;
loop invariant x == \at(x,Pre);
*/
for (int i = 0; i<2; i++);
return x;
}
```
### Steps To Reproduce :
frama-c -wp test.cLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2547"Unknown Error" with Alt-Ergo2021-06-01T11:23:20ZQix"Unknown Error" with Alt-ErgoBefore submitting the issue, please confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](http...Before submitting the issue, please confirm (by adding a X in the [ ]):
- [x] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [X] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *21.1 (Scandium)*
- Plug-in used: *wp*
- OS name: *Windows (via WSL 1)*
- OS version: *Windows 10 Pro build 19041.685*
I have also done `rm -f ~/.why3.conf; why3 config --detect --full-config` quite a few times now.
# Steps to reproduce the issue
Just creating a simple C file called `swap.c`:
```c
/*@
requires \valid(a) && \valid(b);
assigns *a, *b;
ensures *a == \old(*b);
ensures *b == \old(*a);
*/
void swap(int *a, int *b) {
int tmp = *a;
*a = *b;
*b = tmp;
}
int main() {
int a = 42;
int b = 37;
swap(&a, &b);
//@ assert a == 37 && b == 42;
return 0;
}
```
And running it with
```shell
frama-c -wp swap.c
```
# Expected behaviour
All goals proven.
# Actual behaviour
Alt-Ergo gives an `Unknown error`.
```
[kernel] Parsing swap.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Alt-Ergo 2.2.0] Goal typed_swap_ensures : Failed
Unknown error
[wp] Proved goals: 5 / 6
Qed: 5
Alt-Ergo 2.2.0: 0 (failed: 1)
```
I'm seeing this happen with a much larger project for just about every single goal there, too. I cannot verify a single C program with ACSL annotations, it seems.
# Fix ideas
No idea. I can't seem to find any information about this aside from a single unanswered StackOverflow question.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2[wp] non-provable local typing constraints in lemmas2021-05-28T09:30:55ZJens Gerlach[wp] non-provable local typing constraints in lemmas# Steps to reproduce the issue
The attached archive contains the ACSL function `Count` together with several lemma.
Also contained are
- a Makefile
- a coq proof in file `wp0.script.20` for lemma `CountBounds` that works for Frama-C 20...# Steps to reproduce the issue
The attached archive contains the ACSL function `Count` together with several lemma.
Also contained are
- a Makefile
- a coq proof in file `wp0.script.20` for lemma `CountBounds` that works for Frama-C 20
- an attempt of a coq proof in file `wp0.script.21` for lemma `CountBounds` that fails for Frama-C 21
- The files `CountBounds.v.20` and `CountBounds.v.21` contain the coq code as extracted from CoqIde
# Expected behaviour
My problem is that I am unable to adapt the coq proof that worked fro Frama-C 20 to the newer version of Frama-C.
# Actual behaviour
I suspect that this is related to changes in the generated Coq code of the VC of lemma `CountBounds`
This can be best seen when calling `diff CountBounds.v.20 CountBounds.v.21`.
```
$ diff CountBounds.v.20 CountBounds.v.21
39,40c39,40
< (((t.[ (shift_sint32 a x) ]) <> i_2)%Z) -> ((i < i_1)%Z) ->
< ((is_sint32 i_2%Z)) ->
---
> let x_1 := (t.[ (shift_sint32 a x) ])%Z in ((x_1 <> i_2)%Z) ->
> ((i < i_1)%Z) -> ((is_sint32 i_2%Z)) -> ((is_sint32 x_1)) ->
```
# Fix ideas
I think the issue is caused by the condition `((is_sint32 x_1))` for the newly introduced term `x_1 := (t.[ (shift_sint32 a x) ])%Z`. I haven't found a way to satisfy the condition `((is_sint32 x_1))` and I suspect that it is not possible.
If it is possible, then I apologise and ask for a hint.
Regards
Jens Gerlach
[CoqFramac21.tar](/uploads/e95b883ad30f134748c5a7289fa6902d/CoqFramac21.tar)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/499Unexpected error (Invalid_argument("Z.shift_left: count argument must be posi...2021-05-18T08:55:43Zmantis-gitlab-migrationUnexpected error (Invalid_argument("Z.shift_left: count argument must be positive"))ID0002201:
**This issue was created automatically from Mantis Issue 2201. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002201:
**This issue was created automatically from Mantis Issue 2201. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002201 | Frama-C | Plug-in > wp | public | 2016-01-22 | 2016-06-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rcl | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | Ubuntu | **OS Version** | 14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | Frama-C Aluminium |
### Description :
With the help of a custom csmith variant, a program was discovered that causes an unexpected error in the wp plugin. The following program is a reduced minimal example of the failing program discovered by csmith:
/*@ assigns \nothing; */
int main()
{
int foo = 1;
1 & (foo & 0x80000000000001LL) << 1;
return 0;
}
The crash message is:
Raised at file "src/wp/register.ml", line 579, characters 30-32
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 763, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (Invalid_argument("Z.shift_left: count argument must be positive")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
### Steps To Reproduce :
Save the aforementioned program into a file named test.c, then execute
frama-c -wp test.c
to cause the crash.
## Attachments
- [test.c](/uploads/1538550928d60f17405b687f59ab5e2b/test.c)https://git.frama-c.com/pub/frama-c/-/issues/948obligation "2+2==5" simplified to "false" by Qed, but then passed to Alt-Ergo...2021-04-29T02:25:35ZJochen Burghardtobligation "2+2==5" simplified to "false" by Qed, but then passed to Alt-Ergo neverthelessID0001999:
**This issue was created automatically from Mantis Issue 1999. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001999:
**This issue was created automatically from Mantis Issue 1999. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001999 | Frama-Clang | Plug-in > wp | public | 2014-11-27 | 2014-11-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp 167.c" on the attached program yields the output:
...
[wp] [Alt-Ergo] Goal typed_foo_assert : Unknown
...
The corresponding file "foo_assert_Alt-Ergo.mlw" contains the goal "goal foo_assert: false", in line 369.
Apparently, Qed succeeds to recognize that the assertion in line 3 of file "167.c" is provably wrong. However, the obligation is passed to the external prover Alt-Ergo nevertheless.
Similar to goals recognized as true by Qed, goals recognized as false needn't be passed to subsequent provers.
## Attachments
- [167.c](/uploads/612d6b11ee6897ee8e5fd3a99cd4e117/167.c)
- [foo_assert_Alt-Ergo.mlw](/uploads/bd7a96cf29e57c75a469e5b9fe7d5195/foo_assert_Alt-Ergo.mlw)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/919WP-Plugin crashes due to an internal error when terms of sets during union ha...2021-04-15T13:59:49Zmantis-gitlab-migrationWP-Plugin crashes due to an internal error when terms of sets during union have different typesID0002039:
**This issue was created automatically from Mantis Issue 2039. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002039:
**This issue was created automatically from Mantis Issue 2039. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002039 | Frama-C | Plug-in > wp | public | 2014-12-22 | 2014-12-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gaggarwal | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In case type of terms of tset1 and tset2 is different, then assigns \union(tset1, tset2) causes WP to crash.
In the example in attached file, first set has terms of type int, and other set set has terms of type double. union is throwing following error:
failure: c-object of logic type (ℝ)
### Steps To Reproduce :
When attached file is called with the following command-line:
frama-c -wp-fct copy -wp-print -wp-out temp -continue-annot-error array_assigns.c
Frama-C produces below output:
[kernel] preprocessing with "gcc -C -E -I. EditorTest/src/FVal_Infer/array_assigns.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
EditorTest/src/FVal_Infer/array_assigns.c:9:[wp] failure: c-object of logic type (ℝ)
[kernel] Current source was: EditorTest/src/FVal_Infer/array_assigns.c:9
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/wp/LogicSemantics.ml", line 802, characters 2-35
Called from file "list.ml", line 55, characters 20-23
Called from file "src/wp/LogicSemantics.ml", line 808, characters 27-51
Called from file "src/wp/cfgWP.ml", line 412, characters 6-147
Called from file "src/wp/Warning.ml", line 155, characters 14-18
Called from file "src/wp/cfgWP.ml", line 468, characters 22-126
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/Context.ml", line 68, characters 14-17
Re-raised at file "src/wp/Context.ml", line 69, characters 43-48
Called from file "src/wp/calculus.ml", line 334, characters 27-62
Called from file "src/wp/calculus.ml", line 341, characters 23-45
Called from file "src/wp/calculus.ml", line 613, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 586, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 589, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 589, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 583, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 599, characters 22-40
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 583, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 396, characters 20-39
Called from file "src/wp/calculus.ml", line 610, characters 10-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 589, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 579, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 574, characters 20-43
Called from file "src/wp/calculus.ml", line 536, characters 19-40
Called from file "src/wp/calculus.ml", line 699, characters 40-59
Called from file "set.ml", line 304, characters 38-41
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "map.ml", line 168, characters 10-18
Called from file "map.ml", line 168, characters 10-18
Called from file "src/wp/calculus.ml", line 699, characters 4-64
Called from file "src/wp/calculus.ml", line 745, characters 19-51
Called from file "src/wp/cfgWP.ml", line 1382, characters 39-62
Called from file "src/wp/cfgWP.ml", line 1371, characters 14-837
Called from file "src/wp/Model.ml", line 111, characters 17-20
Re-raised at file "src/wp/Model.ml", line 116, characters 25-28
Called from file "src/wp/Model.ml", line 117, characters 19-36
Called from file "src/wp/register.ml", line 435, characters 17-42
Called from file "src/wp/register.ml", line 574, characters 17-24
Re-raised at file "src/wp/register.ml", line 578, characters 29-31
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 32-34
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 735, characters 2-9
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
## Attachments
- [array_assigns.c](/uploads/fc8878d9ca24ca39c8b0ac9c83b61731/array_assigns.c)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/91quantifiers over logic types do not restrict to valid instances2021-04-15T09:37:11Zmantis-gitlab-migrationquantifiers over logic types do not restrict to valid instancesID0002497:
**This issue was created automatically from Mantis Issue 2497. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002497:
**This issue was created automatically from Mantis Issue 2497. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002497 | Frama-C | Plug-in > wp | public | 2020-01-30 | 2020-02-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | amosr | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
When I quantify over an unsigned char, the resulting formula uses the is_uint8 predicate to ensure that it only considers valid uint8s. However, if I define a logic type that contains an unsigned char, there is no corresponding is_ predicate for the logic type:
> //@ type logic_type_with_u8 = value(unsigned char);
This type is represented in the generated formula as an unbounded int rather than an unsigned char. This means that quantifying over the logic type includes more values than are allowed - for example, `\forall logic_type_with_u8 l` has to prove that the predicate is true even for values that won't fit in a u8.
As a concrete example, I expect the following to hold, but it does not:
> lemma u8_is_valid: \forall logic_type_with_u8 n; \exists unsigned char u; n == value(u);
Thanks,
Amos
### Additional Information :
PS. I could not test on the latest version from git - how do I get (read-only) access to the git repository?
### Steps To Reproduce :
Download file logic_type_is_valid.c and run with WP:
> frama-c -wp logic_type_is_valid.c
The lemma in this file should hold, but does not.
## Attachments
- [logic_type_is_valid.c](/uploads/ec550b694fa472b8bd9d08dc35a76d72/logic_type_is_valid.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/103Eprover in Frama-C 20 beta2021-04-15T09:36:20ZJens GerlachEprover in Frama-C 20 betaID0002483:
**This issue was created automatically from Mantis Issue 2483. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002483:
**This issue was created automatically from Mantis Issue 2483. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002483 | Frama-C | Plug-in > wp | public | 2019-11-08 | 2019-11-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Linux | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
I played a bit with various automatic provers in the beta
alt-ergo (2.3.0), native:alt-ergo (2.3.0), cvc4 (1.6), cvc3 (2.4.1), z3 (4.8.6) are recognized.
Eprover (2.4), on the other hand, is not recognized.
To be honest, Eprover is not such a great prover, but it has helped us discovering inconsistencies in our specifications.
Is there a specific reason, Eprover is not supported?
Attached is the error message.
### Steps To Reproduce :
$ frama-c -wp -wp-rte -wp-prover eprover -wp-out abs.wp abs.c
[kernel] Parsing abs.c (with preprocessing)
[rte] annotating function abs_int
[wp] 6 goals scheduled
[wp] [Eprover 2.4] Goal typed_abs_int_ensures_3 : Failed
[Why3 Error] Unknown printer 'tptp-fof'
[wp] [Cache] not used
[wp] Proved goals: 5 / 6
Qed: 5 (0.60ms-3ms-6ms)
Eprover 2.4: 0 (failed: 1)
## Attachments
- [abs.c](/uploads/07380fd95e05b2515b8f7dec3a1bad41/abs.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/324statement contract apparently confuses parser2021-04-15T09:31:56ZJochen Burghardtstatement contract apparently confuses parserID0002301:
**This issue was created automatically from Mantis Issue 2301. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002301:
**This issue was created automatically from Mantis Issue 2301. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002301 | Frama-C | Plug-in > wp | public | 2017-05-11 | 2017-07-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu 16.04.1 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp assigns.c" on the attached program produces a warning:
assigns.c:12:[wp] warning: Missing assigns clause (assigns 'everything' instead)
The warning is unjustified since the loop in line 12 does have a "loop assigns" clauses, and loops don't use (plain) "assigns" clauses.
If the trivial assertion in line 9 is activated, the warning disappears, and everything is proven.
If instead the braces in line 5 and 7 are removed, Frama-c reports a crash (text see "Additional Information").
### Additional Information :
Crash message:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing assigns.c (with preprocessing)
[wp] failure: Several assigns ?
[kernel] Current source was: assigns.c:2
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml", line 568, characters 30-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 562, characters 9-16
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 565, characters 15-16
Called from file "src/plugins/wp/wpStrategy.ml", line 470, characters 13-63
Called from file "src/plugins/wp/wpStrategy.ml", line 505, characters 8-34
Called from file "list.ml", line 73, characters 12-15
Called from file "src/plugins/wp/wpStrategy.ml", line 541, characters 2-34
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "src/plugins/wp/wpAnnot.ml", line 1023, characters 2-39
Called from file "src/plugins/wp/wpAnnot.ml", line 1094, characters 15-41
Called from file "src/plugins/wp/wpAnnot.ml", line 1273, characters 14-39
Called from file "src/plugins/wp/wpAnnot.ml", line 1274, characters 9-22
Called from file "src/plugins/wp/wpAnnot.ml", line 1363, characters 2-47
Called from file "map.ml", line 168, characters 20-25
Called from file "src/plugins/wp/Generator.ml", line 136, characters 4-39
Called from file "src/plugins/wp/register.ml", line 654, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 47-48
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501-beta1.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
## Attachments
- [assigns.c](/uploads/f5df9089249e50094cfbca65b1a403f3/assigns.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/333false postcondition shouldn't be verified in default memory-model setting2021-04-15T09:30:17ZJochen Burghardtfalse postcondition shouldn't be verified in default memory-model settingID0002312:
**This issue was created automatically from Mantis Issue 2312. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002312:
**This issue was created automatically from Mantis Issue 2312. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002312 | Frama-C | Plug-in > wp | public | 2017-06-15 | 2017-06-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte memmodel_default.c" verifies all 11 proof obligations, while the assert clase in line 21 is obviously violated. The reason for Frama-C's behavior is that it assumes the "Hoare Variables mixed with Pointers" memory model as a default (in accordance with WP manual sect.3.4, p.45) without checking its preconditions, viz. the absence of any address-taking of a variable.
A novice user who doesn't yet know about the subtleties of memory models will assume after the above Frama-c run that the program is ok, as is has been formally verified. This may build up unjustified trust in the program, and discredit Frama-C (or even the whole field of formal methods) once the bug is detected at runtime, possibly causing severe damage.
I suggest to either
1. check the applicability of the "Hoare Variables mixed with Pointers" model (this should be easily achievable, if only the source code needs to be scanned for a unary "&"), or
2. use another, less restrictive, model as default.
## Attachments
- [memmodel_default.c](/uploads/05c89d93d3c5c3dde72d94f83901958d/memmodel_default.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/336naming the default behavior influences proven obligations2021-04-15T09:29:03ZJochen Burghardtnaming the default behavior influences proven obligationsID0002309:
**This issue was created automatically from Mantis Issue 2309. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002309:
**This issue was created automatically from Mantis Issue 2309. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002309 | Frama-C | Plug-in > wp | public | 2017-06-01 | 2017-06-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 15-Phosphorus | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp ilog2_beh.c -wp-prop ilog2 -wp-prover alt-ergo -wp-prover cvc4" on the attached program proves everything except (the lemmas and) loop invariant "a".
However, when lines 16,27,30,36,41 are uncommented, i.e. the default behavior is assigned an explicit name, everything except (the lemmas and) the loop variant is proven instead.
Naming vs. not naming a behavior shouldn't have such an influence.
## Attachments
- [ilog2_beh.c](/uploads/61d5de2e4e4cfecc8959933e484a3108/ilog2_beh.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/350"loop assigns" clause ignored in presence of "for"-prefixed clauses2021-04-15T09:27:13ZJochen Burghardt"loop assigns" clause ignored in presence of "for"-prefixed clausesID0002298:
**This issue was created automatically from Mantis Issue 2298. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002298:
**This issue was created automatically from Mantis Issue 2298. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002298 | Frama-C | Plug-in > wp | public | 2017-05-08 | 2017-05-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu 16.04.1 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp beh.c" on the attached program fails to prove ensures clause "x01" and assertion "x10". When the two clauses prefixed by "for five" are removed from the loop invariant, everything is proven (except ensures clause "x02", which is about behavior "five").
Apparently, the two "for five" clauses (in fact, the first of them alone does) make Frama-c ignore the following "loop assigns x06" clause.
If the two "for five" clauses are moved below the "loop assigns x06" clause, an internal error is raised (output see "Additional information" below). For this reason, I set the Severity to "crash".
### Additional Information :
Frama-C's output for the internal error:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing beh.c (with preprocessing)
[wp] failure: At most one loop assigns can be associated to a behavior
[kernel] Current source was: beh.c:11
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml", line 568, characters 30-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 562, characters 9-16
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 565, characters 15-16
Called from file "src/plugins/wp/wpAnnot.ml", line 855, characters 14-43
Called from file "list.ml", line 84, characters 24-34
Called from file "hashtbl.ml", line 200, characters 23-35
Called from file "hashtbl.ml", line 204, characters 12-33
Called from file "src/kernel_services/ast_data/annotations.ml", line 499, characters 4-187
Called from file "src/plugins/wp/wpAnnot.ml", line 865, characters 4-46
Called from file "src/plugins/wp/wpAnnot.ml", line 1015, characters 36-62
Called from file "map.ml", line 168, characters 20-25
Called from file "map.ml", line 168, characters 10-18
Called from file "map.ml", line 168, characters 10-18
Called from file "src/plugins/wp/wpAnnot.ml", line 1023, characters 2-39
Called from file "src/plugins/wp/wpAnnot.ml", line 1094, characters 15-41
Called from file "src/plugins/wp/wpAnnot.ml", line 1273, characters 14-39
Called from file "src/plugins/wp/wpAnnot.ml", line 1274, characters 9-22
Called from file "src/plugins/wp/wpAnnot.ml", line 1363, characters 2-47
Called from file "map.ml", line 168, characters 20-25
Called from file "src/plugins/wp/Generator.ml", line 136, characters 4-39
Called from file "src/plugins/wp/register.ml", line 654, characters 15-40
Called from file "src/libraries/stdlib/extlib.ml", line 299, characters 14-17
Re-raised at file "src/libraries/stdlib/extlib.ml", line 299, characters 47-48
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "src/libraries/stdlib/extlib.ml", line 300, characters 2-12
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501-beta1.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
## Attachments
- [beh.c](/uploads/76212e7a4f3bee138c94f155a5d71946/beh.c)
- [beh2.c](/uploads/649046670c48074897a180a4e2785cc5/beh2.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/351Some ACSL mathematical functions crash WP2021-04-15T09:25:54Zmantis-gitlab-migrationSome ACSL mathematical functions crash WPID0002299:
**This issue was created automatically from Mantis Issue 2299. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002299:
**This issue was created automatically from Mantis Issue 2299. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002299 | Frama-C | Plug-in > wp | public | 2017-05-10 | 2017-05-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boyer | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | high | **Severity** | block | **Reproducibility** | always |
| **Platform** | VirtualBox (Host Win7) | **OS** | Ubuntu | **OS Version** | 16.04.2 |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Some of the mathematical functions enumerated in http://frama-c.com/download/acsl.pdf, p24 are not correctly supported by Frama-c. For instance, the keywords \pow, \cos and \sin are recognized at parsing and supported by EVA whereas an error is reported for WP (builtin functions are not defined) followed by an internal error.
### Additional Information :
Console message:
[kernel] Parsing .opam/4.04.0/share/frama-c/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing ex.c (with preprocessing)
[wp] Running WP plugin...
[wp] warning: Missing RTE guards
[wp] user error: Builtin \round_error(float32) not defined
[wp] failure: Logic '\round_error' undefined
==================================================================================
Crash report:
Current source was: :0
The full backtrace is:
Raised at file "hashtbl.ml", line 440, characters 17-32
Called from file "src/libraries/project/state_topological.ml", line 62, characters 23-38
Plug-in wp aborted: internal error.
Reverting to previous state.
[...]
### Steps To Reproduce :
Using Example 2.9, p25 from the ACSL manual:
/*@ requires \abs(\exact(x)) <= 0x1p-5;
@ requires \round_error(x) <= 0x1p-20;
@ ensures \abs(\exact(\result)-\cos(\exact(x))) <= 0x1p-24;
@ ensures \round_error(\result) <= \round_error(x) + 0x3p-24;
@*/
float cosine(float x) {
return 1.0f - x * x * 0.5f;
}
Then:
frama-c-gui -wp cosine.c
## Attachments
- [wp-bug.zip](/uploads/df0c5400fe8b77153075db0a5a303098/wp-bug.zip)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/352axiom about bounds of lsl result needed in the long run2021-04-15T09:23:47ZJochen Burghardtaxiom about bounds of lsl result needed in the long runID0002296:
**This issue was created automatically from Mantis Issue 2296. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002296:
**This issue was created automatically from Mantis Issue 2296. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002296 | Frama-C | Plug-in > wp | public | 2017-05-08 | 2017-05-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Phosphorus-20170501-beta1 | **OS** | xubuntu 16.04.1 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp and.c" on the attached program fails to prove the assertion in line 5, although it should follow immediately from the assignment in line 4.
Looking at the generated mlw file shows that "k=to_uint16(k)" can't be proven (variable name taken from c source). Apparently, the range boundaries of m from the contract in line 2 aren't propagated to m<<1.
In the long run, when bit operations will be handled in a satisfactory way, this issue should be resolved, too; the attached program can be used as a regeression test for it.
## Attachments
- [and.c](/uploads/5606c50a1cbb03c84ebc7bed8173b379/and.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/353Frama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis t...2021-04-15T09:23:06ZJochen BurghardtFrama-C gives succeeding lemma, rather than preceding lemmas, as hypothesis to e.g. Cvc4ID0002293:
**This issue was created automatically from Mantis Issue 2293. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002293:
**This issue was created automatically from Mantis Issue 2293. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002293 | Frama-C | Plug-in > wp | public | 2017-03-16 | 2017-03-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
I ran "frama-c -wp -wp-prover cvc4 -wp-prover alt-ergo -wp-prop bar gcd.c" and observed the input file "lemma_bar_Alt-Ergo.mlw" and "why_4e8b6a_Axiomatic-T-Q_bar.smt2" to Alt-ergo and Cvc4, respectively.
The former file contains as assumptions the lemmas "bar1" and "divisor1" (side remark: note the reversed order, compared to the Acsl source), which is ok.
However, the latter file contains as assumption just lemma "X", which imho is wrong.
In any case, the assumption sets given to Alt-ergo and Cvc4 should agree.
The problem might be a remainder of issue #2237, which is meanwhile closed.
## Attachments
- [gcd.c](/uploads/c50eb3ebd539d7224a0819fa7b628728/gcd.c)
- [lemma_bar_Alt-Ergo.mlw](/uploads/910b6b80e9ad2fdab9b8b30e5d212fbe/lemma_bar_Alt-Ergo.mlw)
- [why_4e8b6a_Axiomatic-T-Q_bar.smt2](/uploads/9612614ae617a11e9e3fd903e99f9020/why_4e8b6a_Axiomatic-T-Q_bar.smt2)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/354signature axiom omitted in Coq and Alt-ergo translation2021-04-15T09:22:17ZJochen Burghardtsignature axiom omitted in Coq and Alt-ergo translationID0002292:
**This issue was created automatically from Mantis Issue 2292. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002292:
**This issue was created automatically from Mantis Issue 2292. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002292 | Frama-C | Plug-in > wp | public | 2017-03-13 | 2017-03-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-prover cvc4 -wp-prover alt-ergo -wp-prover coq -wp-script wp0.script -wp-prop incAdd input_it.c" on the attached file generates an insufficient translation to Coq: There is a clause "Parameter L_add : S1__Iter -> Z -> S1__Iter." in file "lemma_incAdd_Coq.v", but no corresponding "Hypothesis Q_TL_add". Both clauses are needed to describe the signature of the Acsl logic function "add". The hypothesis "Q_TL_add" would be needed in the Coq proof (see out-commented lines in file "wp0.script"). For the Acsl function "inc", which is defined in a different "axiomatic" block, both signature description clauses (viz. "Parameter L_inc" and "Hypothesis Q_TL_inc") are contained in file "A_IterAxioms.v".
When considering the output to Alt-Ergo, viz. file "lemma_incAdd_Alt-Ergo.mlw", the same problem appears: there is a declaration "logic L_inc" in line 606, an "axiom Q_TL_inc" in line 610, a declaration "logic L_add" in line 632, but no corresponding "axiom Q_TL_add".
When considering the output to Why3, everything appears to be ok: in file "A_addAxioms.why", both "function l_add" and "axiom Q_TL_add" is found, and in file "A_IterAxioms.why", both "function l_inc" and "axiom Q_TL_inc" is found.
## Attachments
- [input_it.c](/uploads/88e27e089e806bc7a33ec394a5a03895/input_it.c)
- [wp0.script](/uploads/072ee52979588420d483d6c91cde6dae/wp0.script)
- [lemma_incAdd_Coq.v](/uploads/9e66d6cd32f3c22f20024c64a684ac91/lemma_incAdd_Coq.v)
- [A_IterAxioms.v](/uploads/28dcafa275d9a551a511ca58577daba7/A_IterAxioms.v)
- [lemma_incAdd_Alt-Ergo.mlw](/uploads/284bc586b8a9569b8bd931c022fe93d5/lemma_incAdd_Alt-Ergo.mlw)
- [A_addAxioms.why](/uploads/5604dca431021ff929e54115829f47aa/A_addAxioms.why)
- [A_IterAxioms.why](/uploads/74423afd66c8b9493003003934166c7b/A_IterAxioms.why)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/360suggestion: translate axioms and implication premises in forward order to coq2021-04-15T09:12:22ZJochen Burghardtsuggestion: translate axioms and implication premises in forward order to coqID0002291:
**This issue was created automatically from Mantis Issue 2291. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002291:
**This issue was created automatically from Mantis Issue 2291. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002291 | Frama-C | Plug-in > wp | public | 2017-03-13 | 2017-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Silicon-20161101 | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C 14-Silicon | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-prover coq -wp-out wp-out coqtest.c" on the attached file generates two Coq files, viz. "A_eqAxioms.v" and "lemma_goal_Coq.v".
The former contains the translation of "axiomatic eqAxioms", with the axioms ("eqRefl" and "eqTrns") appearing in the same order as in the source. The file "lemma_goal_Coq.v" contains the translation of "axiomatic incAxioms", however, with the axioms ("incLf" and "incRg") appearing in reverse order, compared to the source.
A similar issue concerns the translation of the body formula of axiom "eqTrns", where the first and second premise, viz. "eq(x,y)" and "eq(y,z)" in the source, appear in reverse order in the Coq translation.
(As a side remark: names of locally bound variables could be translated such that a target name closely resembles its source name; for example the source name could appear as a prefix of the target name.)
While probably easy to implement, these suggestions would considerably lower the overall complexity of the user's task.
## Attachments
- [coqtest.c](/uploads/74070de0221ca10812d16c76f7136c21/coqtest.c)
- [A_eqAxioms.v](/uploads/069306903f4c37b11f8f97b4a7df853c/A_eqAxioms.v)
- [lemma_goal_Coq.v](/uploads/231b70565ab0de2adf794e9662aae91e/lemma_goal_Coq.v)Loïc CorrensonLoïc Correnson