frama-c issues
https://git.frama-c.com/pub/frama-c/-/issues
2021-04-15T09:17:07Z
https://git.frama-c.com/pub/frama-c/-/issues/2251
11 if-statements lead to why-runtime >12 min
2021-04-15T09:17:07Z
Jochen Burghardt
11 if-statements lead to why-runtime >12 min
ID0000688:
**This issue was created automatically from Mantis Issue 688. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000688:
**This issue was created automatically from Mantis Issue 688. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000688 | Frama-C | Plug-in > jessie | public | 2011-01-25 | 2011-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | no change required |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I tried to test whether "why" builds one proof obligation per relevant program-path, came up with the attached program to cause a combinatorial explosion, and succeeded. I guess, this problem is unavoidable.
However, I'd expected "why" to be able to cope with at least 2^16 paths, rather than <2^11 only. There might be programs of practical relevance with a variable's value at some program point depending of that much case distinctions.
Maybe the manual should recommend for such programs the use of intermediate assert-clause, like "assert (y & 0xff) == (x & 0xff)" between line 10 and 11 in ftest.c.
## Attachments
- [ftest.c](/uploads/6b6ecdc81819bf06e05aa1a8190db3d6/ftest.c)
https://git.frama-c.com/pub/frama-c/-/issues/1276
12799, doubtful choice of promotion x86_64 mode (csmith)
2021-02-22T13:25:44Z
Pascal Cuoq
12799, doubtful choice of promotion x86_64 mode (csmith)
ID0000785:
**This issue was created automatically from Mantis Issue 785. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000785:
**This issue was created automatically from Mantis Issue 785. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000785 | Frama-C | Kernel | public | 2011-04-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
int x;
long x2;
unsigned long x9[6][2];
#if 0
#define d(n, v) Frama_C_show_each##n(v);
#else
#define d(n, v)
#endif
main(){
x2 = 2793414595;
for (int i = 0; i < 6; i++)
{
for (int j = 0; j < 2; j++)
x9[i][j] = 1U;
}
d(102, (0x090E7AF82577C8A6LL | x9[1][0]) )
d(103, (~(x2 || x9[1][0])) )
d(95, ((0x090E7AF82577C8A6LL | x9[0][1]) <= (~(x2 || x9[0][1]))))
x = ((0x090E7AF82577C8A6LL | x9[0][1]) <= (~(x2 || x9[0][1])));
return x;
}
~/ppc/bin/toplevel.opt -val -machdep x86_64 r.c -slevel 5000
...
[value] Values for function main:
x ? {0; }
BUT:
gcc -std=c99 r.c ; ./a.out ; echo $?
1
NOTE THAT:
~/ppc/bin/toplevel.opt -print -machdep x86_64 r.c [kernel] preprocessing with "gcc -C -E -I. r.c"
...
x = (0x090E7AF82577C8A6LL | (long long )x9[0][1]) <= (long long )(~ tmp);
}
return (x);
}
gcc is the computation server's, supposed to match x86_64.
x9[0][1] is an unsigned long. The promotion of the arguments of | seems to be wrong in Frama-C's front-end according to 6.3.1.8 (p 45), where the very last case of §1 seems to apply.
### Additional Information :
In addition to the computation server's GCC (version 4.4.3 (Ubuntu 4.4.3-4ubuntu5)), this one also predicts the result 1 for x when compiling with -m64:
gcc -m64 -v
Using built-in specs.
Target: powerpc-apple-darwin9
Configured with: /var/tmp/gcc/gcc-5493~1/src/configure --disable-checking -enable-werror --prefix=/usr --mandir=/share/man --enable-languages=c,objc,c++,obj-c++ --program-transform-name=/^[cg][^.-]*$/s/$/-4.0/ --with-gxx-include-dir=/include/c++/4.0.0 --with-slibdir=/usr/lib --build=i686-apple-darwin9 --program-prefix= --host=powerpc-apple-darwin9 --target=powerpc-apple-darwin9
Thread model: posix
gcc version 4.0.1 (Apple Inc. build 5493)
https://git.frama-c.com/pub/frama-c/-/issues/1268
12816: Missing label in sliced program (csmith)
2021-02-22T14:02:52Z
Pascal Cuoq
12816: Missing label in sliced program (csmith)
ID0000786:
**This issue was created automatically from Mantis Issue 786. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000786:
**This issue was created automatically from Mantis Issue 786. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000786 | Frama-C | Plug-in > slicing | public | 2011-04-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Same conventions as usual, the slicing command was
~/ppc/bin/toplevel.opt -val-signed-overflow-alarms s.11215416.1.c -cpp-command "gcc -C -E -D__FRAMAC -I. -I$CSMITH/runtime " -machdep x86_64 -slice-calls Frama_C_show_each -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -no-slice-force -no-val -print -ocode s.11215416.1.s.c
But when compiling the sliced program:
$ gcc s.11215416.1.s.c show_each.c
s.11215416.1.s.c: In function ‘func_10_slice_1’:
s.11215416.1.s.c:163: error: label ‘_LOR’ used but not defined
## Attachments
- [missing_label.tgz](/uploads/c96167e8377f46c437e19ec0babd22a6/missing_label.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/2150
12825, sliced program does not terminate
2021-02-22T14:04:20Z
Pascal Cuoq
12825, sliced program does not terminate
ID0000789:
**This issue was created automatically from Mantis Issue 789. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000789:
**This issue was created automatically from Mantis Issue 789. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000789 | Frama-C | Plug-in > slicing | public | 2011-04-12 | 2011-10-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
This example is smaller than 787, all the settings are the same.
## Attachments
- [smaller.tgz](/uploads/5e10dc62105f1af62eee7df866dd39e1/smaller.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/2085
14055: sliced program does not terminate (csmith)
2021-02-22T13:50:39Z
Pascal Cuoq
14055: sliced program does not terminate (csmith)
ID0000880:
**This issue was created automatically from Mantis Issue 880. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000880:
**This issue was created automatically from Mantis Issue 880. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000880 | Frama-C | Plug-in > slicing | public | 2011-07-06 | 2011-12-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Same conditions as bug 879.
## Attachments
- [t.c](/uploads/1b116faffb854838fd37514fc5ff94d8/t.c)
https://git.frama-c.com/pub/frama-c/-/issues/1786
14292: warn for unspecified side-effect that are separated by a function call...
2021-02-22T13:41:45Z
Pascal Cuoq
14292: warn for unspecified side-effect that are separated by a function call (csmith)
ID0000888:
**This issue was created automatically from Mantis Issue 888. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000888:
**This issue was created automatically from Mantis Issue 888. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000888 | Frama-C | Kernel | public | 2011-07-25 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
~ $ ppc/bin/toplevel.opt -val u.c -unspecified-access
...
u.c:5:[kernel] warning: undefined multiple accesses in expression. assert \separated(& x,& x);
...
~ $ cat u.c
int f(int);
main(){
int x;
x = f(x=2);
}
https://git.frama-c.com/pub/frama-c/-/issues/2082
14403: last slicing bug (csmith)
2021-02-22T13:50:34Z
Pascal Cuoq
14403: last slicing bug (csmith)
ID0000905:
**This issue was created automatically from Mantis Issue 905. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000905:
**This issue was created automatically from Mantis Issue 905. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000905 | Frama-C | Plug-in > slicing | public | 2011-07-31 | 2011-12-19 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | Anne | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
The value analysis does not find any alarm and finds the values below
~/ppc/bin/toplevel.opt -val-signed-overflow-alarms -no-val-show-progress -cpp-command "gcc -m32 -E -C -I runtime -D__FRAMAC" -no-results -slevel 100000 -machdep x86_32 s.31013054.p.c -val
[value] Called Frama_C_show_each({3781742995})
[value] Called Frama_C_show_each({4095739724})
[value] Called Frama_C_show_each({550094235})
[value] Called Frama_C_show_each({252820852})
[value] Called Frama_C_show_each({624713289})
[value] Called Frama_C_show_each({1426802424})
[value] Called Frama_C_show_each({397183221})
[value] Called Frama_C_show_each({320991826})
[value] Called Frama_C_show_each({1015897994})
[value] Called Frama_C_show_each({3069753974})
[value] Called Frama_C_show_each({4276963908})
[value] Called Frama_C_show_each({1968234281})
[value] Called Frama_C_show_each({1968234281})
Executing (32-bit) finds the same values as above.
But the program sliced with:
~/ppc/bin/toplevel.opt -val-signed-overflow-alarms -no-val-show-progress s.31013054.p.i -slice-calls Frama_C_show_each -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -print -ocode res.c
$ gcc -m32 res.c show_each.c
$ ./a.out
[value] Called Frama_C_show_each({3781742995})
[value] Called Frama_C_show_each({4095739724})
[value] Called Frama_C_show_each({550094235})
[value] Called Frama_C_show_each({252820852})
[value] Called Frama_C_show_each({624713289})
[value] Called Frama_C_show_each({1426802424})
[value] Called Frama_C_show_each({397183221})
[value] Called Frama_C_show_each({320991826})
[value] Called Frama_C_show_each({1015897994})
[value] Called Frama_C_show_each({1148365541})
[value] Called Frama_C_show_each({3051573531})
[value] Called Frama_C_show_each({2309422687})
[value] Called Frama_C_show_each({2309422687})
### Additional Information :
Le bug a pris 36h * 5 processeurs pour se montrer, ce sera presque sûrement le dernier, sauf si tu en introduis un nouveau en corrigeant celui-ci :)
1015897994 est la dernière valeur correcte. Cela indique une différence dans la valeur finale de g_89[2].
## Attachments
- [p.tgz](/uploads/bb1ca13c3c893dc54600c9d571283708/p.tgz)
https://git.frama-c.com/pub/frama-c/-/issues/1368
17514, -unspecified-access and if (*p = (*p < 3)) (csmith)
2024-03-12T17:06:13Z
Pascal Cuoq
17514, -unspecified-access and if (*p = (*p < 3)) (csmith)
ID0001114:
**This issue was created automatically from Mantis Issue 1114. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001114:
**This issue was created automatically from Mantis Issue 1114. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001114 | Frama-C | Kernel | public | 2012-03-10 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
In the program below, line 6 is as innocuous as line 5, but:
$ bin/toplevel.opt -val -unspecified-access t.c
[kernel] preprocessing with "gcc -C -E -I. t.c"
t.c:6:[kernel] warning: Unspecified sequence with side effect:
/* <- *p p */
tmp = *p < 3;
/* *p <- tmp p */
*p = tmp;
...
t.c:6:[kernel] warning: undefined multiple accesses in expression. assert \separated(p, p);;
int x, *p;
main(){
p = &x;
*p = (*p < 3);
if (*p = (*p < 3))
x = 4;
}
https://git.frama-c.com/pub/frama-c/-/issues/2066
17517: defined program behaves differently after going through -print (csmith)
2021-02-22T13:50:12Z
Pascal Cuoq
17517: defined program behaves differently after going through -print (csmith)
ID0001115:
**This issue was created automatically from Mantis Issue 1115. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001115:
**This issue was created automatically from Mantis Issue 1115. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001115 | Frama-C | Kernel | public | 2012-03-10 | 2012-03-11 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | - | **Resolution** | no change required |
| **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 :
Program o.i is defined for a x86_64 architecture according to:
$ ~/ppc/bin/toplevel.opt -val -obviously-terminates o.i -machdep x86_64 -no-val-show-progress -unspecified-access -val-signed-overflow-alarms -no-collapse-call-cast
Compiling and executing o.i:
$ gcc o.i show_each.c -o o
t3.c: In function ‘func_31’:
t3.c:281: warning: large integer implicitly truncated to unsigned type
t3.c:299: warning: comparison of distinct pointer types lacks a cast
$ ./o
...
[value] Called Frama_C_show_each({3203885237})
However, parsing and printing o.i into t.i yields a program that computes differently when compiled:
$ ~/ppc/bin/toplevel.opt -machdep x86_64 o.i -print > t.i
$ gcc t.i show_each.c -o t
$ ./t
...
[value] Called Frama_C_show_each({4108310006})
## Attachments
- [t.i](/uploads/701b8fe4db3e2d684d2bc633ced43b57/t.i)
- [o.i](/uploads/45c2294cc609a8aeca8e16a3d35136d3/o.i)
- [show_each.c](/uploads/251a8941b78e8ae907f11334c8520b10/show_each.c)
https://git.frama-c.com/pub/frama-c/-/issues/1376
17944 using option -unspecified-access, no alarm for x + (x=0)
2021-02-22T13:29:09Z
Pascal Cuoq
17944 using option -unspecified-access, no alarm for x + (x=0)
ID0001144:
**This issue was created automatically from Mantis Issue 1144. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001144:
**This issue was created automatically from Mantis Issue 1144. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001144 | Frama-C | Kernel | public | 2012-04-07 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
On the program below, with bin/toplevel.opt -val -unspecified-access t.c, it would be desireable to have an alarm. Instead, the return value is computed as zero.
int main(void) { int d = 5; return d + (d=0);
}
https://git.frama-c.com/pub/frama-c/-/issues/2419
-2147483647<=0 unprovable by Simplify, except in switch
2021-04-15T09:17:24Z
Jochen Burghardt
-2147483647<=0 unprovable by Simplify, except in switch
ID0000415:
**This issue was created automatically from Mantis Issue 415. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000415:
**This issue was created automatically from Mantis Issue 415. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000415 | Frama-C | Plug-in > jessie | public | 2010-02-22 | 2010-03-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | cmarche | **Resolution** | no change required |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Simplify can prove neither -2147483648<=0 nor -2147483647<=0, see ftest8() and ftest7() in the attached file. However, it proves -2147483646<=0, see ftest6().
I suggest a jessie cmd-line option to generate -2147483646 rather than -2147483648 as MinInt, in order to circumvent this bug of Simplify, which causes many unprovable no-underflow-obligations in my programs.
Moreover, as a case of a switch, Simplify behaves different on -2147483647<=0: it can prove it there, see case 7 in ftest(). Probably, this is again a problem of Simplify. To ensure this, you could check that the proof obligations you generate are correct.
## Attachments
- [minInt01.c](/uploads/edf84b4457f0e4a42ec5f6bf1a2629ef/minInt01.c)
https://git.frama-c.com/pub/frama-c/-/issues/996
22446: unknown sizes of types and value initialization
2021-02-22T14:02:04Z
Pascal Cuoq
22446: unknown sizes of types and value initialization
ID0001416:
**This issue was created automatically from Mantis Issue 1416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001416:
**This issue was created automatically from Mantis Issue 1416. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001416 | Frama-C | Plug-in > Eva | public | 2013-05-07 | 2014-07-28 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Commit 22446 transforms a crash when some types have unknown sizes into a clean exit, but there remains a problem with the test below:
Sending src/value/initial_state.ml
Transmitting file data .
Committed revision 22446.
~/ppc $ cat t.c
struct s;
struct larger {
struct s t[2];
int i;
} v;
int main(int c, char **v)
{
return 0;
}
~/ppc $ bin/toplevel.opt -val t.c
[kernel] warning: cannot load 5 plug-ins (incompatible with Fluorine-20130401+dev).
Aorai; Obfuscator; Report; Security_slicing;
Wp
[kernel] preprocessing with "gcc -C -E -I. t.c"
[value] Analyzing a complete application starting at main
[value] Computing initial state
t.c:6:[value] warning: during initialization of variable 'v', size of type 'struct s' cannot be
computed (abstract type 'struct s')
[value] Initial state computed
[value] Values of globals at initialization
[kernel] Current source was: t.c:6
The full backtrace is:
Raised at file "cil/src/cil.ml", line 4250, characters 40-64
Called from file "cil/src/cil.ml", line 4763, characters 17-35
Called from file "src/project/state_builder.ml", line 556, characters 17-22
Called from file "src/misc/bit_utils.ml", line 245, characters 37-66
Called from file "list.ml", line 86, characters 24-34
Called from file "src/misc/bit_utils.ml", line 242, characters 37-1023
Called from file "src/misc/bit_utils.ml", line 432, characters 4-58
Called from file "src/memory_state/offsetmap.ml", line 1726, characters 14-160
Called from file "src/memory_state/offsetmap.ml", line 424, characters 10-34
Called from file "format.ml", line 1166, characters 10-25
Called from file "format.ml", line 1166, characters 10-25
Called from file "src/lib/pretty_utils.ml", line 89, characters 2-121
Called from file "format.ml", line 1166, characters 10-25
Called from file "src/value/eval_funs.ml", line 317, characters 6-176
Called from file "src/value/eval_funs.ml", line 567, characters 11-40
Re-raised at file "src/value/eval_funs.ml", line 583, characters 47-50
Called from file "src/project/state_builder.ml", line 839, characters 9-13
Re-raised at file "src/project/state_builder.ml", line 847, characters 15-18
Called from file "src/value/register.ml", line 82, characters 4-24
Called from file "queue.ml", line 135, characters 6-20
Called from file "src/kernel/boot.ml", line 37, characters 4-20
Called from file "src/kernel/cmdline.ml", line 732, characters 2-9
Called from file "src/kernel/cmdline.ml", line 212, characters 4-8
Unexpected error (Cil.SizeOfError("abstract type 'struct s'", _)).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Fluorine-20130401+dev.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
~/ppc $
https://git.frama-c.com/pub/frama-c/-/issues/223
2D variable length array
2021-02-22T14:01:16Z
Julien Signoles
2D variable length array
ID0002186:
**This issue was created automatically from Mantis Issue 2186. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002186:
**This issue was created automatically from Mantis Issue 2186. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002186 | Frama-C | Kernel | public | 2015-11-03 | 2018-11-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | duplicate |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
2D variable length arrays are valid wrt C99 but rejected by Frama-C:
=====
extern int n;
int main(void) {
int a[n]; // accepted
int b[n][n]; // should be accepted, but refused
return 0;
}
=====
$ frama-c a.i
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing a.i (no preprocessing)
a.i:4:[kernel] warning: Variable-sized local variable a
a.i:5:[kernel] user error: Length of array is not a constant: n
a.i:5:[kernel] warning: Variable-sized local variable b
[kernel] user error: stopping on file "a.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
### Additional Information :
Reported by email by G. Karpenkov
https://git.frama-c.com/pub/frama-c/-/issues/803
Able to assert a false statement
2021-04-15T08:31:46Z
mantis-gitlab-migration
Able to assert a false statement
ID0002087:
**This issue was created automatically from Mantis Issue 2087. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002087:
**This issue was created automatically from Mantis Issue 2087. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002087 | Frama-C | Plug-in > wp | public | 2015-03-03 | 2015-03-09 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Ian | **Assigned To** | correnson | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | Ubuntu | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In the attached program, 'absurd' validates when it should not. The is only observed when all of the following conditions are met.
'num' must be part of a struct, which can be global (as in the program below) or returned from split.
Changing the assigns to only r.num cause the correct behavior. However, if the struct is returned from split, absurd still validates.
'split' must be called, if the body is inlined, the bad behavior is not observed.
Alt-ergo 0.99.1 must be used, can not replicate using 0.95.2
The expression must be '5/2', I have not found any other numbers that causes this behavior.
### Steps To Reproduce :
Create struc_div.c (attached):
struct result {
int num;
};
struct result r;
/*@
assigns r;
ensures r.num == 5/2;
*/
void split() {
r.num = 5/2;
}
void test_split() {
split();
//@ assert absurd: r.num == -99 && r.num == 99;
}
Run:
frama-c struct_div.c -wp -wp-rte
Results:
[kernel] preprocessing with "gcc -C -E -I. struct_div.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function split
[rte] annotating function test_split
[wp] 3 goals scheduled
[wp] [Qed] Goal typed_split_post : Valid
[wp] [Qed] Goal typed_split_assign : Valid
[wp] [Alt-Ergo] Goal typed_test_split_assert_absurd : Valid (26ms) (18)
[wp] Proved goals: 3 / 3
Qed: 2
Alt-Ergo: 1 (26ms-26ms) (18)
Expected that 'absurd' assertion should not validate.
## Attachments
- [struct_div.c](/uploads/bcd65e49d23e7f76196a0a8f49474af9/struct_div.c)
- [foo.mlw](/uploads/7def6a9caa1198c52f69c52f37493bc9/foo.mlw)
Loïc Correnson
Loïc Correnson
https://git.frama-c.com/pub/frama-c/-/issues/893
access to nested union/struct component causes crash
2021-03-29T16:12:05Z
Jochen Burghardt
access to nested union/struct component causes crash
ID0001803:
**This issue was created automatically from Mantis Issue 1803. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001803:
**This issue was created automatically from Mantis Issue 1803. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001803 | Frama-Clang | Kernel | public | 2014-06-06 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | xubuntu-cfe13.10 | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
If, in the resolved issue #1754, the outermost "struct" is changed to "union" (file "1_4_2us.cpp"), the crash re-appears:
Now output intermediate result
1_4_2us.cpp:2:[fclang] failure: No usable default constructor for _s::_w
[kernel] Current source was: 1_4_2us.cpp:2
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "convert.ml", line 1367, characters 30-75
Called from file "convert.ml", line 1399, characters 17-43
Called from file "list.ml", line 74, characters 24-34
Called from file "convert.ml", line 1425, characters 23-65
Called from file "convert.ml", line 1802, characters 21-133
Called from file "list.ml", line 74, characters 24-34
Called from file "convert.ml", line 1876, characters 19-78
Called from file "convert.ml", line 2102, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "convert.ml", line 2106, characters 4-79
Called from file "frama_Clang_register.ml", line 82, characters 13-36
Called from file "src/kernel/file.ml", line 1058, characters 10-43
Called from file "src/kernel/file.ml", line 1102, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1099, characters 6-520
Called from file "src/kernel/file.ml", line 2144, characters 12-30
Called from file "src/kernel/file.ml", line 2229, characters 4-27
Called from file "src/kernel/ast.ml", line 113, characters 2-28
Called from file "src/kernel/ast.ml", line 125, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 735, characters 2-9
Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301.
If instead, or additionally, the inner "struct" is changed to "union" (files "1_4_2su.cpp" and "1_4_2uu.cpp"), a strange warning is issued:
Now output intermediate result
1_4_2su.cpp:3:[kernel] warning: Calling undeclared function Frama_C_memcpy. Old style K&R code?
## Attachments
- [1_4_2us.cpp](/uploads/d21782d1d8724590e1a9f532c053ab0f/1_4_2us.cpp)
- [1_4_2su.cpp](/uploads/c40254eb1bf606da7ca5bb1fd976753e/1_4_2su.cpp)
- [1_4_2uu.cpp](/uploads/b8d0faf5f634dc32b476e057713a797c/1_4_2uu.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/638
access to static struct fields unsupported in annotation
2021-02-22T13:39:53Z
Jochen Burghardt
access to static struct fields unsupported in annotation
ID0002116:
**This issue was created automatically from Mantis Issue 2116. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002116:
**This issue was created automatically from Mantis Issue 2116. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002116 | Frama-Clang | Plug-in > clang | public | 2015-05-07 | 2015-05-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Sodium-20150201 | **OS** | - | **OS Version** | xubuntu14.04 |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 479.cpp (external front-end)
479.cpp:9:18: Unsupported Field Access to s in struct Cl
Now output intermediate result
(Despite the error message, provers are called, when command-line option "-wp" is used.)
The error disappears if (line 8 is activated and) line 9 is deactivated.
## Attachments
- [479.cpp](/uploads/abca3d8bf2819f8cdb4b49d9f829011c/479.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/1190
access to volatile variable is eliminated from AST
2021-02-22T13:22:42Z
Pascal Cuoq
access to volatile variable is eliminated from AST
ID0001589:
**This issue was created automatically from Mantis Issue 1589. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001589:
**This issue was created automatically from Mantis Issue 1589. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001589 | Frama-C | Kernel | public | 2013-12-26 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
~ $ cat n.c
volatile int x;
int main(){
x; x; x;
}
~ $ ~/ppc/bin/toplevel.opt -print n.c
[kernel] preprocessing with "gcc -C -E -I. n.c"
/* Generated by Frama-C */
int volatile x;
int main(void)
{
int __retres;
__retres = 0;
return __retres;
}
This transformation does not respect the semantics of the program because x is volatile.
https://git.frama-c.com/pub/frama-c/-/issues/1929
ACSL builtins
2021-02-22T13:46:18Z
Loïc Correnson
ACSL builtins
ID0000816:
**This issue was created automatically from Mantis Issue 816. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...
ID0000816:
**This issue was created automatically from Mantis Issue 816. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000816 | Frama-C | Plug-in > wp | public | 2011-05-10 | 2012-12-06 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | correnson | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | N/A |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Support for ACSL builtin functions (\max, \abs, \is_finite ...) with their overloaded specifications
https://git.frama-c.com/pub/frama-c/-/issues/896
ACSL comment rejected in function template
2021-02-22T13:27:13Z
Jochen Burghardt
ACSL comment rejected in function template
ID0002048:
**This issue was created automatically from Mantis Issue 2048. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0002048:
**This issue was created automatically from Mantis Issue 2048. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002048 | Frama-Clang | Plug-in > clang | public | 2015-01-12 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 430.cpp (external front-end)
inadequate comment at 430.cpp:5:2
If line 2 is commented-in and line 3 is commented-out, the error message disappears.
## Attachments
- [430.cpp](/uploads/fb7c1b9a2c7e740eb0e5c7200661ce99/430.cpp)
Virgile Prevosto
Virgile Prevosto
https://git.frama-c.com/pub/frama-c/-/issues/1173
ACSL label LoopEntry not handled by WP
2022-10-06T14:57:24Z
mantis-gitlab-migration
ACSL label LoopEntry not handled by WP
ID0001353:
**This issue was created automatically from Mantis Issue 1353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...
ID0001353:
**This issue was created automatically from Mantis Issue 1353. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001353 | Frama-C | Plug-in > wp | public | 2013-01-30 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | correnson | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
As said in the title, the ACSL label LoopEntry seems to be not handled by WP but it is accepted by the kernel.
Using the -wp-warnings option I got warnings like :
- Warning: Generalization of un-labeled values
Reason: Some labels may escape the control flow
but it took me some time to understand the problem.
In the example below, changing LoopEntry by L in the loop invariant makes it work.
BTW, in the example below, it doesn't work either when removing the first (c++;) statement !
### Additional Information :
int G;
//@ requires G == 0; ensures G == 0;
void f (int c) {
c++;
L: //@ loop invariant G == \at (G, LoopEntry);
while (c) c++;
}