frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2024-03-15T09:13:18Zhttps://git.frama-c.com/pub/frama-c/-/issues/1316Results differ between value analysis and GCC on bitfields2024-03-15T09:13:18ZBenjamin MonateResults differ between value analysis and GCC on bitfieldsID0000890:
**This issue was created automatically from Mantis Issue 890. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000890:
**This issue was created automatically from Mantis Issue 890. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000890 | Frama-C | Plug-in > Eva | public | 2011-07-25 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | monate | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
On the program
==bug.i==============
union U0 {
unsigned short f0 ;
int f1 ;
int f2 : 5 ;
unsigned char const f3 ;
};
unsigned short G0 ;
int G1 ;
int G2;
unsigned char G3 ;
union U0 G={(unsigned short)65532U};
int main() {
G0=G.f0;
G1=G.f1;
G2=G.f2;
G3=G.f3;
printf("%d %d %d %d : %d\n",G0,G1,G2,G3,G2==-4);
return (G2==-4);
}
=========================
frama-c -val bug.i
returns:
===
[value] Values for function main:
G0 ? {65532}
G1[bits 0 to 15] ? {65532}
[bits 16 to 31] ? {0}
G2 ? {28}
G3# ? {65532} misaligned 0%16
__retres ? {0}
===
but gcc bug.i && ./a.out ; echo $?
displays :
===
65532 65532 -4 252 : 1
1
===
They do not agree on the result nor on the value of G2.https://git.frama-c.com/pub/frama-c/-/issues/1313Crash du builtin memcpy, par une exception non rattrapable2023-11-27T14:01:56ZBoris YakobowskiCrash du builtin memcpy, par une exception non rattrapableID0000883:
**This issue was created automatically from Mantis Issue 883. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000883:
**This issue was created automatically from Mantis Issue 883. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000883 | Frama-C | Plug-in > Eva | public | 2011-07-07 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | yakobowski | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
À analyser avec -val
extern unsigned int i;
char src[20];
char dst[10];
void main () {
if (i <= 10)
Frama_C_memcpy(dst+1, src, i);
}
### Additional Information :
svn 14142https://git.frama-c.com/pub/frama-c/-/issues/1258Unexpected error (Ival.Float_abstract.Bottom)2023-11-27T14:01:56Zmantis-gitlab-migrationUnexpected error (Ival.Float_abstract.Bottom)ID0000752:
**This issue was created automatically from Mantis Issue 752. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000752:
**This issue was created automatically from Mantis Issue 752. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000752 | Frama-C | Plug-in > Eva | public | 2011-03-11 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kerstin | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Nitrogen-20111001 |
### Description :
Crash if the 3 assertions are added to the program.
Unexpected error (Ival.Float_abstract.Bottom).
commandline: frama-c-gui -val -slevel 10 -main interp interp_bug.c
frama-c -val -slevel 10 -main interp interp_bug.c
## Attachments
- [interp_bug.c](/uploads/d959ec698d88e05db6586ff4c99a6246/interp_bug.c)https://git.frama-c.com/pub/frama-c/-/issues/2668[EVA] unsoundness when initializing in switch statement before first case2023-09-20T08:51:15ZJulien Lepiller[EVA] unsoundness when initializing in switch statement before first case<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
The following code is validated by EVA:
```c
#include <stdio.h>
int main(int argc, char *argv[]) {
switch(argc) {
int i = 5;
case 0:
i = 17;
// fall-through
default:
//@ assert i == 17;
printf("%d\n", i);
}
return 0;
}
```
The file is run through frama-c:
```bash
frama-c -eva test.c
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Eva should not validate the assert, since "i" is possibly uninitialized. This is because in C, code between the switch statement and the first case is not executed. Note that frama-c-gui correctly shows that code as dead code.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Eva validates the assert. No warnings are generated.
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *27.1 (Cobalt)*
- Plug-in used: *Eva*
- OS name: *Ubuntu*
- OS version: *22.04*
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
When using `-slevel 2` or above, Eva does not validate the assert, but still validates the generated `\initialized` assert for `printf`.
If `int i` is not initialized before the first case, Eva does not validate the assert. If a `break` is inserted, it does not validate the assert either.David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/2660[Eva] The plugin doesn't terminate on this program2023-05-17T08:21:52ZCharles Babu M[Eva] The plugin doesn't terminate on this program### Steps to reproduce the issue
I ran ```dune exec -- frama-c loop_nla.c -eva```
```
/* Compute the floor of the square root, by Dijkstra */
extern void abort(void);
extern void __assert_fail(const char *, const char *, unsigned int...### Steps to reproduce the issue
I ran ```dune exec -- frama-c loop_nla.c -eva```
```
/* Compute the floor of the square root, by Dijkstra */
extern void abort(void);
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
void reach_error() { __assert_fail("0", "dijkstra-u.c", 5, "reach_error"); }
extern unsigned int __VERIFIER_nondet_uint(void);
extern void abort(void);
void assume_abort_if_not(int cond) {
if(!(cond)) { abort();}
return;
}
void __VERIFIER_assert(int cond) {
if (!(cond)) {
ERROR:
{reach_error();}
}
return;
}
int counter = 0;
int main() {
unsigned int n, p, q, r, h;
n = __VERIFIER_nondet_uint();
assume_abort_if_not(n < 4294967295 / 4); // Avoid non-terminating loop
p = 0;
q = 1;
r = n;
h = 0;
while (counter++<1) {
if (!(q <= n))
break;
q = 4 * q;
}
//q == 4^n
while (counter++<1) {
__VERIFIER_assert(r < 2 * p + q);
__VERIFIER_assert(p*p + r*q - n*q == 0);
__VERIFIER_assert(h * h * h - 12 * h * n * q + 16 * n * p * q - h * q * q - 4 * p * q * q + 12 * h * q * r - 16 * p * q * r == 0);
__VERIFIER_assert(h * h * n - 4 * h * n * p + 4 * (n * n) * q - n * q * q - h * h * r + 4 * h * p * r - 8 * n * q * r + q * q * r + 4 * q * r * r == 0);
__VERIFIER_assert(h * h * p - 4 * h * n * q + 4 * n * p * q - p * q * q + 4 * h * q * r - 4 * p * q * r == 0);
__VERIFIER_assert(p * p - n * q + q * r == 0);
if (!(q != 1))
break;
q = q / 4;
h = p + q;
p = p / 2;
if (r >= h) {
p = p + q;
r = r - h;
}
}
__VERIFIER_assert(h*h*h - 12*h*n + 16*n*p + 12*h*r - 16*p*r - h - 4*p == 0);
__VERIFIER_assert(p*p - n + r == 0);
__VERIFIER_assert(h*h*p - 4*h*n + 4*n*p + 4*h*r - 4*p*r - p == 0);
return 0;
}
```
### Expected behaviour
It should terminate
### Actual behaviour
It does not terminate.
But if I change the ```assume_abort_if_not``` function by replacing the condition as below, it terminates
```
void assume_abort_if_not(int cond) {
if((cond)==0) { abort();}
return;
}
```
### Contextual information
- Frama-C installation mode: from source
- Frama-C version: 25.0~beta (Manganese)
- Plug-in used: EVA
- OS name: Ubuntu
- OS version: 20.04.6 LTSAndre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/1209Interpretation of @ assigns \result;2023-05-16T12:35:51Zmantis-gitlab-migrationInterpretation of @ assigns \result;ID0001448:
**This issue was created automatically from Mantis Issue 1448. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001448:
**This issue was created automatically from Mantis Issue 1448. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001448 | Frama-C | Plug-in > Eva | public | 2013-06-20 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Anne | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130501 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Sorry for the title which is not very informative, but here is the problem :
in this example :
//@ assigns \result;
extern char * get_ptr (void);
int main (void) { char * p = get_ptr (); int x = p ? 0 : 1; return x; }
The value analysis tells me that the else branch is dead, so x is always 0.
If I change the assigns property into :
//@ assigns \result \from \nothing;
The problem disappears.https://git.frama-c.com/pub/frama-c/-/issues/1248possible unsoundness bug2023-05-05T02:36:31ZJohn Regherpossible unsoundness bugID0000717:
**This issue was created automatically from Mantis Issue 717. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000717:
**This issue was created automatically from Mantis Issue 717. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000717 | Frama-C | Plug-in > Eva | public | 2011-02-12 | 2014-02-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | regehr | **Assigned To** | pascal | **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 Nitrogen-20111001 |
### Description :
This is on Ubuntu 10.10 on x86.
Analyzing the attached program like this:
toplevel.opt -val -slevel 24 foo_pp.c
Gives output including:
*(unsigned char*)((unsigned char*)&g_8+30) == 0
However, running the program leaves the value 243 in this byte.
## Attachments
- [foo_pp.c](/uploads/d4618293170dad277408009f857c0c3d/foo_pp.c)https://git.frama-c.com/pub/frama-c/-/issues/918Value analysis generates incorrect Imperative outputs for arrays2022-10-06T14:57:24Zmantis-gitlab-migrationValue analysis generates incorrect Imperative outputs for arraysID0002030:
**This issue was created automatically from Mantis Issue 2030. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002030:
**This issue was created automatically from Mantis Issue 2030. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002030 | Frama-C | Plug-in > Eva | public | 2014-12-12 | 2015-01-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gaggarwal | **Assigned To** | yakobowski | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | - |
### Description :
In case, the size of an array is not known, value analysis generated array[0..1] as Imperative outputs of a function updating array.
### Additional Information :
In above example I tried adding some bound on variable count using requires clause as below:
/*@
requires 0 < count < 8;
*/
void copy(int* src, int* dest, int count) {
for(int i=0; i<count; i++) {
dest[i] = src[i];
}
}
Even then imperative output of function copy generated was S_dest[0..1]
### Steps To Reproduce :
For example: Consider a file f.c has below copy function:
void copy(int* src, int* dest, int count) {
for(int i=0; i<count; i++) {
dest[i] = src[i];
}
}
Execute: frama-c -val -out-external -lib-entry -main copy f.c
Result: [inout] Out (external) for function copy:
S_dest[0..1]
S_dest[0..1] is not a over-estimation of location which can be modified by function copy.https://git.frama-c.com/pub/frama-c/-/issues/1157Logging just enough information for failed pre-conditions2022-10-03T08:07:55ZPascal CuoqLogging just enough information for failed pre-conditionsID0001415:
**This issue was created automatically from Mantis Issue 1415. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001415:
**This issue was created automatically from Mantis Issue 1415. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001415 | Frama-C | Plug-in > Eva | public | 2013-05-03 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
There was a bit of a discussion over an analysis made on an example provided by a StackOverflow user:
http://stackoverflow.com/a/16356519/139746
The current message is:
.../libc/string.h:54:[value] Function memcpy: precondition got status invalid.
That is a bit frustrating. The localization of the call to memcpy() can be found just above in the log:
[value] computing for function memcpy <- main.
Called from mem.c:13.
but the exact nature of the detected issue is only printed as a reference to libc/string.h, a file that the user did not even provide emself.
There are at least two solutions suggested by the discussion:
- annotate the libc preconditions with nice labels, and when a pre-condition fails, print any label it may have, or
- print the entire ACSL pre-condition that failed, including any label it may have.https://git.frama-c.com/pub/frama-c/-/issues/2585Unexpected error (Stack overflow) with large array sizes and expressions2022-09-15T15:56:24Zarindam-8Unexpected error (Stack overflow) with large array sizes and expressions
### Steps to reproduce the issue
[fc-bug.c](/uploads/a314f79930f93d2f2a1cea3080b7b043/fc-bug.c)Run the following command:
```
frama-c -eva -eva-slevel 100 -eva-plevel 256 -eva-precision 5 -eva-warn-undefined-pointer-comparison pointe...
### Steps to reproduce the issue
[fc-bug.c](/uploads/a314f79930f93d2f2a1cea3080b7b043/fc-bug.c)Run the following command:
```
frama-c -eva -eva-slevel 100 -eva-plevel 256 -eva-precision 5 -eva-warn-undefined-pointer-comparison pointer -eva-no-alloc-returns-null -warn-signed-overflow -eva-no-show-progress -machdep x86_64 fuzzer-file-102106.c
```
### Expected behaviour
Frama-C when run on the test program with the given command should exit gracefully instead of resulting in an "Unexpected
stackoverflow error"
### Actual behaviour
When Frama-C is run on the program with the given command parameters it results in a Frama-C crash. with the following trace (abbreviated)
```
[kernel] Parsing _rmv_fuzzer-file-102106.c (with preprocessing)
[eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
option -eva-min-loop-unroll set to 0 (default value).
option -eva-auto-loop-unroll set to 128.
option -eva-widening-delay set to 3 (default value).
option -eva-partition-history set to 0 (default value).
option -eva-slevel already set to 100.
option -eva-ilevel set to 48.
option -eva-plevel already set to 256 (not modified).
option -eva-subdivide-non-linear set to 100.
option -eva-remove-redundant-alarms set to true (default value).
option -eva-domains set to 'cvalue,equality,gauges,octagon,symbolic-locations'.
option -eva-split-return set to 'auto'.
option -eva-equality-through-calls set to 'formals' (default value).
option -eva-octagon-through-calls set to false (default value).
[eva] Splitting return states on:
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
b.f2 ∈ {0}
.f3 ∈ {65006}
.[bits 65047 to 65055] ∈ {0}
.f5 ∈ {65005}
.[bits 130059 to 130063] ∈ {0}
.f6 ∈ {-536}
g.f2 ∈ {65008}
.f3 ∈ {65000}
.[bits 65047 to 65055] ∈ {0}
.f5 ∈ {65005}
.[bits 130059 to 130063] ∈ {0}
.f6 ∈ {-536}
d ∈ {0}
l ∈ {0}
a ∈ {0}
c ∈ {0}
h ∈ {65008}
e[0] ∈ {-20}
[1..65236] ∈ {0}
f ∈ {{ &d }}
i[0] ∈ {-533}
[1..65004] ∈ {0}
j ∈ {0}
k ∈ {{ &c }}
[kernel] Current source was: _rmv_fuzzer-file-102106.c:20
The full backtrace is:
Raised by primitive operation at file "src/blocks.ml", line 691, characters 11-59
Called from file "src/blocks.ml", line 703, characters 17-53
Called from file "src/libraries/utils/wto.ml", line 168, characters 18-36
Called from file "src/libraries/utils/wto.ml", line 170, characters 34-66
...
Unexpected error (Stack overflow).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 22.0 (Titanium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: Bionic 18.04
### Additional information (optional)
The crash seems inconsistent and appears sporadically. It seg-faults on some occasions while on others it crashes like mentioned above. With such expression length issues the crash seems legitimate.David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/1152strange warning "postcondition got status invalid"2022-08-29T14:56:07ZJochen Burghardtstrange warning "postcondition got status invalid"ID0001369:
**This issue was created automatically from Mantis Issue 1369. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001369:
**This issue was created automatically from Mantis Issue 1369. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001369 | Frama-C | Plug-in > Eva | public | 2013-02-15 | 2014-03-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | yakobowski | **Resolution** | fixed |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Oxygen-20120901 | **Target Version** | Frama-C Neon-20140301 | **Fixed in Version** | Frama-C Neon-20140301 |
### Description :
Running "frama-c -val ftest.c" on the attached program produces a "[value] Function foo: postcondition got status invalid" in line 6, although the ensures clause looks quite reasonable. (I don't understand the notion of a "postcondition status": shouldn't the postconditions of a function be satisfied automatically if all its preconditions are?) The warning disappears if the ensures clause in line 5 is removed or an appropriate function body (e.g. the one commented out at the end of line 6) is added.
## Attachments
- [ftest.c](/uploads/0c897adefea2db69ea93598a19ce19bc/ftest.c)https://git.frama-c.com/pub/frama-c/-/issues/2610Unexpected error (File "src/plugins/value/engine/evaluation.ml", line 1176, c...2022-06-10T07:53:40ZKarine EMUnexpected error (File "src/plugins/value/engine/evaluation.ml", line 1176, characters 14-20: Assertion failed)<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
frama-c -eva -eva-slevel 100 -eva-plevel 256 -eva-precision 5 -eva-warn-undefined-pointer-comparison pointer -eva-no-alloc-returns-null -warn-signed-overflow -eva-no-show-progress -machdep x86_64 test.c
with this test case:
```
struct a c;
struct a {
unsigned b;
} d(struct a *e, unsigned f) {
g(e);
0 - e->b * -((long)f >> (int)e->b >> 3 * f - e->b) * -e->b - (int)e;
}
main() { d(&c, 55); }
```
will crash with this error:
```
[kernel] Parsing fuzzer-file-17090.c (with preprocessing)
[kernel:typing:implicit-function-declaration] fuzzer-file-17090.c:5: Warning:
Calling undeclared function g. Old style K&R code?
[kernel:CERT:MSC:37] fuzzer-file-17090.c:6: Warning:
Body of function d falls-through. Adding a return statement
[eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
option -eva-min-loop-unroll set to 0 (default value).
option -eva-auto-loop-unroll set to 128.
option -eva-widening-delay set to 3 (default value).
option -eva-partition-history set to 0 (default value).
option -eva-slevel already set to 100.
option -eva-ilevel set to 48.
option -eva-plevel already set to 256 (not modified).
option -eva-subdivide-non-linear set to 100.
option -eva-remove-redundant-alarms set to true (default value).
option -eva-domains set to 'cvalue,equality,gauges,octagon,symbolic-locations'.
option -eva-split-return set to 'auto'.
option -eva-equality-through-calls set to 'formals' (default value).
option -eva-octagon-through-calls set to false (default value).
[eva] Splitting return states on:
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
c ∈ {0}
[kernel:annot:missing-spec] fuzzer-file-17090.c:5: Warning:
Neither code nor specification for function g, generating default assigns from the prototype
[eva] using specification for function g
[kernel] Current source was: fuzzer-file-17090.c:6
The full backtrace is:
Raised at Evaluation.Make.find_val in file "src/plugins/value/engine/evaluation.ml", line 1176, characters 14-26
Called from Evaluation.Make.internal_backward.(fun) in file "src/plugins/value/engine/evaluation.ml", line 1301, characters 6-17
Called from Evaluation.Make.internal_backward.(fun) in file "src/plugins/value/engine/evaluation.ml", line 1307, characters 6-36
Called from Evaluation.Make.evaluate.(fun) in file "src/plugins/value/engine/evaluation.ml", line 1534, characters 8-56
Called from Bottom.Type.(>>-) in file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from Evaluation.Make.evaluate in file "src/plugins/value/engine/evaluation.ml", line 1532, characters 8-163
Called from Transfer_stmt.Make.evaluate_and_check in file "src/plugins/value/engine/transfer_stmt.ml", line 164, characters 14-59
Called from Transfer_stmt.Make.assign_by_eval in file "src/plugins/value/engine/transfer_stmt.ml", line 184, characters 4-54
Called from Transfer_stmt.Make.assign_lv_or_ret in file "src/plugins/value/engine/transfer_stmt.ml", line 258, characters 10-55
Called from Initialization.Make.apply_cil_single_initializer in file "src/plugins/value/engine/initialization.ml", line 131, characters 10-48
Called from Initialization.Make.initialize_local_variable in file "src/plugins/value/engine/initialization.ml", line 304, characters 8-95
Called from Iterator.Make_Dataflow.lift' in file "src/plugins/value/engine/iterator.ml", line 234, characters 33-36
Called from Partition.MakeFlow.transfer.transfer in file "src/plugins/value/partitioning/partition.ml", line 649, characters 29-42
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Iterator.Make_Dataflow.process_edge in file "src/plugins/value/engine/iterator.ml", line 436, characters 15-74
Called from Iterator.Make_Dataflow.process_vertex.process_source in file "src/plugins/value/engine/iterator.ml", line 501, characters 18-35
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Iterator.Make_Dataflow.process_vertex in file "src/plugins/value/engine/iterator.ml", line 503, characters 18-60
Called from Iterator.Make_Dataflow.iterate_element in file "src/plugins/value/engine/iterator.ml", line 550, characters 13-31
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Iterator.Make_Dataflow.iterate_list in file "src/plugins/value/engine/iterator.ml" (inlined), line 547, characters 4-31
Called from Iterator.Make_Dataflow.compute in file "src/plugins/value/engine/iterator.ml", line 609, characters 6-22
Called from Iterator.Computer.compute.compute in file "src/plugins/value/engine/iterator.ml", line 776, characters 20-39
Called from Value_util.protect in file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from Compute_functions.Make.compute_using_spec_or_body in file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from Compute_functions.Make.compute_and_cache_call in file "src/plugins/value/engine/compute_functions.ml", line 228, characters 26-36
Called from Transfer_stmt.Make.process_call.process in file "src/plugins/value/engine/transfer_stmt.ml", line 326, characters 10-53
Called from Value_util.protect in file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from Transfer_stmt.Make.do_one_call in file "src/plugins/value/engine/transfer_stmt.ml", line 463, characters 22-70
Called from Transfer_stmt.Make.call.(fun).process_one_function.(fun) in file "src/plugins/value/engine/transfer_stmt.ml", line 767, characters 14-73
Called from Bottom.Type.(>>-:) in file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from Transfer_stmt.Make.call.(fun).process_one_function in file "src/plugins/value/engine/transfer_stmt.ml", line 762, characters 12-489
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Bottom.Type.(>>-:) in file "src/kernel_services/abstract_interp/bottom.ml", line 36, characters 25-30
Called from Transfer_stmt.Make.call in file "src/plugins/value/engine/transfer_stmt.ml", line 749, characters 6-1023
Called from Iterator.Make_Dataflow.transfer_call in file "src/plugins/value/engine/iterator.ml", line 278, characters 6-47
Called from Partition.MakeFlow.transfer.transfer in file "src/plugins/value/partitioning/partition.ml", line 649, characters 29-42
Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34
Called from Iterator.Make_Dataflow.process_edge in file "src/plugins/value/engine/iterator.ml", line 436, characters 15-74
Called from Iterator.Make_Dataflow.process_vertex.process_source in file "src/plugins/value/engine/iterator.ml", line 501, characters 18-35
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Iterator.Make_Dataflow.process_vertex in file "src/plugins/value/engine/iterator.ml", line 503, characters 18-60
Called from Iterator.Make_Dataflow.iterate_element in file "src/plugins/value/engine/iterator.ml", line 550, characters 13-31
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Iterator.Make_Dataflow.iterate_list in file "src/plugins/value/engine/iterator.ml" (inlined), line 547, characters 4-31
Called from Iterator.Make_Dataflow.compute in file "src/plugins/value/engine/iterator.ml", line 609, characters 6-22
Called from Iterator.Computer.compute.compute in file "src/plugins/value/engine/iterator.ml", line 776, characters 20-39
Called from Value_util.protect in file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from Compute_functions.Make.compute_using_spec_or_body in file "src/plugins/value/engine/compute_functions.ml", line 206, characters 8-45
Called from Compute_functions.Make.compute.compute in file "src/plugins/value/engine/compute_functions.ml", line 344, characters 8-63
Called from Value_util.protect in file "src/plugins/value/utils/value_util.ml", line 114, characters 6-10
Called from Analysis.force_compute in file "src/plugins/value/engine/analysis.ml", line 181, characters 2-49
Called from State_builder.apply_once.(fun) in file "src/libraries/project/state_builder.ml", line 998, characters 9-13
Re-raised at State_builder.apply_once.(fun) in file "src/libraries/project/state_builder.ml", line 1006, characters 9-18
Called from Register.main in file "src/plugins/value/register.ml", line 39, characters 46-66
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 846, characters 2-9
Called from Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 876, characters 18-64
Called from Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 235, characters 4-8
Unexpected error (File "src/plugins/value/engine/evaluation.ml", line 1176, characters 14-20: Assertion failed).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Not to crash
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Crashed with this error
```
Unexpected error (File "src/plugins/value/engine/evaluation.ml", line 1176, characters 14-20: Assertion failed).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: eva
- OS name: Unix Ubuntu
- OS version: 18.04 LTS
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
This is a fuzzed + reduced programDavid BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/2577[EVA] Question about \tainted2022-02-15T09:15:50ZAlix Trieu[EVA] Question about \taintedHi,
I know the taint analysis is still in experimental phase, but I was wondering why Frama-C cannot prove the following assertion in this program.
```C
#include "__fc_builtin.h"
int tainted;
int main(void){
tainted = Frama_C_nonde...Hi,
I know the taint analysis is still in experimental phase, but I was wondering why Frama-C cannot prove the following assertion in this program.
```C
#include "__fc_builtin.h"
int tainted;
int main(void){
tainted = Frama_C_nondet(0, 1);
//@ taint tainted;
//@ assert \tainted(tainted);
return 0;
}
```
Frama-C commit `437130a79253e90571fc44a90732290da5957f07` using the command `frama-c -eva -eva-domains taint -eva-msg-key=d-taint,-d-c-value test.c` says
```Assertions 0 valid 1 unknown 0 invalid 1 total```
Even though `Frama_C_domain_show_each` shows that the variable is indeed tainted.
```
Frama_C_domain_show_each:
tainted : # cvalue: {0; 1}
# taint: true
```
Is `\tainted` just a placeholder to be implemented for now ?David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/2576Eva plugin crashed with program calling memset2021-12-03T14:07:13ZKarine EMEva plugin crashed with program calling memset<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
frama-c -eva with the following program:
```
#include <string.h>
int main (void)
{
void *x;
memset (x, 0, 2 * 4);
return 0;
}
```
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Not to crash.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Crash with this error:
```
frama-c -eva ../../9-reduce-bugs/crash-frama-c/9-error-Not_found/6185ea1b8f1da01180c959fe26694bb58e3d3241_reduced.c
[kernel] Parsing /home/user42/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/crash-frama-c/9-error-Not_found/6185ea1b8f1da01180c959fe26694bb58e3d3241_reduced.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva:alarm] /home/user42/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/crash-frama-c/9-error-Not_found/6185ea1b8f1da01180c959fe26694bb58e3d3241_reduced.c:5: Warning:
function memset: precondition 'valid_s' got status unknown.
[eva] FRAMAC_SHARE/libc/string.h:118:
cannot evaluate ACSL term, unsupported ACSL construct: logic function memset
[kernel] Current source was: /home/user42/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/crash-frama-c/9-error-Not_found/6185ea1b8f1da01180c959fe26694bb58e3d3241_reduced.c:5
The full backtrace is:
Raised at file "src/kernel_services/abstract_interp/map_lattice.ml", line 220, characters 14-29
Called from file "src/kernel_services/abstract_interp/map_lattice.ml", line 230, characters 25-42
Called from file "src/kernel_services/abstract_interp/map_lattice.ml", line 237, characters 25-42
Called from file "src/plugins/value/domains/cvalue/builtins_memory.ml", line 580, characters 35-73
Called from file "src/plugins/value/domains/cvalue/builtins_memory.ml", line 634, characters 10-61
Called from file "src/plugins/value/domains/cvalue/builtins.ml", line 253, characters 6-27
Called from file "src/plugins/value/domains/cvalue/builtins.ml", line 268, characters 12-54
Called from file "src/plugins/value/engine/compute_functions.ml", line 304, characters 10-65
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 318, characters 10-43
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 456, characters 22-60
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 758, characters 26-75
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 754, characters 10-447
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 769, characters 24-59
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 742, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 274, characters 6-47
Called from file "src/plugins/value/partitioning/partition.ml", line 494, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
Called from file "src/plugins/value/engine/iterator.ml", line 494, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 543, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 540, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 602, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 769, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 201, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 333, characters 25-75
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (Not_found).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 22.0 (Titanium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
This is program compiles but got runtime errors, I would expect frama-c to give a warning. It seems like it crashed when analysing the memset line.
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/2563Frama-C crashed with an unexpected error Abstract_interp.Error_Bottom2021-06-10T09:45:22ZKarine EMFrama-C crashed with an unexpected error Abstract_interp.Error_Bottom<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
I ran frama-c with these parameters:
```
frama-c -eva -slevel 100 -plevel 255 -eva-precision 5 -val-warn-undefined-pointer-comparison pointer -no-val-alloc-returns-null -warn-signed-overflow -val -no-val-show-progress -machdep x86_64 4ee67af5850fa1e85ef52301e74c7093eba28573.c
```
and 4ee67af5850fa1e85ef52301e74c7093eba28573.c is the following program:
```
__attribute__((noinline)) int
f (int a, int b, int d)
{
int r = 8;
b += d + 42 -((short)((((int)(b)) %((int)(d)))))-((short)((((int)(b)) >>((int)(b))))) + 42 -((short)((((int)(b)) %((int)(d + 42 -((short)((((int)(b)) %((int)(d)))))-((short)((((int)(b)) >>((int)(b))))))))))-((short)((((int)(b)) >>((int)(b)))));
r = b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))) + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) %((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))))-((long)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) ^((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))))+((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) &((int)(r)))))-((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) >>((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))))-((short)((((int)(r)) >>((int)(r)))))-((int)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) >>((int)(r)))))+((long)((((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))) &((int)(b - d + 42 +((long)((((double)(r)) -((double)(r)))))-((int)((((double)(b - d)) -((double)(d)))))-((long)((((int)(b - d)) ^((int)(d)))))+((int)((((double)(b - d)) *((double)(b)))))-((int)((((int)(d)) >>((int)(b - d)))))-((short)((((int)(b)) >>((int)(r)))))-((int)((((int)(b - d)) >>((int)(b)))))+((long)((((int)(d)) &((int)(b - d))))))))));
return r;
}
int
main (void)
{
int l = 8;
asm ("" : "=r" (l) : "0" ((-(-2))));
if (((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))) != -(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)))))))+((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))) + 42 -((short)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)))))))+((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) %((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))+((long)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))) &((int)(((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))-((short)((((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)((int)f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) &((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))-((short)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3))))))))) |((int)(((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))+((short)((((int)(((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))) &((int)(((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))))))*((int)((((int)(((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) <<((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3))))))))))))-((long)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3))))))))) %((int)(((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3))))))))))))+((long)((((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((long)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) %((int)(-(-(-3)))))))+((long)((((int)(-(-(-3)))) |((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))) |((int)(-(-(-3)) + 42 -((short)((((double)(-(-(-3)))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((int)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) -((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))+((long)((((double)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) *((double)(-(-(-3)))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))*((short)((((int)(-(-(-3)))) &((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))))))-((short)((((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6))))) |((int)(-(-(-3)))))))+((short)((((double)(-(-(-3)))) *((double)(-(-(-3)))))))*((int)((((int)(-(-(-3)))) <<((int)(f (l + (-(-2)), l + (-(-3)), l + (-(-6)))))))))))))))
return 0;
}
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Not to crash.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
The program crashed with this trace:
```
[kernel] Warning: -slevel is a deprecated alias for option -eva-slevel.
Please use -eva-slevel instead.
[kernel] Warning: -plevel is a deprecated alias for option -eva-plevel.
Please use -eva-plevel instead.
[kernel] Warning: -val-warn-undefined-pointer-comparison is a deprecated alias
for option -eva-warn-undefined-pointer-comparison.
Please use -eva-warn-undefined-pointer-comparison instead.
[kernel] Warning: -no-val-alloc-returns-null is a deprecated alias
for option -eva-no-alloc-returns-null.
Please use -eva-no-alloc-returns-null instead.
[kernel] Warning: -val is a deprecated alias for option -eva. Please use -eva instead.
[kernel] Warning: -no-val-show-progress is a deprecated alias for option -eva-no-show-progress.
Please use -eva-no-show-progress instead.
[kernel] Parsing 4ee67af5850fa1e85ef52301e74c7093eba28573.c (with preprocessing)
[eva] Option -eva-precision 5 detected, automatic configuration of the analysis:
option -eva-min-loop-unroll set to 0 (default value).
option -eva-auto-loop-unroll set to 128.
option -eva-widening-delay set to 3 (default value).
option -eva-partition-history set to 0 (default value).
option -eva-slevel already set to 100.
option -eva-ilevel set to 48.
option -eva-plevel already set to 255 (not modified).
option -eva-subdivide-non-linear set to 100.
option -eva-remove-redundant-alarms set to true (default value).
option -eva-domains set to 'cvalue,equality,gauges,octagon,symbolic-locations'.
option -eva-split-return set to 'auto'.
option -eva-equality-through-calls set to 'formals' (default value).
option -eva-octagon-through-calls set to false (default value).
[eva] Splitting return states on:
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:17: Warning:
signed overflow. assert l + (int)(-((int)(-6))) ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
division by zero. assert d ≢ 0;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
invalid RHS operand for shift. assert 0 ≤ b < 32;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow. assert d + 42 ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow.
assert -2147483648 ≤ (int)(d + 42) - (int)((short)((int)(b % d)));
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow.
assert (int)(d + 42) - (int)((short)((int)(b % d))) ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
division by zero.
assert
(int)((int)((int)(d + 42) - (int)((short)((int)(b % d)))) -
(int)((short)((int)(b >> b))))
≢ 0;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow.
assert
(int)((int)((int)(d + 42) - (int)((short)((int)(b % d)))) -
(int)((short)((int)(b >> b))))
+ 42 ≤ 2147483647;
[eva:alarm] 4ee67af5850fa1e85ef52301e74c7093eba28573.c:6: Warning:
signed overflow.
assert
b +
(int)((int)((int)((int)((int)((int)(d + 42) - (int)((short)((int)(b % d)))) -
(int)((short)((int)(b >> b))))
+ 42)
-
(int)((short)((int)(b %
(int)((int)((int)(d + 42) -
(int)((short)((int)(b % d))))
- (int)((short)((int)(b >> b))))))))
- (int)((short)((int)(b >> b))))
≤ 2147483647;
[kernel] Current source was: 4ee67af5850fa1e85ef52301e74c7093eba28573.c:8
The full backtrace is:
Raised at file "src/kernel_services/abstract_interp/ival.ml", line 267, characters 14-32
Called from file "src/kernel_services/abstract_interp/ival.ml", line 281, characters 16-30
Called from file "src/plugins/value/domains/octagons.ml", line 352, characters 11-43
Called from file "src/plugins/value/domains/octagons.ml", line 360, characters 8-74
Called from file "src/plugins/value/domains/octagons.ml", line 395, characters 19-48
Called from file "src/plugins/value/domains/octagons.ml", line 1054, characters 6-77
Called from file "src/plugins/value/domains/domain_product.ml", line 94, characters 6-42
Called from file "src/plugins/value/domains/domain_product.ml", line 95, characters 6-44
Called from file "src/plugins/value/domains/domain_product.ml", line 95, characters 6-44
Called from file "src/plugins/value/domains/domain_product.ml", line 95, characters 6-44
Called from file "src/plugins/value/engine/evaluation.ml", line 837, characters 36-73
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 907, characters 6-33
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 899, characters 6-34
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 907, characters 6-33
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 1103, characters 6-36
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 664, characters 25-60
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 602, characters 21-38
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 618, characters 23-76
Called from file "src/plugins/value/engine/subdivided_evaluation.ml", line 685, characters 17-73
Called from file "src/plugins/value/engine/evaluation.ml" (inlined), line 1148, characters 4-67
Called from file "src/plugins/value/engine/evaluation.ml", line 1509, characters 23-77
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 157, characters 14-59
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 177, characters 4-54
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 251, characters 10-55
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 233, characters 28-33
Called from file "src/plugins/value/engine/iterator.ml", line 261, characters 4-60
Called from file "src/plugins/value/partitioning/partition.ml", line 494, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
Called from file "src/plugins/value/engine/iterator.ml", line 494, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 543, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 540, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 602, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 769, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 201, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 221, characters 26-36
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 318, characters 10-43
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 456, characters 22-60
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 758, characters 26-75
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 754, characters 10-447
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 769, characters 24-59
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 742, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 274, characters 6-47
Called from file "src/plugins/value/partitioning/partition.ml", line 494, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
Called from file "src/plugins/value/engine/iterator.ml", line 494, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 543, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 540, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 602, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 769, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 201, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 333, characters 25-75
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (Abstract_interp.Error_Bottom).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: *Frama-C version* (as reported by `frama-c -version`) 22.0 (Titanium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2555Crash in abstract_interp with an unexpected error when the input program has ...2021-05-21T09:25:42ZKarine EMCrash in abstract_interp with an unexpected error when the input program has a syntax error.<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
### Steps to reproduce the issue
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
The following program has a syntax error that crashed frama-c instead of returning an alarm.
E.g., gcc returns the following compile-time error:
```
user42@srg08:~/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/Frama-C-zone$ gcc -w 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c
0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c:10:11: error: negative width in bit-field ‘b’
10 | int32_t b:(-19);
|
```
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
The following code crashed frama-c:
```
user42@srg08:~/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/Frama-C-zone$ more 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c
#if __SIZEOF_INT__ < 4
__extension__ typedef __INT32_TYPE__ int32_t;
#else
typedef int int32_t;
#endif
#pragma pack(1)
struct S
{
int32_t b:(-19);
} i;
int main ()
{
return (-1);
}
```
with the following error:
```
user42@srg08:~/directed-compiler-fuzzing-code/scripts/9-reduce-bugs/Frama-C-zone$ frama-c -eva 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c
[kernel] Parsing 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[kernel] Current source was: 0bd2a2aa5631e87ab09386dc82e092f5aab23f0e.c:11
The full backtrace is:
Raised at file "src/kernel_services/abstract_interp/base.ml", line 217, characters 2-27
Called from file "src/kernel_services/abstract_interp/base.ml", line 480, characters 17-43
Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
Called from file "src/plugins/value/domains/cvalue/cvalue_domain.ml", line 394, characters 15-38
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/domains/cvalue/cvalue_domain.ml", line 405, characters 4-34
Called from file "src/plugins/value/engine/initialization.ml", line 309, characters 16-68
Called from file "list.ml", line 121, characters 24-34
Called from file "src/kernel_services/ast_data/globals.ml" (inlined), line 128, characters 33-72
Called from file "src/plugins/value/engine/initialization.ml", line 324, characters 15-65
Called from file "src/libraries/project/state_builder.ml", line 403, characters 17-21
Called from file "src/plugins/value/engine/initialization.ml", line 396, characters 20-43
Called from file "src/plugins/value/engine/compute_functions.ml", line 357, characters 10-55
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (File "src/kernel_services/abstract_interp/base.ml", line 217, characters 2-8: Assertion failed).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: *Frama-C version* (as reported by `frama-c -version`) 22.0 (Titanium)
- Plug-in used: -eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
I reduced the program manually, I can also share the original code or other examples.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2551Frama-c crash with Cil.SizeOfError sizeof(void)2021-04-30T07:59:31ZKarine EMFrama-c crash with Cil.SizeOfError sizeof(void)<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the iss...<!--
Thank you for submitting an issue to the Frama-C team.
We propose the following template to ease the process.
Please directly edit it inline to provide the required information.
Before submitting the issue, please verify:
- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
If the issue applies to a specific Frama-C plug-in, please prefix the title
by the plug-in name: [Eva], [WP], [E-ACSL]…
-->
This issue looks like a similar one to https://git.frama-c.com/pub/frama-c/-/issues/263, which was closed because it is related to jessie plug-in. The example here gives an error message that is almost the same as the one reported in bug 263 but with eva plug-in.
Since I am getting this error quite a lot, I was thinking it is important to report.
### Steps to reproduce the issue
```
frama-c -eva test.c
```
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Expected behaviour
Not to crash frama-c.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
Frama-c crashed with this error trace:
<!--
Please explain here what is the actual (faulty) behaviour.
-->
```
[kernel] Parsing test.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
[kernel] Current source was: test.c:5
The full backtrace is:
Raised at file "src/kernel_services/ast_queries/cil.ml", line 4038, characters 22-72
Called from file "src/kernel_services/ast_queries/cil.ml", line 4533, characters 42-58
Called from file "src/kernel_services/ast_queries/cil.ml", line 4793, characters 8-29
Called from file "src/plugins/value/engine/evaluation.ml", line 917, characters 12-35
Called from file "src/plugins/value/engine/evaluation.ml", line 864, characters 6-40
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 907, characters 6-33
Called from file "src/plugins/value/engine/evaluation.ml", line 834, characters 35-69
Called from file "src/plugins/value/engine/evaluation.ml", line 801, characters 27-57
Called from file "src/plugins/value/engine/evaluation.ml", line 1103, characters 6-36
Called from file "src/plugins/value/engine/evaluation.ml" (inlined), line 1148, characters 4-67
Called from file "src/plugins/value/engine/evaluation.ml", line 1509, characters 23-77
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 157, characters 14-59
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 177, characters 4-54
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 526, characters 6-65
Called from file "src/plugins/value/eval.ml", line 48, characters 29-32
Called from file "list.ml", line 126, characters 16-37
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 564, characters 4-68
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 752, characters 29-72
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 769, characters 24-59
Called from file "src/kernel_services/abstract_interp/bottom.ml" (inlined), line 31, characters 18-21
Called from file "src/plugins/value/engine/transfer_stmt.ml", line 742, characters 6-1023
Called from file "src/plugins/value/engine/iterator.ml", line 274, characters 6-47
Called from file "src/plugins/value/partitioning/partition.ml", line 494, characters 29-34
Called from file "list.ml", line 121, characters 24-34
Called from file "src/plugins/value/engine/iterator.ml", line 430, characters 15-71
Called from file "src/plugins/value/engine/iterator.ml", line 494, characters 18-35
Called from file "list.ml", line 92, characters 20-23
Called from file "src/plugins/value/engine/iterator.ml", line 496, characters 18-60
Called from file "src/plugins/value/engine/iterator.ml", line 543, characters 13-31
Called from file "list.ml", line 110, characters 12-15
Called from file "src/plugins/value/engine/iterator.ml" (inlined), line 540, characters 4-31
Called from file "src/plugins/value/engine/iterator.ml", line 602, characters 6-22
Called from file "src/plugins/value/engine/iterator.ml", line 769, characters 20-39
Called from file "src/plugins/value/engine/compute_functions.ml", line 201, characters 8-45
Called from file "src/plugins/value/engine/compute_functions.ml", line 333, characters 25-75
Called from file "src/libraries/project/state_builder.ml", line 994, characters 9-13
Re-raised at file "src/libraries/project/state_builder.ml", line 1002, characters 9-18
Called from file "src/plugins/value/register.ml", line 39, characters 46-66
Called from file "queue.ml", line 121, characters 6-15
Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 842, characters 2-9
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 872, characters 18-64
Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 231, characters 4-8
Unexpected error (Cil.SizeOfError("Undefined sizeof(void).", _)).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 22.0 (Titanium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: Frama-C version is 21.0 (Scandium) and Frama-C version is 22.0 (Titanium)
- Plug-in used: eva
- OS name: Ubuntu
- OS version: 18
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
I reduced the program that crashed Frama-c into this: (via Creduce)
```
void a(char *b, int align) {}
#define c(d) #d
#define f() c()
#define a(e) a(f(), __alignof__(e))
int main() { a(void); return 0; }
```David BühlerDavid Bühlerhttps://git.frama-c.com/pub/frama-c/-/issues/54An option to return error code if there are any problems with the analysis, s...2021-03-29T11:49:28ZvarosiAn option to return error code if there are any problems with the analysis, so that frama-c is easier to be used in CI/CD workflowsFeature Request
- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*...Feature Request
- [X] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
- [X] the issue has not yet been reported on our old
[BTS](https://bts.frama-c.com) (*note: the old BTS is deprecated*);
- [X] you installed Frama-C as prescribed in the [instructions](INSTALL.md).
# Contextual information
- Frama-C installation mode: Docker: framac/frama-c:22.0
- Frama-C version: 22.0
- Plug-in used: WP and EVA
- OS name: macOS
- OS version: 11.1
# Steps to reproduce the issue
I put frama-c in a BitBucket CI pipeline. With calling directly frama-c executable. CI pipelines fail when error code returned from executables is different than 0. That way it stops you from pushing erroneous code.
# Expected behaviour
It would be great if there is an option so that frama-c executable return non-zero error code if in EVA found any error in my code, or in WP not all conditions are met.
# Actual behaviour
frama-c return 0 even if EVA show errors from the analysed code. It returns 0 if WP have found non correct behaviour also.https://git.frama-c.com/pub/frama-c/-/issues/295Should warn for overlapping lv=lv; assignments2021-03-29T08:03:16ZPascal CuoqShould warn for overlapping lv=lv; assignmentsID0000945:
**This issue was created automatically from Mantis Issue 945. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000945:
**This issue was created automatically from Mantis Issue 945. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000945 | Frama-C | Plug-in > Eva | public | 2011-09-01 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | pascal | **Assigned To** | maroneze | **Resolution** | open |
| **Priority** | low | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Frama-C should warn for this program:
struct S { int x; int y; };
struct T { int z; struct S s; };
union U { struct S f ; struct T g; } u;
main(){
u.f = u.g.s;
return 0;
}
6.5.16.1 3:
If the value being stored in an object is read from another object that overlaps in any way the storage of the first object, then the overlap shall be exact and the two objects shall have qualified or unqualified versions of a compatible type; otherwise, the behavior is undefined.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/301Substraction results in unknown values2021-03-26T16:58:43Zmantis-gitlab-migrationSubstraction results in unknown valuesID0002166:
**This issue was created automatically from Mantis Issue 2166. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002166:
**This issue was created automatically from Mantis Issue 2166. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002166 | Frama-C | Plug-in > Eva | public | 2015-09-17 | 2017-12-17 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | kroeckx | **Assigned To** | buhler | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Sodium | **Target Version** | - | **Fixed in Version** | - |
### Description :
This line of code has:
if (len + n >= 64) len -= n;
For callstack [SHA256_Update :: frama-test.c:19 <- main]
Before this statement / after this statement:
n ∈ [1..63]
and:
For callstack [SHA256_Update :: frama-test.c:19 <- main]
Before this statement:
len ∈ [1..1024]
After this statement:
len ∈ [--..--]
I was expecting len after this to be:
len ∈ [0..1023]
It might be non-obvious to get that completely correct from the first time, and could understand that it would be turned in:
len ∈ [-62..1023]
KurtDavid BühlerDavid Bühler