frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-04-15T09:17:45Z
https://git.frama-c.com/pub/frama-c/-/issues/2534
Default invariant should be inferred for loops
2021-04-15T09:17:45Z
Virgile Prevosto
Default invariant should be inferred for loops
ID0000042:
**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/2535
Why- error :-jessie-no-regions and assigns does not work
2021-04-15T09:17:44Z
Virgile Prevosto
Why- error :-jessie-no-regions and assigns does not work
ID0000031:
**This issue was created automatically from Mantis Issue 31. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000031:
**This issue was created automatically from Mantis Issue 31. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000031 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-06-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7242 of old bts reported by Christoph Weber]
Hello,
for the following function I get the error:
in memory set (mem-field(int_M),a_20),
(mem-field(int_M),b_21)
File "jc/jc_interp_misc.ml", line 707, characters 7-7:
Uncaught exception: File "jc/jc_interp_misc.ml", line 707, characters 7-13: Asse
rtion failed
Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs i
nt_alignment.cloc int_alignment.jc
======
/*@
requires 0 <= length;
requires \valid_range (a, 0, length-1);
requires \valid_range (b, 0, length-1);
ensures \forall integer i; 0 <= i < length ==> b[i] == a[i];
*/
void copy (int* a, int length, int* b)
{
int i=0;
/*@
loop invariant 0 <= i <= length;
loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k];
loop assigns b[0 .. i-1];
*/
for(;i<length;i++ )
b[i]=a[i];
}
int main()
{
int array_int[10]={1,2,3,4,5,6,7,8,9,0};
int* first_int = &array_int[0];
char array_char_to_int[50];
copy(first_int, 10, array_char_to_int);
//create pointers to the same array,
//shift the second by one byte
int* first_char_to_int = &array_char_to_int[0];
int* first_char_to_int_shift = &array_char_to_int[1];
//call copy to the same array
//why error
copy(first_char_to_int, 10, first_char_to_int_shift);
return 0;
}
By the way, assigns b[0..length-1]; is never provable.
Cheers
Christoph
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2542
Internal error with assign specification on bi-dimensional arrays
2021-04-15T09:17:44Z
Virgile Prevosto
Internal error with assign specification on bi-dimensional arrays
ID0000032:
**This issue was created automatically from Mantis Issue 32. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000032:
**This issue was created automatically from Mantis Issue 32. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000032 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-04-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7435 from old bts, reported by David Mentré]
Hello,
Using this code:
=== bidim_array.c
int a[12][45] = {0, };
//@ assigns a[..][..];
void f(void)
{
a[1][3] = 42;
}
void main(void)
{
f();
}
===
The assigns clause triggers an internal error in Jessie.
$ frama-c -jessie-analysis -jessie-gen-only bidim_array.c
Parsing
[preprocessing] running gcc -C -E -I. -include
/usr/local/stow/frama-c-lithium-2008-12-01/share/frama-c/jessie/jessie_prolog.h -dD bidim_array.c
Cleaning unused parts
Symbolic link
Starting semantical analysis
Starting Jessie translation
Fatal error: exception Assert_failure("src/jessie/interp.ml", 807, 33)
Yours,
d.
### Additional Information :
Normalization of multi-dimensional array accesses in jessie plugin is not compatible with use of range.
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2543
Jessie crashes on simple program without annotations
2021-04-15T09:17:44Z
Virgile Prevosto
Jessie crashes on simple program without annotations
ID0000038:
**This issue was created automatically from Mantis Issue 38. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000038:
**This issue was created automatically from Mantis Issue 38. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000038 | Frama-C | Plug-in > jessie | public | 2009-04-07 | 2009-04-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
[bug 7541 from old bts, reported by Boris Hollas]
Jessie crashes on the following code:
void Copy(int *p, int *q)
{
*q = *p;
}
int foo(int a[]) {
int i=1;
Copy(&a[0], &a[i]);
return i;
}
int main() {
int a[2] = {1,2};
printf("%d\n", foo(a));
}
Output:
~/progs/fc/tst> frama-c -jessie-analysis tst4.c
Parsing
[preprocessing] running gcc -C -E -I. -include C:\Frama-C\share\frama-c\jessie\jessie_prolog.h -dD tst4.c
tst4.c:17: Warning: Body of function main falls-through. Adding a return statement
Cleaning unused parts
Symbolic link
Starting semantical analysis
Starting Jessie translation
No code for function printf, default assigns generated
tst4.c:15: Warning: skipping all arguments of implicit prototype printf
Producing Jessie files in subdir tst4.jessie
File tst4.jessie/tst4.jc written.
File tst4.jessie/tst4.cloc written.
Calling Jessie tool in subdir tst4.jessie
Generating Why function Copy
Generating Why function foo
Generating Why function main
Calling VCs generator.
why -simplify [...] why/tst4.why
File "why/tst4.why", line 1418, characters 8-49:
Term i_27 is expected to have type int
make: *** [simplify/tst4_why.sx] Error 1
Jessie subprocess failed: make -f tst4.makefile simplify
### Additional Information :
Claude Marché: Issues lies in the lack of a conversion from int32 into int in pset generation (in jessie plugin)
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2521
Jessie/GWhy/Gappa: format file and invalid POs proved valid
2021-04-15T09:17:43Z
Dillon Pariente
Jessie/GWhy/Gappa: format file and invalid POs proved valid
ID0000046:
**This issue was created automatically from Mantis Issue 46. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000046:
**This issue was created automatically from Mantis Issue 46. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000046 | Frama-C | Plug-in > jessie | public | 2009-04-10 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
Hello,
Under Cygwin, for the following code:
/*@ requires -1.0 <= x <= 1.0;
assigns \nothing;
ensures -1.0 <= \result <= 1.0;
*/
float f(float x) { return ( -2.0*x ); }
with command-line:
frama-c -jessie-analysis -jessie-gui faux.c
all POs are proved Valid under GWhy, even they are *not*!
In GWhy's Debug mode, standard output displays:
oblig : f_ensures_default_po_1
calling Gappa on c:\TEMP\gwhyd42d1e_why.gappa
command line: gappa < c:\TEMP\gwhyd42d1e_why.gappa
Output file c:\TEMP\outba8609:
input in flex scanner failed
...
Trying to prove the 1st PO through the following command line:
gappa c:\TEMP\gwhyd42d1e_why.gappa
yields:
Error: syntax error, unexpected $undefined at line 1 column 27
1/ It seems that gappa files are expected to be in UNIX format, and not in DOS' one (i.e. with CR/LF ending lines).
2/ When gappa fails in achieving file parsing, GWhy seems to wrongly interpret it as proved Valid.
Best regards,
Dillon
https://git.frama-c.com/pub/frama-c/-/issues/2520
Jessie/Gwhy: cpulimit-win.c
2021-04-15T09:17:43Z
Dillon Pariente
Jessie/Gwhy: cpulimit-win.c
ID0000049:
**This issue was created automatically from Mantis Issue 49. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000049:
**This issue was created automatically from Mantis Issue 49. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000049 | Frama-C | Plug-in > jessie | public | 2009-04-11 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
Hello,
The release of cpulimit-win.c currently distributed is not the good one but an old one: it does not take into account exit code from process.
A second version was forwarded by email (on 12/07/08) correcting this bug. Please find it enclosed!
Best regards,
Dillon
## Attachments
- [cpulimit-win.c](/uploads/167e27021d0ee7a802efe50778c4d08c/cpulimit-win.c)
https://git.frama-c.com/pub/frama-c/-/issues/2332
labels are not correctly translated in jessie+why
2021-04-15T09:17:43Z
François Bobot
labels are not correctly translated in jessie+why
ID0000071:
**This issue was created automatically from Mantis Issue 71. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000071:
**This issue was created automatically from Mantis Issue 71. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000071 | Frama-C | Plug-in > jessie | public | 2009-04-30 | 2010-12-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bobot | **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 Beryllium-20090902 |
### Description :
An example with a label in a ghost (or not) statement,
label.c :
===============
void myfun(int p){
p = 1;
//@ ghost Mylabel:
p = 2;
//@ assert \at(p,Mylabel)==p-1;
}
====================
Why complains about an unbound label.
frama-c -jessie-analysis label.c :
===================================
[...]
File "why/label.why", line 350, characters 30-47:
Unbound label 'Mylabel'
===================================
In fact the label is defined in the jessie file.
label.jc :
===================================
unit myfun(int32 p)
behavior default:
assumes true;
ensures (C_4 : true);
{
{ (C_1 : (p = 1));
(Mylabel : ());
(C_2 : (p = 2));
{
(assert for default: (C_3 : (\at(p,Mylabel) == (p - 1))));
()
};
(return ())
}
}
====================================
and in the why file, but perhaps not well scoped.
why/label.why :
====================================
let myfun_safety =
fun (p : int32) ->
{ (JC_4: true) }
(let mutable_p = ref p in
(init:
try
begin
(C_1:
(let jessie_1 = (mutable_p := (safe_int32_of_integer_ (1))) in void));
(Mylabel:
(let jessie_2 = (mutable_p := (safe_int32_of_integer_ (2))) in void));
[ { } unit reads mutable_p
{ (JC_9:
eq_int(integer_of_int32(mutable_p@Mylabel),
sub_int(integer_of_int32(mutable_p), (1)))) } ];
void;
(raise Return);
(raise Return)
end
with
Return ->
void end))
{ true }
=================================
### Additional Information :
frama-c release 5186
https://git.frama-c.com/pub/frama-c/-/issues/2426
The specifications of statements are not translated
2021-04-15T09:17:42Z
François Bobot
The specifications of statements are not translated
ID0000072:
**This issue was created automatically from Mantis Issue 72. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000072:
**This issue was created automatically from Mantis Issue 72. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000072 | Frama-C | Plug-in > jessie | public | 2009-04-30 | 2010-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bobot | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
No vc are produced with this function.
spec_statement.c :
==============================
void myfun(int p){
p = 1;
/*@ requires p==1;
@ ensures \old(p)==p-1;
@*/
p = 2;
}
=============================
spec_statement.jc:
========================
unit myfun(integer p)
behavior default:
assumes true;
ensures (C_3 : true);
{
{ (C_1 : (p = 1));
(C_2 : (p = 2));
(return ())
}
}
========================
### Additional Information :
frama-c : 5186
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2517
A pure predicate in an axiomatic with some "unpure" axioms have some strange ...
2021-04-15T09:17:42Z
François Bobot
A pure predicate in an axiomatic with some "unpure" axioms have some strange results
ID0000073:
**This issue was created automatically from Mantis Issue 73. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000073:
**This issue was created automatically from Mantis Issue 73. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000073 | Frama-C | Plug-in > jessie | public | 2009-04-30 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bobot | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
A pure predicate in an axiomatic with some "unpure" axioms have some strange results. In this case an assertion failed :
myc.c
============================
/*@
axiomatic myaxioms{
predicate myrelation(int p,int q);
logic int mylogic{L}(int * p);
axiom myaxiom{L} :
\forall int * p, q; \at(myrelation(mylogic(p),q),L);
}
@*/
frama-c -jessie-analysis unwanted_label.c.assertion_failed.c :
=========================
Calling Jessie tool in subdir unwanted_label.c.assertion_failed.jessie
File "jc/jc_typing.ml", line 2687, characters 20-20:
Uncaught exception: File "jc/jc_typing.ml", line 2687, characters 20-26: Assertion failed
===========================
### Additional Information :
frama-c : 5186
https://git.frama-c.com/pub/frama-c/-/issues/2444
Assertion failed in jc_interp_misc.ml
2021-04-15T09:17:42Z
mantis-gitlab-migration
Assertion failed in jc_interp_misc.ml
ID0000080:
**This issue was created automatically from Mantis Issue 80. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000080:
**This issue was created automatically from Mantis Issue 80. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000080 | Frama-C | Plug-in > jessie | public | 2009-05-11 | 2009-11-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | cmarche | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Jessie crashes on code [1] with error message [2].
Environment: Windows XP, cygwin
---------------------------------------
[1]
/*@ requires \valid(p) && \valid(q);
ensures *p == \old(*q);
ensures *q == \old(*p);
assigns *p, *q;
*/
void Swap(int *p, int *q)
{
int temp;
temp = *p;
*p = *q;
*q = temp;
}
/*@ requires \valid(a+ (0..k));
*/
void foo(int a[], int k) {
Swap(&a[0], &a[k]);
}
[2]
memory (mem-field(int_M),q_21)
in memory set (mem-field(int_M),p_20),
(mem-field(int_M),q_21)
File "jc/jc_interp_misc.ml", line 707, characters 7-7:
Uncaught exception: File "jc/jc_interp_misc.ml", line 707, characters 7-13: Assertion failed
Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs tst2.cloc tst2.jc
### Additional Information :
This bug is likely related to bug 38 http://bts.frama-c.com/view.php?id=38
https://git.frama-c.com/pub/frama-c/-/issues/2533
Why error with logic functions returning a pointer
2021-04-15T09:17:42Z
Virgile Prevosto
Why error with logic functions returning a pointer
ID0000092:
**This issue was created automatically from Mantis Issue 92. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000092:
**This issue was created automatically from Mantis Issue 92. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000092 | Frama-C | Plug-in > jessie | public | 2009-05-20 | 2009-06-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | cmarche | **Resolution** | reopened |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following code (a stripped down example of the bug reported by Alan Dunn on the mailing list: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-May/001151.html) gives an erroneous Why file when analyzed with
frama-c -jessie-analysis file.c
Either jessie should exit with an appropriate error message, or the why compilation should succeed.
char T;
/*@
axiomatic foo {
logic char* foo{L}(integer x) = &T;
}
*/
/*@ predicate strcmp{L}(char *x, char* y) =
\forall integer i; (\forall integer j; 0<=j<i ==> *(x+j) !=0) ==>
*(x+i) == *(y+i);
*/
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2512
"//@ assert i >= CHAR_MIN;" not proven for char
2021-04-15T09:17:41Z
Jens Gerlach
"//@ assert i >= CHAR_MIN;" not proven for char
ID0000095:
**This issue was created automatically from Mantis Issue 95. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000095:
**This issue was created automatically from Mantis Issue 95. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000095 | Frama-C | Plug-in > jessie | public | 2009-05-25 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mottainai | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
The first assertion in the the following code fragment is not proven.
(neither alt-ergo nor yices nor cvc3).
char char_range(char i)
{
//@ assert i >= CHAR_MIN;
//@ assert i <= CHAR_MAX;
return i;
}
### Additional Information :
I am using Frama-C Lithium-20081201 on Mac OS X 10.5.7
This is probably related to bug http://bts.frama-c.com/view.php?id=94
https://git.frama-c.com/pub/frama-c/-/issues/2513
"assert i >= 0;" not proven for unsigned char
2021-04-15T09:17:41Z
Jens Gerlach
"assert i >= 0;" not proven for unsigned char
ID0000094:
**This issue was created automatically from Mantis Issue 94. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000094:
**This issue was created automatically from Mantis Issue 94. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000094 | Frama-C | Plug-in > jessie | public | 2009-05-25 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mottainai | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
The first assertion in the the following code fragment is not proven.
(neither alt-ergo nor yices nor cvc3).
unsigned char uchar_range(unsigned char i)
{
//@ assert i >= 0;
//@ assert i <= UCHAR_MAX;
return i;
}
### Additional Information :
I am using Frama-C Lithium-20081201 on Mac OS X 10.5.7
https://git.frama-c.com/pub/frama-c/-/issues/2357
Jessie: struct field's validity
2021-04-15T09:17:41Z
Dillon Pariente
Jessie: struct field's validity
ID0000102:
**This issue was created automatically from Mantis Issue 102. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000102:
**This issue was created automatically from Mantis Issue 102. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000102 | Frama-C | Plug-in > jessie | public | 2009-05-27 | 2010-07-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)
The following annotated code can not be proved by ATPs.
Function f() needs an invariant on global var v :
//@ global invariant aa: \valid(&v.c);
that should normally be generated automatically.
Function f2() needs a type invariant :
//@ type invariant Tt(las* l) = \valid(&(l->c)); but this type invariant is visibly not taken into account in the Why generated file (predicate Tt does exist but is not axiomatized).
Source code:
typedef struct { int c; } las;
las v;
//@ requires \valid(p);
void g(int * p);
void f(){ g(&v.c); }
//@ requires \valid(x);
void f2(las * x){ g(&(x->c)); }
Commande line:
frama-c -jessie-analysis -jessie-gui file.c
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2441
Jessie: infinite or not annotated loops
2021-04-15T09:17:41Z
Dillon Pariente
Jessie: infinite or not annotated loops
ID0000103:
**This issue was created automatically from Mantis Issue 103. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000103:
**This issue was created automatically from Mantis Issue 103. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000103 | Frama-C | Plug-in > jessie | public | 2009-05-27 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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** | - |
### Description :
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)
As all POs generated by Jessie/Why from the following annotated code are automatically discharged by ATPs, one might conclude that ensures clause is also validated! Which is not the case, of course!
Source code:
//@ requires \valid(p); assigns *p; ensures *p==4; void g(int*p){
int i=0;
while(1>0) { *p=3; }
}
Commande line:
frama-c -jessie-analysis -jessie-gui file.c
What could be done in Jessie to warn users about:
- the loop for which termination condition or loop variant are not provided?
- unreachable return control point due to infinite loop (=> no post-condition can be met)?
https://git.frama-c.com/pub/frama-c/-/issues/2539
Jessie: float_P[..] expected instead of real
2021-04-15T09:17:40Z
Dillon Pariente
Jessie: float_P[..] expected instead of real
ID0000105:
**This issue was created automatically from Mantis Issue 105. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000105:
**This issue was created automatically from Mantis Issue 105. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000105 | Frama-C | Plug-in > jessie | public | 2009-05-27 | 2009-05-28 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | - | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)
Please, find below the contents of files foo.c and foo.h:
//===== file foo.c
typedef struct {float k;} las;
void g (float * y);
void f (las *c) { g(&(c->k)); }
//===== file foo.h
typedef struct {float k;} las;
//@ requires \valid(c); assigns c->k;
void f (las * c);
command line:
frama-c.exe -jessie-analysis -jessie-gui foo.c foo.h
Error message:
Calling Jessie tool in subdir wholeprogram.jessie File "wholeprogram.jc", line 401, characters 15-26: typing error: type float_P[..] expected instead of real
Jessie subprocess failed: jessie -why-opt -split-user-conj -v
-why-opt -fast-wp -separation -locs wholeprogram.cloc w
holeprogram.jc
https://git.frama-c.com/pub/frama-c/-/issues/2540
Jessie: memory in memeory set
2021-04-15T09:17:40Z
Dillon Pariente
Jessie: memory in memeory set
ID0000106:
**This issue was created automatically from Mantis Issue 106. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000106:
**This issue was created automatically from Mantis Issue 106. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000106 | Frama-C | Plug-in > jessie | public | 2009-05-27 | 2009-05-28 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | - | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)
An uncaugth exception is generated on the followin code:
typedef struct {int i;int j;} las;
/*@ requires \valid(a) && \valid(b);
assigns *a, *b; */
void g (int *a,int *b){ *a=11; *b=15; }
/*@ requires \valid(p) ;
assigns p->i,p->j;
*/
void f (las *p)
{ g (&(p->i), &(p->j)); }
Command line:
frama-c.exe -jessie-analysis -jessie-gui foo.c
Error message:
memory (mem-field(int_M),b_2)
in memory set (mem-field(int_M),a_1),
(mem-field(int_M),b_2)
File "jc/jc_interp_misc.ml", line 714, characters 7-7:
Uncaught exception: File "jc/jc_interp_misc.ml", line 714, characters 7-13: Assertion failed
https://git.frama-c.com/pub/frama-c/-/issues/2437
(* TODO: parameters *)
2021-04-15T09:17:40Z
Sylvie Boldo
(* TODO: parameters *)
ID0000112:
**This issue was created automatically from Mantis Issue 112. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000112:
**This issue was created automatically from Mantis Issue 112. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000112 | Frama-C | Plug-in > jessie | public | 2009-06-02 | 2009-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sboldo | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
hello,
I am in trunk, svn version 5349.
I fell into an
assert false) (* TODO: parameters *)
which is at line 718 of jc/jc_interp_misc.ml
The C file is attached. It tackles loops with floating-point matrices.
Regards,
Sylvie Boldo
## Attachments
- [int_matrix.c](/uploads/684d06b33caba66a5c5c7b153c5f0bbb/int_matrix.c)
https://git.frama-c.com/pub/frama-c/-/issues/2537
Unable to verify pointer dereferencing
2021-04-15T09:17:39Z
mantis-gitlab-migration
Unable to verify pointer dereferencing
ID0000156:
**This issue was created automatically from Mantis Issue 156. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000156:
**This issue was created automatically from Mantis Issue 156. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000156 | Frama-C | Plug-in > jessie | public | 2009-06-09 | 2009-06-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | - | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Jessie is unable to verify pointer dereferencing in the following code:
/*@ requires \valid(a+ (left..right));
*/
void foo(int a[], int left, int right) {
int k;
k = a[right]; // Jessie fails here
}
https://git.frama-c.com/pub/frama-c/-/issues/1575
\at(...,Post) in assigns clause
2021-04-15T09:17:39Z
Dillon Pariente
\at(...,Post) in assigns clause
ID0000160:
**This issue was created automatically from Mantis Issue 160. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000160:
**This issue was created automatically from Mantis Issue 160. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000160 | Frama-C | Plug-in > jessie | public | 2009-06-22 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
"at"'s labels support in assigns clause is needed in Jessie to be able to discharge all behavioral POs from the following annotated test code:
typedef struct { int * rc; } S;
/*@ requires \valid(p) && \valid(p->rc) && \valid(r);
assigns *\at(p->rc,Post),p->rc; */
int main1( S* p,int* r)
{p->rc = r;
*(p->rc) = 55;
return 1;
}
//Command-line: frama-c -jessie-analysis e28.c