frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-02-22T13:56:49Zhttps://git.frama-c.com/pub/frama-c/-/issues/2337newbie trying to make operable2021-02-22T13:56:49Zmantis-gitlab-migrationnewbie trying to make operableID0000592:
**This issue was created automatically from Mantis Issue 592. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000592:
**This issue was created automatically from Mantis Issue 592. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000592 | Frama-C | Graphical User Interface | public | 2010-09-23 | 2010-12-03 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | blackdiamond | **Assigned To** | monate | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi :
I have installed the Boron Frama-C windows with Cygwin 2.721 setup version.
Also I installed the gcc and so.
After trying to load a c program in the frame dialog, an error appear with the next:
"gcc" not recognized as an internal or external command, program or executable lot file
Also, the message:
"Note that no C preprocessor is installed by Frama-C itself.
We encourage you to install cygwin from http://cygwin.org and to
launch Frama-C tools from a shell which contains "gcc" and the "bin"
directory of Frama-C in its path."
I have added the PATH of Frama-C/bin but it still does not work.
DO I need to set windows environment in order to enable Frama gets the gcc??
What steps are missed in order to make operable Frama-C ?
Thanks in Advance
### Additional Information :
Also, I have the environment with Frama-C installed.
HOMEPATH=\Documents and Settings\sal
CAML_LD_LIBRARY_PATH=C:\Frama-C\lib\stublibs
MANPATH=/usr/local/man:/usr/share/man:/usr/man:
APPDATA=C:\Documents and Settings\sal\Datos de programa
HOSTNAME=ACER1
TERM=cygwin
PROCESSOR_IDENTIFIER=x86 Family 6 Model 28 Stepping 2, GenuineIntel
FRAMAC_SHARE=C:\Frama-C\share\frama-c
WINDIR=C:\WINDOWS
OLDPWD=/usr/bin
USERDOMAIN=ACER1
OS=Windows_NT
ALLUSERSPROFILE=C:\Documents and Settings\All Users
USER=sal
!::=::\
TEMP=/cygdrive/c/DOCUME~1/sal/CONFIG~1/Temp
COMMONPROGRAMFILES=C:\Archivos de programa\Archivos comunes
WHYLIB='C:\Frama-C\lib\why'
VXIPNPPATH=C:\VXIpnp\
FRAMAC_LIB=C:\Frama-C\lib\frama-c
USERNAME=sal
PROCESSOR_LEVEL=6
PATH=/usr/local/bin:/usr/bin:/bin:/cygdrive/c/WINDOWS/system32:/cygdrive/c/WINDOWS:/cygdrive/c/WINDOWS/System32/Wbem:/cygdrive/c/Archivos de programa/Microsoft USB Flash Drive Manager/:/cygdrive/c/VXIpnp/WinNT/Bin:/cygdrive/c/Archivos de programa/GtkSharp/2.12/bin:/cygdrive/c/Archivos de programa/doxygen/bin:/cygdrive/c/Archivos de programa/Graphviz2.26.3/bin:/cygdrive/c/MCC18/mpasm:/cygdrive/c/MCC18/bin:/cygdrive/c/Archivos de programa/Microsoft USB Flash Drive Manager/:C:/Frama-C/bin
FP_NO_HOST_CHECK=NO
PWD=/cygdrive/c/Documents and Settings/sal
SYSTEMDRIVE=C:
LANG=C.UTF-8
USERPROFILE=C:\Documents and Settings\sal
CLIENTNAME=Console
PS1=\[\e]0;\w\a\]\n\[\e[32m\]\u@\h \[\e[33m\]\w\[\e[0m\]\n\$
LOGONSERVER=\\ACER1
PROCESSOR_ARCHITECTURE=x86
!C:=C:\cygwin\bin
ERGOLIB=C:\Frama-C\lib\alt-ergo
SHLVL=1
QUCSDIR=C:\Archivos de programa\Qucs
OCAMLLIB=C:\Frama-C\lib
HOME=/cygdrive/c/Documents and Settings/sal
PATHEXT=.COM;.EXE;.BAT;.CMD;.VBS;.VBE;.JS;.JSE;.WSF;.WSH
HOMEDRIVE=C:
FRAMAC_PLUGIN=C:\Frama-C\lib\frama-c\plugins
PROMPT=$P$G
MCC_INCLUDE=C:\MCC18\h;
COMSPEC=C:\WINDOWS\system32\cmd.exe
TMP=/cygdrive/c/DOCUME~1/sal/CONFIG~1/Temp
SYSTEMROOT=C:\WINDOWS
ASCODIR=C:\Archivos de programa\Qucs
PRINTER=CutePDF Printer
CVS_RSH=/bin/ssh
PROCESSOR_REVISION=1c02
tvdumpflags=8
INFOPATH=/usr/local/info:/usr/share/info:/usr/info:
PROGRAMFILES=C:\Archivos de programa
NUMBER_OF_PROCESSORS=2
SESSIONNAME=Console
COMPUTERNAME=ACER1
_=/usr/bin/envhttps://git.frama-c.com/pub/frama-c/-/issues/2336Don't edit files in make install. Instead, just use all plug-ins in the plugi...2021-02-22T14:04:39Zmantis-gitlab-migrationDon't edit files in make install. Instead, just use all plug-ins in the plugin directoryID0000606:
**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.htmlhttps://git.frama-c.com/pub/frama-c/-/issues/2335crashed value analysis2021-02-22T13:56:46Zmantis-gitlab-migrationcrashed value analysisID0000547:
**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.comhttps://git.frama-c.com/pub/frama-c/-/issues/2334Crash in2021-02-22T13:56:45Zmantis-gitlab-migrationCrash inID0000333:
**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/2332labels are not correctly translated in jessie+why2021-04-15T09:17:43ZFrançois Bobotlabels are not correctly translated in jessie+whyID0000071:
**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 5186https://git.frama-c.com/pub/frama-c/-/issues/2331Uncaught exception: assert false on bitvector2021-04-15T09:17:34ZDillon ParienteUncaught exception: assert false on bitvectorID0000273:
**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.21https://git.frama-c.com/pub/frama-c/-/issues/2330Error while processing legitimate C construction2021-04-15T09:17:39Zmantis-gitlab-migrationError while processing legitimate C constructionID0000187:
**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.20https://git.frama-c.com/pub/frama-c/-/issues/2329Decreases clause2021-04-15T09:17:27ZDillon ParienteDecreases clauseID0000369:
**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/2328Jessie translation unexpected failure2021-04-15T09:17:24ZVictoria Moya LamielJessie translation unexpected failureID0000410:
**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/2325error in analyzing xen 4.0.0 code2021-02-22T13:56:34Zmantis-gitlab-migrationerror in analyzing xen 4.0.0 codeID0000516:
**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.comhttps://git.frama-c.com/pub/frama-c/-/issues/2324Empty specification causes syntax error2021-02-22T13:56:32Zmantis-gitlab-migrationEmpty specification causes syntax errorID0000605:
**This issue was created automatically from Mantis Issue 605. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000605:
**This issue was created automatically from Mantis Issue 605. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000605 | Frama-C | Kernel > ACSL implementation | public | 2010-10-13 | 2010-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | boris | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
File [1] causes error [2] when processed with frama-c -val. However, processing with frama-c -jessie causes no errors.
### Additional Information :
[1]
int* p;
int foo();
/*@
*/
int main() {
int i, t[10];
for(i=0; i<=10; i++)
t[i]=i;
if(foo()) p[2] = 1;
return 0;
}
[2]
[kernel] preprocessing with "gcc -C -E -I. val1.c"
val1.c:6:[kernel] user error: syntax error while parsing annotation
[kernel] user error: skipping file "val1.c" that has errors.
[kernel] Frama-C aborted because of an invalid user input.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2323no multiple assert-clauses accepted in /*@...*/-style comment2021-02-22T13:56:31ZJochen Burghardtno multiple assert-clauses accepted in /*@...*/-style commentID0000601:
**This issue was created automatically from Mantis Issue 601. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000601:
**This issue was created automatically from Mantis Issue 601. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000601 | Frama-C | Kernel > ACSL implementation | public | 2010-10-12 | 2010-12-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
See attached program: when #define multipleAsserts is in force, the kernel complains about line 11-12, containing two assert-clauses in a single /*@...*/ comment.
I'm not sure this contradicts some ASCL-syntax definition.
However, it appears strange to me, since multiple requires, ensures, and loop invariant are admitted (although they could be joined into a single one by &&, as for assert, too).
## Attachments
- [ftest.c](/uploads/92ec6efb44e5b83b7f0d4baf1022eecc/ftest.c)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2309incorrect(?) jessie code generated from strcpy2021-04-15T09:17:14Zmantis-gitlab-migrationincorrect(?) jessie code generated from strcpyID0000584:
**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/2308Default assigns generation2021-02-22T13:56:15ZPatrick BaudinDefault assigns generationID0000620:
**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/2304Checking number of arguments passed to C functions2021-02-22T13:56:10ZPascal CuoqChecking number of arguments passed to C functionsID0000552:
**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/2301slicing produces uncompilable program when formal used as a local variable2021-02-22T13:56:05ZPascal Cuoqslicing produces uncompilable program when formal used as a local variableID0000529:
**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/2299Frama-C should produce more specific error messages when parsing annotations2021-02-22T14:04:36Zmantis-gitlab-migrationFrama-C should produce more specific error messages when parsing annotationsID0000538:
**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);
^ herehttps://git.frama-c.com/pub/frama-c/-/issues/2296inchoherence of types between enumitems and enum type with multi-files2021-02-22T13:55:56ZStephane Dupratinchoherence of types between enumitems and enum type with multi-filesID0000525:
**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/2294Makefile.dynamic should not change known_plugins.ac2021-02-22T14:04:39Zmantis-gitlab-migrationMakefile.dynamic should not change known_plugins.acID0000462:
**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/2282for behav : invariant INV ;2021-02-22T13:55:32ZPatrick Baudinfor 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.