frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2022-06-16T18:43:10Zhttps://git.frama-c.com/pub/frama-c/-/issues/2616`frama-c-script build` NEEDS Blug installed... where do I get Blug?2022-06-16T18:43:10Zstephengaito`frama-c-script build` NEEDS Blug installed... where do I get Blug?Hello,
I am trying to run `frama-c-script build` in a directory which has a valid `compile_commands.json` file.
I am getting the following error:
> frama-c-script build
> error: path to 'blug' binary must be in PATH or variable BLUG...Hello,
I am trying to run `frama-c-script build` in a directory which has a valid `compile_commands.json` file.
I am getting the following error:
> frama-c-script build
> error: path to 'blug' binary must be in PATH or variable BLUG
I can find nowhere in your documentation, your various blog articles, nor any issues about where I should get and/or how I should install `Blug`.
(I see from the source code for `share/analysis-scripts/build.py` that the only uses of `blug` are the `blug_jbdb` and `prettify` sub-code... I can find no `blug` project (on opam nor PyPi.com) which contains these "symbols").
Where can I find this Python script/module?
Regards, Stephen GaitoAndre 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/2614Asking the UI to evaluate an invalid ACSL term makes the UI crash2022-06-10T07:42:41ZAlexCidAsking the UI to evaluate an invalid ACSL term makes the UI crash<!--
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.
-->
Open the UI (using at least the EVA plugin) to analyze any file, right-click almost anywhere, select "Evaluate ACSL term" and enter any invalid ACSL term.
### Expected behaviour
The UI should display a warning but continue to be usable afterwards.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
The following dialog is shown:
"Error: Invalid term: Unbound variable azerty" (for example), and then:
```
Error
Current source was filename.c:lineno
The full backtrace is:
Raised at file "map.ml", line 135, characters 10-25
Called from file "src/plugins/value/engine/abstractions.ml" line 96, characters 19-61
Unexpected error (Failure("dialog destroyed")).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 24.0 (Chromium).
...
```
After that, trying to evaluate _any_ ACSL term summons that same dialog.
<!--
Please explain here what is the actual (faulty) behaviour.
-->
### Contextual information
- Frama-C installation mode: docker image
- Frama-C version: 24.0
- Plug-in used: ?
- OS name: Linux
- OS version: Ubuntu 20.04https://git.frama-c.com/pub/frama-c/-/issues/2601[WP] [RTE] Unable to verify valid memory access in array using bitwise-ANDed ...2022-05-30T12:20:54ZCostava[WP] [RTE] Unable to verify valid memory access in array using bitwise-ANDed index when array is function parameter<!--
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.
-->
With Alt-Ergo 2.4.1 installed:
`frama-c -wp -wp-rte poc.c` / `frama-c-gui -wp -wp-rte poc.c`
using [poc.c](/uploads/62e84944634b546da975b2397c7c4e4d/poc.c) :
```c
/*@
requires \valid_read(arr + (0 .. 3));
assigns \nothing;
*/
int foo(const int arr[const static 4]) {
const unsigned int h = 7 & 0b11;
//@ assert 0 <= h < 4;
const int hvalue = arr[h];
const unsigned int i = 7 % 4;
//@ assert 0 <= i < 4;
const int ivalue = arr[i];
/*@
loop invariant 0 <= s <= 8;
loop assigns s;
loop variant 8 - s;
*/
for (unsigned int s = 0; s < 8; s += 1) {
const unsigned int j = s & 0b11;
//@ assert 0 <= j < 4;
const int jvalue = arr[j];
const unsigned int k = s % 4;
//@ assert 0 <= k < 4;
const int kvalue = arr[k];
}
return 0;
}
/*@
assigns \nothing;
*/
int main(void) {
const int arr[4] = {0, 1, 2, 3};
const unsigned int h = 7 & 0b11;
//@ assert 0 <= h < 4;
const int hvalue = arr[h];
const unsigned int i = 7 % 4;
//@ assert 0 <= i < 4;
const int ivalue = arr[i];
/*@
loop invariant 0 <= s <= 8;
loop assigns s;
loop variant 8 - s;
*/
for (unsigned int s = 0; s < 8; s += 1) {
const unsigned int j = s & 0b11;
//@ assert 0 <= j < 4;
const int jvalue = arr[j];
const unsigned int k = s % 4;
//@ assert 0 <= k < 4;
const int kvalue = arr[k];
}
foo(arr);
return 0;
}
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
All goals proved.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
```sh
$ frama-c -wp -wp-rte poc.c
[kernel] Parsing poc.c (with preprocessing)
[rte] annotating function foo
[rte] annotating function main
[wp] 34 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_foo_assert_rte_mem_access_3 : Timeout (Qed:9ms) (10s)
[wp] Proved goals: 33 / 34
Qed: 23 (2ms-5ms-14ms)
Alt-Ergo 2.4.1: 10 (7ms-17ms-30ms) (556) (interrupted: 1)
```
33/34 goals proved.
The verification of `/*@ assert rte: mem_access: \valid_read(arr + j); */` for code `const int jvalue = arr[j];` in function `foo` is not successful.
From a naive perspective, the `arr[j]` accesses in main and foo are equivalent, so the assert in foo should be verifiable if the assert in main is.
(I am aware that a different assert is generated in main: `/*@ assert rte: index_bound: j < 4; */`)
Also, the `//@ assert 0 <= j < 4;` immediately before the access can be verified, both in main and foo, so it seems the rte assert should be able to be verified also.
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: WP, RTE
- OS name: Manjaro Linux
- OS version: Qonos 21.2.4
### 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.
-->
The poc.c is a simplified proof of concept, but I did hit this situation when working on a real program.
To be explicit about the provers involved:
```sh
$ why3 config detect
Found prover Alt-Ergo version 2.4.1, OK.
1 prover(s) added
Save config to /home/user/.why3.conf
```
I was uncertain whether to submit this here or at the [alt-ergo issues](https://github.com/OCamlPro/alt-ergo/issues).
Apologies if this is the wrong place. Let me know if I should post there instead.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2608[WP] Fails to verify loop invariant of type-independent pattern-fill function...2022-05-30T12:18:06ZCostava[WP] Fails to verify loop invariant of type-independent pattern-fill function only when type of array elements is floating point<!--
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
With Alt-Ergo 2.4.1,
`frama-c -wp -wp-rte main.c` / `frama-c-gui -wp -wp-rte main.c`
using `main.c` (note that all of the function bodies are exactly the same, also the annotations for all of the functions):
```c
#include <stdbool.h>
#include <stddef.h>
/*@
requires \valid(&buf[0 .. bufLen-1]);
requires \valid_read(&pattern[0 .. 3]);
requires \separated(&buf[0 .. bufLen-1], &pattern[0 .. 3]);
assigns buf[0 .. bufLen-1];
ensures \forall size_t i; (0 <= i < bufLen) ==>
buf[i] == pattern[i % 4];
*/
void PatternFillInt(
int *const buf,
const size_t bufLen,
const int pattern[const static 4])
{
/*@
loop invariant 0 <= i <= bufLen;
loop invariant \forall size_t j; (0 <= j < i) ==>
buf[j] == pattern[j % 4];
loop assigns i, buf[0 .. bufLen-1];
loop variant bufLen - i;
*/
for (size_t i = 0; i < bufLen; i += 1) {
buf[i] = pattern[i % 4];
}
}
/*@
requires \valid(&buf[0 .. bufLen-1]);
requires \valid_read(&pattern[0 .. 3]);
requires \separated(&buf[0 .. bufLen-1], &pattern[0 .. 3]);
assigns buf[0 .. bufLen-1];
ensures \forall size_t i; (0 <= i < bufLen) ==>
buf[i] == pattern[i % 4];
*/
void PatternFillUInt(
unsigned int *const buf,
const size_t bufLen,
const unsigned int pattern[const static 4])
{
/*@
loop invariant 0 <= i <= bufLen;
loop invariant \forall size_t j; (0 <= j < i) ==>
buf[j] == pattern[j % 4];
loop assigns i, buf[0 .. bufLen-1];
loop variant bufLen - i;
*/
for (size_t i = 0; i < bufLen; i += 1) {
buf[i] = pattern[i % 4];
}
}
/*@
requires \valid(&buf[0 .. bufLen-1]);
requires \valid_read(&pattern[0 .. 3]);
requires \separated(&buf[0 .. bufLen-1], &pattern[0 .. 3]);
assigns buf[0 .. bufLen-1];
ensures \forall size_t i; (0 <= i < bufLen) ==>
buf[i] == pattern[i % 4];
*/
void PatternFillBool(
bool *const buf,
const size_t bufLen,
const bool pattern[const static 4])
{
/*@
loop invariant 0 <= i <= bufLen;
loop invariant \forall size_t j; (0 <= j < i) ==>
buf[j] == pattern[j % 4];
loop assigns i, buf[0 .. bufLen-1];
loop variant bufLen - i;
*/
for (size_t i = 0; i < bufLen; i += 1) {
buf[i] = pattern[i % 4];
}
}
/*@
requires \valid(&buf[0 .. bufLen-1]);
requires \valid_read(&pattern[0 .. 3]);
requires \separated(&buf[0 .. bufLen-1], &pattern[0 .. 3]);
assigns buf[0 .. bufLen-1];
ensures \forall size_t i; (0 <= i < bufLen) ==>
buf[i] == pattern[i % 4];
*/
void PatternFillFloat(
float *const buf,
const size_t bufLen,
const float pattern[const static 4])
{
/*@
loop invariant 0 <= i <= bufLen;
loop invariant \forall size_t j; (0 <= j < i) ==>
buf[j] == pattern[j % 4];
loop assigns i, buf[0 .. bufLen-1];
loop variant bufLen - i;
*/
for (size_t i = 0; i < bufLen; i += 1) {
buf[i] = pattern[i % 4];
}
}
/*@
requires \valid(&buf[0 .. bufLen-1]);
requires \valid_read(&pattern[0 .. 3]);
requires \separated(&buf[0 .. bufLen-1], &pattern[0 .. 3]);
assigns buf[0 .. bufLen-1];
ensures \forall size_t i; (0 <= i < bufLen) ==>
buf[i] == pattern[i % 4];
*/
void PatternFillDouble(
double *const buf,
const size_t bufLen,
const double pattern[const static 4])
{
/*@
loop invariant 0 <= i <= bufLen;
loop invariant \forall size_t j; (0 <= j < i) ==>
buf[j] == pattern[j % 4];
loop assigns i, buf[0 .. bufLen-1];
loop variant bufLen - i;
*/
for (size_t i = 0; i < bufLen; i += 1) {
buf[i] = pattern[i % 4];
}
}
/*@
requires \valid(&buf[0 .. bufLen-1]);
requires \valid_read(&pattern[0 .. 3]);
requires \separated(&buf[0 .. bufLen-1], &pattern[0 .. 3]);
assigns buf[0 .. bufLen-1];
ensures \forall size_t i; (0 <= i < bufLen) ==>
buf[i] == pattern[i % 4];
*/
void PatternFillIntPtr(
int* *const buf,
const size_t bufLen,
const int *const pattern[const static 4])
{
/*@
loop invariant 0 <= i <= bufLen;
loop invariant \forall size_t j; (0 <= j < i) ==>
buf[j] == pattern[j % 4];
loop assigns i, buf[0 .. bufLen-1];
loop variant bufLen - i;
*/
for (size_t i = 0; i < bufLen; i += 1) {
buf[i] = pattern[i % 4];
}
}
/*@
requires \valid(&buf[0 .. bufLen-1]);
requires \valid_read(&pattern[0 .. 3]);
requires \separated(&buf[0 .. bufLen-1], &pattern[0 .. 3]);
assigns buf[0 .. bufLen-1];
ensures \forall size_t i; (0 <= i < bufLen) ==>
buf[i] == pattern[i % 4];
*/
void PatternFillFloatPtr(
float* *const buf,
const size_t bufLen,
const float *const pattern[const static 4])
{
/*@
loop invariant 0 <= i <= bufLen;
loop invariant \forall size_t j; (0 <= j < i) ==>
buf[j] == pattern[j % 4];
loop assigns i, buf[0 .. bufLen-1];
loop variant bufLen - i;
*/
for (size_t i = 0; i < bufLen; i += 1) {
buf[i] = pattern[i % 4];
}
}
```
<!--
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.
-->
Since all of the function bodies and all of the function annotations are exactly identical and assigning a value is equivalent for any type (unless?),
I would expect either all functions to be verified, or all functions to fail to verify in the same way.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
The `loop invariant \forall size_t j; (0 <= j < i) ==> buf[j] == pattern[j % 4];` fails only for `PatternFillFloat` and `PatternFillDouble` functions.
```sh
$ frama-c -wp -wp-rte main.c
[kernel] Parsing main.c (with preprocessing)
[rte] annotating function PatternFillBool
[rte] annotating function PatternFillDouble
[rte] annotating function PatternFillFloat
[rte] annotating function PatternFillFloatPtr
[rte] annotating function PatternFillInt
[rte] annotating function PatternFillIntPtr
[rte] annotating function PatternFillUInt
[wp] 92 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_PatternFillFloat_loop_invariant_2_preserved : Timeout (Qed:8ms) (10s)
[wp] [Alt-Ergo 2.4.1] Goal typed_PatternFillDouble_loop_invariant_2_preserved : Timeout (Qed:10ms) (10s)
[wp] Proved goals: 90 / 92
Qed: 35 (0.33ms-6ms-41ms)
Alt-Ergo 2.4.1: 55 (8ms-37ms-131ms) (1523) (interrupted: 2)
[wp:pedantic-assigns] main.c:133: Warning:
No \from specification for assigned pointer '*(buf + (0 .. bufLen - 1))'.
Callers assumptions might be imprecise.
[wp:pedantic-assigns] main.c:158: Warning:
No \from specification for assigned pointer '*(buf + (0 .. bufLen - 1))'.
Callers assumptions might be imprecise.
```
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: WP, RTE
- OS name: Manjaro Linux
- OS version: Qonos 21.2.5
### 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.
-->
N/Ahttps://git.frama-c.com/pub/frama-c/-/issues/2594Unsafe uses of Obj in Unmarshal2022-05-30T08:20:54ZVincent LavironUnsafe uses of Obj in UnmarshalA few pieces of code in the `Unmarshal` module are too obviously unsafe for the Flambda 2 compiler's taste, and results in the compiler deliberately inserting a segfault.
The `Sys.opaque_identity` function can be used to tell the compile...A few pieces of code in the `Unmarshal` module are too obviously unsafe for the Flambda 2 compiler's taste, and results in the compiler deliberately inserting a segfault.
The `Sys.opaque_identity` function can be used to tell the compiler not to make any assumptions on the underlying value, and is available since OCaml 4.03, so I'd like to see it used here to allow testing Frama C with Flambda 2.
The three places that are affected are:
- The code for initialising `arch_bigendian`. This can be fixed by inserting a call to `Sys.opaque_identity`.
- The code for initialising `arch_float_endianness`. This can be fixed by inserting a call to `Sys.opaque_identity`.
- The code for computing the `null` value. I assume that the code was intended to compute a null pointer, but it was reading the wrong field anyway so this was instead a pointer to a C-allocated struct (which, it seems, works as well). I'd like to replace it with `Obj.repr (Sys.opaque_identity (ref 0))`, which should work too (it gives you a unique static pointer) and has the advantage of not manipulating naked pointers.
I could propose a patch if you'd like (or even open a merge request, if your GitLab instance accepts merge requests from external contributors)25 (Manganese)François BobotFrançois Bobothttps://git.frama-c.com/pub/frama-c/-/issues/2612e-acsl-gcc.sh syntax error2022-05-29T07:04:49ZJaeD-Shine-acsl-gcc.sh syntax errormy test code is cat2.i
```
#include <stdio.h>
char buf[128*1024];
int main()
{
size_t count;
/*@ assert buf==11; */
while ((count = fread(buf, 1, sizeof(buf), stdin)) > 0)
fwrite(buf, 1, count, stdout);
return 0;
}
```
wh...my test code is cat2.i
```
#include <stdio.h>
char buf[128*1024];
int main()
{
size_t count;
/*@ assert buf==11; */
while ((count = fread(buf, 1, sizeof(buf), stdin)) > 0)
fwrite(buf, 1, count, stdout);
return 0;
}
```
when i run `e-acsl-gcc.sh -Omonitored_cat2.i cat2.i`, happened problem.
```
+ /home/.opam/default/bin/frama-c -remove-unused-specified-functions -machdep gcc_x86_64 -cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 -no-frama-c-stdlib cat2.i -e-acsl -e-acsl-share=/home/.opam/default/bin/../share/frama-c/e-acsl -then-last -print -ocode a.out.frama.c
[kernel] Parsing cat2.i (no preprocessing)
[kernel] cat2.i:6:
syntax error:
Location: between lines 6 and 7, before or at token: count
4
5 int main()
6 {
7 size_t count;
8 /*@ assert buf==11; */
9 while ((count = fread(buf, 1, sizeof(buf), stdin)) > 0)
[kernel] Frama-C aborted: invalid user input.
```Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/1133Very big integer constants2022-05-12T14:21:47ZJulien SignolesVery big integer constantsID0000745:
**This issue was created automatically from Mantis Issue 745. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000745:
**This issue was created automatically from Mantis Issue 745. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000745 | Frama-C | Kernel > ACSL implementation | public | 2011-03-04 | 2014-03-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | signoles | **Assigned To** | virgile | **Resolution** | fixed |
| **Priority** | low | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | Frama-C Oxygen-20120901 |
### Description :
Integer constants are de facto limited to int64 by Cil. Should use Big_int to accept any constant.
### Steps To Reproduce :
void main(void) {
/*@ assert 0xfffffffffffffffff == 0xfffffffffffffffff; */
}
$ frama-c a.c
a.c:1:[kernel] failure: Cannot represent on 64 bits the integer 0xfffffffffffffffffhttps://git.frama-c.com/pub/frama-c/-/issues/2604e-acsl-gcc.sh segmentation fault2022-05-12T12:25:35ZJaeD-Shine-acsl-gcc.sh segmentation faultWhenever option --validate-format-strings of e-acsl-gcc.sh is set, E-ACSL detects format-string vulnerabilities in printf-like function. Below is an example which incorrectly tries to print a string through a %d format.
File printf.c
``...Whenever option --validate-format-strings of e-acsl-gcc.sh is set, E-ACSL detects format-string vulnerabilities in printf-like function. Below is an example which incorrectly tries to print a string through a %d format.
File printf.c
```
#include <stdio.h>
int main(void) {
printf ("is %d really an int?", "foo");
return 0;
}
```
```
jaeyoung@jaeyoung-VirtualBox:~/Downloads/frama$ e-acsl-gcc.sh -Oprintf -c --validate-format-strings print.c
+ /home/jaeyoung/.opam/default/bin/frama-c -remove-unused-specified-functions -variadic-no-translation -machdep gcc_x86_64 '-cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 ' -no-frama-c-stdlib print.c -e-acsl -e-acsl-validate-format-strings -e-acsl-share=/home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl -then-last -print -ocode a.out.frama.c
[kernel] Parsing print.c (with preprocessing)
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] /usr/include/x86_64-linux-gnu/bits/thread-shared-types.h:92: Warning:
unnamed fields are a C11 extension (use -c11 to avoid this warning)
[e-acsl] translation done in project "e-acsl".
+ gcc -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body print.c -o printf
+ gcc -DE_ACSL_SEGMENT_MMODEL -DE_ACSL_VALIDATE_FORMAT_STRINGS -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body -I/home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl -o printf.e-acsl a.out.frama.c /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/e_acsl_rtl.c /home/jaeyoung/.opam/default/bin/../lib/frama-c/e-acsl/libeacsl-dlmalloc.a -lgmp -lm
jaeyoung@jaeyoung-VirtualBox:~/Downloads/frama$ ./printf.e-acsl
Segmentation fault (core dumped)
```
The error in the printf.c file cannot be detected because a 'segmentation fault' has occurred.
The result of running gdb of ./printf.e-acsl is as follows.
```
(gdb) run
Starting program: /home/jaeyoung/Downloads/frama/printf.e-acsl
Program received signal SIGSEGV, Segmentation fault.
0x000055555555c1fa in shadow_alloca (
ptr=ptr@entry=0x7ffff7ddb6a0 <_IO_2_1_stdout_>, size=size@entry=216)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c:302
302 sec_shadow[j++] = size;
(gdb) bt
#0 0x000055555555c1fa in shadow_alloca (
ptr=ptr@entry=0x7ffff7ddb6a0 <_IO_2_1_stdout_>, size=size@entry=216)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c:302
#1 0x000055555555e9bf in register_safe_locations (
thread_only=thread_only@entry=0)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c:720
#2 0x000055555555ea88 in do_eacsl_memory_init (argc_ref=<optimized out>,
argv_ref=<optimized out>, ptr_size=<optimized out>)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c:324
#3 0x000055555555ebd9 in __e_acsl_memory_init (argc_ref=<optimized out>,
argv_ref=<optimized out>, ptr_size=<optimized out>)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c:331
#4 0x0000555555557856 in main () at a.out.frama.c:243
```Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/2605Segmentation fault of e-acsl(feat.E-acsl user manual)2022-05-12T12:25:23ZJaeD-ShinSegmentation fault of e-acsl(feat.E-acsl user manual)I followed the user's manual, but the following result does not come out and 'Segmentation fault (core dumped)' occurs.
I don't know what is the problem.
(URL: https://frama-c.com/fc-plugins/e-acsl.html)
* **expected result**
![expecte...I followed the user's manual, but the following result does not come out and 'Segmentation fault (core dumped)' occurs.
I don't know what is the problem.
(URL: https://frama-c.com/fc-plugins/e-acsl.html)
* **expected result**
![expected_result](/uploads/ebc7591b516b32a3631380e8abdfaaaa/expected_result.png)
* **my result**
```
jaeyoung@jaeyoung-VirtualBox:~/Documents$ e-acsl-gcc.sh -c -omonitored_first.i first.i
+ /home/jaeyoung/.opam/default/bin/frama-c -remove-unused-specified-functions -machdep gcc_x86_64 '-cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 ' -no-frama-c-stdlib first.i -e-acsl -e-acsl-share=/home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl -then-last -print -ocode monitored_first.i
[kernel] Parsing first.i (no preprocessing)
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] /usr/include/x86_64-linux-gnu/bits/thread-shared-types.h:92: Warning:
unnamed fields are a C11 extension (use -c11 to avoid this warning)
[e-acsl] translation done in project "e-acsl".
+ gcc -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body first.i -o a.out
+ gcc -DE_ACSL_SEGMENT_MMODEL -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body -I/home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl -o a.out.e-acsl monitored_first.i /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/e_acsl_rtl.c /home/jaeyoung/.opam/default/bin/../lib/frama-c/e-acsl/libeacsl-dlmalloc.a -lgmp -lm
jaeyoung@jaeyoung-VirtualBox:~/Documents$ ls
a.out first.i monitored_first.c monitored_first.o pow.i
a.out.e-acsl format-string.c monitored_first.i no_main.i
jaeyoung@jaeyoung-VirtualBox:~/Documents$ ./a.out.e-acsl
Segmentation fault (core dumped)
```
**I checked it through gdb, can you tell me how to solve it?**
```
jaeyoung@jaeyoung-VirtualBox:~/Documents$ gdb -q ./a.out.e-acsl
Reading symbols from ./a.out.e-acsl...
(gdb) run
Starting program: /home/jaeyoung/Documents/a.out.e-acsl
Program received signal SIGSEGV, Segmentation fault.
0x000055555555bf0a in shadow_alloca (ptr=ptr@entry=0x7ffff7ddb6a0 <_IO_2_1_stdout_>,
size=size@entry=216)
at /home/jaeyoung/.opam/default/bin/../share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c:302
302 sec_shadow[j++] = size;
(gdb) info locals
i = 0
j = 1
k = 0
boundary = 216
prim_shadow = <optimized out>
prim_shadow_alt = 0x0
sec_shadow = 0x0
i = <optimized out>
j = 0
k = 0
(gdb)
```Julien SignolesJulien Signoleshttps://git.frama-c.com/pub/frama-c/-/issues/2611Frama-c instal2022-05-12T12:24:59ZJaeD-ShinFrama-c instal- ubuntu: 20.04.4 LTS
- opam version :2.0.5
```
ocamlfind 1.9.3 A library manager for OCaml
why3 1.4.1 pinned to version 1.4.0
```
```
ocaml -version
The OCaml toplevel, version 4.08.1
```
I ran as bel...- ubuntu: 20.04.4 LTS
- opam version :2.0.5
```
ocamlfind 1.9.3 A library manager for OCaml
why3 1.4.1 pinned to version 1.4.0
```
```
ocaml -version
The OCaml toplevel, version 4.08.1
```
I ran as below.
```
# 1. Install opam (OCaml package manager)
sudo apt install opam # or dnf, pacman, etc.
# 2. Install Frama-C's dependencies
opam install depext
opam depext frama-c
# 3. Install Frama-C itself
opam install frama-c
```
In step 3, the following error occurs.
```
@ubuntu:~$ opam install frama-c
The following actions will be performed:
↘ downgrade menhirLib 20220210 to 20211128 [required by menhir]
↘ downgrade menhirSdk 20220210 to 20211128 [required by menhir]
∗ install conf-zlib 1 [required by camlzip]
∗ install ocplib-simplex 0.4 [required by alt-ergo-free]
↘ downgrade menhir 20220210 to 20211128 [required by alt-ergo-free]
∗ install camlzip 1.11 [required by alt-ergo-free]
∗ install psmt2-frontend 0.1 [required by alt-ergo-free]
↻ recompile why3 1.4.1 [uses menhir]
∗ install alt-ergo-free 2.2.0 [required by frama-c]
∗ install frama-c 24.0
===== ∗ 6 ↻ 1 ↘ 3 =====
Do you want to continue? [Y/n] Y
<><> Gathering sources <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[frama-c.24.0] found in cache
[why3.1.4.1] found in cache
[ERROR] The sources of the following couldn't be obtained, aborting:
- alt-ergo-free.2.2.0: Download command failed
- camlzip.1.11: Download command failed
- menhir.20211128: Download command failed
- menhirLib.20211128: Download command failed
- menhirSdk.20211128: Download command failed
- ocplib-simplex.0.4: Download command failed
- psmt2-frontend.0.1: Download command failed
```
How to solve it? please let me know.https://git.frama-c.com/pub/frama-c/-/issues/2599Problem with dependencies: Alt-Ergo set to 1.012022-05-11T06:28:08ZJaeD-ShinProblem with dependencies: Alt-Ergo set to 1.01my ubuntu version is Ubuntu 20.04.3 LTS
opam version is 4.08.1
After run 'opam install frama-c error', happening this issue.
```
[ERROR] The compilation of alt-ergo failed at
"/home/jaeyoung/.opam/opam-init/hooks/sandbox.sh ...my ubuntu version is Ubuntu 20.04.3 LTS
opam version is 4.08.1
After run 'opam install frama-c error', happening this issue.
```
[ERROR] The compilation of alt-ergo failed at
"/home/jaeyoung/.opam/opam-init/hooks/sandbox.sh build make".
∗ installed why3.1.4.1
#=== ERROR while compiling alt-ergo.1.01 ======================================#
# context 2.0.5 | linux/x86_64 | ocaml-system.4.08.1 | https://opam.ocaml.org#257f9ce1
# path ~/.opam/default/.opam-switch/build/alt-ergo.1.01
# command ~/.opam/opam-init/hooks/sandbox.sh build make
# exit-code 2
# env-file ~/.opam/log/alt-ergo-23270-89b24d.env
# output-file ~/.opam/log/alt-ergo-23270-89b24d.out
### output ###
# [...]
# ocamlopt.opt -c -annot -inline 100 -I /home/jaeyoung/.opam/default/lib/zarith -I /home/jaeyoung/.opam/default/lib/lablgtk2 -I +threads -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/myUnix.ml
# ocamlc.opt -c -annot -g -I /home/jaeyoung/.opam/default/lib/zarith -I /home/jaeyoung/.opam/default/lib/lablgtk2 -I +threads -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/util.mli
# ocamlopt.opt -c -annot -inline 100 -I /home/jaeyoung/.opam/default/lib/zarith -I /home/jaeyoung/.opam/default/lib/lablgtk2 -I +threads -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/util.ml
# ocamlc.opt -c -annot -g -I /home/jaeyoung/.opam/default/lib/zarith -I /home/jaeyoung/.opam/default/lib/lablgtk2 -I +threads -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/lists.mli
# ocamlopt.opt -c -annot -inline 100 -I /home/jaeyoung/.opam/default/lib/zarith -I /home/jaeyoung/.opam/default/lib/lablgtk2 -I +threads -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/lists.ml
# ocamlc.opt -c -annot -g -I /home/jaeyoung/.opam/default/lib/zarith -I /home/jaeyoung/.opam/default/lib/lablgtk2 -I +threads -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/numbersInterface.mli
# ocamlc.opt -c -annot -g -I /home/jaeyoung/.opam/default/lib/zarith -I /home/jaeyoung/.opam/default/lib/lablgtk2 -I +threads -I src/util -I src/structures -I src/theories -I src/instances -I src/sat -I src/preprocess -I src/parsing -I src/gui -I src/main -I non-free/plugins/common -I non-free/plugins/satML -I non-free/plugins/profiler -I non-free/plugins/fm-simplex src/util/numsNumbers.mli
# File "src/util/numsNumbers.mli", line 24, characters 47-62:
# 24 | module Z : NumbersInterface.ZSig with type t = Big_int.big_int
# ^^^^^^^^^^^^^^^
# Error: Unbound module Big_int
# make: *** [Makefile.users:220: src/util/numsNumbers.cmi] Error 2
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build alt-ergo 1.01
└─
┌─ The following changes have been performed (the rest was aborted)
│ ∗ install conf-autoconf 0.1
│ ∗ install conf-gmp 4
│ ∗ install conf-gnomecanvas 2
│ ∗ install conf-graphviz 0.1
│ ∗ install conf-gtk2 1
│ ∗ install conf-gtksourceview 2
│ ∗ install lablgtk 2.18.12
│ ∗ install ocamlgraph_gtk 2.0.0
│ ∗ install why3 1.4.1
│ ∗ install zarith 1.12
└─
# Run eval $(opam env) to update the current shell environment
The former state can be restored with:
opam switch import
"/home/jaeyoung/.opam/default/.opam-switch/backup/state-20220315135530.export"
```
I'm not sure how to handle the bottom part.https://git.frama-c.com/pub/frama-c/-/issues/2600[WP] Assertion failed in Instance tactic called from a custom strategy2022-05-09T13:44:19ZLélio Brun[WP] Assertion failed in Instance tactic called from a custom strategy### Steps to reproduce the issue
I tried to narrow down the example, but it's hard to determine where is the problem exactly.
I have an example file [foo_lemma.c](/uploads/a25d0ec0213d97096ccd3fd237b822f5/foo_lemma.c) and a custom strat...### Steps to reproduce the issue
I tried to narrow down the example, but it's hard to determine where is the problem exactly.
I have an example file [foo_lemma.c](/uploads/a25d0ec0213d97096ccd3fd237b822f5/foo_lemma.c) and a custom strategy plugin [strategy_foo.ml](/uploads/2ca56a5f301482f8dad081fbaaa2e839/strategy_foo.ml).
Essentially the strategy tries to guide the solvers by finding witnesses in the hypotheses to instantiate existentially quantified predicates in the goal. It follows the iterative nature of the `T` predicates by unfolding them one step at a time until success. As recommended by the WP manual, the custom strategy only uses pre-defined tactics (namely _Definition_ and _Instance_).
Launch `frama-c -wp -load-module strategy_foo.ml -wp-auto Foo:T foo_lemma.c`.
### Expected behaviour
Frama-C should prove the lemma or at least not fail.
### Actual behaviour
Frama-C fails with the following error:
```
[wp] foo_lemma.c:55: Warning:
[Instance] Exception <File "src/plugins/qed/term.ml", line 2516, characters 4-10: Assertion failed>
[kernel] Current source was: foo_lemma.c:55
The full backtrace is:
Raised at ProverSearch.fork in file "src/plugins/wp/ProverSearch.ml", line 57, characters 6-13
Called from ProverSearch.lookup in file "src/plugins/wp/ProverSearch.ml", line 62, characters 10-33
Called from ProverSearch.first in file "src/plugins/wp/ProverSearch.ml", line 84, characters 25-54
Called from ProverScript.Env.search in file "src/plugins/wp/ProverScript.ml", line 192, characters 12-62
Called from ProverScript.autosearch in file "src/plugins/wp/ProverScript.ml", line 299, characters 8-34
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.bind.(fun) in file "src/libraries/utils/task.ml", line 92, characters 42-47
Called from Task.Monad.progress in file "src/libraries/utils/task.ml" (inlined), line 98, characters 19-29
Called from Task.progress in file "src/libraries/utils/task.ml", line 363, characters 14-36
Re-raised at Task.progress in file "src/libraries/utils/task.ml", line 369, characters 6-13
Called from Task.server_progress.(fun) in file "src/libraries/utils/task.ml", line 475, characters 14-27
Called from Stdlib__list.find_all.find in file "list.ml", line 242, characters 17-20
Called from Task.server_progress in file "src/libraries/utils/task.ml", line 473, characters 22-273
Called from Task.on_idle.(fun) in file "src/libraries/utils/task.ml", line 344, characters 14-18
Called from Register.do_wp_proofs in file "src/plugins/wp/register.ml", line 656, characters 4-33
Called from Register.cmdline_run in file "src/plugins/wp/register.ml", line 722, characters 8-26
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 280, characters 14-17
Re-raised at Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 280, characters 41-48
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 281, characters 2-12
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 281, characters 2-12
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/qed/term.ml", line 2516, characters 4-10: 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
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04.4 LTS
### Additional information
I tried to see if the error would raise in GUI mode by manually activating the custom tactics in the editor instead of using `-wp-auto Foo:T`:
`frama-c-gui -wp -load-module strategy_foo.ml foo_lemma.c`
It turns out that it won't raise an error dialog, but the following stderr message `** (frama-c-gui:426361): CRITICAL **: 17:47:51.667: GSourceFunc: callback raised an exception`, and the GUI remains in a somewhat stuck state.
This could be another issue by itself maybe.
---
I tracked down the error: the assertion fails [here (`qed/term.ml:2516`)](https://git.frama-c.com/pub/frama-c/-/blob/24.0/src/plugins/qed/term.ml#L2516), from the call [here (`wp/TacInstance.ml:163`)](https://git.frama-c.com/pub/frama-c/-/blob/24.0/src/plugins/wp/TacInstance.ml#L163).
It seems that for some reason (maybe related to the way I wrote my tactic?), the variable `x` chosen to _unbind_ `phi` actually is not fresh (enough).
On a local version of Frama-C I tried to replace the [code at line 157](https://git.frama-c.com/pub/frama-c/-/blob/24.0/src/plugins/wp/TacInstance.ml#L157) with the following:
```ocaml
let pool = F.pool ~copy:env.feedback#pool () in
List.iter (F.add_var pool) (F.e_vars (F.QED.lc_repr phi));
let x = F.fresh pool tau in
```
Basically I'm force-ensuring that the subsequent assertion will not fail, and this seems to solve the problem, as far as I can tell.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/131Can't view publications on the wiki2022-05-09T13:31:47Zmantis-gitlab-migrationCan't view publications on the wikiID0002474:
**This issue was created automatically from Mantis Issue 2474. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002474:
**This issue was created automatically from Mantis Issue 2474. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002474 | Frama-C | Documentation > website | public | 2019-09-10 | 2019-09-18 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | abutterfield | **Assigned To** | bobot | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
Clicking the link low down on https://frama-c.com/support.html to acess the wiki to
see list of publications results in a "404 not found" error.
That link is: https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:publications
The shorter link https://bts.frama-c.com/dokuwiki/ also fails with a 404
### Steps To Reproduce :
Try to visit https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:publications
or https://bts.frama-c.com/dokuwiki/François BobotFrançois Bobothttps://git.frama-c.com/pub/frama-c/-/issues/1131E-ACSL reports use of invalid pointer while in fact the pointer is valid2022-05-02T09:10:40ZDavid MentréE-ACSL reports use of invalid pointer while in fact the pointer is validID0001478:
**This issue was created automatically from Mantis Issue 1478. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001478:
**This issue was created automatically from Mantis Issue 1478. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001478 | Frama-C | Plug-in > E-ACSL | public | 2013-09-04 | 2014-03-25 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | dmentre | **Assigned To** | signoles | **Resolution** | fixed |
| **Priority** | normal | **Severity** | major | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Fluorine-20130601 |
### Description :
On attached program, E-ACSL reports use of invalid pointer:
"""
Precondition failed at line 7 in function loop.
The failing predicate is:
\valid(global_i_ptr).
"""
But in fact the pointer is valid.
This is checked by reading and executing the program, but also statically with WP and Value analysis.
The attached program is compiled with following script, replacing $1 with q7_invalid_under_eacsl.c.
"""
PATH=/usr/local/stow/frama-c-Fluorine-20130601/bin:$PATH
export PATH
eacsl_path=`frama-c -print-share-path`/e-acsl
frama-c \
-cpp-command 'gcc -C -E -I/usr/local/stow/frama-c-Fluorine-20130601/share/frama-c/libc -I SSI'\
-e-acsl \
$1 \
-then-on e-acsl -print -ocode a-e-acsl.c \
&& \
gcc -I$eacsl_path $eacsl_path/memory_model/e_acsl_bittree.c $eacsl_path/memory_model/e_acsl_mmodel.c $eacsl_path/e_acsl.c a-e-acsl.c
"""
## Attachments
- [q7_invalid_under_eacsl.c](/uploads/fc3279cdc60e5191500031773634387f/q7_invalid_under_eacsl.c)https://git.frama-c.com/pub/frama-c/-/issues/2559No support for complex numbers via the keyword _Complex2022-04-27T15:22:34ZKarine EMNo support for complex numbers via the keyword _Complex<!--
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.
-->
Frama-c does not support complex numbers via the keyword _Complex for C code.
See here: https://gcc.gnu.org/onlinedocs/gcc-4.1.2/gcc/Complex.html
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
When running this code:
```
float _Complex f;
int main () { }
```
Frama-c returns an error:
```
[kernel] Parsing test12.c (with preprocessing) [kernel] test12.c:1:
syntax error:
Location: line 1, between columns 6 and 15, before or at token: f
1 float _Complex f;
^^^^^^^^^^^^^^^^^
2 int main () { }
[kernel] Frama-C aborted: invalid user input.
```
### 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.
-->
We use Frama-c to automatically analyse code from llvm and gcc test-suites; some of the programs triggered this error message.
I reduced the code but I can add the link to the original one.Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2564[frama-clang] std::forward with non-primitive type causes NON TERMINATING2022-04-22T13:54:07ZStefan Gränitz[frama-clang] std::forward with non-primitive type causes NON TERMINATING<!--
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 find attached two example sources that demonstrate the issue: [fails.cpp](/uploads/69d2c79afe05be14b237e337c90f0d9b/fails.cpp) [works.cpp](/uploads/a28e5308e6b0f638172b084eb5572861/works.cpp)~~
Please find attached the narrowed example sources that demonstrate the issue with `std::forward` alone:
[fails.cpp](/uploads/8f135c54a38dc95e8cb162033dc7e29b/fails.cpp)[works.cpp](/uploads/1c2846a51c27d8cd745afff3baf6d950/works.cpp)
**Further investigation details can be found in the comments.** What follows here is the original issue description:
```
> cat fails.cpp
#include <memory>
struct Foo {
int val;
Foo(int val) : val(val) {}
int bar() { return val; }
};
int main(int argc, char **argv) {
std::unique_ptr<Foo> foo1(new Foo(argc));
std::unique_ptr<Foo> foo2 = std::move(foo1);
return foo2->bar();
}
> frama-c -deps fails.cpp
```
### Expected behaviour
```
[kernel] Parsing fails.cpp (external front-end)
Now output intermediate result
...
[from] Function main:
__malloc_main_l10 FROM argc
\result FROM argc
[from] ====== END OF DEPENDENCIES ======
```
### Actual behaviour
```
[kernel] Parsing fails.cpp (external front-end)
Now output intermediate result
...
[from] Function main:
NON TERMINATING - NO EFFECTS
[from] ====== END OF DEPENDENCIES ======
```
### Minimal working diff
It works if we avoid the move assignment:
```
> diff -u fails.cpp works.cpp
--- fails.cpp 2021-06-21 10:40:26.613967584 +0000
+++ works.cpp 2021-06-21 10:38:12.276859713 +0000
@@ -8,6 +8,5 @@
int main(int argc, char **argv) {
std::unique_ptr<Foo> foo1(new Foo(argc));
- std::unique_ptr<Foo> foo2 = std::move(foo1);
- return foo2->bar();
+ return foo1->bar();
}
```
### Contextual information
* Frama-C: framac/frama-c:22.0 Docker Image ID e45780e160f1
* Plug-in used: frama-clang-0.0.10 built from official source drop
* Compiler: Debian clang version 11.1.0
* Target: x86_64-pc-linux-gnu
### Additional information
One more observation is that the plugin is unable to parse a preprocessed source file:
```
> clang++-11 -E -o works.ii works.cpp
> frama-c -deps works.ii
[kernel] Parsing works.ii (external front-end)
works.ii:316:32: error: __int128 is not supported on this target
template<> struct __is_integer<__int128> { enum { __value = 1 }; typedef __true_type __type; }; template<> struct __is_integer<unsigned __int128> { enum { __value = 1 }; typedef __true_type __type; };
^
...
code generation aborted due to compilation errors
[kernel] User Error: Failed to parse C++ file. See Clang messages for more information
[kernel] User Error: stopping on file "works.ii" that has errors.
[kernel] Frama-C aborted: invalid user input.
```Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2597[WP] Out of memory crash2022-04-20T07:18:53ZLélio Brun[WP] Out of memory crash### Steps to reproduce the issue
Here is a (not necessarily) minimal example (see [excludes.c](/uploads/af45da85624b741546d0e395a330d1e5/excludes.c)):
```c
void excludes8(_Bool x1, _Bool x2, _Bool x3, _Bool x4,
_Bool x...### Steps to reproduce the issue
Here is a (not necessarily) minimal example (see [excludes.c](/uploads/af45da85624b741546d0e395a330d1e5/excludes.c)):
```c
void excludes8(_Bool x1, _Bool x2, _Bool x3, _Bool x4,
_Bool x5, _Bool x6, _Bool x7, _Bool x8,
_Bool *excludes)
{
*excludes =
(!x1 && !x2 && !x3 && !x4 && !x5 && !x6 && !x7 && !x8) ||
( x1 && !x2 && !x3 && !x4 && !x5 && !x6 && !x7 && !x8) ||
(!x1 && x2 && !x3 && !x4 && !x5 && !x6 && !x7 && !x8) ||
(!x1 && !x2 && x3 && !x4 && !x5 && !x6 && !x7 && !x8) ||
(!x1 && !x2 && !x3 && x4 && !x5 && !x6 && !x7 && !x8) ||
(!x1 && !x2 && !x3 && !x4 && x5 && !x6 && !x7 && !x8) ||
(!x1 && !x2 && !x3 && !x4 && !x5 && x6 && !x7 && !x8) ||
(!x1 && !x2 && !x3 && !x4 && !x5 && !x6 && x7 && !x8) ||
(!x1 && !x2 && !x3 && !x4 && !x5 && !x6 && !x7 && x8);
//@ assert *excludes == 1;
return;
}
```
Launch Frama-C / WP: `frama-c -wp excludes.c`
### Expected behaviour
The (silly) assertion should be tried by the solvers.
### Actual behaviour
Out of memory crash (on a 16G laptop):
```
[kernel] Parsing FIREFLY_1.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
'frama-c -wp FIREFLY_1.c' terminated by signal SIGKILL
```
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 24.0 (Chromium)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04.4 LTS
- Memory: 15605 MiB
### Additional information (optional)
I tried to profile the execution by using [Memtrace](https://github.com/janestreet/memtrace) on a local installation of Frama-C. It seems that WP is filling huge identifiers tables ([Intmap](https://git.frama-c.com/pub/frama-c/-/blob/24.0/src/plugins/qed/intmap.ml#L273), [Idxmap](https://git.frama-c.com/pub/frama-c/-/blob/24.0/src/plugins/qed/idxmap.ml#L72)) when executing code from [Conditions](https://git.frama-c.com/pub/frama-c/-/blob/24.0/src/plugins/wp/Conditions.ml) module.
Here is the corresponding trace, that can be viewed using [Memtrace_viewer](https://github.com/janestreet/memtrace_viewer): [trace.ctf](/uploads/42173f2b5017d16f12a46cf943dc09e7/trace.ctf)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2561[frama-clang] Cannot parse C++14 generic lambda2022-04-14T17:19:42ZStefan Gränitz[frama-clang] Cannot parse C++14 generic lambda<!--
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 find attached two example sources that demonstrate the issue:
[fails.cpp](/uploads/2a5f09fd150e99bb9978ee9eb06d252f/fails.cpp)
[works.cpp](/uploads/e4f05a0dd3348d8d0367afde1d2f1ec0/works.cpp)
```
> cat fails.cpp
int main(int argc, char *argv[]) {
auto lambda = [](auto argc) { return argc; };
return lambda(argc);
}
> clang++-11 -E -o fails.ii fails.cpp
> frama-c -deps -cpp-extra-args="-std=c++14" fails.ii
```
### Expected output
```
[kernel] Parsing fails.ii (external front-end)
Now output intermediate result
<...>
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
These dependencies hold at termination for the executions that terminate:
[from] Function UliEUcE__cons:
__fc_lam FROM __fc_closure; __fc_func
[from] Function __fc_lambda_def:
\result FROM argc
[from] Function main:
\result FROM argc
[from] ====== END OF DEPENDENCIES ======
```
### Actual output
```
[kernel] Parsing fails.ii (external front-end)
framaCIRGen: /usr/lib/llvm-11/include/clang/AST/Type.h:671: const clang::ExtQualsTypeCommonBase *clang::QualType::getCommonPtr() const: Assertion `!isNull() && "Cannot retrieve a NULL type pointer"' failed.
Aborted
[kernel] User Error: Failed to parse C++ file. See Clang messages for more information
[kernel] User Error: stopping on file "fails.ii" that has errors.
[kernel] Frama-C aborted: invalid user input.
```
### Minimal working diff
It works if we write `int` instead of `auto` for the type of the lambda parameter:
```
> diff -u fails.cpp works.cpp
--- fails.cpp 2021-06-08 22:42:13 +0200
+++ works.cpp 2021-06-08 22:43:48 +0200
@@ -1,4 +1,4 @@
int main(int argc, char *argv[]) {
- auto lambda = [](auto argc) { return argc; };
+ auto lambda = [](int argc) { return argc; };
return lambda(argc);
}
```
### Contextual information
- Frama-C: framac/frama-c:22.0 Docker Image ID e45780e160f1
- Plug-in used: frama-clang-0.0.10 built from official source drop
- Compiler: Debian clang version 11.1.0
- Target: x86_64-pc-linux-gnu
### Additional information
Generic lambdas are a C++14 language feature:
https://isocpp.org/wiki/faq/cpp14-language#generic-lambdasVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/860identifier unknown after leaving inner scope that declared same name2022-04-02T21:12:27ZJochen Burghardtidentifier unknown after leaving inner scope that declared same nameID0001983:
**This issue was created automatically from Mantis Issue 1983. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001983:
**This issue was created automatically from Mantis Issue 1983. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001983 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-16 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
145.cpp:7:16: unknown identifier 'x'
Now output intermediate result
...
[wp] Proved goals: 0 / 0
The error message disappears and a proof obligation is generated (and proven by Qed) if "x" is changed to "y" in the inner scope (line 5).
## Attachments
- [145.cpp](/uploads/73be9f397b0fdbf37c7e518259c9bf24/145.cpp)Virgile PrevostoVirgile Prevosto