frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-09-20T08:51:15Zhttps://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/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/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/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/2462For function f(int a) ; ensures a==\old(a) may be invalid2021-02-22T13:59:27ZPatrick BaudinFor function f(int a) ; ensures a==\old(a) may be invalidID0000168:
**This issue was created automatically from Mantis Issue 168. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000168:
**This issue was created automatically from Mantis Issue 168. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000168 | Frama-C | Plug-in > Eva | public | 2009-06-29 | 2009-09-24 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | patrick | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | Frama-C Beryllium-20090901 |
### Description :
The command "toplevel.opt -val old.c" gives the following line:
old.c:8: Warning: Function f, behavior default: postcondition got status valid
This is wrong: the postcondition is invalid.
### Additional Information :
Revision 5634
Contents of the file old.c
int *p, *q ;
/*@ ensures *q == a ;
*/
void f (int a) {
*q = a ;
*p = 3 ;
}
int main (int x, int y) {
q = &y ;
p = &x ;
f (x) ;
return x ;
}https://git.frama-c.com/pub/frama-c/-/issues/2396Wrong postconditions are "valid according to value analysis"2021-02-22T13:58:10ZGuillaume MelquiondWrong postconditions are "valid according to value analysis"ID0000372:
**This issue was created automatically from Mantis Issue 372. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000372:
**This issue was created automatically from Mantis Issue 372. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000372 | Frama-C | Plug-in > Eva | public | 2010-01-13 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | gmelquio | **Assigned To** | virgile | **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 Boron-20100401 |
### Description :
/*@ ensures \result == 1; */
int main() {
return 0;
}
When clicking on the "ensures" clause, Frama-C GUI (r7298) reports:
This is an ensures clause.
Status: Valid according to value analysishttps://git.frama-c.com/pub/frama-c/-/issues/2391Failure("Function 'From.find_deps_no_transitivity' not registered yet")2021-02-22T13:58:03Zmantis-gitlab-migrationFailure("Function 'From.find_deps_no_transitivity' not registered yet")ID0000392:
**This issue was created automatically from Mantis Issue 392. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000392:
**This issue was created automatically from Mantis Issue 392. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000392 | Frama-C | Plug-in > Eva | public | 2010-02-03 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | djs52 | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Attempting value analysis on a large code base, using -mem-exec to exclude some difficult functions. Running frama-c -val -mem-exec ... seems to complete without error; frama-c-gui with the same options fails with
Unexpected error (Failure("Function 'From.find_deps_no_transitivity' not registered yet"))https://git.frama-c.com/pub/frama-c/-/issues/2387imprecision in widening/narrowing for char and short index2021-02-22T14:04:43ZStephane Dupratimprecision in widening/narrowing for char and short indexID0000414:
**This issue was created automatically from Mantis Issue 414. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000414:
**This issue was created automatically from Mantis Issue 414. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000414 | Frama-C | Plug-in > Eva | public | 2010-02-19 | 2010-04-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sduprat | **Assigned To** | pascal | **Resolution** | fixed |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090902 | **Target Version** | - | **Fixed in Version** | Frama-C Boron-20100401 |
### Description :
Hello Stéphane,
> Depending the type of i, the range is not the same.
> The range of i in the loop is [0..10] (for int) or [0..15] for char or
> short.
_____
void main(void)
{
char i=0;
int j=0;
while (i<10) i++;
while (j<10) j++;
}
[value] ====== VALUES COMPUTED ======
[value] Values for function main:
i IN {10; 11; 12; 13; 14; 15; }
j IN {10; }
_____
It's interesting that you noticed this behavior,
because I fixed a comparable problem on short
notice this summer for an intern who had to demo
his plug-in the following week.
Note that the AST for the two loops is different:
i = (char)0;
j = 0;
while ((int )i < 10) {i = (char )((int )i + 1);}
while (j < 10) {j ++;}
CIL transforms the code thus because the C standard
specifies that operators such as ++ do not operate on
types smaller than int, and that values of these types
are implicitly promoted to int in these conditions.
Meanwhile, in the absence of any loop-related
option, the value analysis tries to keep computations
short at the price of precision by using a technique
called "widening". In order to limit the loss of precision,
however, various heuristics are used, including a
syntactic one for the j loop that recognizes that
j IN [0..10] is a good candidate for the loop invariant.
This heuristic does not currently recognize the condition
((int )i < 10) as one where it would be valuable to try
the same kind of invariant.
I have filed this issue as "feature wish" in the Bug Tracking
System, so that it is not forgotten.
http://bts.frama-c.com/view.php?id=325
Pascalhttps://git.frama-c.com/pub/frama-c/-/issues/2342star_star dump2021-02-22T14:02:46Zmantis-gitlab-migrationstar_star dumpID0000623:
**This issue was created automatically from Mantis Issue 623. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000623:
**This issue was created automatically from Mantis Issue 623. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000623 | Frama-C | Plug-in > Eva | public | 2010-11-10 | 2010-11-12 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | teamod | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
I preprocessed the Apache project (httpd-2.2.15) by Gcc-4.2.4 on linux2.6.28, and applied "frama-c -val apr_pools.i -main apr_pool_create_ex". Then the frama-c kernel dumped a lot of star_star_blablabla, and seems to be trapped into a deadlock.
Like below:
"
It contains a garbled mix of {star_star_star_allocator_0nth__owner_0nth__parent;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__parent_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__child_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__sibling_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__ref_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__cleanups_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__free_cleanups_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__allocator_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__subprocesses_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__abort_fn_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__user_data_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__tag_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__active_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__self_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__self_first_avail_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_0nth__pre_cleanups_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_1nth__parent_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_1nth__child_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_1nth__sibling_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_1nth__ref_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_1nth__cleanups_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_1nth__free_cleanups_WELL;
star_star_star_allocator_0nth__owner_0nth__parent_1nth__allocator_WELL;
"
## Attachments
- [apr_pools.i](/uploads/c3bbcca5ed518b25062a920c7f29435c/apr_pools.i)https://git.frama-c.com/pub/frama-c/-/issues/2325error in analyzing xen 4.0.0 code2021-02-22T13:56:34Zmantis-gitlab-migrationerror in analyzing xen 4.0.0 codeID0000516:
**This issue was created automatically from Mantis Issue 516. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000516:
**This issue was created automatically from Mantis Issue 516. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000516 | Frama-C | Plug-in > Eva | public | 2010-06-19 | 2010-12-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | amkhalid | **Assigned To** | pascal | **Resolution** | unable to reproduce |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
[kernel] Parsing stage early
[kernel] Parsing stage extending
[kernel] Parsing stage extended
[kernel] Parsing stage exiting
[kernel] Parsing stage loading
[kernel] Parsing stage configuring
[kernel] preprocessing with "gcc -C -E -I. -I/home/ak729/xen-4.0.0/xen/include/ /home/ak729/xen-4.0.0/xen/common/kernel.c"
/home/ak729/xen-4.0.0/xen/include/public/domctl.h:51:[kernel] user error: syntax error
[kernel] The full backtrace is:
[kernel] Raised at file "cil/src/frontc/frontc.ml", line 209, characters 9-28
[kernel] Called from file "cil/src/frontc/frontc.ml", line 124, characters 13-38
[kernel] Called from file "cil/src/frontc/frontc.ml", line 263, characters 13-32
[kernel] Called from file "src/kernel/file.ml", line 546, characters 27-46
[kernel] Called from file "src/kernel/file.ml", line 582, characters 16-23
[kernel] Re-raised at file "src/kernel/file.ml", line 585, characters 52-55
[kernel] Called from file "list.ml", line 74, characters 24-34
[kernel] Called from file "src/kernel/file.ml", line 579, characters 6-314
[kernel] Called from file "src/kernel/file.ml", line 1027, characters 12-30
[kernel] Called from file "src/kernel/file.ml", line 1108, characters 4-27
[kernel] Called from file "src/kernel/ast.ml", line 57, characters 29-45
[kernel] Called from file "src/project/computation.ml", line 108, characters 17-21
[kernel] Called from file "src/kernel/file.ml", line 1147, characters 12-22
[kernel] Called from file "src/project/project.ml", line 432, characters 12-15
[kernel] Re-raised at file "src/project/project.ml", line 437, characters 10-11
[kernel] Called from file "src/kernel/boot.ml", line 44, characters 33-47
[kernel] Called from file "src/kernel/cmdline.ml", line 170, characters 4-8
[kernel]
[kernel] Unexpected error (Parsing.Parse_error).
[kernel] Please report as 'crash' at http://bts.frama-c.comhttps://git.frama-c.com/pub/frama-c/-/issues/2235star_star dump issue2021-02-22T13:54:32Zmantis-gitlab-migrationstar_star dump issueID0000746:
**This issue was created automatically from Mantis Issue 746. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000746:
**This issue was created automatically from Mantis Issue 746. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000746 | Frama-C | Plug-in > Eva | public | 2011-03-05 | 2011-03-07 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | haihao | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Boron-20100401 | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hi,
Recently I used Frama-C to analyze the input/output information for each C function. However, I found for some functions, there are many inputs (more than 200, but most of them are similar).
Here is one sample input, and hope that you could help me figure out why these are generated by Frama-C.
##star_star_star_xx_pointer_0nth__inner_pointer_0nth__field[bits 0 to 549755813887]## xx_pointer is one of pointers used in a function, inner_pointer is a field of structure, pointed by xx_pointer, while field is a field of structure, pointed by inner_pointer.
Since there are many similar inputs, I am wondering whether they are really inputs for a function.
Any comments are welcome!
Thanks,
Haihao
### Additional Information :
I used a simple file to reproduce similar issue. Please tell me how to understand the star_star dump infomation. Thanks.
## Attachments
- [frama.c](/uploads/bc1a19580ec11baf490aed779ca30833/frama.c)https://git.frama-c.com/pub/frama-c/-/issues/2226How to break down the fields in strcuture (nested structures)2021-02-22T13:54:14Zmantis-gitlab-migrationHow to break down the fields in strcuture (nested structures)ID0000760:
**This issue was created automatically from Mantis Issue 760. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000760:
**This issue was created automatically from Mantis Issue 760. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000760 | Frama-C | Plug-in > Eva | public | 2011-03-22 | 2011-03-22 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | haihao | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | Frama-C Carbon-20110201 |
### Description :
Hi,
Frama-C value analysis could provide the detailed input and output. I am wondering whether users could use Frama-C to get the break-down fields of a structure if there is a nested structure.
Thanks, Haihao
### Additional Information :
Hi Pascal, I am sorry that I could find a suitable discussion place to let me ask the question, so I post the question here.
Sorry for the inconvenience.
Haihaohttps://git.frama-c.com/pub/frama-c/-/issues/2223Base.create_varinfo has no with_alarms arguments2021-02-22T13:54:11ZBenjamin MonateBase.create_varinfo has no with_alarms argumentsID0000773:
**This issue was created automatically from Mantis Issue 773. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000773:
**This issue was created automatically from Mantis Issue 773. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000773 | Frama-C | Plug-in > Eva | public | 2011-03-30 | 2011-03-30 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | monate | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Thus Kernel.warning ~current:true ~once:true
"Periodic variable %s of period %d@."
name
will be emitted even if it is called by a function in eval.ml which is supposed to honor its with_alarms argument.https://git.frama-c.com/pub/frama-c/-/issues/2194Unexpected error (File "cil/ocamlutil/cilutil.ml", line 918, characters 10-16...2021-02-22T14:04:25Zmantis-gitlab-migrationUnexpected error (File "cil/ocamlutil/cilutil.ml", line 918, characters 10-16: Assertion failed).ID0000836:
**This issue was created automatically from Mantis Issue 836. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000836:
**This issue was created automatically from Mantis Issue 836. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000836 | Frama-C | Plug-in > Eva | public | 2011-05-25 | 2011-05-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | senema | **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 Carbon-20110201 |
### Description :
Seen on Linux i686
[kernel] The full backtrace is:
Called from file "src/value/eval.ml", line 3869, characters 6-16
Called from file "list.ml", line 57, characters 20-23
Called from file "src/value/eval.ml", line 3838, characters 7-1023
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval.ml", line 4081, characters 7-62
Called from file "cil/src/ext/dataflow.ml", line 274, characters 27-46
Called from file "cil/src/ext/dataflow.ml", line 287, characters 16-40
Called from file "cil/src/ext/dataflow.ml", line 402, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 406, characters 9-22
Called from file "src/value/eval.ml", line 4672, characters 14-37
Called from file "src/value/eval.ml", line 5305, characters 5-60
Called from file "src/value/eval.ml", line 3891, characters 2-105
Called from file "src/value/eval.ml", line 3909, characters 7-93
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval.ml", line 4081, characters 7-62
Called from file "cil/src/ext/dataflow.ml", line 274, characters 27-46
Called from file "cil/src/ext/dataflow.ml", line 287, characters 16-40
Called from file "cil/src/ext/dataflow.ml", line 402, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 406, characters 9-22
Called from file "src/value/eval.ml", line 4672, characters 14-37
Called from file "src/value/eval.ml", line 5305, characters 5-60
Called from file "src/value/eval.ml", line 3891, characters 2-105
Called from file "src/value/eval.ml", line 3909, characters 7-93
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval.ml", line 4081, characters 7-62
Called from file "cil/src/ext/dataflow.ml", line 274, characters 27-46
Called from file "cil/src/ext/dataflow.ml", line 287, characters 16-40
Called from file "cil/src/ext/dataflow.ml", line 402, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 406, characters 9-22
Called from file "src/value/eval.ml", line 4672, characters 14-37
Called from file "src/value/eval.ml", line 5305, characters 5-60
Called from file "src/value/eval.ml", line 3891, characters 2-105
Called from file "src/value/eval.ml", line 3909, characters 7-93
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval.ml", line 4081, characters 7-62
Called from file "cil/src/ext/dataflow.ml", line 274, characters 27-46
Called from file "cil/src/ext/dataflow.ml", line 287, characters 16-40
Called from file "cil/src/ext/dataflow.ml", line 402, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 406, characters 9-22
Called from file "src/value/eval.ml", line 4672, characters 14-37
Called from file "src/value/eval.ml", line 5305, characters 5-60
Called from file "src/value/eval.ml", line 3891, characters 2-105
Called from file "src/value/eval.ml", line 3909, characters 7-93
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval.ml", line 4081, characters 7-62
Called from file "cil/src/ext/dataflow.ml", line 274, characters 27-46
Called from file "cil/src/ext/dataflow.ml", line 287, characters 16-40
Called from file "cil/src/ext/dataflow.ml", line 402, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 406, characters 9-22
Called from file "src/value/eval.ml", line 4672, characters 14-37
Called from file "src/value/eval.ml", line 5305, characters 5-60
Called from file "src/value/eval.ml", line 3891, characters 2-105
Called from file "src/value/eval.ml", line 3909, characters 7-93
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval.ml", line 4081, characters 7-62
Called from file "cil/src/ext/dataflow.ml", line 274, characters 27-46
Called from file "cil/src/ext/dataflow.ml", line 287, characters 16-40
Called from file "cil/src/ext/dataflow.ml", line 402, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 406, characters 9-22
Called from file "src/value/eval.ml", line 4672, characters 14-37
Called from file "src/value/eval.ml", line 5305, characters 5-60
Called from file "src/value/eval.ml", line 3891, characters 2-105
Called from file "src/value/eval.ml", line 3909, characters 7-93
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval.ml", line 4081, characters 7-62
Called from file "cil/src/ext/dataflow.ml", line 274, characters 27-46
Called from file "cil/src/ext/dataflow.ml", line 287, characters 16-40
Called from file "cil/src/ext/dataflow.ml", line 402, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 406, characters 9-22
Called from file "src/value/eval.ml", line 4672, characters 14-37
Called from file "src/value/eval.ml", line 5305, characters 5-60
Called from file "src/value/eval.ml", line 3891, characters 2-105
Called from file "src/value/eval.ml", line 3909, characters 7-93
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval.ml", line 4081, characters 7-62
Called from file "cil/src/ext/dataflow.ml", line 274, characters 27-46
Called from file "cil/src/ext/dataflow.ml", line 287, characters 16-40
Called from file "cil/src/ext/dataflow.ml", line 402, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 406, characters 9-22
Called from file "src/value/eval.ml", line 4672, characters 14-37
Called from file "src/value/eval.ml", line 5305, characters 5-60
Called from file "src/value/eval.ml", line 3891, characters 2-105
Called from file "src/value/eval.ml", line 3909, characters 7-93
Called from file "list.ml", line 74, characters 24-34
Called from file "src/value/eval.ml", line 4081, characters 7-62
Called from file "cil/src/ext/dataflow.ml", line 274, characters 27-46
Called from file "cil/src/ext/dataflow.ml", line 287, characters 16-40
Called from file "cil/src/ext/dataflow.ml", line 402, characters 8-21
Called from file "cil/src/ext/dataflow.ml", line 406, characters 9-22
Called from file "src/value/eval.ml", line 4672, characters 14-37
Called from file "src/value/eval.ml", line 5136, characters 4-67
Called from file "src/value/eval.ml", line 5391, characters 11-44
Re-raised at file "src/value/eval.ml", line 5407, characters 47-50
Called from file "src/project/state_builder.ml", line 1025, characters 2-6
Re-raised at file "src/project/state_builder.ml", line 1029, characters 8-11
Called from file "src/value/register.ml", line 59, characters 4-24
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/boot.ml", line 36, characters 4-20
Called from file "src/kernel/cmdline.ml", line 713, characters 2-9
Called from file "src/kernel/cmdline.ml", line 195, characters 4-8
Unexpected error (File "cil/ocamlutil/cilutil.ml", line 918, characters 10-16: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/
Note that a backtrace alone often does not have 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_guidelineshttps://git.frama-c.com/pub/frama-c/-/issues/2192assert-clause recommended by tool doesn't make warning vanish2021-02-22T13:53:20ZJochen Burghardtassert-clause recommended by tool doesn't make warning vanishID0000863:
**This issue was created automatically from Mantis Issue 863. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000863:
**This issue was created automatically from Mantis Issue 863. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000863 | Frama-C | Plug-in > Eva | public | 2011-06-10 | 2011-06-10 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | pascal | **Resolution** | no change required |
| **Priority** | normal | **Severity** | text | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Carbon-20110201 | **Target Version** | - | **Fixed in Version** | - |
### Description :
When running "frama-c -val ftest.c" on the attached program, I get the messages:
ftest.c:4:[value] Assertion got status unknown.
ftest.c:5:[kernel] warning: out of bounds read. assert \valid(argv+0);
However, the assertion recommended in the above warning is already in the code (in line 4); so I'd expect the warning to have vanished.
## Attachments
- [ftest.c](/uploads/fab2960212e81ebd8c8d79b441cd5ac2/ftest.c)