frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-02-22T14:04:39Z
https://git.frama-c.com/pub/frama-c/-/issues/2336
Don't edit files in make install. Instead, just use all plug-ins in the plugi...
2021-02-22T14:04:39Z
mantis-gitlab-migration
Don't edit files in make install. Instead, just use all plug-ins in the plugin directory
ID0000606:
**This issue was created automatically from Mantis Issue 606. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000606:
**This issue was created automatically from Mantis Issue 606. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000606 | Frama-C | Kernel > Makefile | public | 2010-10-13 | 2010-12-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dwheeler | **Assigned To** | signoles | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
The current Frama-C architecture makes packaging Frama-C (and anything using it) unnecessarily difficult. Mark Rader and I managed to package "Frama-C" and "Why" for Fedora, but a few minor changes to Frama-C would make it MUCH easier to package and install (and thus update in the future).
In particular, please change Frama-C so that adding or removing a plug-in does NOT require any file contents to be changed. Instead, Frama-C should just look at the plug-in directory, and presume that all files in that directory (with the proper extensions) are to be used. That way, to add a plug-in, an installer only needs to add a file to that directory; to remove the plug-in, the installer only needs to remove the files in that directory.
This would also require changing the Frama-C "Makefile.dynamic" file so that installation would never modify the file "$(FRAMAC_SHARE)/known_plugins.ac"
or any other file during "make install".
The reason is that modern packaging systems (e.g. rpm of Red Hat/Fedora/Novell/SuSE and deb for Debian/Ubuntu) separate the install step into TWO stages. The first one, which does NOT have root privileges, is done by the distributor to create a package; this normally runs "make install DESTDIR=tempdir". The contents of tempdir are then stored in the package.
When the user installs the package, that is the second stage, but normally that just copies files and that's it.
Thanks!
### Additional Information :
For more about how to make source releases easy to install, please see:
"Releasing Free/Libre/Open Source Software (FLOSS) for Source Installation"
http://www.dwheeler.com/essays/releasing-floss-software.html
https://git.frama-c.com/pub/frama-c/-/issues/2335
crashed value analysis
2021-02-22T13:56:46Z
mantis-gitlab-migration
crashed value analysis
ID0000547:
**This issue was created automatically from Mantis Issue 547. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000547:
**This issue was created automatically from Mantis Issue 547. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000547 | Frama-C | Kernel | public | 2010-07-23 | 2010-12-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | amkhalid | **Assigned To** | - | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
[kernel] The full backtrace is:
Raised at file "cil/src/cil.ml", line 2228, characters 30-31
Called from file "src/memory_state/locations.ml", line 490, characters 14-32
Called from file "src/memory_state/locations.ml", line 498, characters 45-64
Called from file "src/value/eval.ml", line 4772, characters 17-49
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval.ml", line 4768, characters 3-206
Called from file "src/value/eval.ml", line 4811, characters 4-67
Called from file "src/value/eval.ml", line 5155, characters 11-44
Re-raised at file "src/value/eval.ml", line 5170, characters 47-50
Called from file "src/project/computation.ml", line 914, characters 2-6
Re-raised at file "src/project/computation.ml", line 918, characters 8-11
Called from file "src/value/register.ml", line 58, characters 4-24
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 50, characters 4-20
Called from file "src/kernel/cmdline.ml", line 170, characters 4-8
Unexpected error (Cil.SizeOfError("abstract type: empty struct exist only with MSVC (comp struct huft)", _)).
Please report as 'crash' at http://bts.frama-c.com
https://git.frama-c.com/pub/frama-c/-/issues/2334
Crash in
2021-02-22T13:56:45Z
mantis-gitlab-migration
Crash in
ID0000333:
**This issue was created automatically from Mantis Issue 333. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000333:
**This issue was created automatically from Mantis Issue 333. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000333 | Frama-C | Plug-in > security slicing | public | 2009-11-17 | 2010-12-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | rovar | **Assigned To** | pascal | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
bspclient/bsp_client.c:411:[kernel] warning: more than 200(1799) elements to enumerate. Approximating.
[kernel] Unexpected error (File "src/memory_state/lmap_bitwise.ml", line 586, characters 4-10: Assertion failed).
### Additional Information :
The offending line in ML
let copy_paste_map ~f src_loc dst_loc mm =
assert (Int_Base.equal src_loc.size dst_loc.size );
I think the offending C source line it was processing was:
pgsessdes->type = SYS_TYPE_GWY;
where pgsessdes is a simple struct, type is an int, and SYS_TYPE_GWY is #defined to 0.
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/2331
Uncaught exception: assert false on bitvector
2021-04-15T09:17:34Z
Dillon Pariente
Uncaught exception: assert false on bitvector
ID0000273:
**This issue was created automatically from Mantis Issue 273. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000273:
**This issue was created automatically from Mantis Issue 273. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000273 | Frama-C | Plug-in > jessie | public | 2009-10-08 | 2010-12-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
Command line: frama-c -jessie foo.c
with foo.c containing:
/* ==================================== */
typedef float real;
struct T26_27 { real _F0 ; real _F1 ; };
typedef struct T26_27 _T26;
struct T28_29 { _T26 _F0 ; _T26 _F1 ; };
typedef struct T28_29 _T28;
typedef _T28 RR;
void f(RR const *tab , real *y )
{ *y = (float )(double )(*((real *)tab + 1)); }
/* ==================================== */
yields:
Uncaught exception: File "jc/jc_interp.ml", line 1819, characters 1-7: Assertion failed
Any means allowing to overcome temporarily this exception (by modifying the C source code) will be welcome!
Regards,
Dillon
### Additional Information :
fixed in Why 2.21
https://git.frama-c.com/pub/frama-c/-/issues/2330
Error while processing legitimate C construction
2021-04-15T09:17:39Z
mantis-gitlab-migration
Error while processing legitimate C construction
ID0000187:
**This issue was created automatically from Mantis Issue 187. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000187:
**This issue was created automatically from Mantis Issue 187. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000187 | Frama-C | Plug-in > jessie | public | 2009-07-14 | 2010-12-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | lukaszc | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090601-beta1 | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090902 |
### Description :
The system generates an error when encounters the following code:
PTT & 0x10
where PTT is of type (unsigned char*)
### Additional Information :
Fixed in Why 2.20
https://git.frama-c.com/pub/frama-c/-/issues/2329
Decreases clause
2021-04-15T09:17:27Z
Dillon Pariente
Decreases clause
ID0000369:
**This issue was created automatically from Mantis Issue 369. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000369:
**This issue was created automatically from Mantis Issue 369. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000369 | Frama-C | Plug-in > jessie | public | 2010-01-13 | 2010-12-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dpariente | **Assigned To** | cmarche | **Resolution** | duplicate |
| **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 :
When analyzing the following annotated code by "frama-c -jessie", one PO related to 'decreases' clause can not be discharged by ATP.
This problem might be related to BTS#102 (Frama-C team said in previous discussions).
///////////////////////////////////////////////////
# pragma JessieIntegerModel(exact)
typedef struct qr { int q; int r; } qr;
// md is a recursive function
/*@ requires d>0 && n>=0;
decreases n;
*/
qr md(int n,int d)
{ int q,r; qr v;
if (n==0)
{ v.q = 0;
v.r = 0;
return v;
} else { v = md(n-1,d);
return v;
}
}
https://git.frama-c.com/pub/frama-c/-/issues/2328
Jessie translation unexpected failure
2021-04-15T09:17:24Z
Victoria Moya Lamiel
Jessie translation unexpected failure
ID0000410:
**This issue was created automatically from Mantis Issue 410. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000410:
**This issue was created automatically from Mantis Issue 410. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000410 | Frama-C | Plug-in > jessie | public | 2010-02-17 | 2010-12-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | vmoyalam | **Assigned To** | cmarche | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Jessie crashes on the attached file.
WHY version : 2.21
command : "frama-c -jessie test.c".
### Additional Information :
It seems there is a problem with structure comparisons.
Command-line output :
[kernel] preprocessing with "gcc -C -E -I. -dD test.c"
[jessie] Starting Jessie translation
test.c:14:[jessie] failure: Unexpected failure.
Please submit bug report (Ref. "interp.ml:631:14").
[kernel] Plugin jessie aborted because of an internal error.
Please report with 'crash' at http://bts.frama-c.com
## Attachments
- [test.c](/uploads/f198f20d8a427daa21da709b89e888a4/test.c)
https://git.frama-c.com/pub/frama-c/-/issues/2325
error in analyzing xen 4.0.0 code
2021-02-22T13:56:34Z
mantis-gitlab-migration
error in analyzing xen 4.0.0 code
ID0000516:
**This issue was created automatically from Mantis Issue 516. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000516:
**This issue was created automatically from Mantis Issue 516. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000516 | Frama-C | Plug-in > Eva | public | 2010-06-19 | 2010-12-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | amkhalid | **Assigned To** | pascal | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
[kernel] Parsing stage early
[kernel] Parsing stage extending
[kernel] Parsing stage extended
[kernel] Parsing stage exiting
[kernel] Parsing stage loading
[kernel] Parsing stage configuring
[kernel] preprocessing with "gcc -C -E -I. -I/home/ak729/xen-4.0.0/xen/include/ /home/ak729/xen-4.0.0/xen/common/kernel.c"
/home/ak729/xen-4.0.0/xen/include/public/domctl.h:51:[kernel] user error: syntax error
[kernel] The full backtrace is:
[kernel] Raised at file "cil/src/frontc/frontc.ml", line 209, characters 9-28
[kernel] Called from file "cil/src/frontc/frontc.ml", line 124, characters 13-38
[kernel] Called from file "cil/src/frontc/frontc.ml", line 263, characters 13-32
[kernel] Called from file "src/kernel/file.ml", line 546, characters 27-46
[kernel] Called from file "src/kernel/file.ml", line 582, characters 16-23
[kernel] Re-raised at file "src/kernel/file.ml", line 585, characters 52-55
[kernel] Called from file "list.ml", line 74, characters 24-34
[kernel] Called from file "src/kernel/file.ml", line 579, characters 6-314
[kernel] Called from file "src/kernel/file.ml", line 1027, characters 12-30
[kernel] Called from file "src/kernel/file.ml", line 1108, characters 4-27
[kernel] Called from file "src/kernel/ast.ml", line 57, characters 29-45
[kernel] Called from file "src/project/computation.ml", line 108, characters 17-21
[kernel] Called from file "src/kernel/file.ml", line 1147, characters 12-22
[kernel] Called from file "src/project/project.ml", line 432, characters 12-15
[kernel] Re-raised at file "src/project/project.ml", line 437, characters 10-11
[kernel] Called from file "src/kernel/boot.ml", line 44, characters 33-47
[kernel] Called from file "src/kernel/cmdline.ml", line 170, characters 4-8
[kernel]
[kernel] Unexpected error (Parsing.Parse_error).
[kernel] Please report as 'crash' at http://bts.frama-c.com
https://git.frama-c.com/pub/frama-c/-/issues/2309
incorrect(?) jessie code generated from strcpy
2021-04-15T09:17:14Z
mantis-gitlab-migration
incorrect(?) jessie code generated from strcpy
ID0000584:
**This issue was created automatically from Mantis Issue 584. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000584:
**This issue was created automatically from Mantis Issue 584. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000584 | Frama-C | Plug-in > jessie | public | 2010-09-15 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pippijn | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
The following code:
// BEGIN
#include <string.h>
char *c_strcpy (char *dest, const char *src)
{
return strcpy (dest, src);
}
// END
causes the following diagnostics:
// BEGIN
$ frama-c -cpp-extra-args=-I`frama-c -print-path`/libc -jessie first.c
[kernel] preprocessing with "gcc -C -E -I. -I/usr/share/frama-c/libc -dD first.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir first.jessie
[jessie] File first.jessie/first.jc written.
[jessie] File first.jessie/first.cloc written.
[jessie] Calling Jessie tool in subdir first.jessie
File "first.jc", line 352, characters 22-39: typing error: label `Here' not found
[jessie] user error: Jessie subprocess failed: jessie -why-opt -split-user-conj -v -locs first.cloc first.jc
// END
Generated .jc file attached.
### Additional Information :
$ frama-c -v
Version: Boron-20100401
Compilation date: Fri Jul 16 12:28:04 UTC 2010
Share path: /usr/share/frama-c (may be overridden with FRAMAC_SHARE variable)
Library path: /usr/lib/frama-c (may be overridden with FRAMAC_LIB variable)
Plug-in paths: /usr/lib/frama-c/plugins (may be overridden with FRAMAC_PLUGIN variable)
$ uname -a
Linux osiris 2.6.32-5-amd64 #1 SMP Wed Aug 25 13:59:41 UTC 2010 x86_64 GNU/Linux
## Attachments
- [first.jc](/uploads/0a55516427088f86603578786b9d355e/first.jc)
https://git.frama-c.com/pub/frama-c/-/issues/2308
Default assigns generation
2021-02-22T13:56:15Z
Patrick Baudin
Default assigns generation
ID0000620:
**This issue was created automatically from Mantis Issue 620. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000620:
**This issue was created automatically from Mantis Issue 620. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000620 | Frama-C | Kernel | public | 2010-11-05 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
Today, Frama-C kernel generates assigns clauses from the prototype (for function without code).
To do nothing is equivalent to virtually generate "assigns everything".
That is not good for some static analysis (such as Value analysis).
When behaviors are completes and each of them has an assigns clause,
it is possible to generate a more restrictive clause (than "assigns everything"), but still correct:
"assigns locs;"
where "locs" is the union of the locations assigned by all behaviors of the complete clause.
### Additional Information :
With this example, the clause "assigns *b" can be added to the default behavior.
requires \valid(b);
behavior positive:
assumes a > 0;
assigns *b;
ensures *b == 0;
behavior not_positive:
assumes a <= 0;
assigns \nothing;
complete behaviors;
disjoint behaviors;
*/ void foo(int a, int* b);
https://git.frama-c.com/pub/frama-c/-/issues/2304
Checking number of arguments passed to C functions
2021-02-22T13:56:10Z
Pascal Cuoq
Checking number of arguments passed to C functions
ID0000552:
**This issue was created automatically from Mantis Issue 552. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000552:
**This issue was created automatically from Mantis Issue 552. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000552 | Frama-C | Kernel | public | 2010-08-02 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
There currently isn't much checking of function arguments in the front-end. The following program is accepted, although it passes the wrong number of arguments for both calls to retint:
int retint(int x )
{
int __retres ;
__retres = 42 + x;
return (__retres);
}
int main(int c )
{
int x ;
int tmp ;
x = retint();
tmp = retint(c,c);
return (tmp);
}
Arguments for not implementing this feature: there are perfectly good compilers to check for this, and not having rigid rules in place may even help with older code containing variadic functions. I am not sure when the current convention for declaring variadic functions became standardized, and it may not have been from the beginning.
https://git.frama-c.com/pub/frama-c/-/issues/2301
slicing produces uncompilable program when formal used as a local variable
2021-02-22T13:56:05Z
Pascal Cuoq
slicing produces uncompilable program when formal used as a local variable
ID0000529:
**This issue was created automatically from Mantis Issue 529. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000529:
**This issue was created automatically from Mantis Issue 529. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000529 | Frama-C | Plug-in > sparecode | public | 2010-07-06 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
Alu:day_2 pascal$ cat s.c
main(int x, int y, int z){
int A, B;
A = x;
y = A;
B = y;
return B;
}
Alu:day_2 pascal$ frama-c -sparecode-analysis s.c
...
/* Generated by Frama-C */
int main(int x )
{
int A ;
int B ;
A = x;
y = A;
B = y;
return (B);
}
The generated program misses a declaration for y.
https://git.frama-c.com/pub/frama-c/-/issues/2299
Frama-C should produce more specific error messages when parsing annotations
2021-02-22T14:04:36Z
mantis-gitlab-migration
Frama-C should produce more specific error messages when parsing annotations
ID0000538:
**This issue was created automatically from Mantis Issue 538. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000538:
**This issue was created automatically from Mantis Issue 538. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000538 | Frama-C | Kernel | public | 2010-07-09 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
If an annotation contains a syntax error, Frama-C should be more specific about the kind of error.
For example, given a source file that contains this line
//@ loop invariant \forall integer i; aLength-1 >= i > high ==> a[i] > val);
a more helpful report may be:
foo.c, line 24: ')' unexpected
//@ loop invariant \forall integer i; aLength-1 >= i > high ==> a[i] > val);
^ here
https://git.frama-c.com/pub/frama-c/-/issues/2296
inchoherence of types between enumitems and enum type with multi-files
2021-02-22T13:55:56Z
Stephane Duprat
inchoherence of types between enumitems and enum type with multi-files
ID0000525:
**This issue was created automatically from Mantis Issue 525. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000525:
**This issue was created automatically from Mantis Issue 525. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000525 | Frama-C | Kernel | public | 2010-06-30 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sduprat | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
When a same type definition of enum is used in several files, but in different order, the type of the enumitem is desynchronised with the enum type.
### Additional Information :
In the following case (see archive files), the output of the demonstrator plugin indicates that :
exp p1 of type enum __anonenum_T_EN1_1
exp E1 of type enum __anonenum_T_EN1_2
So, this prevent us of comparing both types to check their compatibility.
The enumitem is always in the form of __anonenum_<type>.
The var is of Tname type refering to an other anonenum type.
If we reorder the type declarations in source1, the problem will disappear.
There is no problem with just one file at a time.
scripts
- build the plugin (make all install)
- run "frama-c -test1 source1.c source2.c"
[virgile-20100701]
note: the test1.ml in the archive will not compile against current svn. Use the one provided separately instead
## Attachments
- [enums.tar.gz](/uploads/f7802583d8dd19760d29160a2191c2db/enums.tar.gz)
- [test1.ml](/uploads/a937f4b7784dd1dd09e94a237d556bb1/test1.ml)
https://git.frama-c.com/pub/frama-c/-/issues/2294
Makefile.dynamic should not change known_plugins.ac
2021-02-22T14:04:39Z
mantis-gitlab-migration
Makefile.dynamic should not change known_plugins.ac
ID0000462:
**This issue was created automatically from Mantis Issue 462. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000462:
**This issue was created automatically from Mantis Issue 462. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000462 | Frama-C | Kernel > Makefile | public | 2010-04-27 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | mehdi | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
I'm not sure whether this is a bug or a feature, but in my understanding, installing an external plugin for Frama-C should not modify the files installed by Frama-C itself.
In this specific case, when the Jessie plugin wants to install, 'Makefile.dynamic' tells to append a line in '/usr/share/frama-c/known_plugins.ac'. If the user doesn't have write access on 'known_plugins.ac', the installation fails. Specifically, this would have lead to a build failure on any Debian build daemon. For now, I've desactivated this "feature" in 'Makefile.dynamic' using the attached patch.
'known_plugins.ac' is used only by the configure scripts of aorai and security_slicing. IMHO, they should rely on the existence of plugin files rather than some text file with (potentially) random content.
## Attachments
- [0005-Don-t-modify-system-files.patch](/uploads/a2a99b05668822004392ce1b153044af/0005-Don-t-modify-system-files.patch)
https://git.frama-c.com/pub/frama-c/-/issues/2282
for behav : invariant INV ;
2021-02-22T13:55:32Z
Patrick Baudin
for behav : invariant INV ;
ID0000482:
**This issue was created automatically from Mantis Issue 482. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000482:
**This issue was created automatically from Mantis Issue 482. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000482 | Frama-C | Kernel > ACSL implementation | public | 2010-05-17 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
Invariant clauses can be associated to named behaviors like assert clauses.
https://git.frama-c.com/pub/frama-c/-/issues/2281
Stoping external process (why)
2021-02-22T13:55:31Z
mantis-gitlab-migration
Stoping external process (why)
ID0000569:
**This issue was created automatically from Mantis Issue 569. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000569:
**This issue was created automatically from Mantis Issue 569. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000569 | Frama-C | Graphical User Interface | public | 2010-08-23 | 2010-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | monate | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101201-beta1 |
### Description :
For instance, when proving a property with WP, WHY processes are running.
When the user stop the computation (STOP button), is it possible to also stop those external processes ?
https://git.frama-c.com/pub/frama-c/-/issues/2278
Jessie internal error
2021-04-15T09:17:22Z
David Delmas
Jessie internal error
ID0000426:
**This issue was created automatically from Mantis Issue 426. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000426:
**This issue was created automatically from Mantis Issue 426. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000426 | Frama-C | Plug-in > jessie | public | 2010-03-12 | 2010-12-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ddelmas | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101202-beta2 |
### Description :
Running 'frama-c -jessie crash.c' on the attached source file (with either Why 2.21 or 2.23) crashes Jessie :
[kernel] preprocessing with "gcc -C -E -I. -dD crash.c"
[jessie] Starting Jessie translation
crash.c:8:[jessie] failure: Unexpected failure.
Please submit bug report (Ref. "norm.ml:1122:50").
[kernel] Plugin jessie aborted because of an internal error.
Please report with 'crash' at http://bts.frama-c.com
## Attachments
- [crash.c](/uploads/826e0c4dab17ac14dcdd9a6c66221a14/crash.c)
https://git.frama-c.com/pub/frama-c/-/issues/2277
Jessie crashes on \old(*ptr)
2021-04-15T09:17:22Z
mantis-gitlab-migration
Jessie crashes on \old(*ptr)
ID0000427:
**This issue was created automatically from Mantis Issue 427. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000427:
**This issue was created automatically from Mantis Issue 427. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000427 | Frama-C | Plug-in > jessie | public | 2010-03-13 | 2010-12-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | clandcx | **Assigned To** | cmarche | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20101202-beta2 |
### Description :
$ frama-c --version
Version: Beryllium-20090902
$ uname -a
FreeBSD viper.internal.network 8.0-RELEASE-p2
FreeBSD 8.0-RELEASE-p2 #0: Tue Jan 5 21:11:58 UTC 2010
root@amd64-builder.daemonology.net:/usr/obj/usr/src/sys/GENERIC amd64
Jessie crashes with the following (probably invalid) set of annotations.
Specifically, the problem line is:
@ ensures !stack_full (\old (*stack)) ==> \old(stack->used) < stack->used;
$ frama-c -jessie stack.c
[kernel] preprocessing with "gcc -C -E -I. -dD stack.c"
[jessie] Starting Jessie translation
stack.c:57:[jessie] failure: Unexpected failure.
Please submit bug report (Ref. "norm.ml:494:27").
[kernel] Plugin jessie aborted because of an internal error.
Please report with 'crash' at http://bts.frama-c.com
stack.c:
#include <stddef.h>
typedef struct stack_t {
int *data;
unsigned long size;
unsigned long used;
} stack_t;
void stack_init (stack_t *, int *, unsigned long);
int stack_valid (const stack_t *stack);
int stack_push (stack_t *, int);
int stack_pop (stack_t *, int *);
/*@ predicate stack_initialized (stack_t s) =
@ (0 < s.size) && \valid (s.data) && \valid_range (s.data, 0, s.size);
@
@ predicate stack_full (stack_t s) =
@ stack_initialized (s) && (s.used == s.size);
@
@ predicate stack_empty (stack_t s) =
@ stack_initialized (s) && (s.used == 0);
@ */
/*@ requires \valid (stack);
@ ensures 0 <= \result <= 1;
@ ensures stack_initialized (*stack) ==> \result == 1;
@ */
int
stack_valid (const stack_t *stack)
{
return ((stack->data != NULL) && (stack->size != 0));
}
/*@ requires \valid (stack);
@ requires \valid (data);
@ requires \valid_range (data, 0, size);
@ requires 0 < size;
@ ensures stack_initialized (*stack);
@ ensures stack->used == 0;
@ */
void
stack_init (stack_t *stack, int *data, unsigned long size)
{
stack->data = data;
stack->size = size;
stack->used = 0;
}
/*@ requires \valid (stack);
@ requires stack_initialized (*stack);
@ ensures !stack_full (\old (*stack)) ==> \old(stack->used) < stack->used;
@ */
int
stack_push (stack_t *stack, int item)
{
if (stack->used < stack->size) {
stack->used++;
stack->data [stack->used] = item;
return 1;
} else
return 0;
}
/*@ requires \valid (stack);
@ requires stack_initialized (*stack);
@ requires \valid (item); */
int
stack_pop (stack_t *stack, int *item)
{
if (stack->used > 0) {
*item = stack->data [stack->used];
stack->used--;
return 1;
} else
return 0;
}
### Additional Information :
Attached is the stack.jessie directory.
MD5 (stack.jessie.tar.gz) = d4a27838551febf2252b712e308e7ca6
## Attachments
- [stack.jessie.tar.gz](/uploads/cb71358c52ff2661669cb1ac6315b1f3/stack.jessie.tar.gz)