frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2021-04-15T09:17:07Zhttps://git.frama-c.com/pub/frama-c/-/issues/225111 if-statements lead to why-runtime >12 min2021-04-15T09:17:07ZJochen Burghardt11 if-statements lead to why-runtime >12 minID0000688:
**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/127612799, doubtful choice of promotion x86_64 mode (csmith)2021-02-22T13:25:44ZPascal Cuoq12799, 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/126812816: Missing label in sliced program (csmith)2021-02-22T14:02:52ZPascal Cuoq12816: 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/215012825, sliced program does not terminate2021-02-22T14:04:20ZPascal Cuoq12825, sliced program does not terminateID0000789:
**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/208514055: sliced program does not terminate (csmith)2021-02-22T13:50:39ZPascal Cuoq14055: 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/178614292: warn for unspecified side-effect that are separated by a function call...2021-02-22T13:41:45ZPascal Cuoq14292: 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/208214403: last slicing bug (csmith)2021-02-22T13:50:34ZPascal Cuoq14403: 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/136817514, -unspecified-access and if (*p = (*p < 3)) (csmith)2024-03-12T17:06:13ZPascal Cuoq17514, -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/206617517: defined program behaves differently after going through -print (csmith)2021-02-22T13:50:12ZPascal Cuoq17517: 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/137617944 using option -unspecified-access, no alarm for x + (x=0)2021-02-22T13:29:09ZPascal Cuoq17944 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 switch2021-04-15T09:17:24ZJochen Burghardt-2147483647<=0 unprovable by Simplify, except in switchID0000415:
**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/99622446: unknown sizes of types and value initialization2021-02-22T14:02:04ZPascal Cuoq22446: unknown sizes of types and value initializationID0001416:
**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/2232D variable length array2021-02-22T14:01:16ZJulien Signoles2D variable length arrayID0002186:
**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. Karpenkovhttps://git.frama-c.com/pub/frama-c/-/issues/803Able to assert a false statement2021-04-15T08:31:46Zmantis-gitlab-migrationAble to assert a false statementID0002087:
**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 CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/893access to nested union/struct component causes crash2021-03-29T16:12:05ZJochen Burghardtaccess to nested union/struct component causes crashID0001803:
**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 PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/1190access to volatile variable is eliminated from AST2021-02-22T13:22:42ZPascal Cuoqaccess to volatile variable is eliminated from ASTID0001589:
**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/1929ACSL builtins2021-02-22T13:46:18ZLoïc CorrensonACSL builtinsID0000816:
**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 specificationshttps://git.frama-c.com/pub/frama-c/-/issues/1173ACSL label LoopEntry not handled by WP2022-10-06T14:57:24Zmantis-gitlab-migrationACSL label LoopEntry not handled by WPID0001353:
**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++;
}https://git.frama-c.com/pub/frama-c/-/issues/549ACSL manual:issues affecting technical correctness or understanding2021-02-22T13:56:09ZDavid CokACSL manual:issues affecting technical correctness or understandingID0002114:
**This issue was created automatically from Mantis Issue 2114. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002114:
**This issue was created automatically from Mantis Issue 2114. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002114 | Frama-C | Documentation > ACSL | public | 2015-05-05 | 2016-01-26 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dcok@grammatech.com | **Assigned To** | patrick | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | Frama-C Magnesium | **Fixed in Version** | Frama-C Magnesium |
### Description :
These are issues affecting technical correctness or understanding that I encountered in a recent read through of the ACSL 1.9 manual.
p. 27: There are extraneous { delimiters in the example.
p. 51/52, Example 2.42: Either line 3 of the example should have ? (n-1) :" instead of "? n :" or the explanation should be corrected.
p. 56, Example 2.47: "modifies t[k]" -> "only modifies t[k]"
p. 57: "where the file list.acsl contains logic definitions" -> "where the file List.acsl contains logic definitions" - at least I presume the name of the file must be a case-senstive match to the name of the module
p. 58: "\valid {L}(p) <==> \valid{L}(((char *)p)+(0..sizeof(*p)))" should be "\valid {L}(p) <==> \valid{L}(((char *)p)+(0..sizeof(*p)-1))" and similarly for \valid_read
p. 71, Example 2.59: These specs allow forbidden to have more values than the union of {\result} and \old(forbidden)
p. 72: In "It is however possible to write multi-line annotations for ghost code. These annotations
are enclosed between /@ and @/. As in normal annotations, @s at the beginning of a line
and at the end of the comment (before the final @/) are considered as blank." the /@ and @/ should be /*@ and @*/
### Steps To Reproduce :
Read the documentationhttps://git.frama-c.com/pub/frama-c/-/issues/1840ACSL parser + pretty-printer2021-02-22T13:43:50Zmantis-gitlab-migrationACSL parser + pretty-printerID0000862:
**This issue was created automatically from Mantis Issue 862. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000862:
**This issue was created automatically from Mantis Issue 862. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000862 | Frama-C | Kernel > ACSL implementation | public | 2011-06-10 | 2013-06-20 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | ckunz | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | normal | **Severity** | tweak | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130401 |
### Description :
Logic assertions of the form
(a) //@ assert x == y^z;
are parsed as (x==y)^y and are thus rejected by the type-checker. One must instead write the assertion above as follows
(b) //@ assert x == (y^z);
This may be understandable. The pretty-printer, however, after parsing the term (b), outputs the term (a), making the output of the pretty-printer a program that is syntactically invalid.