frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-12-28T10:05:19Zhttps://git.frama-c.com/pub/frama-c/-/issues/2459Frama-C fails to parse a file2022-12-28T10:05:19Zmantis-gitlab-migrationFrama-C fails to parse a fileID0000261:
**This issue was created automatically from Mantis Issue 261. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000261:
**This issue was created automatically from Mantis Issue 261. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000261 | Frama-C | Kernel | public | 2009-10-01 | 2009-10-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jonathan-Christofer Demay | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
It compiles fine with "gcc -I. -I./libtomcrypt/src/headers/ -DDROPBEAR_SERVER -DDROPBEAR_CLIENT dbutil.c -c -o dbutil.o"
But when given to Frama-C (CPP is set accordinly), I get the following error:
libtommath/tommath.h:77:[kernel] user error: GCC width mode TI applied to unexpected type, or unexpected mode
In tommath.h line 77 we have a mysterious GCC incantation (>_<):
typedef unsigned long mp_word __attribute__ ((mode(TI)));
### Additional Information :
Uploaded a preprocessed file: "gcc -I. -I./libtomcrypt/src/headers/ -DDROPBEAR_SERVER -DDROPBEAR_CLIENT dbutil.c -C -E -o dbutil.i"
## Attachments
- [dbutil.i](/uploads/ca1ba34059bd1dd4efa823437f09a2c6/dbutil.i)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2347Parse error when using a wide string literal to initialize uint16 array2021-02-22T13:56:58Zmantis-gitlab-migrationParse error when using a wide string literal to initialize uint16 arrayID0000593:
**This issue was created automatically from Mantis Issue 593. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000593:
**This issue was created automatically from Mantis Issue 593. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000593 | Frama-C | Kernel | public | 2010-09-30 | 2010-10-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Maria | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm trying to analyze Brew with Frama-C. OS - windows XP.
I've created simple Brew project(see attach), preprocessed it with Visual Studio and after it try to analyze with Frama-C:
C:\Frama-C\bin>frama-c.exe "\Program Files\BREW 3.1.5\sdk\examples\helloworld"\*.i
Also, I've tried to add files to project, using user interface, but nothing happened.
## Attachments
- [helloworld.zip](/uploads/e1faf5861730eaa7d75da589b90c18c6/helloworld.zip)Virgile PrevostoVirgile Prevostohttps://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/2255Strange AST produced with unspecified side-effects involve function calls in ...2021-02-22T14:02:55ZPascal CuoqStrange AST produced with unspecified side-effects involve function calls in expressionsID0000676:
**This issue was created automatically from Mantis Issue 676. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000676:
**This issue was created automatically from Mantis Issue 676. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000676 | Frama-C | Kernel | public | 2011-01-18 | 2011-01-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20101202-beta2 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Original code:
if(((fast_read(o, 3) ^ fetch) & 0xffffff) == 0 && o < src - MINOFFSET)
Transformed as:
ui32 tmp_1 ;
{ /*undefined sequence*/
tmp_1 = fast_read((void const *)o,(unsigned int )3);
;
}
if (((tmp_1 ^ fetch) & (unsigned int )0xffffff) == (unsigned int )0) {
if (o < src - 2) {
Contact Pascal for whole function.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2045__builtin_alloca2021-02-22T13:49:38Zmantis-gitlab-migration__builtin_allocaID0001190:
**This issue was created automatically from Mantis Issue 1190. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001190:
**This issue was created automatically from Mantis Issue 1190. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001190 | Frama-C | Kernel | public | 2012-06-08 | 2012-06-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Nitrogen-20111001 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In a file with a local array which size in defined by a variable :
float a[n];
I get :
[kernel] warning: Variable-sized local variable a
which is ok. But then, when I use the value analysis, I get :
[kernel] warning: No code for function __builtin_alloca,
default assigns generated
because the declaration has been translated in :
__lengthofa = (unsigned int)n;
a = (float *)__builtin_alloca(sizeof(*a) * __lengthofa);
which looks fine, but the question is :
shouldn't the assigns property be defined somewhere inside Frama-C for the builtin functions ?
As a workaround, what prototype and assigns should I write for this function.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/1926Code annotation in the middle of labels2021-03-29T13:52:50ZJulien SignolesCode annotation in the middle of labelsID0001327:
**This issue was created automatically from Mantis Issue 1327. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001327:
**This issue was created automatically from Mantis Issue 1327. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001327 | Frama-C | Kernel | public | 2012-12-12 | 2012-12-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Consider this code:
void foo(int x) {
switch (x) {
case 0: /*@ assert \true; */
case 1: ;
}
}
Frama-C encloses both the assertion and the "case 1: ;" into a block inside the "case 0" as shown below. I'm not sure that it is the expected behavior (either the block should also include "case 0" or this program should be rejected as syntactically incorrect).
$ frama-c -kernel-debug 1 a.i
<skip trace>
/* Generated by Frama-C */
void foo(int x)
{
/* */
/*sid:2*/
switch (x) {
/* */
case 0:
/*sid:3*/
/*block:begin*/
{
/* */
/*sid:4*/ /*@ assert \true; */ ;
case 1: /*sid:5*/ ; }
/*block:end*/
}
/*sid:8*/
return;
}
Note: if you add a semi-colon right after the assertion, there is no issue.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/955Translation of abrupt clause into assert do not take 'for :' clause into account2021-02-22T13:51:40ZVirgile PrevostoTranslation of abrupt clause into assert do not take 'for :' clause into accountID0001632:
**This issue was created automatically from Mantis Issue 1632. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001632:
**This issue was created automatically from Mantis Issue 1632. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001632 | Frama-C | Kernel > ACSL implementation | public | 2014-01-27 | 2014-10-29 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | virgile | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | low | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the program written given below, the returns clause is translated into two assert that are not related to the foo behavior, resulting in an unprovable assertion in the else branch.
### Steps To Reproduce :
/*@ behavior foo:
assumes a == 0;
*/
int foo(int a) {
/*@ for foo:
returns \result == 0;
*/
{ if (a==0) { return 0; }
else return 2;
}
}Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/1137Initializer of static variable refers to size of type of local variable2021-02-22T13:48:28ZPascal CuoqInitializer of static variable refers to size of type of local variableID0001645:
**This issue was created automatically from Mantis Issue 1645. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001645:
**This issue was created automatically from Mantis Issue 1645. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001645 | Frama-C | Kernel | public | 2014-02-13 | 2014-03-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | low | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | - |
### Description :
CONTEXT:
This issue does not originate from an industrial application. It is reported for the lulz.
DESCRIPTION:
The program below is accepted by gcc and clang, and rejected by Frama-C. It seems that the compilers are right to accept it.
~ $ cat t.c
unsigned f(void) {
int a;
static unsigned s = sizeof(a);
return s;
}
~ $ clang -std=c99 -pedantic -Wall -c t.c
~ $ frama-c t.c
[kernel] preprocessing with "gcc -C -E -I. t.c"
t.c:4:[kernel] user error: Forbidden access to local variable a in static initializer
[kernel] user error: skipping file "t.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
~ $Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/196Wrong specification for standard library function memmove2021-02-22T12:56:09ZPascal CuoqWrong specification for standard library function memmoveID0001648:
**This issue was created automatically from Mantis Issue 1648. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001648:
**This issue was created automatically from Mantis Issue 1648. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001648 | Frama-C | Kernel | public | 2014-02-17 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
CONTEXT:
This issue does not originate from an industrial application. It is reported for the lulz.
DESCRIPTION:
The post-condition for memmove() incorrectly describes its effects when source and destination overlap.
/*@ ...
@ ensures memcmp((char*)dest,(char*)src,n) == 0;
...
@*/
extern void *memmove(void *dest, const void *src, size_t n);
In order to be maximally useful, the memcmp logic function, which is defined thus:
/*@ axiomatic MemCmp {
@ logic ℤ memcmp{L}(char *s1, char *s2, ℤ n)
@ reads s1[0..n - 1], s2[0..n - 1];
...
would need to be parameterized by two labels L1 and L2, and state that the memory zone pointed by s1 in L1 is identical to the memory zone pointed by s2 in L2.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/357Check that all occurrences of *p in assigns are guarded by a \valid(p) in req...2021-02-22T13:00:08ZJens GerlachCheck that all occurrences of *p in assigns are guarded by a \valid(p) in requiresID0001761:
**This issue was created automatically from Mantis Issue 1761. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001761:
**This issue was created automatically from Mantis Issue 1761. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001761 | Frama-C | Kernel > ACSL implementation | public | 2014-04-23 | 2017-03-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Here is a simple function foo where the assigns clause refers to the pointer a+n that is not
guarded by a \valid in the requires clause.
/*@
requires \valid(a + (0..n-1));
assigns a[0..n]; // should be a[0..n-1]
*/
void foo(int* a, unsigned int n)
{
/*@
loop invariant 0 <= i <= n;
loop assigns i, a[0..n]; // should be a[0..n-1];
loop variant n-i;
*/
for(unsigned int i = 0; i < n; ++i)
a[i] = 0;
}
Using the command line
frama-c-gui.byte -wp -wp-rte -wp-model Typed+ref -wp-timeout 10 -wp-prover alt-ergo -wp-out loop_assigns.wp loop_assigns.c
I can see that all proof obligations are discharged by either Qed or Alt-Ergo.
My question is about the assigns clause which refers to all offsets of a in the range [0..n].
(Note that I use the same range in the loop assigns clause.)
The precondition, however, only states that array offsets in the range [0..n-1] are valid.
I think I would prefer if WP (or the Frama-C kernel) issued a warning about this discrepancy.
### Additional Information :
I posted this on the Frama-C mailing list. As far as I understood the discussion there it might be a feature request for the Frama-C kernel.
I noticed this problem when writing specs for code from a partner in the OpenETCS project.Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/1034option -nostdinc does not seem to work2021-02-22T14:02:33ZJens Gerlachoption -nostdinc does not seem to workID0001786:
**This issue was created automatically from Mantis Issue 1786. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001786:
**This issue was created automatically from Mantis Issue 1786. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001786 | Frama-Clang | Kernel | public | 2014-05-26 | 2014-05-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When calling the following sample code (nostdinc.cpp)
#include "limits.h"
int foo(int a)
{
if (a >= INT_MAX/2)
return INT_MAX;
else
return a;
}
with
frama-c-gui -cpp-command 'gcc -C -E -nostdinc -I/usr/local/share/frama-c/libc' -cxx-clang-command="framaCIRGen" -cxx-stdinc -cxx-demangling-full -wp -wp-rte -wp-proof alt-ergo nostdin.cpp
refers to std header such as
In file included from nostdin.cpp:2:
In file included from /usr/include/clang/3.3/include/limits.h:38:
In file included from /usr/include/limits.h:25:
In file included from /usr/include/features.h:398:
/usr/include/x86_64-linux-gnu/gnu/stubs.h:7:11: fatal error: 'gnu/stubs-32.h' file not found
# include <gnu/stubs-32.h>
^Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/845Frama-C-clang does not unfold typedef2021-02-22T14:02:14ZJens GerlachFrama-C-clang does not unfold typedefID0001805:
**This issue was created automatically from Mantis Issue 1805. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001805:
**This issue was created automatically from Mantis Issue 1805. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001805 | Frama-Clang | Kernel | public | 2014-06-12 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When Frama-Clang analyses the following code example
struct A
{
int n;
};
typedef struct A B;
/*@
requires \valid(b);
assigns \nothing;
ensures \result == b->n;
*/
int foo(B* b)
{
return b->n;
}
then it complains
problem207.cpp:12:29: expecting a struct with field
problem207.cpp:12:29: type is not a pointer type
### Steps To Reproduce :
The source code of the example is available under acslplusplus/C++Examples/Problems/problem207.cpp
It was analysed with the following command line:
frama-c.byte -cxx-clang-command="framaCIRGen" -wp problem207.cppVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/844reference typedef causes conversion error in contract2021-02-22T14:02:14ZJochen Burghardtreference typedef causes conversion error in contractID0001948:
**This issue was created automatically from Mantis Issue 1948. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001948:
**This issue was created automatically from Mantis Issue 1948. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001948 | Frama-Clang | Plug-in > clang | public | 2014-10-30 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
114.cpp:7:37: invalid implicit conversion
Now output intermediate result
The error disappears if "reference" is changed to "int&" in line 8.
## Attachments
- [114.cpp](/uploads/47dd1e60cc1a1a5d2510ce3ad1ed608f/114.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/851Declaration order of static class member2021-02-22T13:13:26ZJens GerlachDeclaration order of static class memberID0001950:
**This issue was created automatically from Mantis Issue 1950. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001950:
**This issue was created automatically from Mantis Issue 1950. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001950 | Frama-Clang | Plug-in > clang | public | 2014-11-02 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | jens | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | high | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
The following file contains two classes A and B that contain a single static variable count.
A::count is declared at the beginning of class A. Everything is fine.
B::count, however, is defined at the end of class B. Here Frama-Clang complains.
problem209.cpp:26:[fclang] failure: Unknown global variable B::count
### Additional Information :
Note, the problem does not occur, when B::count is a non-static member.
## Attachments
- [problem209.cpp](/uploads/12b2d0b16ba9d25bf52bd8af599cf33c/problem209.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/880public variables of superclass not visible in subclass invariant2021-02-22T14:02:19ZJochen Burghardtpublic variables of superclass not visible in subclass invariantID0001959:
**This issue was created automatically from Mantis Issue 1959. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001959:
**This issue was created automatically from Mantis Issue 1959. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001959 | Frama-Clang | Plug-in > clang | public | 2014-11-10 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
120.cpp:9:[kernel] user error: Cannot find field a
If "a ==" is deleted from line 9, the error message disappears.
Note that "a" is visible in the code in line 11.
## Attachments
- [120.cpp](/uploads/64602eaf38dd440ae1fe439ce89706fd/120.cpp)
- [127.cpp](/uploads/cd8fe9eacdedaad20a6a8966f6923c25/127.cpp)
- [120a.cpp](/uploads/00f63c1e84fb84a81269bc2d3301d26d/120a.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/841Wp can't prove validity of access to public variable from superclass2021-02-22T14:02:09ZJochen BurghardtWp can't prove validity of access to public variable from superclassID0001963:
**This issue was created automatically from Mantis Issue 1963. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001963:
**This issue was created automatically from Mantis Issue 1963. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001963 | Frama-Clang | Plug-in > clang | public | 2014-11-13 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running Wp (with rte) on the attached file "128.cpp" results in one obligation unproven by Alt-Ergo, see the attached file "_ZN1BEC1_assert_rte_mem_access_Alt-Ergo.mlw".
In the latter file, the name "valid_rw" appears only in the goal (line 566-573), in the definition (l.464-466), and in 2 axioms (l.468-470, 477-480).
None of these axioms can be used to prove a goal of the form "... -> valid_rw(...,...,...)", since they contain "valid_rw" only at negated positions.
However, using the definition would require to establish a relations between "t" and "t1", in order to show "... & ...<=t[...] -> ...<=t1[...]". Probably, something like e.g. "t=t1" is missing amount the preconditions of the goal.
The .mlw file remains literally the same if a call ":A()" is inserted in the B() constructor definition in line 8.
BTW: I wonder why "valid_rw" can be applied to "t" which has type "int farray", while the definition says the first argument should have the type "(int,int) farray". However, Alt-Ergo doesn't complain about ill-typedness.
## Attachments
- [128.cpp](/uploads/d8a9595d7860e5dc446d1919753f1185/128.cpp)
- [_ZN1BEC1_assert_rte_mem_access_Alt-Ergo.mlw](/uploads/70cb7046724b12759e6fc1d6ce188318/_ZN1BEC1_assert_rte_mem_access_Alt-Ergo.mlw)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/650template parameter type can't used in typedef2021-02-22T13:08:05ZJochen Burghardttemplate parameter type can't used in typedefID0001972:
**This issue was created automatically from Mantis Issue 1972. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001972:
**This issue was created automatically from Mantis Issue 1972. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001972 | Frama-Clang | Plug-in > clang | public | 2014-11-17 | 2015-04-27 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
136.cpp:6:[kernel] failure: Cannot find type _ZN6traitsIiE2stE2tp (kind:type)
The problem disappears if the surrounding "struct st {" and "};" is deleted in line 3, and "st::" is deleted in line 6.
BTW: A call of "c++filt -n _ZN6traitsIiE2stE2tp" yields "traits<int>::st(tp)", while I would have expected "traits<int>::st::tp".
(Importance: this code is used via #include <vector>.)
Other issues that involve both typedef and templates were/are #1705, #1580, #1531. One of them might be related to the problem here.
## Attachments
- [136.cpp](/uploads/7681db01d5299465de8a20e5ebe39490/136.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/831missing ";" after clause causes its tacit omission2021-02-22T14:01:54ZJochen Burghardtmissing ";" after clause causes its tacit omissionID0001976:
**This issue was created automatically from Mantis Issue 1976. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001976:
**This issue was created automatically from Mantis Issue 1976. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001976 | Frama-Clang | Plug-in > clang | public | 2014-11-20 | 2015-02-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
The goal "typed_main_assert" generated from the file "141.cpp" can't be proven; the corresponding .mlw file contains the goal formula "goal main_assert: forall i : int. is_sint32(i) -> (111 = i)"; that is, the "ensures" clause from line 2 isn't used there.
If the missing ";" at the end of line 2 is appended, the generated goal reads "goal main_assert: forall i : int. (222 = (2 * i)) -> is_sint32(i) -> (111 = i)", and is proven by Alt-Ergo.
No warning or error message about the missing ";" is issued. When the file is renamed to "141.c", frama-c prints an error message "141.c:2:[kernel] user error: expecting ';' before end of annotation".
## Attachments
- [141.cpp](/uploads/a78879845eac9a5610cf9c89525d755d/141.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/804false assertion apparently undetected in the presence of overloaded virtual f...2021-02-22T13:12:20ZJochen Burghardtfalse assertion apparently undetected in the presence of overloaded virtual functionsID0001975:
**This issue was created automatically from Mantis Issue 1975. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001975:
**This issue was created automatically from Mantis Issue 1975. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001975 | Frama-Clang | Plug-in > clang | public | 2014-11-20 | 2015-02-23 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Running "frama-c -wp -wp-rte" on the attached file generates 117 proof obligations of which 43 can be proven. I suppose that the obligation for the false assertion from line 19 is also proven, by qed; probably it has the name "typed_main_assert".
My reasons are:
If the assertion wasn't proven, an .mlw file for Alt-Ergo should appear in the wp-out directory which should contain the string "333"; however, no that string couldn't be found there, nor could "111"; while "222" occurs (in many/all .mlw files) only as value of the global variable "G__ZN6SquareE12_frama_c_vmt_221" which, in turn, is used only as index to an int array "t" and as an argument to "region" in global variables axioms, i.e. "222" doesn't occur in a goal.
If the value "333" in line 19 of file 139.cpp is changed to "222", i.e. if the assertion is made true, then the very same proof goal names and Valid/Unknown/Timeout results appear in the verification log. Similarly, if the value is changed to "111". All three log differ only in prover timings and obligation order, as can be seen by applying the shell-script "normalizeVerificationLog.sh" to the 117 obligation log lines in each of the log files "139_111orig.txt", "139_222orig.txt", and "139_333orig.txt" (all files attached).
Possibly, some precondition equivalent to \false is given to qed together with the goal for the line 19 assertion.
## Attachments
- [139.cpp](/uploads/ef54ab397fe24e7f040155064b4cbe62/139.cpp)
- [normalizeVerificationLog.sh](/uploads/dcc5ba9bf493c9ed7dd9a93ff699baa9/normalizeVerificationLog.sh)
- [139_111orig.txt](/uploads/d46a11670a724511c9293096ea0f790b/139_111orig.txt)
- [139_222orig.txt](/uploads/b31db051941cf23713b5f74417a79750/139_222orig.txt)
- [139_333orig.txt](/uploads/62f230fcf7b7523510583b46e105480c/139_333orig.txt)
- [139a.cpp](/uploads/8d62c589f4a19d553396ee705e4ef581/139a.cpp)
- [139a.fc_log](/uploads/fe53caffaae1a7cbdec8f3b76dfc4889/139a.fc_log)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/861scope resolution operator not recognized in assertion2021-02-22T13:26:43ZJochen Burghardtscope resolution operator not recognized in assertionID0001984:
**This issue was created automatically from Mantis Issue 1984. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001984:
**This issue was created automatically from Mantis Issue 1984. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001984 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
146.cpp:9:14: unexpected token 'operator -> ::' when starting to parse a term
Now output intermediate result
(Lines 5-8 aren't really needed to produce the error message.)
## Attachments
- [146.cpp](/uploads/73158ee47b3e3b872d5c8187cf72008b/146.cpp)Virgile PrevostoVirgile Prevosto