frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:39:30Zhttps://git.frama-c.com/pub/frama-c/-/issues/611implicit conversion of terms to predicates2021-02-22T13:39:30ZDavid Cokimplicit conversion of terms to predicatesID0002148:
**This issue was created automatically from Mantis Issue 2148. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002148:
**This issue was created automatically from Mantis Issue 2148. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002148 | Frama-C | Kernel > ACSL implementation | public | 2015-07-17 | 2015-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
ACSL distinguishes carefully between terms and predicates. For example, a predicate (e.g. \valid(...) ) cannot be placed in a term position, such as the argument of a cast.
However, clauses such as 'requires 1;' are accepted by Frama-C, even though the 1.9 grammar nowhere permits terms to be implicitly converted to predicates. Integer-typed terms maybe implicitly converted to boolean terms, but there is no indication that terms are converted to predicates.
Is this an oversight in the grammar? or does Frama-C accept more than the grammar as a convenience?Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/609Control dependencies between labelled instructuctions and the corresponding ...2022-09-28T14:07:01Zmantis-gitlab-migrationControl dependencies between labelled instructuctions and the corresponding goto statementID0001992:
**This issue was created automatically from Mantis Issue 1992. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001992:
**This issue was created automatically from Mantis Issue 1992. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001992 | Frama-C | Plug-in > pdg | public | 2014-11-25 | 2015-08-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nguenaomer | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | X68 | **OS** | Linux | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Issue1: Does the pdg of frama-c include the transitive closure of standard control and data dependency relation?
Issue2: I think that there is an error in the PDG (or only the dot version).
The PDG of the function below states that the "while_0_break" statement control the "goto while_0_break" when using the -simplify-cfg option. To me, it should be the converse. The same with Neon.
Note that Issue1 and Issue2 are related.
### Steps To Reproduce :
I executed the following commamds with the C code below
$frama-c -pdg example2.c -main transfer_func -pdg-dot pdg2 -simplify-cfg
$dot -Tpng -o pdg2.transfer_func.png pdg2.transfer_func.dot
int x1,x2 ;
void transfer_func(int time) {
int prod =1 ;
int k =1 ;
while (k<=10) {
if (time/k > prod) break ;
prod *= k;
k++ ;
}
x1++;
x2++;
}
Enclosed is the pdg.
## Attachments
- ![pdg2.transfer_func](/uploads/89e7e73de0bccff6146ec1bca3678b43/pdg2.transfer_func.png)Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/608Slicing does not preserve some ACSL constructs2021-02-22T14:01:48ZJulien SignolesSlicing does not preserve some ACSL constructsID0000690:
**This issue was created automatically from Mantis Issue 690. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000690:
**This issue was created automatically from Mantis Issue 690. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000690 | Frama-C | Plug-in > slicing | public | 2011-01-26 | 2015-08-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | yakobowski | **Resolution** | not fixable |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The slicer does not keep ACSL annotations if it does not understand them. This behavior may prevent to prove properties of the sliced program.
### Steps To Reproduce :
Consider the following program:
==== a.c
int t[10];
void main(void) {
/*@ loop invariant 0 <= i <= 10;
@ loop invariant \forall integer k; 0 <= k < i ==> t[k] == 0;
@ */
for(int i = 0; i < 10; i++) t[i] = 0;
/*@ assert t[0] == 0; */
}
====
Run it with:
$ frama-c -slice-assert main -slice-print a.c
The printed program forget the second loop invariant. Thus, for instance, plug-in WP cannot prove the final assertion anymore.
/* Generated by Frama-C */
int t[10] ;
void main(void)
{
{ int i ; i = 0;
/*@ loop invariant (0 ? i) ? (i ? 10); */
while (i < 10) { t[i] = 0; i ++; }
}
/*@ assert (t[0] ? 0); */ ;
return;
}https://git.frama-c.com/pub/frama-c/-/issues/604suggest to warn about ensures clauses containing only \old variables2021-02-22T13:06:57ZJochen Burghardtsuggest to warn about ensures clauses containing only \old variablesID0001017:
**This issue was created automatically from Mantis Issue 1017. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001017:
**This issue was created automatically from Mantis Issue 1017. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001017 | Frama-C | Kernel > ACSL implementation | public | 2011-11-10 | 2015-08-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
A novice student wrote "ensures 0<=\old(n)<10;" when he actually meant "requires 0<=n<10;" in his solution to an Acsl exercise.
As this kind of error can be detected easily (ensures clauses should contain at least one identifier outside of \old), I suggest to add a warning in these cases.
See attached file for an own minimal example.
## Attachments
- [ftest.c](/uploads/843b644ab8a3c44a7e6e286c4b05969e/ftest.c)https://git.frama-c.com/pub/frama-c/-/issues/602With struct containing arrays, option -unspecified-access is too strict2021-04-28T09:34:03ZPascal CuoqWith struct containing arrays, option -unspecified-access is too strictID0002152:
**This issue was created automatically from Mantis Issue 2152. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002152:
**This issue was created automatically from Mantis Issue 2152. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002152 | Frama-C | Kernel | public | 2015-08-21 | 2015-08-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The program given below is correct, but:
$ frama-c -val t.c -unspecified-access
...
t.c:4:[kernel] warning: Unspecified sequence with side effect:
/* s.t[1] <- s.t */
s.t[1] = (char)0;
/* s.t[2] <- s.t */
s.t[2] = s.t[1];
[value] Analyzing a complete application starting at main
...
t.c:4:[kernel] warning: undefined multiple accesses in expression. assert \separated(&s.t[1], &s.t);
[value] Recording results for main
[value] done for function main
t.c:4:[value] Assertion 'Value,separation' got final status invalid.
...
I expected this program would be accepted without a warning about multiple accesses in expressions.
### Additional Information :
The struct is necessary for the bug to appear. With a toplevel array t, the assignment t[2] = t[1] = 0; does not cause a warning.
### Steps To Reproduce :
```c
struct s { char t[3]; } s;
int main() {
s.t[2] = s.t[1] = 0;
return 0;
}
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/601bound variable names in Coq file depend on unrelated function later in C sour...2021-04-15T06:45:00ZJochen Burghardtbound variable names in Coq file depend on unrelated function later in C source codeID0002153:
**This issue was created automatically from Mantis Issue 2153. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002153:
**This issue was created automatically from Mantis Issue 2153. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002153 | Frama-C | Plug-in > wp | public | 2015-08-31 | 2015-09-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -pp-annot -wp -wp-split -kernel-msg-key pp -wp-model Typed+ref -wp-driver ../BitTest.driver -cpp-command 'gcc -C -E' -wp-timeout 2 -wp-coq-timeout 5 -wp-prover cvc4 -wp-prover coq 0.c -wp-out 0.wp" on the attached file "0.c", and the corresponding command on "1.c", generate Coq proof obligation files "0.wp/typed_ref_BitTest/Bitstream_WriteThenRead_assert_left.coq" and "1.wp/typed_ref_BitTest/Bitstream_WriteThenRead_assert_left.coq" that differ in bound variable names.
However, "0.c" initially just includes "1.c" and the defines a function "Bitstream_ReadThenWrite" that is unrelated to the code in "1.c"; for this reason, it shouldn't influence the proof obligation of "Bitstream_WriteThenRead_assert_left". The influence apparently depends on the name of the trailing extra-function in "0.c": if it is named "Bitstream_XeadThenWrite", then the problem disappears. Frama-C handles functions in alphabetical order, as can be seen by its stdout messages.
## Attachments
- [0.c](/uploads/5e9c47840cfd6d001d24d36f3d401dfa/0.c)
- [1.c](/uploads/456c5e464671fb845a75362f43ec8bb3/1.c)
- [BitTest.driver](/uploads/fb98b62b3dcf8b0dad1d87be5184dfd7/BitTest.driver)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/599invalid statement contract ("assigns") verified with CVC4 under strange circu...2021-02-22T13:29:19ZJochen Burghardtinvalid statement contract ("assigns") verified with CVC4 under strange circumstancesID0002110:
**This issue was created automatically from Mantis Issue 2110. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002110:
**This issue was created automatically from Mantis Issue 2110. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002110 | Frama-Clang | Plug-in > wp | public | 2015-04-30 | 2015-09-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp-prover cvc4 -wp 473.c" on the attached file (referred to as version "(0)" in the modification discussion below) results in verifying all proof obligations, including the statement contract in line 27, which is obviously false, since "myRead" also assigns "fd->pos" (line 13) and definitely changes it (line 15). I can't see a contradiction from which line 27 could be proven.
CVC4 still proves all obligations if one of the following changes is made:
(+1) myRead's "assigns" clauses in line 13 and 14 are joined into a single one, viz. "assigns fd->pos,*a;"
(+2) all "requires" clauses in line 10-12 and 20-22 are commented-in simultaneously
CVC4 fails to prove the statement contract in line 27 if one of the following changes is made:
(-1) myRead's "assigns" clauses in line 13 and 14 are swapped,
(-2) myRead's "assigns" clauses in line 13 and 14 are joined into a single "assigns *a,fd->pos;"
(-3) the "ensures" clauses in line 15 is deleted
(-4) the "ensures" clauses in line 23 (i.e. the whole contract) is deleted
(-5) the type of "a" is changed from "struct A*" to "int*" in line 17 and 25
From (+1) vs. (-2), as well as from (0) vs. (-1), it seems that the order of the memory location specifiers in myRead's "assigns" clause does matter.
In (0) vs. (-4), the "ensures" clause of "myMain" apparently influences its body code.
## Attachments
- [473.c](/uploads/11dc1d524233fc5202f6d678f181dca2/473.c)
- [wp-out.tar.gz](/uploads/ab1dd06676ca947a179dfe9d25490319/wp-out.tar.gz)
- [myMain_0b.why](/uploads/7dbe248cc0d0ba6fe57db28b2ffe6d19/myMain_0b.why)
- [myMain_0b1.smt2](/uploads/d3a0414d7a30295360902d885a8b6107/myMain_0b1.smt2)
- [myMain_0b2.smt2](/uploads/0835c74f12ab3e7a82f4a7d6ad984ac0/myMain_0b2.smt2)
- [myMain_0.smt2](/uploads/22b46ceffb1f126b776507e741a9134c/myMain_0.smt2)
- [myMain_-4.smt2](/uploads/7c12b3f5df33a42109d0215a16cc65c9/myMain_-4.smt2)
- [myMain_0.why](/uploads/e153c4b48d2e88354dae40eea92a4613/myMain_0.why)
- [myMain_-4.why](/uploads/45ab78b845a9d3f96afb1065a32e9184/myMain_-4.why)https://git.frama-c.com/pub/frama-c/-/issues/598Slow in proof obligation generation2021-04-15T08:41:46Zmantis-gitlab-migrationSlow in proof obligation generationID0002156:
**This issue was created automatically from Mantis Issue 2156. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002156:
**This issue was created automatically from Mantis Issue 2156. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002156 | Frama-C | Plug-in > wp | public | 2015-09-03 | 2015-09-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | juki21c | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Both Ubuntu and OS X | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I experienced that Frama-C/WP was very slow in generating the proof obligations only (skipping invoking any provers). For the attached files, code6.c takes about 1 min. code10.c takes about 15 min. code12.c abnormally terminates Frama-C with a stack overflow error.
### Steps To Reproduce :
> frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code6.c
> frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code10.c
> frama-c -wp -wp-prover why3ide -pp-annot -wp-gen -wp-out out code12.c
## Attachments
- [code.zip](/uploads/f899faa93ff0631830e910686ea4ef7d/code.zip)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/597typo in grammar2021-02-22T13:06:42ZDavid Coktypo in grammarID0001784:
**This issue was created automatically from Mantis Issue 1784. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001784:
**This issue was created automatically from Mantis Issue 1784. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001784 | Frama-C | Documentation > ACSL | public | 2014-05-25 | 2015-09-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | DavidCok | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C Sodium |
### Description :
The ACSL Neon documentation, in Fig 2.12, uses 'lemma-def' but defines 'lemma-decl'.
Presumably these should both be 'lemma-def'https://git.frama-c.com/pub/frama-c/-/issues/595assertion failure using memset on a char2021-04-15T08:43:01Zmantis-gitlab-migrationassertion failure using memset on a charID0002160:
**This issue was created automatically from Mantis Issue 2160. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002160:
**This issue was created automatically from Mantis Issue 2160. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002160 | Frama-C | Plug-in > wp | public | 2015-09-14 | 2015-09-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
When trying to analyse the this:
#include <string.h>
int main()
{
char a;
memset(&a, 0, 1);
}
Using wp I get:
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: No definition for 'memchr' interpreted as reads nothing
[wp] warning: No definition for 'strlen' interpreted as reads nothing
[wp] warning: No definition for 'memset' interpreted as reads nothing
[wp] warning: No definition for 'strchr' interpreted as reads nothing
[wp] warning: No definition for 'strcmp' interpreted as reads nothing
[wp] warning: No definition for 'strncmp' interpreted as reads nothing
[wp] warning: No definition for 'wcscmp' interpreted as reads nothing
[wp] warning: No definition for 'wcslen' interpreted as reads nothing
[wp] warning: No definition for 'wcsncmp' interpreted as reads nothing
[wp] warning: Missing RTE guards
[kernel] Current source was: test.c:6
The full backtrace is:
Raised at file "src/wp/MemVar.ml", line 474, characters 54-66
Called from file "src/wp/MemVar.ml", line 519, characters 16-38
Called from file "src/wp/MemVar.ml", line 543, characters 9-38
Called from file "list.ml", line 55, characters 20-23
Called from file "src/wp/Lang.ml", line 735, characters 25-40
Called from file "src/wp/Warning.ml", line 139, characters 6-10
Called from file "src/wp/LogicSemantics.ml", line 813, characters 12-42
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 "list.ml", line 55, characters 20-23
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/cfgWP.ml", line 1087, characters 18-60
Called from file "src/wp/Warning.ml", line 155, characters 14-18
Called from file "src/wp/cfgWP.ml", line 1118, characters 23-207
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 448, characters 14-224
Called from file "src/wp/calculus.ml", line 595, characters 10-57
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 724, 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 "src/wp/calculus.ml", line 724, characters 4-64
Called from file "src/wp/calculus.ml", line 770, characters 19-51
Called from file "src/wp/cfgWP.ml", line 1402, characters 39-62
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/lib/bag.ml", line 96, characters 16-24
Called from file "src/wp/cfgWP.ml", line 1391, 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 15-40
Called from file "src/wp/register.ml", line 574, characters 17-24
Re-raised at file "src/wp/register.ml", line 578, characters 27-29
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-raised at file "src/wp/register.ml", line 579, characters 30-32
Called from file "src/wp/register.ml", line 575, characters 17-24
Re-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 (File "src/wp/MemVar.ml", line 474, characters 54-60: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
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_guidelinesLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/594Relocable buckx2022-08-09T08:54:52Zmantis-gitlab-migrationRelocable buckxID0002165:
**This issue was created automatically from Mantis Issue 2165. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002165:
**This issue was created automatically from Mantis Issue 2165. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002165 | Frama-C | Kernel > Makefile | public | 2015-09-16 | 2015-09-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ploc | **Assigned To** | signoles | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Please add, as a default option, the relocation for buckx_c files:
GEN_BUCKX_CFLAGS="-fPIC"https://git.frama-c.com/pub/frama-c/-/issues/593suggest command-line option to avoid sophisticated expression transformations...2021-04-15T08:43:45ZJochen Burghardtsuggest command-line option to avoid sophisticated expression transformations, in particular for Coq obligationsID0002168:
**This issue was created automatically from Mantis Issue 2168. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002168:
**This issue was created automatically from Mantis Issue 2168. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002168 | Frama-C | Plug-in > wp | public | 2015-09-21 | 2015-09-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp 482b.c" on the attached file, the assertion "zzz" can't be proven by Alt-Ergo, although it should be an immediate consequence of assertion "yyy" and axiom "xxx". Looking at the file "bar_assert_zzz_Alt-Ergo.mlw" shows that some sophisticated expression transformations have been applied to the goal, but not to the axiom:
763 axiom Q_xxx:
764 forall lg_0,pos_0 : int.
765 (forall i : int. (pos_0 <= i) -> (i < (lg_0 + pos_0)) -> P_Tst(i)) ->
766 P_Prp(1 - lg_0)
772 goal bar_assert_zzz:
787 (forall i_1 : int. (i_1 < i) -> (x <= i_1) -> P_Tst(i_1)) ->
788 P_Prp(1 + x - i)
It is not a problem of Frama-C/Wp, but a problem of Alt-Ergo: it just should apply the lemma "xxx" with instantiation { pos_0:=x, lg_0 := i-x } to obtain line 788 from line 787.
However, when trying to prove the "zzz" assertion manually using Coq, Wp's transformation causes additional confusion. It would be desirable if the was a command-line switch to generate proof obligations as close to the source code as possible, i.e. to avoid the transformation.
As a side note, if the "assert" in line 20 is replaced by the statement-contract "ensures" in line 18, the transformation disappears, the goal is fairly good readable, and Alt-Ergo find the proof.
## Attachments
- [482b.c](/uploads/2c17baa4edc565f1b208267d133e0f42/482b.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/592incomplete Alt-Ergo obligation files generated in presence of lemma "forall i...2021-04-15T08:44:57ZJochen Burghardtincomplete Alt-Ergo obligation files generated in presence of lemma "forall int x; ..." with "x" not occurring in "..."ID0002169:
**This issue was created automatically from Mantis Issue 2169. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002169:
**This issue was created automatically from Mantis Issue 2169. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002169 | Frama-C | Plug-in > wp | public | 2015-09-21 | 2015-09-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp 483.c -wp-out wp-out" on the attached file generates an Alt-Ergo obligation file "foo_assert_Alt-Ergo.mlw" which contains neither the lemma "xxx" nor the proof goal for the assertion in line 5. Apparently, Frama-C/Wp tacitly crashes during translating the lemma.
The problem disappears ifin line 2 "int" is changed to "integer", or "\false" is changed to some formula containing "x".
## Attachments
- [483.c](/uploads/b7743ec7ca8f15e3df9b2238386f8533/483.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/591set of set2021-02-22T13:06:36ZPatrick Baudinset of setID0000575:
**This issue was created automatically from Mantis Issue 575. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000575:
**This issue was created automatically from Mantis Issue 575. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000575 | Frama-C | Kernel > ACSL implementation | public | 2010-08-25 | 2015-09-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
For exemple, there is not way to build the set containing the empty set without using comprehension set construct.
The proposition is to extend the actual ACSL grammar in order to allow "{" term "}" as set expression.https://git.frama-c.com/pub/frama-c/-/issues/590ACSL typing fails when performing unification of type variables2021-03-29T18:04:28ZPatrick BaudinACSL typing fails when performing unification of type variablesID0002170:
**This issue was created automatically from Mantis Issue 2170. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002170:
**This issue was created automatically from Mantis Issue 2170. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002170 | Frama-C | Kernel > ACSL implementation | public | 2015-09-24 | 2015-09-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-C fails while typing the given ACSL axiomatic.
### Additional Information :
Typing is succesful when axiom "a" is replaced by:
@ axiom a: P(aList,Nil);
### Steps To Reproduce :
```
> cat list.i
//@ type List<A> = Nil | Cons(A,List<A>);
/*@ axiomatic L {
@ predicate P<B>(List<B> l1, List<B> l2);
@ logic List<integer> aList{L} ;
@ axiom a: P(Nil, aList);
@ }
@*/
> frama-c list.i
...
../tests/list.i:8:[kernel] user error: invalid implicit conversion from ℤ to A#4
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/588mixed virtual/nonvirtual base class causes error2021-02-22T13:39:25ZJochen Burghardtmixed virtual/nonvirtual base class causes errorID0002077:
**This issue was created automatically from Mantis Issue 2077. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002077:
**This issue was created automatically from Mantis Issue 2077. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002077 | Frama-Clang | Plug-in > clang | public | 2015-02-09 | 2015-10-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | fvedrine | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 462.cpp (external front-end)
Now output intermediate result
462.cpp:5:[kernel] failure: Cannot resolve variable __frama_c_arg_0
[kernel] user error: stopping on file "462.cpp" that has errors.
If "virtual" is deleted in line 4, the error disappears; similarly if "virtual" is inserted in line 3.
Since in Stroustrup's book no mixed virtual/nonvirtual base class is discussed, the example in file "462.cpp" may not be of any relevance. However, the clang++ compiler accepts that file without any problems.
## Attachments
- [462.cpp](/uploads/6c5857ed398e1a937d5fade5314a5a1e/462.cpp)Franck VedrineFranck Vedrinehttps://git.frama-c.com/pub/frama-c/-/issues/584Unable to prove things that are provable, gets confused2021-04-15T08:45:52Zmantis-gitlab-migrationUnable to prove things that are provable, gets confusedID0002179:
**This issue was created automatically from Mantis Issue 2179. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002179:
**This issue was created automatically from Mantis Issue 2179. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002179 | Frama-C | Plug-in > wp | public | 2015-10-18 | 2015-10-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
In the attached file as is using wp -wp-model Typed,cast test-final.c, the last assert can't be proven, resulting in the ensures and assigns to be valid under hypotheses. This is a minimal version that still shows the problem.
However, there are several ways to make it be able to prove it and as far as I can see should have no effect on it. The different ways are:
- Removing any of the following 3 lines:
p[n] = 0x80; /* there is always room for one */
HASH_BLOCK_DATA_ORDER(c, p, 1);
c->num = 0;
- Removing the first assert
- Removing the requires \valid_read(c->data+(0 .. c->num-1));
I assume it gets confused because the \valid_read() overlaps with the \valid(c). It's not really needed. (In the full version the \valid_read() should more be something like \initialized.)
## Attachments
- [test-final.c](/uploads/d2b5913be633bcbecc3fbfb5a5fd886c/test-final.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/582Plug-in wp aborted: internal error, Raised at file "src/wp/register.ml", line...2021-04-14T15:32:57Zmantis-gitlab-migrationPlug-in wp aborted: internal error, Raised at file "src/wp/register.ml", line 579ID0002182:
**This issue was created automatically from Mantis Issue 2182. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002182:
**This issue was created automatically from Mantis Issue 2182. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002182 | Frama-C | Plug-in > wp | public | 2015-10-27 | 2015-10-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lorenz | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following (minimized) example file crashes the wp plugin of frama-c:
#> frama-c -wp min3.c
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing min3.c (with preprocessing)
/tmp/ppannotc0c3e2.c:1:0: warning: "__STDC_VERSION__" redefined
#define __STDC_VERSION__ 201112L
^
<built-in>: note: this is the location of the previous definition
/tmp/ppannotc0c3e2.c:2:0: warning: "__STDC_UTF_16__" redefined
#define __STDC_UTF_16__ 1
^
<built-in>: note: this is the location of the previous definition
/tmp/ppannotc0c3e2.c:3:0: warning: "__STDC_UTF_32__" redefined
#define __STDC_UTF_32__ 1
^
<built-in>: note: this is the location of the previous definition
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] failure: *** Label Label 'L' not-found
[kernel] Current source was: min3.c:16
The full backtrace 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
Plug-in wp aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Sodium-20150201.
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
#>
### Steps To Reproduce :
frama-c -wp min3.c
## Attachments
- [min3.c](/uploads/31cca83763f8d99e4ce71ae17158d08f/min3.c)Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/581Nested VLA are not supported2022-09-28T14:37:05ZPascal CuoqNested VLA are not supportedID0001718:
**This issue was created automatically from Mantis Issue 1718. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001718:
**This issue was created automatically from Mantis Issue 1718. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001718 | Frama-C | Kernel | public | 2014-03-25 | 2015-11-04 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Note that I have never seen this feature actually used, but it appears to be supported by GCC and Clang.
To reiterate, I have never seen code that does int t[a][a];
This report is only for the sake of completeness.
### Steps To Reproduce :
```
~/gitlab/frama-c $ bin/toplevel.opt -print t.c
[kernel] warning: cannot load plug-in `Aorai' (incompatible with Neon-20140301+dev).
[kernel] warning: cannot load plug-in `Obfuscator' (incompatible with Neon-20140301+dev).
[kernel] warning: cannot load plug-in `Report' (incompatible with Neon-20140301+dev).
[kernel] warning: cannot load plug-in `Security_slicing' (incompatible with Neon-20140301+dev).
[kernel] warning: cannot load plug-in `Wp' (incompatible with Neon-20140301+dev).
[kernel] preprocessing with "gcc -C -E -I. t.c"
t.c:4:[kernel] user error: Length of array is not a constant: a
t.c:4:[kernel] warning: Variable-sized local variable t
[kernel] user error: skipping file "t.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
~/gitlab/frama-c $ cat t.c
int main(int c, char **v)
{
int a = 3;
int t[a][a];
t[a-1][a-1] = 1;
}
~/gitlab/frama-c $ gcc -pedantic -std=c99 t.c
~/gitlab/frama-c $
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/579bit_test axiomatization doesn't imply == equality from bit-by-bit equality fo...2021-04-15T06:57:41ZJochen Burghardtbit_test axiomatization doesn't imply == equality from bit-by-bit equality for e.g. uint32ID0002188:
**This issue was created automatically from Mantis Issue 2188. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002188:
**This issue was created automatically from Mantis Issue 2188. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002188 | Frama-C | Plug-in > wp | public | 2015-11-30 | 2015-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
I ran "frama-c -wp -wp-out wp-out -wp-model Typed+ref -wp-driver jb.drv 484.c" on the attached program (and the attached driver file), and alt-ergo couldn't prove the lemma in line 10-15.
Looking at the background theory in (also attached) file "lemma_l_Alt-Ergo.mlw", it seems that in fact it doesn't imply the goal: axioms about "bit_test" occur only in lines 600 to 819; the only axioms that speak about something different from bit_test in their conclusion are (with line numbers):
604 axiom bit_test_def1 : relates to bit_testb, which isn't used further
612 axiom bit_test_extraction1 : relates to land(lsl(1,...))
622 axiom bit_test_extraction_bis_eq : implies only LSB=1
701 axiom lsl1_extraction : implies equality of bit position, not of values
757 axiom to_sint8_extraction_sup : implies negativity, not equality
773 axiom to_sint16_extraction_sup : similar
789 axiom to_sint32_extraction_sup : similar
805 axiom to_sint64_extraction_sup : similar
Axioms about lsl appear only in lines 608 to 1019; axioms speaking about something different from "lsl" and "bit_test" in their conclusion are:
616 axiom lsl_1_0 : (lsl(1, 0) = 1)
672 axiom land_1_lsl_1 : is about <, not about =
833 axiom is_uint8_lsl1_inf : about lsl(1,...) fitting into a uint8
837 axiom is_uint8_lsl1_sup : about lsl(1,...) not fitting into a uint8
853 axiom is_uint16_lsl1_inf : similar
857 axiom is_uint16_lsl1_sup : similar
873 axiom is_uint32_lsl1_inf : similar
877 axiom is_uint32_lsl1_sup : similar
893 axiom is_uint64_lsl1_inf : similar
897 axiom is_uint64_lsl1_sup : similar
921 axiom is_sint8_lsl1 : (lsl(1, 7) = 128)
923 axiom is_sint8_lsl1_inf : about lsl(1,...) fitting into an sint8
927 axiom is_sint8_lsl1_sup : about lsl(1,...) not fitting into an sint8
951 axiom is_sint16_lsl1 : (lsl(1, 15) = 32768)
953 axiom is_sint16_lsl1_inf : similar
957 axiom is_sint16_lsl1_sup : similar
981 axiom is_sint32_lsl1 : (lsl(1, 31) = 2147483648)
983 axiom is_sint32_lsl1_inf : similar
987 axiom is_sint32_lsl1_sup : similar
1011 axiom is_sint64_lsl1 : (lsl(1, 63) = 9223372036854775808)
1013 axiom is_sint64_lsl1_inf : similar
1017 axiom is_sint64_lsl1_sup : similar
Alltogether, I think there is no way to infer some equality relation from the agreement of bit_test (or land(lsl(...))) results.
I'm not sure whether I used the driver-file mechanism in an appropriate way; this might be the cause for my problem.
## Attachments
- [484.c](/uploads/a8645270645bbbcae0fa2802bc761c15/484.c)
- [jb.drv](/uploads/e5776c86ccbf4fec7dd49143e9b4625d/jb.drv)
- [lemma_l_Alt-Ergo.mlw](/uploads/869a0eda0b87de7cf6a05c199a23f624/lemma_l_Alt-Ergo.mlw)Loïc CorrensonLoïc Correnson