frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-04-15T09:17:26Z
https://git.frama-c.com/pub/frama-c/-/issues/2384
int32 and real can't be unified
2021-04-15T09:17:26Z
Sylvie Boldo
int32 and real can't be unified
ID0000386:
**This issue was created automatically from Mantis Issue 386. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000386:
**This issue was created automatically from Mantis Issue 386. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000386 | Frama-C | Plug-in > jessie | public | 2010-02-01 | 2010-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sboldo | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Hello,
With the svn version of frama-c and jessie, I have the following problem: an integer cannot be promoted to real inside a function call.
The function \pow takes 2 real numbers. If I give it an int32. Jessie fails to type it.
### Additional Information :
# pragma JessieFloatModel(strict)
double malcolm1() {
double A;
A=2.0;
/*@ assert A==2.; */
/*@ ghost int i = 1; */
/*@ loop invariant A== \pow(2.,i) &&
@ 1 <= i <= 53;
@ loop variant (53-i); */
while (A != (A+1)) {
A*=2.0;
/*@ ghost i++; */
}
/*@ assert A== 0x1.p53; */
}
https://git.frama-c.com/pub/frama-c/-/issues/2383
Why keywords as ACSL identifiers
2021-04-15T09:17:26Z
Julien Signoles
Why keywords as ACSL identifiers
ID0000391:
**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 error
https://git.frama-c.com/pub/frama-c/-/issues/2382
Statement contract and "hiding" of statement
2021-04-15T09:17:25Z
Dillon Pariente
Statement contract and "hiding" of statement
ID0000399:
**This issue was created automatically from Mantis Issue 399. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000399:
**This issue was created automatically from Mantis Issue 399. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000399 | Frama-C | Plug-in > jessie | public | 2010-02-06 | 2010-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Hello,
On the following annotated code:
int main(int x)
{ int y=0;
//@ assigns y; ensures y==3;
y=x;
//@ assert y>0;
}
analyzed by: frama-c -jessie foo.c
assert y>0 is not discharged (no matter the preceding statement contract is valid or not).
Indeed, statement contract (assigns y; ensures y==3;) doesn't seem to be taken into account as it does not appear in .jc file.
### Additional Information :
https://git.frama-c.com/pub/frama-c/-/issues/2380
same formula translated differently as axiom/lemma
2021-04-15T09:17:23Z
Jochen Burghardt
same formula translated differently as axiom/lemma
ID0000420:
**This issue was created automatically from Mantis Issue 420. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000420:
**This issue was created automatically from Mantis Issue 420. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000420 | Frama-C | Plug-in > jessie | public | 2010-02-25 | 2010-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Axiom ax2 (line 5,6 in attached file) is translated into a proof obligation on 2 memory labels. However, in lemma lm1 (line 11,12), the literally same formula is translated into a proof obligation on 4 memory labels; and so is the assertion in line 24, which is an instance of the ax2/lm1 formula.
As a consequence, when lm1 is omitted, the assertion cannot be proved (by Alt-ergo; Simplify doesnt prove it in any case); but when lm1 is present, the assertion can be proved, while the lemma itself can not.
(While the example program in the attached file is nonsensical, it has been boiled down from a program that does make sense.)
## Attachments
- [axiomLabels01.c](/uploads/8d9a723d0c34c7d7ac05d975dd8380aa/axiomLabels01.c)
https://git.frama-c.com/pub/frama-c/-/issues/2379
assigns clause unchecked on arrays
2021-04-15T09:17:21Z
Jochen Burghardt
assigns clause unchecked on arrays
ID0000443:
**This issue was created automatically from Mantis Issue 443. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000443:
**This issue was created automatically from Mantis Issue 443. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000443 | Frama-C | Plug-in > jessie | public | 2010-04-06 | 2010-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | urgent | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | Frama-C Boron-20100401 | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
While a write-access to a simple variable (int a) is recognized to violate an assigns-clause, a similar access to an array variable (int a[1]) is not.
No proof obligation is generated in the latter case.
See attached file; uncomment / comment-out the #define to demonstrate the different behaviors.
I tried jessie only without the option "-jessie-no-regions".
## Attachments
- [ftest.c](/uploads/4c25bf5876421bb9641223da29b0d4de/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/2378
Jessie subprocess failed with enumerated type
2021-04-15T09:17:21Z
Victoria Moya Lamiel
Jessie subprocess failed with enumerated type
ID0000449:
**This issue was created automatically from Mantis Issue 449. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000449:
**This issue was created automatically from Mantis Issue 449. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000449 | Frama-C | Plug-in > jessie | public | 2010-04-13 | 2010-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vmoyalam | **Assigned To** | cmarche | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Jessie crashes on the attached file with the exact model option.
WHY version : 2.21
command : "frama-c -jessie -jessie-int-model exact test2.c".
### Additional Information :
It seems there is a problem with enumerated types.
Command-line output :
[kernel] preprocessing with "gcc -C -E -I. -D JESSIE_EXACT_INT_MODEL -dD test2.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir test2.jessie
[jessie] File test2.jessie/test2.jc written.
[jessie] File test2.jessie/test2.cloc written.
[jessie] Calling Jessie tool in subdir test2.jessie
File "test2.jc", line 25, characters 0-74: typing error: inferred type differs from declared type
[jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs test2.cloc test2.jc
## Attachments
- [test2.c](/uploads/0c8e9411b06a7eff4c0d8cd836b83756/test2.c)
https://git.frama-c.com/pub/frama-c/-/issues/2377
Jessie translation fails with double assignment
2021-04-15T09:17:21Z
Victoria Moya Lamiel
Jessie translation fails with double assignment
ID0000450:
**This issue was created automatically from Mantis Issue 450. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000450:
**This issue was created automatically from Mantis Issue 450. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000450 | Frama-C | Plug-in > jessie | public | 2010-04-13 | 2010-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vmoyalam | **Assigned To** | cmarche | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Jessie crashes on the attached file.
WHY version : 2.21
command : "frama-c -jessie test4.c".
### Additional Information :
It seems there is a problem with double assignment.
Command-line output :
[kernel] preprocessing with "gcc -C -E -I. -dD test4.c"
[jessie] Starting Jessie translation
test4.c:13:[jessie] failure: Unexpected failure.
Please submit bug report (Ref. "interp.ml:1798:18").
[kernel] Plugin jessie aborted because of an internal error.
Please report with 'crash' at http://bts.frama-c.com
## Attachments
- [test4.c](/uploads/3184950f1379cfe6d9dfd2999f7d563d/test4.c)
https://git.frama-c.com/pub/frama-c/-/issues/2376
"why" reports "unbound label"
2021-04-15T09:17:28Z
Jochen Burghardt
"why" reports "unbound label"
ID0000361:
**This issue was created automatically from Mantis Issue 361. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000361:
**This issue was created automatically from Mantis Issue 361. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000361 | Frama-C | Plug-in > jessie | public | 2009-12-15 | 2010-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
"why" reports an "unbound label" if a C-label of a statement having more than one effect (e.g. "b[j++] = 3;") is referred to in an "\at(...)" within an acsl-assertion.
See attached file "labelBug.c"; process it with and without the initial "#define showBug" uncommented.
## Attachments
- [labelBug.c](/uploads/64e341aa1f7b230cbd5aa963b35d5107/labelBug.c)
https://git.frama-c.com/pub/frama-c/-/issues/2375
wrong proof obligation generated with axiomatic def and array quantification
2021-04-15T09:17:29Z
Jochen Burghardt
wrong proof obligation generated with axiomatic def and array quantification
ID0000362:
**This issue was created automatically from Mantis Issue 362. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000362:
**This issue was created automatically from Mantis Issue 362. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000362 | Frama-C | Plug-in > jessie | public | 2009-12-15 | 2010-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
For line 18 in the attached file, the proof obligation generated for Simplify uses validity of line 17 as one assumption. However, this assumption is generated wrong, viz. as "all c: s(c,8,result)=s(c,8,result)", whereas the 3rd params of "s" should differ. Thus, the implication 17->18 can't be proved, although I consider it a direct consequence of the all-elim-rule. I couldn't produce a similar example without an axiomatic definition involved.
## Attachments
- [instBug.c](/uploads/f1f078db34ca0f0f048a0e1210313dc9/instBug.c)
https://git.frama-c.com/pub/frama-c/-/issues/2374
bug with constants like 1E-6
2021-04-15T09:17:28Z
mantis-gitlab-migration
bug with constants like 1E-6
ID0000367:
**This issue was created automatically from Mantis Issue 367. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000367:
**This issue was created automatically from Mantis Issue 367. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000367 | Frama-C | Plug-in > jessie | public | 2010-01-07 | 2010-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | toomanycsh | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
bool_t func1(float32_t x);
/*@ ensures \result == TRUE
*/
bool_t func1(float32_t x)
{
if (x < 1E-6){
;
}
return TRUE;
}
Alt-Ergo and CVC3 claim a syntax error on the input from Frama-C.
https://git.frama-c.com/pub/frama-c/-/issues/2373
pragma JessieIntegerModel
2021-04-15T09:17:27Z
Dillon Pariente
pragma JessieIntegerModel
ID0000370:
**This issue was created automatically from Mantis Issue 370. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000370:
**This issue was created automatically from Mantis Issue 370. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000370 | Frama-C | Plug-in > jessie | public | 2010-01-13 | 2010-04-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
On the following annotated code, omitting the pragma (first line in comments), generates an error (see below) :
/////////////////////////////////////
//# pragma JessieIntegerModel(exact)
typedef struct qr { int q; int r; } qr;
// md is a recursive function
/*@ requires d>0 && n>=0;
decreases n;
*/
qr md(int n,int d)
{ int q,r; qr v;
if (n==0)
{ v.q = 0;
v.r = 0;
return v;
} else { v = md(n-1,d);
return v;
}
}
Error:
gwhy-bin [...] why/d4.why
Computation of VCs...
File "why/d4.why", line 781, characters 68-178:
Term (JC_22 : jessie_35) is expected to have type int
make: *** [d4.stat] Error 1
[jessie] user error: Jessie subprocess failed: make -f d4.makefile gui
This problem might be related to BTS#178 (first feedback from Frama-C team).
https://git.frama-c.com/pub/frama-c/-/issues/2372
Lack of parameter generation
2021-04-15T09:17:20Z
mantis-gitlab-migration
Lack of parameter generation
ID0000456:
**This issue was created automatically from Mantis Issue 456. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000456:
**This issue was created automatically from Mantis Issue 456. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000456 | Frama-C | Plug-in > jessie | public | 2010-04-23 | 2010-04-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gava | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following program (even if there are not enought annotations) works with Frama-C Berylium (with why-2.23) but crashes with Boron/why-2.24
The VC of WHY is launched and it said that a parameter is missing... The pb does not arise with why-2.23/Brylium
Frédéric G.
ps: the file "bsp.h" in the "additional information"
pps : I used "frama-c -jessie bspinprod.c"
### Additional Information :
typedef value_type;
/*@
axiomatic GoodNumberProcessor
{
logic integer bsp_p;
axiom good_bsp_p: 0<bsp_p;
}
*/
/*@
ensures \result==bsp_p;
*/
int bsp_nprocs();
/*@
ensures 0<=\result<bsp_p;
*/
int bsp_pid();
int bsp_l();
int bsp_g();
int bsp_r();
/*@
assigns \nothing;
*/
void bsplib_init(int* argc, char*** argv);
void bsplib_done();
double bsp_time();
void bsp_sync();
/* void bsp_push_reg(void* ident, int size); */
/*@
assigns \nothing;
*/
void bsp_push_reg(value_type* ident, int n);
/* void bsp_pop_reg(void* ident); */
/*@
assigns \nothing;
*/
void bsp_pop_reg(value_type* ident);
/* void bsp_put(int destPID, void* src, void* dest, int offset, int nbytes); */
/*@
assigns \nothing;
*/
void bsp_put(int destPID, value_type* src, value_type* dest, int offset, int nbytes);
/* void bsp_get(int srcPID, value_type* src, int offset, value_type* dest, int nbytes); */
/*@
assigns \nothing;
*/
void bsp_get(int srcPID, value_type* src, int offset, void* dest, int nbytes);
/* void bsp_send(int dest, void* buffer, int size); */
/*@
assigns \nothing;
*/
void bsp_send(int dest, value_type* buffer, int size);
/* void* bsp_getmsg(int proc_id, int index); */
/*@
assigns \nothing;
*/
value_type *bsp_getmsg(int proc_id, int index);
/*@
assigns \nothing;
*/
int bspmsg_size(int proc_id, int index);
/*@
assigns \nothing;
*/
int bsp_nmsgs(int proc_id);
## Attachments
- [bspinprod.c](/uploads/467920e94c6fea4a7aa01db518329466/bspinprod.c)
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2370
volatile annotation breaks type checker
2021-04-15T09:17:19Z
mantis-gitlab-migration
volatile annotation breaks type checker
ID0000480:
**This issue was created automatically from Mantis Issue 480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000480:
**This issue was created automatically from Mantis Issue 480. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000480 | Frama-C | Plug-in > jessie | public | 2010-05-12 | 2010-05-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | tomahawkins | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Adding a volatile annotation on some variables breaks the type checker. (Why 2.26) For example:
#include <stdint.h>
// This works.
//int32_t a;
// This doesn't.
volatile int32_t a;
void f(double b) {
a = (int32_t) b;
}
Yields:
e0082888@e0082888-laptop:~$ frama-c -jessie test.c
[kernel] preprocessing with "gcc -C -E -I. -dD test.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir test.jessie
[jessie] File test.jessie/test.jc written.
[jessie] File test.jessie/test.cloc written.
[jessie] Calling Jessie tool in subdir test.jessie
File "test.jc", line 34, characters 41-55: typing error: bad cast to integer
[jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs test.cloc test.jc
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2369
I am not able to use the jessie plugin to analysis files in the frama-c.
2021-04-15T09:17:20Z
mantis-gitlab-migration
I am not able to use the jessie plugin to analysis files in the frama-c.
ID0000477:
**This issue was created automatically from Mantis Issue 477. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000477:
**This issue was created automatically from Mantis Issue 477. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000477 | Frama-C | Plug-in > jessie | public | 2010-05-11 | 2010-05-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | luoting | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
~$ frama-c -jessie-analysis '/home/fuwuqi/desktop/b.c'
Parsing
[preprocessing] running gcc -C -E -I. -include /usr/lib/frama-c/jessie/jessie_prolog.h -dD /home/fuwuqi/desktop/b.c
Cleaning unused parts
Symbolic link
Starting semantical analysis
Starting Jessie translation
Producing Jessie files in subdir /home/fuwuqi/desktop/b.jessie
File /home/fuwuqi/desktop/b.jessie/b.jc written.
File /home/fuwuqi/desktop/b.jessie/b.cloc written.
Calling Jessie tool in subdir /home/fuwuqi/desktop/b.jessie
File "b.jc", line 350, characters 18-19: syntax error
Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs b.cloc b.jc
### Additional Information :
When I use ~$ frama-c -jessie '/home/fuwuqi/??/b.c'
then,
frama-c: unknown option `-jessie'.
toplevel options files...
https://git.frama-c.com/pub/frama-c/-/issues/2368
Segmentation fault: plugin reading from Cil_types
2021-02-22T13:57:25Z
mantis-gitlab-migration
Segmentation fault: plugin reading from Cil_types
ID0000481:
**This issue was created automatically from Mantis Issue 481. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000481:
**This issue was created automatically from Mantis Issue 481. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000481 | Frama-C | Kernel | public | 2010-05-17 | 2010-05-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | tomahawkins | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Ubuntu Linux x86 10.04 | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
A plugin that reads data from the Cil_types module, trips a segmentation fault.
The plugin reads all data from the Cil_types module. Are there any values in Cil_types that are invalid to read, and which would cause a segfault when referenced?
Attached in the plugin (dump_cil.ml), the Makefile to build and install the pluging, and a test file (plugin_segfaults.c) that demonstrates C syntax that works and syntax that segfaults.
## Attachments
- [dump_cil.ml](/uploads/0bfe6c9ea6268fa512807fdce430eb7b/dump_cil.ml)
- [Makefile](/uploads/ab42f3de07a524bf5d522f26ce035b5c/Makefile)
- [plugin_segfaults.c](/uploads/b7438400154254b45333b8a2f174649d/plugin_segfaults.c)
https://git.frama-c.com/pub/frama-c/-/issues/2367
How to update frama-c-gui
2021-02-22T13:57:24Z
mantis-gitlab-migration
How to update frama-c-gui
ID0000483:
**This issue was created automatically from Mantis Issue 483. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000483:
**This issue was created automatically from Mantis Issue 483. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000483 | Frama-C | Graphical User Interface | public | 2010-05-17 | 2010-05-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | luoting | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi ,Signoles
I once installed frama-c (version 20081201)by Synaptic ,and you said the version was a bit old. So I downloaded the frama-c (version Boron-20100401)source file and full installed it (./configure&&make&&sudo make install).However ,I find frama-c is version Boron-20100401 ,while frama-c-gui is still version 20081201.Why ? How to update frama-c-gui?
Thanks!
### Additional Information :
I have not removed the frama-c (version 20081201) before install the new version.
https://git.frama-c.com/pub/frama-c/-/issues/2366
Code containing consts should be verifiable
2021-04-15T09:17:19Z
mantis-gitlab-migration
Code containing consts should be verifiable
ID0000485:
**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/2365
Annotations analysis does not find preprocessor macro
2021-04-15T09:17:19Z
mantis-gitlab-migration
Annotations analysis does not find preprocessor macro
ID0000486:
**This issue was created automatically from Mantis Issue 486. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000486:
**This issue was created automatically from Mantis Issue 486. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000486 | Frama-C | Plug-in > jessie | public | 2010-05-18 | 2010-05-21 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | virgile | **Resolution** | not fixable |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following is correct c-code, but is doesn't verify.
#define BUFF_SIZE 4
/*@ requires \valid(msg+(0..BUFF_SIZE));
ensures msg[BUFF_SIZE] == '\0';
*/
int setFoo(char* msg) {
msg[BUFF_SIZE] = '\0';
return 0;
}
~/progs/C/frama-c/test$ frama-c -jessie -pp-annot t.c
[kernel] preprocessing with "gcc -C -E -I. -dD t.c"
t.c:3:[kernel] user error: Error during annotations analysis: unbound logic variable BUFF_SIZE
[kernel] user error: skipping file "t.c" that has errors.
[kernel] Plugin kernel aborted because of invalid user input(s).
A work-around is to add a space between .. and BUFF_SIZE.
https://git.frama-c.com/pub/frama-c/-/issues/2362
unsoundness of Jessie with respect to expression evaluation of ANSI-C
2021-04-15T09:17:34Z
mantis-gitlab-migration
unsoundness of Jessie with respect to expression evaluation of ANSI-C
ID0000289:
**This issue was created automatically from Mantis Issue 289. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000289:
**This issue was created automatically from Mantis Issue 289. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000289 | Frama-C | Plug-in > jessie | public | 2009-10-19 | 2010-06-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Sylvain Boulme | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following program is completely proved by Jessie (using Alt-Ergo 0.9). However, when compiled with gcc on my Linux-PC, it leads to a segmentation fault.
The problem seems to come from the fact that Jessie chooses an order of evaluation for subexpressions which is different from my gcc. Actually ANSI-C specifies that the order of evaluation is indeterminate.
Some hints to fix this problem:
+ detect and forbids expressions which depend on evaluation order.
+ alternatively, emulate the semantics of
x = c - decr()
by
if (anybool()) {
tmp_l=c ;
tmp_r=decr() ;
} else {
tmp_r=decr();
tmp_l=c ;
}
x = tmp_l - tmp_r ;
where anybool is simply declared as:
/*@ assigns \nothing ; */
int anybool () ;
However, this last approach may lead to an explosion of proof obligations.
## Attachments
- [nondetexp_KO.c](/uploads/6b19b3190dceeebe32a6d41edd9f75a1/nondetexp_KO.c)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/2361
Unbound label in Jessie-generated Why file when using logic function in assig...
2021-04-15T09:17:18Z
Pascal Cuoq
Unbound label in Jessie-generated Why file when using logic function in assigns clause
ID0000502:
**This issue was created automatically from Mantis Issue 502. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000502:
**This issue was created automatically from Mantis Issue 502. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000502 | Frama-C | Plug-in > jessie | public | 2010-06-09 | 2010-06-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | low | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
rot13.c:
_________
/*@ predicate string_of_length{L}(unsigned char *s, integer n) =
n >= 0 &&
\valid_range(s, 0, n) &&
s[n] == 0 &&
\forall integer k ; (0 <= k < n) ==> (s[k] != 0) ;
lemma always_the_same_length{L}:
\forall unsigned char *s, integer n1, integer n2 ;
(string_of_length(s, n1) && string_of_length(s, n2)) ==> n1 == n2 ;
*/
/*@ axiomatic Length
{
logic integer length{L}(unsigned char *s) reads s[..] ;
axiom string_length{L}:
\forall integer n, unsigned char *s ;
string_of_length(s, n) ==> length(s) == n ;
}
*/
/*@
assigns \nothing ;
*/
unsigned char rot13_char(unsigned char c)
{
if ((c >= 'a' && c <= 'm') || (c >= 'A' && c <= 'M')) return c + 13;
if ((c >= 'n' && c <= 'z') || (c >= 'N' && c <= 'Z')) return c - 13;
return c;
}
/*@
requires \exists integer n ; 0 <= n <= 2000000000 && string_of_length(s,n) ;
assigns s[..length{Old}(s)] ;
// ensures is_rot13{Pre,Post}(s,s) ;
*/
void rot13(unsigned char *s)
{
int i;
for(i=0; s[i]; ++i)
{
s[i] = rot13_char(s[i]);
}
}
_________
Command:
frama-c-Jessie -jessie rot13.c
Obtained result:
...
[jessie] Calling Jessie tool in subdir rot13.jessie
Generating Why function rot13_char
Generating Why function rot13
[jessie] Calling VCs generator.
gwhy-bin [...] why/rot13.why
Computation of VCs...
File "why/rot13.why", line 836, characters 30-66:
Unbound label ''
make: *** [rot13.stat] Error 1
[jessie] user error: Jessie subprocess failed: make -f rot13.makefile gui
The problem is caused by the line:
assigns s[..length{Old}(s)] ;
Claude Marché
Claude Marché