frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-04-15T09:17:43Z
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/1551
code normalisation issue when return variable is named __retres
2021-02-22T13:34:30Z
David Delmas
code normalisation issue when return variable is named __retres
ID0000059:
**This issue was created automatically from Mantis Issue 59. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000059:
**This issue was created automatically from Mantis Issue 59. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000059 | Frama-C | Kernel | public | 2009-04-23 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ddelmas | **Assigned To** | monate | **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 :
"frama-c file.c -print" outputs non-compilable code for examples such as the following :
float g()
{
double __retres=2;
return __retres;
}
On this example, the output is the following :
float g(void)
{ double __retres ;
float __retres ;
{__retres = (double )2;
__retres = (float )__retres;
return (__retres);}
}
Because of the normalisation scheme, variable __retres is being defined twice, with conflicting types.
https://git.frama-c.com/pub/frama-c/-/issues/1550
Conversion from integer to real
2021-02-22T14:03:21Z
Guillaume Melquiond
Conversion from integer to real
ID0000060:
**This issue was created automatically from Mantis Issue 60. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000060:
**This issue was created automatically from Mantis Issue 60. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000060 | Frama-C | Kernel | public | 2009-04-23 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gmelquio | **Assigned To** | virgile | **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-20090601-beta1 |
### Description :
While the documentation says that "there are implicit coercions for numeric types: integer is itself a subtype of type real" and that cast are allowed in logic expressions, neither seem to work.
/*@ ensures 1.0 == 1; */
void f();
/*@ ensures 1.0 == (real)1; */
void g();
When running "frama-c test.c" (revision 5096), I get
File test.c, line 1, characters 19-20:
Error during analysis of annotation: invalid cast between real and integer. Use conversion functions instead
test.c:1: Warning: Ignoring specification of function f
File test.c, line 4, characters 19-26:
Error during analysis of annotation: cannot cast to logic type
test.c:4: Warning: Ignoring specification of function g
The error message talks about some "conversion functions", but there are no such things in the documentation. The Jessie plugin seems to know about a \real_of_int function, but the CIL front end does not. So how does one convert an integer to a real, if neither implicit nor explicit casts work?
https://git.frama-c.com/pub/frama-c/-/issues/2519
frama-c --help
2021-02-22T14:04:56Z
Guillaume Melquiond
frama-c --help
ID0000061:
**This issue was created automatically from Mantis Issue 61. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000061:
**This issue was created automatically from Mantis Issue 61. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000061 | Frama-C | Kernel | public | 2009-04-24 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gmelquio | **Assigned To** | signoles | **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 Beryllium-20090601-beta1 |
### Description :
$ frama-c --help
frama-c: option `--help' is unknown.
Use `frama-c --help' for more information.
Yeah, right... (revision 5126)
https://git.frama-c.com/pub/frama-c/-/issues/1549
integer is not well-casted in real
2021-02-22T14:03:20Z
Sylvie Boldo
integer is not well-casted in real
ID0000062:
**This issue was created automatically from Mantis Issue 62. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000062:
**This issue was created automatically from Mantis Issue 62. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000062 | Frama-C | Kernel | public | 2009-04-24 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sboldo | **Assigned To** | virgile | **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 Beryllium-20090601-beta1 |
### Description :
The following program fails with
"Error during analysis of annotation: invalid cast between real and integer. Use conversion functions instead"
But it works with int instead of integer....
/*@ axiomatic toto {
@ logic integer g;
@ } */
void f() {
double B;
/*@ assert B==g; */
}
### Additional Information :
Release ID: 5098
https://git.frama-c.com/pub/frama-c/-/issues/1597
Plug-in inout fails to parse clause /*@ assigns s[..]; */
2021-02-22T14:03:27Z
David Delmas
Plug-in inout fails to parse clause /*@ assigns s[..]; */
ID0000068:
**This issue was created automatically from Mantis Issue 68. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000068:
**This issue was created automatically from Mantis Issue 68. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000068 | Frama-C | Plug-in > Eva | public | 2009-04-28 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ddelmas | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | Frama-C Boron-20100401 | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
Consider the following example:
//@ assigns s[..];
void F1(char *s);
char T[100];
void F2(int c)
{
if (c) F1(T);
}
Running "frama-c file.c -main F2 -lib-entry -out" yields a parse error.
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/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/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/1554
int a; main(){ return 100 / (int)(&a + 2); } fails to report a division by zero
2021-02-22T13:34:33Z
Pascal Cuoq
int a; main(){ return 100 / (int)(&a + 2); } fails to report a division by zero
ID0000076:
**This issue was created automatically from Mantis Issue 76. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000076:
**This issue was created automatically from Mantis Issue 76. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000076 | Frama-C | Plug-in > Eva | public | 2009-05-04 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
See summary
https://git.frama-c.com/pub/frama-c/-/issues/1553
if((int)(&a+2)) fails to warn about being unspecified
2021-02-22T13:34:32Z
Pascal Cuoq
if((int)(&a+2)) fails to warn about being unspecified
ID0000077:
**This issue was created automatically from Mantis Issue 77. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000077:
**This issue was created automatically from Mantis Issue 77. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000077 | Frama-C | Plug-in > Eva | public | 2009-05-05 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **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 Beryllium-20090601-beta1 |
### Description :
see summary.
This is related to bug 76, which is fixed and partially fixes
this problem too: at least the condition is correctly
analyzed as being 0 or 1. But the policy is to emit an alarm
(that is complicated to express, but that's another issue)
and to consider the condition to be 1 modulo the verification
of the alarm.
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/2427
Better support of //@ style
2021-02-22T14:01:36Z
mantis-gitlab-migration
Better support of //@ style
ID0000079:
**This issue was created automatically from Mantis Issue 79. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000079:
**This issue was created automatically from Mantis Issue 79. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000079 | Frama-C | Kernel > ACSL implementation | public | 2009-05-11 | 2010-02-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Lithium-20081201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Annotation consisting of several //@ lines should be supported. Eg, the following code produces a syntax error, whereas the /*@ ... */ style works:
//@ loop invariant a[0] == 1;
//@ loop invariant 1 <= i;
for(i=1; i<10; i++)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/1569
Frama-C should stop on error in annotations instead of issuing a warning
2021-02-22T13:34:53Z
David Mentré
Frama-C should stop on error in annotations instead of issuing a warning
ID0000088:
**This issue was created automatically from Mantis Issue 88. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000088:
**This issue was created automatically from Mantis Issue 88. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000088 | Frama-C | Kernel | public | 2009-05-19 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dmentre | **Assigned To** | virgile | **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 Beryllium-20090601-beta1 |
### Description :
Hello,
Currently, Frama-C is issuing a warning if there is a typo in an annotation and ignores the annotation.
Typically once have:
"""
File jenn-issue.c, line 13, characters 55-56:
Error during analysis of annotation: unbound logic variable k
jenn-issue.c:13: Warning: ignoring logic code annotation
"""
I think this issue is source of errors and further issues for the user.
Instead, Frama-C should stop processing the file and issue a fatal error.
Of course, one could add a command line option to restore current behaviour for legitimate(?) use.
Yours,
david
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/1809
Remove generated annotations from slicing results
2021-02-22T14:01:49Z
mantis-gitlab-migration
Remove generated annotations from slicing results
ID0000090:
**This issue was created automatically from Mantis Issue 90. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000090:
**This issue was created automatically from Mantis Issue 90. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000090 | Frama-C | Plug-in > slicing | public | 2009-05-20 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
We should only keep user annotations : generated annotations will be regenerated by the analysis of the new project.
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/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/2495
"logic set<struct something *> f(...)" throw a syntax error
2021-02-22T14:00:07Z
François Bobot
"logic set<struct something *> f(...)" throw a syntax error
ID0000096:
**This issue was created automatically from Mantis Issue 96. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |...
ID0000096:
**This issue was created automatically from Mantis Issue 96. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000096 | Frama-C | Kernel | public | 2009-05-25 | 2009-07-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | bobot | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | Frama-C Beryllium-20090601-beta1 | **Fixed in Version** | Frama-C Beryllium-20090601-beta1 |
### Description :
============
typedef struct node {
int hd;
struct list * next;
} list;
/*@
logic set<struct node *> tata(struct node * p) = \empty;
@*/
=============
throw:
File "empty.c", line 7, characters 19-23: syntax error while parsing annotation
However there is a natural work around :
=============
/*@
logic set<list *> tata(struct node * p) = \empty;
@*/
=============
is correct.
### Additional Information :
svn id : 5303
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