frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-04-16T06:46:54Zhttps://git.frama-c.com/pub/frama-c/-/issues/392option "-print" prints array upper bound in type before parameter name, rathe...2021-04-16T06:46:54ZJochen Burghardtoption "-print" prints array upper bound in type before parameter name, rather than after itID0002248:
**This issue was created automatically from Mantis Issue 2248. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002248:
**This issue was created automatically from Mantis Issue 2248. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002248 | Frama-C | Kernel | public | 2016-10-06 | 2016-12-08 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu | **OS Version** | - |
| **Product Version** | Frama-C Aluminium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -print ftest.c" on the attached program doesn't reproduce the input program; insteadt, it prints the "[a]" before the "b", not after it.
## Attachments
- [ftest.c](/uploads/d30107ddbd8fa94ff16f4958ab80029f/ftest.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/1023WP crash when type casting in lemma2021-04-15T15:42:55Zmantis-gitlab-migrationWP crash when type casting in lemmaID0001804:
**This issue was created automatically from Mantis Issue 1804. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001804:
**This issue was created automatically from Mantis Issue 1804. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001804 | Frama-C | Plug-in > wp | public | 2014-06-06 | 2014-06-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When using Typed+cast, a cast in a lemma can cause wp to crash.
In the below example, removing the lemma will cause the assert to validate.
### Steps To Reproduce :
Create file ptr_cast.c :
/*@
lemma valid_pointers:
\forall int **ptr; sizeof(int *) >= sizeof(int) ==> \valid(ptr) ==> \valid((int *) ptr);
*/
void f(int **ptr){
//@ assert sizeof(int *) >= sizeof(int) ==> \valid(ptr) ==> \valid((int *) ptr);
}
Run :
frama-c -cpp-command 'gcc -C -E' -pp-annot -wp -wp-model Typed+cast ptr_cast.c
Receive output :
[kernel] preprocessing with "gcc -C -E -dD ptr_cast.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
ptr_cast.c:4:[wp] warning: Cast with incompatible pointers types (source: int**) (target: sint32*)
[wp] failure: Context 'Warning' non-initialized.
[kernel] Current source was: ptr_cast.c:7
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/Warning.ml", line 117, characters 10-31
Called from file "src/wp/MemTyped.ml", line 799, characters 3-111
Called from file "src/wp/MemVar.ml", line 374, characters 23-51
Called from file "src/wp/Cvalues.ml", line 433, characters 30-42
Called from file "src/wp/LogicSemantics.ml", line 768, characters 12-27
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 358, characters 20-35
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 357, characters 28-51
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 357, characters 28-51
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/Lang.ml", line 869, characters 33-38
Re-raised at file "src/wp/Lang.ml", line 870, characters 40-43
Called from file "src/wp/LogicSemantics.ml", line 684, characters 11-54
Called from file "src/wp/LogicSemantics.ml", line 779, characters 12-37
Called from file "src/wp/Context.ml", line 31, characters 12-17
Re-raised at file "src/wp/Context.ml", line 34, characters 41-46
Called from file "src/wp/LogicCompiler.ml", line 326, characters 14-25
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/LogicCompiler.ml", line 401, characters 24-83
Called from file "src/wp/LogicCompiler.ml", line 673, characters 6-97
Called from file "src/wp/LogicCompiler.ml", line 690, characters 19-41
Called from file "src/wp/cfgWP.ml", line 1294, characters 31-42
Called from file "map.ml", line 169, characters 20-25
Called from file "src/wp/cfgWP.ml", line 1369, characters 14-54
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_guidelinesAllan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/1867Fatal error: exception Env.Error("C:\Frama-C\lib/pervasives.cmi")2021-04-15T15:18:02Zmantis-gitlab-migrationFatal error: exception Env.Error("C:\Frama-C\lib/pervasives.cmi")ID0001418:
**This issue was created automatically from Mantis Issue 1418. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001418:
**This issue was created automatically from Mantis Issue 1418. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001418 | Frama-C | Kernel > configure | public | 2013-05-09 | 2013-05-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | aogrcs | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
When I did as the INSTALL file said every time under Cygwin, the configure command always gave me this messag, why?
ThanksVirgile PrevostoVirgile Prevostohttps://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/43Frama-C 22 beta also runs on macOS 11.0.1 Beta ("Big Sur")2021-04-15T11:37:39ZJens GerlachFrama-C 22 beta also runs on macOS 11.0.1 Beta ("Big Sur")This might be of minor interest but Titanium beta also runs on the latest beta-version
of Apple's upcoming macOS 11.0 release.
I only checked WP.
RegardsThis might be of minor interest but Titanium beta also runs on the latest beta-version
of Apple's upcoming macOS 11.0 release.
I only checked WP.
Regardshttps://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/1496Lithum- Z3 shell aborts with error message2021-04-15T09:17:49ZVirgile PrevostoLithum- Z3 shell aborts with error messageID0000030:
**This issue was created automatically from Mantis Issue 30. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000030:
**This issue was created automatically from Mantis Issue 30. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000030 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
[bug #7241 from old bts, reported by Christoph Weber]
Hello,
while I was trying to proof a function I got an error message.
Unfortunatly, I dont have time to figure out a smaller example
But the error occured when I altered the clause:
======
ensures
(
(\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) &&
a[k1] < b[k1]) ||
(\forall integer k2; (0 <= k2 < length_a) ==>
length_a < length_b && a[k2] == b[k2])
) ==> \result == 1 ;
--------
into:
ensures
(
(\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) &&
a[k1] < b[k1]) ||
(\forall integer k2; (0 <= k2 < length_a) ==>
length_a < length_b && a[k2] == b[k2])
) ^^ \result == 0 ;
==========
Here the source-code:
/*@
requires 0 <= length_a;
requires 0 <= length_b;
requires \valid_range (a, 0, length_a-1);
requires \valid_range (b, 0, length_b-1);
assigns \nothing;
ensures \result == 1 || \result == 0;
ensures
(
(\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) &&
a[k1] < b[k1]) ||
(\forall integer k2; (0 <= k2 < length_a) ==>
length_a < length_b && a[k2] == b[k2])
) ^^ \result ==0 ;
*/
int lexicographical_compare_array (int* a, int length_a, int* b, int length_b)
{
int i = 0;
/*@
loop invariant 0 <= i <= length_a;
loop invariant 0 <= i <= length_b;
loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k];
*/
for ( ; i != length_a && i != length_b; ++i)
{
if (a[i] < b[i])
{
/*@
assert \exists integer k1; 0 <= k1 <= i && a[k1] < b[k1];
*/
return 1;
}
if (b[i] < a[i])
{
return 0;
}
}
//return i == length_a && i != length_b ? 1 : 0;
if (i == length_a && i != length_b)
{
/*@
assert
(
(\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) &&
a[k1] < b[k1]) ||
(\forall integer k2; (0 <= k2 < length_a) ==>
length_a < length_b && a[k2] == b[k2])
);
*/
return 1;
}
else
{
return 0;
}
}
Sorry for the complex function,
Cheers
Christophhttps://git.frama-c.com/pub/frama-c/-/issues/1629Lithium: behavior, complete disjoint does not work2021-04-15T09:17:49ZVirgile PrevostoLithium: behavior, complete disjoint does not workID0000026:
**This issue was created automatically from Mantis Issue 26. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000026:
**This issue was created automatically from Mantis Issue 26. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000026 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7080 in old bts]
Hello, I am using the latest Lithium,
if I am using the short notation for complete, disjoint beaviors, i get:
File "find_array.h", line 46, characters 24-25: syntax error while parsing annot
ation
If i list the behaviors manually,
i get:
Warning: [Jessie plugin] complete behaviors specification ignored
Warning: [Jessie plugin] disjoint behaviors specification ignored
Cheers
Christophhttps://git.frama-c.com/pub/frama-c/-/issues/2101Ordering of lemma in coq output of jessie2021-04-15T09:17:48ZVirgile PrevostoOrdering of lemma in coq output of jessieID0000024:
**This issue was created automatically from Mantis Issue 24. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000024:
**This issue was created automatically from Mantis Issue 24. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000024 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2011-10-28 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
(bug 5878 from old bts)
The file in attachment declares a predicate together with two axioms on it, and has a lemma which can be inferred from
the axioms. However, in the coq output, axioms and lemmas are sorted alphabetically, so that the lemma comes before
the axioms, making the proof impossible to complete. The relative ordering of axioms and lemmas in the C file should
be preserved.
## Attachments
- [logic.c](/uploads/fd6b15724dcfe623df3e05f0aa7d6c60/logic.c)https://git.frama-c.com/pub/frama-c/-/issues/2220Highlighted text in code part of the GUI does not take into account size of #...2021-04-15T09:17:48ZVirgile PrevostoHighlighted text in code part of the GUI does not take into account size of #defined symbolsID0000035:
**This issue was created automatically from Mantis Issue 35. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000035:
**This issue was created automatically from Mantis Issue 35. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000035 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2011-04-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | virgile | **Resolution** | not fixable |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hello,
With following code:
===
#define MAX 5
int c[5] = {0, };
int global = 0;
void main(void)
{
//@ assert global == 0;
//@ assert \forall integer i; 0 <= i < MAX ==> c[i] == 0;
return;
}
===
After launching Jessie GUI on it, if one selects assertion 2., the highlighted text in the lower right corner of the
GUI does not cover the " 0" characters.
The previous assertion (1.) is correclty highlighted.
I assume this is because the GUI rely on the size of the expression after preprocessor (CPP) pass while it highlights
source code as seen before preprocessor pass.
[bug 7496 from old bts, reported by David Mentré]
In above example, the expand #define "MAX" is "5", only 1 character wide compared to 3
of "MAX", corresponding to the 3-1=2 characters not highlighted.
I have observed similar behaviour on bigger code, when the highlight is not covering the correct expression at all.
Yours,
d.