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/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/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/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/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/2509
Jessie: static function specification
2021-02-22T14:00:24Z
Dillon Pariente
Jessie: static function specification
ID0000104:
**This issue was created automatically from Mantis Issue 104. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000104:
**This issue was created automatically from Mantis Issue 104. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000104 | Frama-C | Kernel | public | 2009-05-27 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | virgile | **Resolution** | no change required |
| **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 :
(This issue was previously discussed through private messages but not fully resolved. It is now recorded into the BTS for traceability reasons.)
An annotated header file "foo.h" contains:
//***** foo.h
/*@ requires \valid(p); assigns *p; ensures *p==3; */ void f(int *p);
and this is the related "foo.c" file:
//***** foo.c
static void f(int *p) { *p = 3; }
Command line:
frama-c.byte.exe -jessie-analysis -jessie-gui foo.c foo.h
Logical specifications from foo.h file are - apparently - not taken into account in the generated POs.
https://git.frama-c.com/pub/frama-c/-/issues/2508
Compilation error if options --with-jessie-static --with-ltl_to_acsl-static a...
2021-02-22T14:00:22Z
mantis-gitlab-migration
Compilation error if options --with-jessie-static --with-ltl_to_acsl-static are present.
ID0000111:
**This issue was created automatically from Mantis Issue 111. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000111:
**This issue was created automatically from Mantis Issue 111. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000111 | Frama-C | Kernel | public | 2009-06-02 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nstouls | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | block | **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 :
With ocamlc 3.10.2
If the configure script is launched with following options :
--with-jessie-static --with-ltl_to_acsl-static
then this error occurs during compilation:
Ocamlc src/lib/dynlink_common_interface.cmo
The implementation src/lib/dynlink_common_interface.ml
does not match the interface src/lib/dynlink_common_interface.cmi:
The field `is_native' is required but not provided
make: *** [src/lib/dynlink_common_interface.cmo] Erreur 2
Removing configure options resolves the problem.
https://git.frama-c.com/pub/frama-c/-/issues/2506
int -> integer -> real
2022-12-25T02:32:53Z
Sylvie Boldo
int -> integer -> real
ID0000117:
**This issue was created automatically from Mantis Issue 117. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000117:
**This issue was created automatically from Mantis Issue 117. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000117 | Frama-C | Kernel | public | 2009-06-05 | 2009-06-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sboldo | **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 :
From ACSL, I assume that
"C integral types char , short , int and long , signed or unsigned, are all subtypes of type integer ;
integer is itself a subtype of type real ;"
Therefore int is a subtype of real. But it does not work in practice:
int i;
/*@ loop invariant C== \pow(2., i) */
\pow takes 2 real numbers.
This annotation is refused by the message:
Error during analysis of annotation: invalid implicit conversion from int to real
https://git.frama-c.com/pub/frama-c/-/issues/2496
Order of the functions in gui
2021-02-22T14:00:09Z
mantis-gitlab-migration
Order of the functions in gui
ID0000157:
**This issue was created automatically from Mantis Issue 157. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000157:
**This issue was created automatically from Mantis Issue 157. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000157 | Frama-C | Graphical User Interface | public | 2009-06-18 | 2009-06-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | monate | **Resolution** | won't fix |
| **Priority** | low | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The function list in the gui sidebar is in reverse order compared to the list of the functions in the C code.
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/2494
type error in generated why file
2021-04-15T09:17:39Z
Fabrice Derepas
type error in generated why file
ID0000178:
**This issue was created automatically from Mantis Issue 178. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000178:
**This issue was created automatically from Mantis Issue 178. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000178 | Frama-C | Plug-in > jessie | public | 2009-07-09 | 2009-07-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | derepas | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Let us consider the following program 'simple.c':
void g(int * j, int *k) {
int tmp= *j;
*j=*k;
*k=tmp;
}
void f(int * vector, int size) {
int i=0;
if (i<size)
g (&vector[i],&vector[i+1]);
}
The command line 'frama-c -main f -jessie simple.c' generates the following error:
[kernel...] preprocessing with "gcc -C -E -I. -dD simple.c"
Starting Jessie translation
Producing Jessie files in subdir simple.jessie
File simple.jessie/simple.jc written.
File simple.jessie/simple.cloc written.
Calling Jessie tool in subdir simple.jessie
Generating Why function g
Generating Why function f
Calling VCs generator.
gwhy-bin [...] why/simple.why
Computation of VCs...
File "why/simple.why", line 552, characters 9-49:
Term i is expected to have type int
make: *** [simple.stat] Erreur 1
Jessie subprocess failed: make -f simple.makefile gui
The funny thing is that when the body of function g is empty this error does not occur (though the error seems to be in function f).
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2493
Indicates errors in annotations when should not
2021-02-22T14:00:04Z
mantis-gitlab-migration
Indicates errors in annotations when should not
ID0000188:
**This issue was created automatically from Mantis Issue 188. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000188:
**This issue was created automatically from Mantis Issue 188. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000188 | Frama-C | Plug-in > slicing | public | 2009-07-14 | 2009-07-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | Anne | **Resolution** | won't fix |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
- jessie accepts this code and properly infers based on it, the slicing plug-in on the other hand indicates an error in the annotations
---------------------------------------------------------------------
test.c
---------------------------------------------------------------------
#include "test.h"
/*@
@ requires y == CONS_FROM_TEST_H_DEFINED_USING_DEFINE;
@ ensures
@ \result == 2*y;
@*/
int x(int y, int z)
{
/*@ slice pragma ctrl; */
//@ assert y == 1;
//@ assert y + z == 3;
return 2*y*z1();
}
int main()
{
x(1,2);
return 0;
}
int z1()
{
return 1;
}
-------------------------------------------------------------------------
test.h
-------------------------------------------------------------------------
#define CONS_FROM_TEST_H_DEFINED_USING_DEFINE 1
https://git.frama-c.com/pub/frama-c/-/issues/2492
Frama-C cannot process properly arrays of structures
2021-04-15T09:17:38Z
mantis-gitlab-migration
Frama-C cannot process properly arrays of structures
ID0000185:
**This issue was created automatically from Mantis Issue 185. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000185:
**This issue was created automatically from Mantis Issue 185. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000185 | Frama-C | Plug-in > jessie | public | 2009-07-14 | 2009-07-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | cmarche | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
This code leads to an error
x = &str_array[i1][i2].field1;
However, this (in fact the same code), is processed properly
struct str *temp = &str_array[i1][i2];
x = &(*temp).field1;
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2491
Slicing removes more code than it should
2021-02-22T14:00:01Z
mantis-gitlab-migration
Slicing removes more code than it should
ID0000201:
**This issue was created automatically from Mantis Issue 201. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000201:
**This issue was created automatically from Mantis Issue 201. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000201 | Frama-C | Plug-in > slicing | public | 2009-07-24 | 2009-07-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | Anne | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Slicing removes more code than it should leading to erronous results.
In the example below I wanted to leave the code which influences value of temp in fun(). To this end I used the following command. However, the obtained result (no slicing errors were indicated) presented below is not equivalnet to the input.
command-----------------------------------------------
frama-c -slice-print -slice-value temp -slicing-level 3 -main fun -lib-entry -pp-annot temp.c -ocode temp2.c
input-----------------------------------------------
#define arr *(unsigned char *)
#define Alarm1_On {arr(0) |= 0;}
#define Alarm1_Off {arr(0) |= 0;}
int temp;
int temp2;
void fun()
{
temp = 2;
fun2();
}
void fun2()
{
if (temp2)
{
temp = 0;
Alarm1_Off;
}
else
{
temp = 1;
Alarm1_On;
}
}
output----------------------------------------------
/* Generated by CIL v. 1.3.6 */
/* print_CIL_Input is false */
void fun(void)
{
return;
}
https://git.frama-c.com/pub/frama-c/-/issues/2490
-slice-print ignored when -ocode is used
2021-02-22T13:59:59Z
mantis-gitlab-migration
-slice-print ignored when -ocode is used
ID0000191:
**This issue was created automatically from Mantis Issue 191. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000191:
**This issue was created automatically from Mantis Issue 191. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000191 | Frama-C | Plug-in > slicing | public | 2009-07-15 | 2009-07-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
when I use the option -slice-print together with -ocode then -slice-print is ignored
https://git.frama-c.com/pub/frama-c/-/issues/2489
Mise en hypothèse de la précondition d'une opération appelée
2021-04-15T09:17:38Z
mantis-gitlab-migration
Mise en hypothèse de la précondition d'une opération appelée
ID0000215:
**This issue was created automatically from Mantis Issue 215. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000215:
**This issue was created automatically from Mantis Issue 215. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000215 | Frama-C | Plug-in > jessie | public | 2009-08-24 | 2009-08-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | nstouls | **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 :
bonjour,
Voici donc un petit exemple en pièce jointe.
Si je souhaite le prouver avec Jessie :
frama-c t2.c -jessie &
J'obtiens 5 OP.
Celles qui m'intéressent sont les 2 OP de post-condition du main. Prenons par exemple la première des deux :
main_ensures_default_po_1
H1: true = true and (0 <= integer_of_int32(i) and integer_of_int32(i) <= 1)
result: int32
H6: (integer_of_int32(i) = 1 -> integer_of_int32(result) = 1) and
(integer_of_int32(i) = 0 -> integer_of_int32(result) = 0)
tmp: int32
H7: tmp = result
H8: integer_of_int32(tmp) <> 0
result0: int32
H9: integer_of_int32(result0) = 0
__retres: int32
H10: __retres = result0
return: int32
H11: return = __retres
----------------------------------
integer_of_int32(return) = 0
H1 correspond à la pré-condition de main
H6 est issue de l'appel de fonction f(). C'est la conjonction des assumes impliquant les ensures associés
H7 et + correspond au code de la fonction main.
Dans cet exemple, il n'y a pas d'hypothèse H5 décrivant la pré-condition de f(), alors qu'elle devrait être présente.
En l'occurrence, cette pré-condition étant équivalente à H1, tout se prouve. Mais lorsqu'il est nécessaire de faire un preuve difficile pour faire ce lien, il serait intéressant d'avoir ensuite la pré de f en hypothèse.
Merci beaucoup et bonne journée,
Nicolas.
## Attachments
- [t2.c](/uploads/81e75022140928f05c14dffa872247fd/t2.c)
Claude Marché
Claude Marché
https://git.frama-c.com/pub/frama-c/-/issues/2488
An extra ')' is missing in the Printexc.record_backtrace patch on the Frama-C...
2021-02-22T13:59:57Z
mantis-gitlab-migration
An extra ')' is missing in the Printexc.record_backtrace patch on the Frama-C wiki
ID0000181:
**This issue was created automatically from Mantis Issue 181. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000181:
**This issue was created automatically from Mantis Issue 181. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000181 | Frama-C | Kernel | public | 2009-07-13 | 2009-08-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jonathan-Christofer Demay | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
http://bts.frama-c.com/view.php?id=169 is fixed by a patch posted on the Frama-C wiki (http://bts.frama-c.com/dokuwiki/lib/exe/fetch.php?media=wiki:frama-c-beryllium-20090601-beta1.patch)
However, I think near the end an extra ')' is missing:
- (Printexc.to_string e)
- (if Parameters.Debug.get () > 0 then Printexc.get_backtrace ()
- else ""));
+ (Printexc.to_string e);
It should be:
+ (Printexc.to_string e));
https://git.frama-c.com/pub/frama-c/-/issues/2487
Slicing leaves unreachable code
2021-02-22T13:59:57Z
mantis-gitlab-migration
Slicing leaves unreachable code
ID0000194:
**This issue was created automatically from Mantis Issue 194. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000194:
**This issue was created automatically from Mantis Issue 194. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000194 | Frama-C | Plug-in > slicing | public | 2009-07-15 | 2009-08-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | Anne | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | - |
### Description :
/*@ requires
@ (((v1 && !(v2 && v3) && v4);
@*/
extern void fun(void)
{
if (v1) {
if (v4) {
if (v2) {
if(v3) {goto return_label;}
}
}
}
}
### Additional Information :
It would be nice if slicing could remove such code.
https://git.frama-c.com/pub/frama-c/-/issues/2482
'make top' fails
2021-02-22T13:59:51Z
mantis-gitlab-migration
'make top' fails
ID0000183:
**This issue was created automatically from Mantis Issue 183. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000183:
**This issue was created automatically from Mantis Issue 183. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000183 | Frama-C | Kernel | public | 2009-07-13 | 2009-09-02 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jonathan-Christofer Demay | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
frama-c-Beryllium-20090601-beta1 # make top
Ocamlc src/toplevel/toplevel_topdirs.cmo
Ocamlmktop bin/toplevel.top
Error while linking src/lib/extlib.cmo:
The external function `getperfcount' is not available
make: *** [bin/toplevel.top] Error 2