frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-12-14T12:36:37Zhttps://git.frama-c.com/pub/frama-c/-/issues/2636[WP] Builtin \sign(float64) is not defined2022-12-14T12:36:37ZNiksonber[WP] Builtin \sign(float64) is not defined<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Description
Built-in \\sign is not defined in WP.
`Builtin \sign(float64) not defined`
`[wp] Failure: Logic type 'sign' undefined`
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Steps To Reproduce
Run: `frama-c -wp -wp-out . -wp-prover coq -wp-model +float -wp-interactive update just_sign.c`
Where `just_sign.c` is:
```
#include <math.h>
/*@
predicate is_same_sign(double X, double Y) = \sign(X) == \sign(Y);
*/
/*@
ensures (is_same_sign(a_double, \result)) ;
assigns \nothing;
*/
double dummy (double a_double) {
return a_double;
}
```
I got the following output:
```
[wp] Warning: Missing RTE guards
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
[wp] 2 goals scheduled
[wp] Failure: Logic type 'sign' undefined
```
### Expected behaviour
Expected a definition for \sign.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
WP reports:
```
[wp] Failure: Logic type 'sign' undefined
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
```
<!--
Please explain here what is the actual (faulty) behaviour.
-->
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0, 25.0 (Manganese), 26.0+dev (Iron) (I tried Several versions)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 22.04 LTS
<!--
### Additional information (optional)
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2601[WP] [RTE] Unable to verify valid memory access in array using bitwise-ANDed ...2022-05-30T12:20:54ZCostava[WP] [RTE] Unable to verify valid memory access in array using bitwise-ANDed index when array is function parameter<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
With Alt-Ergo 2.4.1 installed:
`frama-c -wp -wp-rte poc.c` / `frama-c-gui -wp -wp-rte poc.c`
using [poc.c](/uploads/62e84944634b546da975b2397c7c4e4d/poc.c) :
```c
/*@
requires \valid_read(arr + (0 .. 3));
assigns \nothing;
*/
int foo(const int arr[const static 4]) {
const unsigned int h = 7 & 0b11;
//@ assert 0 <= h < 4;
const int hvalue = arr[h];
const unsigned int i = 7 % 4;
//@ assert 0 <= i < 4;
const int ivalue = arr[i];
/*@
loop invariant 0 <= s <= 8;
loop assigns s;
loop variant 8 - s;
*/
for (unsigned int s = 0; s < 8; s += 1) {
const unsigned int j = s & 0b11;
//@ assert 0 <= j < 4;
const int jvalue = arr[j];
const unsigned int k = s % 4;
//@ assert 0 <= k < 4;
const int kvalue = arr[k];
}
return 0;
}
/*@
assigns \nothing;
*/
int main(void) {
const int arr[4] = {0, 1, 2, 3};
const unsigned int h = 7 & 0b11;
//@ assert 0 <= h < 4;
const int hvalue = arr[h];
const unsigned int i = 7 % 4;
//@ assert 0 <= i < 4;
const int ivalue = arr[i];
/*@
loop invariant 0 <= s <= 8;
loop assigns s;
loop variant 8 - s;
*/
for (unsigned int s = 0; s < 8; s += 1) {
const unsigned int j = s & 0b11;
//@ assert 0 <= j < 4;
const int jvalue = arr[j];
const unsigned int k = s % 4;
//@ assert 0 <= k < 4;
const int kvalue = arr[k];
}
foo(arr);
return 0;
}
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
All goals proved.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
```sh
$ frama-c -wp -wp-rte poc.c
[kernel] Parsing poc.c (with preprocessing)
[rte] annotating function foo
[rte] annotating function main
[wp] 34 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_foo_assert_rte_mem_access_3 : Timeout (Qed:9ms) (10s)
[wp] Proved goals: 33 / 34
Qed: 23 (2ms-5ms-14ms)
Alt-Ergo 2.4.1: 10 (7ms-17ms-30ms) (556) (interrupted: 1)
```
33/34 goals proved.
The verification of `/*@ assert rte: mem_access: \valid_read(arr + j); */` for code `const int jvalue = arr[j];` in function `foo` is not successful.
From a naive perspective, the `arr[j]` accesses in main and foo are equivalent, so the assert in foo should be verifiable if the assert in main is.
(I am aware that a different assert is generated in main: `/*@ assert rte: index_bound: j < 4; */`)
Also, the `//@ assert 0 <= j < 4;` immediately before the access can be verified, both in main and foo, so it seems the rte assert should be able to be verified also.
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: WP, RTE
- OS name: Manjaro Linux
- OS version: Qonos 21.2.4
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
The poc.c is a simplified proof of concept, but I did hit this situation when working on a real program.
To be explicit about the provers involved:
```sh
$ why3 config detect
Found prover Alt-Ergo version 2.4.1, OK.
1 prover(s) added
Save config to /home/user/.why3.conf
```
I was uncertain whether to submit this here or at the [alt-ergo issues](https://github.com/OCamlPro/alt-ergo/issues).
Apologies if this is the wrong place. Let me know if I should post there instead.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2534Default invariant should be inferred for loops2021-04-15T09:17:45ZVirgile PrevostoDefault invariant should be inferred for loopsID0000042:
**This issue was created automatically from Mantis Issue 42. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000042:
**This issue was created automatically from Mantis Issue 42. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000042 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-06-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7561 from old bts, reported by Boris Hollas]
For loops that loop on a variable i that is not decreased inside the loop a default loop invariant should be inferred.
For example, in
for(i=0; i<n; i++) {
a[i] = 0;
}
the loop invariant
//@ loop invariant 0 <= i;
should be inferred by default.
A similar loop invariant should be inferred for decreasing loops.Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2487Slicing leaves unreachable code2021-02-22T13:59:57Zmantis-gitlab-migrationSlicing leaves unreachable codeID0000194:
**This issue was created automatically from Mantis Issue 194. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000194:
**This issue was created automatically from Mantis Issue 194. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000194 | Frama-C | Plug-in > slicing | public | 2009-07-15 | 2009-08-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | Anne | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
/*@ requires
@ (((v1 && !(v2 && v3) && v4);
@*/
extern void fun(void)
{
if (v1) {
if (v4) {
if (v2) {
if(v3) {goto return_label;}
}
}
}
}
### Additional Information :
It would be nice if slicing could remove such code.https://git.frama-c.com/pub/frama-c/-/issues/2443Option -jessie-cpu-limit not taken into account in GUI2021-04-15T09:17:48ZVirgile PrevostoOption -jessie-cpu-limit not taken into account in GUIID0000034:
**This issue was created automatically from Mantis Issue 34. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000034:
**This issue was created automatically from Mantis Issue 34. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000034 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7495 from old bts, reported by David Mentré]
Hello,
When calling Frama-C/Jessie with "-jessie-cpu-limit 2 -jessie-gui", the Timeout value in the GUI is not set
to 2 but to the default 10.
To reproduce the issue:
cat minimal.c
void main(void)
{
return;
}
frama-c -jessie-analysis -jessie-atp alt-ergo -jessie-cpu-limit 2 -jessie-gui minimal.c
Yours,
davidhttps://git.frama-c.com/pub/frama-c/-/issues/2421different translation of casted constants in program-code and in assertion2021-04-15T09:17:22ZJochen Burghardtdifferent translation of casted constants in program-code and in assertionID0000433:
**This issue was created automatically from Mantis Issue 433. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000433:
**This issue was created automatically from Mantis Issue 433. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000433 | Frama-C | Plug-in > jessie | public | 2010-03-22 | 2010-03-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the attached file, "my_const" is translated to "1024" in line 8 (C-code),
but to "integer_of_int32(int32_of_integer(1024))" in line 9 (Acsl-code).
As a consequence, Simplify is unable to prove the trivial-looking assertion in line 9 (it seems to lack a rule like
"integer_of_int32(int32_of_integer(x)) <== -maxInt <= x <= +maxInt").
When I remove the cast in line 4, jessie outputs no proof obligation at all, which is (consistent with) what I expected.
## Attachments
- [ftest.c](/uploads/39e21d3026f822775c835db0ba674a74/ftest.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2419-2147483647<=0 unprovable by Simplify, except in switch2021-04-15T09:17:24ZJochen Burghardt-2147483647<=0 unprovable by Simplify, except in switchID0000415:
**This issue was created automatically from Mantis Issue 415. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000415:
**This issue was created automatically from Mantis Issue 415. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000415 | Frama-C | Plug-in > jessie | public | 2010-02-22 | 2010-03-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Simplify can prove neither -2147483648<=0 nor -2147483647<=0, see ftest8() and ftest7() in the attached file. However, it proves -2147483646<=0, see ftest6().
I suggest a jessie cmd-line option to generate -2147483646 rather than -2147483648 as MinInt, in order to circumvent this bug of Simplify, which causes many unprovable no-underflow-obligations in my programs.
Moreover, as a case of a switch, Simplify behaves different on -2147483647<=0: it can prove it there, see case 7 in ftest(). Probably, this is again a problem of Simplify. To ensure this, you could check that the proof obligations you generate are correct.
## Attachments
- [minInt01.c](/uploads/edf84b4457f0e4a42ec5f6bf1a2629ef/minInt01.c)https://git.frama-c.com/pub/frama-c/-/issues/2390assigns clauses are missing from the sliced program2021-02-22T13:58:02ZPascal Cuoqassigns clauses are missing from the sliced programID0000393:
**This issue was created automatically from Mantis Issue 393. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000393:
**This issue was created automatically from Mantis Issue 393. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000393 | Frama-C | Plug-in > slicing | public | 2010-02-04 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
When the original program contains assigns clauses for functions with code,
the assigns are always omitted from the generated sliced program.
On the other hand pre- and post-conditions seem to be properly included.
In the attached example, the command produces a sliced program that contains:
/*@ requires \valid(p);
behavior default:
ensures (p->a > p->b);
*/
void g_slice_1(las *p )
{
...
The expected behavior is for g_slice_1 to contain in its contract the clause:
assigns p->a;
in addition to the requires and ensures.
### Additional Information :
frama-c -slicing-level 3 -slicing-keep-annotations -slice-assert main -slice-print -ocode slice.foo.c -main main -lib-entry -no-unicode -context-valid-pointers foo.c
# pragma JessieIntegerModel(exact)
typedef struct las { int a; int b; } las;
/*@ requires \valid(p); assigns p->a; ensures p->a>p->b; */
void f(las * p){ p->a = p->b + 1;}
/*@ requires \valid(p); assigns p->a; ensures p->a>p->b; */
void g(las * p) { f(p); }
/*@ requires \valid(p); assigns p->a; ensures p->a>p->b; */
void main(las * p) { g(p);
//@ assert p->a>p->b;
}https://git.frama-c.com/pub/frama-c/-/issues/2387imprecision in widening/narrowing for char and short index2021-02-22T14:04:43ZStephane Dupratimprecision in widening/narrowing for char and short indexID0000414:
**This issue was created automatically from Mantis Issue 414. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000414:
**This issue was created automatically from Mantis Issue 414. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000414 | Frama-C | Plug-in > Eva | public | 2010-02-19 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sduprat | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Hello Stéphane,
> Depending the type of i, the range is not the same.
> The range of i in the loop is [0..10] (for int) or [0..15] for char or
> short.
_____
void main(void)
{
char i=0;
int j=0;
while (i<10) i++;
while (j<10) j++;
}
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
i IN {10; 11; 12; 13; 14; 15; }
j IN {10; }
_____
It's interesting that you noticed this behavior,
because I fixed a comparable problem on short
notice this summer for an intern who had to demo
his plug-in the following week.
Note that the AST for the two loops is different:
i = (char)0;
j = 0;
while ((int )i < 10) {i = (char )((int )i + 1);}
while (j < 10) {j ++;}
CIL transforms the code thus because the C standard
specifies that operators such as ++ do not operate on
types smaller than int, and that values of these types
are implicitly promoted to int in these conditions.
Meanwhile, in the absence of any loop-related
option, the value analysis tries to keep computations
short at the price of precision by using a technique
called "widening". In order to limit the loss of precision,
however, various heuristics are used, including a
syntactic one for the j loop that recognizes that
j IN [0..10] is a good candidate for the loop invariant.
This heuristic does not currently recognize the condition
((int )i < 10) as one where it would be valuable to try
the same kind of invariant.
I have filed this issue as "feature wish" in the Bug Tracking
System, so that it is not forgotten.
http://bts.frama-c.com/view.php?id=325
Pascalhttps://git.frama-c.com/pub/frama-c/-/issues/2383Why keywords as ACSL identifiers2021-04-15T09:17:26ZJulien SignolesWhy keywords as ACSL identifiersID0000391:
**This issue was created automatically from Mantis Issue 391. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000391:
**This issue was created automatically from Mantis Issue 391. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000391 | Frama-C | Plug-in > jessie | public | 2010-02-03 | 2010-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
The generated why file contains a syntax error (a keyword is used where an identifier is expected).
### Additional Information :
Fixed in Why CVS
### Steps To Reproduce :
=== t.c ===
/*@ lemma rec: \true; */
===========
$ frama-c -jessie t.c
File "why/t.why", line 94, characters 5-8:
Syntax errorhttps://git.frama-c.com/pub/frama-c/-/issues/2366Code containing consts should be verifiable2021-04-15T09:17:19Zmantis-gitlab-migrationCode containing consts should be verifiableID0000485:
**This issue was created automatically from Mantis Issue 485. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000485:
**This issue was created automatically from Mantis Issue 485. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000485 | Frama-C | Plug-in > jessie | public | 2010-05-18 | 2010-05-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Jessie should be able to verify code that contains global C-constants as declared with the keyword const.
I consider using consts instead of macros good programming practice.
### Additional Information :
// Doesn't verify:
const int size=4;
/*@ requires \valid(msg+(0..size));
*/
int setFoo(char* msg) {
msg[size] = '\0';
return 0;
}Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2356Enhancement on assigns annotation and the name of proof obligation2021-04-15T09:17:15Zmantis-gitlab-migrationEnhancement on assigns annotation and the name of proof obligationID0000544:
**This issue was created automatically from Mantis Issue 544. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000544:
**This issue was created automatically from Mantis Issue 544. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000544 | Frama-C | Plug-in > jessie | public | 2010-07-17 | 2010-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | logan | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider the following functions. Both function violates
ACSL specification, and all of the theorem prover gives
UNKNOWN as result (which is correct and expected).
However, the name of proof obligation of test2() is
"loop invariants initially holds" which is a little
confusing. Since the problem is actually on the assign
statement instead of the while-loop. I think it will be
better to have an independent check for @assigns annotation
just like the "postcondition" proof obligation of test1().
--------------------------------------------------------
int global;
/*@ assigns \nothing;
*/
int test1() {
global = 1;
}
/*@ assigns \nothing;
*/
int test2() {
global = 2;
/*@ loop variant 0; */
while (0) {
}
}
--------------------------------------------------------Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2346Suggest to close a section if each obligation is proven by *some* prover2021-02-22T13:56:58ZJochen BurghardtSuggest to close a section if each obligation is proven by *some* proverID0000602:
**This issue was created automatically from Mantis Issue 602. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000602:
**This issue was created automatically from Mantis Issue 602. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000602 | Frama-C | Graphical User Interface | public | 2010-10-12 | 2010-10-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | monate | **Resolution** | not fixable |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Currently, a section (like e.g. "fctxxx default behaviour" is automatically closed when *one* prover was able to prove all its contained obligations. However, often no single prover can prove them all, but each of them can be proved by some prover (i.e. in each line a green bullet appears, although not in the same column).
As a result, the user has to check all lines by himself, which is tedious (and even error-prone) when sections are large and the process of finding an adequate and verifiable specification involves many edit->vcg->prove cycles.
Therefor, I suggest to close a section once the statistics count has reached 100% of proven obligations (i.e. n/n). A "summary column" could be introduced showing a green bullet for single a obligation if it was proven by some prover, and a green check-mark for a section if its statistics count is 100%. For "very large" programs, it might even be desirable to have an icon summarizing all sections, i.e. the whole program, in a corresponding way.https://git.frama-c.com/pub/frama-c/-/issues/2338Suggest to rename user identifiers to avoid name clashes in ..._why.sx files2021-04-15T09:17:12ZJochen BurghardtSuggest to rename user identifiers to avoid name clashes in ..._why.sx filesID0000632:
**This issue was created automatically from Mantis Issue 632. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000632:
**This issue was created automatically from Mantis Issue 632. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000632 | Frama-C | Plug-in > jessie | public | 2010-11-29 | 2010-11-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Simplify yields a "!" ("failure") on the attached program, seemingly because f's parameter name "EQ" clashes with the name of the equality predicate used in the preamble of ftest_why.sx. Simplfy has similar problems with a couple of other names, e.g. "AND". (Alt-ergo doesn't have these problems).
I'd like to suggest to catch those "reserved identifiers" by Jessie and to rename them, like this seems to be done already for "result".
It seems pretty dangerous that the "0.0" in g's body is currently translated into an occurrence of the quantified variable representing g's parameter. While the incorrect g is not verifiable right now, it might become so in future - as soon as a property like "double_value(real_constant_0_0e) == real_constant_0_0e" becomes derivable.
## Attachments
- [ftest.c](/uploads/cb37bc6d94f7428d03c340ad9836e58a/ftest.c)Claude MarchéClaude Marchéhttps://git.frama-c.com/pub/frama-c/-/issues/2304Checking number of arguments passed to C functions2021-02-22T13:56:10ZPascal CuoqChecking number of arguments passed to C functionsID0000552:
**This issue was created automatically from Mantis Issue 552. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000552:
**This issue was created automatically from Mantis Issue 552. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000552 | Frama-C | Kernel | public | 2010-08-02 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
There currently isn't much checking of function arguments in the front-end. The following program is accepted, although it passes the wrong number of arguments for both calls to retint:
int retint(int x )
{
int __retres ;
__retres = 42 + x;
return (__retres);
}
int main(int c )
{
int x ;
int tmp ;
x = retint();
tmp = retint(c,c);
return (tmp);
}
Arguments for not implementing this feature: there are perfectly good compilers to check for this, and not having rigid rules in place may even help with older code containing variadic functions. I am not sure when the current convention for declaring variadic functions became standardized, and it may not have been from the beginning.https://git.frama-c.com/pub/frama-c/-/issues/2299Frama-C should produce more specific error messages when parsing annotations2021-02-22T14:04:36Zmantis-gitlab-migrationFrama-C should produce more specific error messages when parsing annotationsID0000538:
**This issue was created automatically from Mantis Issue 538. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000538:
**This issue was created automatically from Mantis Issue 538. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000538 | Frama-C | Kernel | public | 2010-07-09 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
If an annotation contains a syntax error, Frama-C should be more specific about the kind of error.
For example, given a source file that contains this line
//@ loop invariant \forall integer i; aLength-1 >= i > high ==> a[i] > val);
a more helpful report may be:
foo.c, line 24: ')' unexpected
//@ loop invariant \forall integer i; aLength-1 >= i > high ==> a[i] > val);
^ herehttps://git.frama-c.com/pub/frama-c/-/issues/2294Makefile.dynamic should not change known_plugins.ac2021-02-22T14:04:39Zmantis-gitlab-migrationMakefile.dynamic should not change known_plugins.acID0000462:
**This issue was created automatically from Mantis Issue 462. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000462:
**This issue was created automatically from Mantis Issue 462. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000462 | Frama-C | Kernel > Makefile | public | 2010-04-27 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
I'm not sure whether this is a bug or a feature, but in my understanding, installing an external plugin for Frama-C should not modify the files installed by Frama-C itself.
In this specific case, when the Jessie plugin wants to install, 'Makefile.dynamic' tells to append a line in '/usr/share/frama-c/known_plugins.ac'. If the user doesn't have write access on 'known_plugins.ac', the installation fails. Specifically, this would have lead to a build failure on any Debian build daemon. For now, I've desactivated this "feature" in 'Makefile.dynamic' using the attached patch.
'known_plugins.ac' is used only by the configure scripts of aorai and security_slicing. IMHO, they should rely on the existence of plugin files rather than some text file with (potentially) random content.
## Attachments
- [0005-Don-t-modify-system-files.patch](/uploads/a2a99b05668822004392ce1b153044af/0005-Don-t-modify-system-files.patch)https://git.frama-c.com/pub/frama-c/-/issues/2282for behav : invariant INV ;2021-02-22T13:55:32ZPatrick Baudinfor behav : invariant INV ;ID0000482:
**This issue was created automatically from Mantis Issue 482. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000482:
**This issue was created automatically from Mantis Issue 482. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000482 | Frama-C | Kernel > ACSL implementation | public | 2010-05-17 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
Invariant clauses can be associated to named behaviors like assert clauses.https://git.frama-c.com/pub/frama-c/-/issues/2267Input computations imprecise when calling unknown function2021-02-22T13:55:13ZVictoria Moya LamielInput computations imprecise when calling unknown functionID0000644:
**This issue was created automatically from Mantis Issue 644. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000644:
**This issue was created automatically from Mantis Issue 644. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000644 | Frama-C | Plug-in > inout | public | 2010-12-20 | 2010-12-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vmoyalam | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101201-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
If a local variable is modified two times consecutively:
1)
local = CONSTANT1;
local = CONSTANT2;
CONSTANT1 and CONSTANT2 are both considered as in operands (-inout and-input options), but if the variable is modified in another way :
2)
//@assigns *i;
extern void f(/* out */ int * const i) ;
local = CONSTANT1;
local = CONSTANT2;
f(&local);
CONSTANT1 and CONSTANT2 are no longer present in the Inout analysis.
### Additional Information :
See the complete example in the attached file.
## Attachments
- [test_II.c](/uploads/31ceac4795f5cd571be9a83b56765a70/test_II.c)https://git.frama-c.com/pub/frama-c/-/issues/2264Launching several instances of the prover in parallel from the GUI?2021-04-15T09:17:48ZVirgile PrevostoLaunching several instances of the prover in parallel from the GUI?ID0000033:
**This issue was created automatically from Mantis Issue 33. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...ID0000033:
**This issue was created automatically from Mantis Issue 33. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000033 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2010-12-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101202-beta2 |
### Description :
Hello,
[bug 7439 from old bts, reported by David Mentré]
I'm using frama-c on multi-core and multi-processor machines. Would it be possible, when proving all obligations or
obligations from a selected function using the GUI (gWhy), to launch several instances of the prover at the same time?
It could speed-up the proving time.
Yours,
d.
### Additional Information :
This feature will be available in Why3 IDE, released in dec 2010
(This won't be avalable in Why2)