frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-01-05T13:41:22Zhttps://git.frama-c.com/pub/frama-c/-/issues/2640Unable to call built-in ACSL pow function that takes integer arguments and re...2023-01-05T13:41:22ZCostavaUnable to call built-in ACSL pow function that takes integer arguments and returns an integer<!--
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.
-->
```c
/*@
assigns \nothing;
ensures 2 <= \result <= 4;
*/
int do_something(void) {
return 2;
}
/*@
assigns \nothing;
*/
int main(void) {
int foo = 8;
int bar = do_something();
int baz = 3;
// Unnatural whitespace so that
// the line number given by the error can be specific.
/*@ assert FooInequality: foo <= pow(
bar
,
baz
);
*/
return foo;
}
```
```sh
$ frama-c -wp -wp-rte main.c
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
The file is parsed successfully, and the goals may or may not be proved successfully.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
```sh
$ frama-c -wp -wp-rte main.c
[kernel] Parsing main.c (with preprocessing)
[kernel:annot-error] main.c:21: Warning:
invalid implicit conversion from 'int' to 'double'. Ignoring code annotation
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "main.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
```
Page 100 of the [ACSL v1.18 manual](https://www.frama-c.com/download/acsl-1.18.pdf) has appendix `A.2 Builtin functions` listing `integer pow(integer x, integer y) ;`
I would expect parsing to succeed due to this.
However, that function is the only in the whole section to not start with a `\`.
If we instead call `\pow`, the parsing succeeds, but we can use `frama-c-gui` to see that reals and not integers are involved in the unproven goal.
Adding `(integer)` casts to `bar` and `baz` in the annotation does not cause an integer pow function to be used.
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 25.0 (Manganese)
- Plug-in used: WP, RTE, alt-ergo 2.4.1
- OS name: Manjaro Linux
- OS version: Sikaris 22.0.0
### 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.
-->
Similar issue: https://git.frama-c.com/pub/frama-c/-/issues/2506Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2630Ghost variable initialization and logic functions2022-09-01T06:31:17ZDavid CokGhost variable initialization and logic functions
### Steps to reproduce the issue
Here is example code:
```
/*@ axiomatic A {
logic integer Lneg(integer i) = -i;
}
*/
/*@ assigns \nothing; ensures \result == -i; */
int neg(int i) { return -i; }
void test(int j) {
//@ ghost i...
### Steps to reproduce the issue
Here is example code:
```
/*@ axiomatic A {
logic integer Lneg(integer i) = -i;
}
*/
/*@ assigns \nothing; ensures \result == -i; */
int neg(int i) { return -i; }
void test(int j) {
//@ ghost int kk = Lneg(j);
int k = neg(j);
//@ assert k == kk;
}
```
`frama-c -wp` produces
```
fc $ frama-c -wp logic.c
[kernel] Parsing logic.c (with preprocessing)
[kernel:typing:implicit-function-declaration] logic.c:10: Warning:
Calling undeclared function Lneg. Old style K&R code?
[kernel:ghost:bad-use] logic.c:10: Warning:
Call to non-ghost function from ghost code is not allowed
[kernel:annot:missing-spec] logic.c:9: Warning:
Neither code nor specification for function Lneg, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_test_assert : Timeout (Qed:1ms) (10s)
[wp] Proved goals: 2 / 3
Qed: 2 (0.21ms-0.72ms)
Alt-Ergo 2.4.1: 0 (interrupted: 1)
[wp:pedantic-assigns] logic.c:9: Warning:
No 'assigns' specification for function 'test'.
Callers assumptions might be imprecise.
[wp:pedantic-assigns] logic.c:10: Warning:
No 'assigns' specification for function 'Lneg'.
Callers assumptions might be imprecise.
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
```
It appears to treat Lneg as a regular function, complaining that it is non-ghost and has no specs.
However, if `neg` is used instead, WP still complains, although now it runs the proof successfully:
```
[kernel] Parsing logic.c (with preprocessing)
[kernel:ghost:bad-use] logic.c:10: Warning:
Call to non-ghost function from ghost code is not allowed
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] Proved goals: 3 / 3
Qed: 3 (0.21ms-0.68ms-1ms)
[wp:pedantic-assigns] logic.c:9: Warning:
No 'assigns' specification for function 'test'.
Callers assumptions might be imprecise.
[kernel] Warning: warning ghost:bad-use treated as deferred error. See above messages for more information.
[kernel] Frama-C aborted: invalid user input.
```
### Expected behaviour
I would expect `Lneg` to be allowed here. If a non-ghost function like `neg` is allowed to be used as a ghost logic function, as it apparently is (e.g. as long as it is pure), then there should be no need for a warning.
### Contextual information
Frama-C 25.0, built from source, with frama-clang added. Using WP as built with Frama-C.
MacOS 12.5Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2621[Frama-C/WP] The history of internal state changes VC goal outcomes2022-09-26T13:49:51Zstephengaito[Frama-C/WP] The history of internal state changes VC goal outcomes### Steps to reproduce the issue
Using Allan Blanchard's answer to exercise 3.1.3.3 (file: `code/function-contract/contract/ex-3-alphabet-answer.c`)...
Start `frama-c-gui code/function-contract/contract/ex-3-alphabet-answer.c`.
Right-...### Steps to reproduce the issue
Using Allan Blanchard's answer to exercise 3.1.3.3 (file: `code/function-contract/contract/ex-3-alphabet-answer.c`)...
Start `frama-c-gui code/function-contract/contract/ex-3-alphabet-answer.c`.
Right-click on the function prototype `int alphabet_letter` and select `Prove function annotations by WP`, the first VC (`ensures`) should fail.
Right-click on the function prototype `int alphabet_letter` a second time and select `Prove function annotations by WP`, the first VC (`ensures`) should succeed.
### Expected behaviour
The order in which WP proof invocations *should* *not* change the VC goal outcomes if there is no change to the underlying code/annotations.
### Actual behaviour
The history of WP proof invocations does seem to change the VC goal outcomes.
### Contextual information
- Frama-C, Why3, Alt-Ergo installation mode: *all via Opam*
- Frama-C version: *25.0-beta (Manganese)*
- Plug-in used: *WP*
- Why3 version: *Why3 platform, version 1.5.0*
- Alt-Ergo version: *2.4.1*
- OS name: *Ubuntu*
- OS version: *21.10 (Impish)*
- Number of CPU's: *2*
- CPU speed: *2.80GHz*
- RAM: *16Gb*Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2617[WP] The support of sets is partial2023-02-06T11:02:59ZYani ZIANI[WP] The support of sets is partial<!--
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
Running Frama-C with WP on the following code after uncommenting any of the designated lines. The main idea here was to try and represent a basic C linked list structure as an ACSL tset to easy reasoning and benefit from already existing ACSL clauses.
```C
#include <stdio.h>
typedef struct NODE_TEST {
int handle;
struct NODE_TEST * next;
} NODE_TEST;
/**
* Reachability in linked lists as defined in the ACSL language implementation
* on the Frama-C website
*/
/*@ inductive reachable_node_t{L}(NODE_TEST *root, NODE_TEST *to) {
case empty{L}:
\forall NODE_TEST *l; reachable_node_t{L}(l,l) ;
case non_empty{L}: \forall NODE_TEST *l1,*l2;
\valid(l1)
&& reachable_node_t{L}(l1->next,l2)
==> reachable_node_t{L}(l1,l2) ;
@}
*/
/**
* Logic function used to tranlate a C linked list of NODE_TEST into an ASCL
* tset of its nodes (or at least an attempt at making one). The aim here
* would be to store each pointer to each node of a given linked list in a
* ACSL structure in order to facilitate the proofs of properties such as
* memory separation (by applying the \separated clause to the whole tset),
* loop invariants (using, for instance, the existing \in clause for tsets),
* and others.
*/
/*@ axiomatic NodeTestTSet {
logic set<NODE_TEST *> node_to_tset{L}(NODE_TEST *node)
reads { nod->next | struct NODE_TEST* nod ;
reachable_node_t{L}(nod, \null) && nod \in node_to_tset(node) };
axiom node_empty_tset{L}:
\forall NODE_TEST *node;
node == \null
==> node_to_tset{L}(node) == \empty;
axiom node_not_empty_tset{L}:
\forall NODE_TEST *node;
\let tail = node_to_tset{L}(node->next);
( \valid(node) && reachable_node_t{L}(node->next, \null) )
==> node_to_tset{L}(node) == \union({node}, tail);
}
*/
/**
* Axiomatic definition of the length of a well typed linked list
*/
/*@ axiomatic NodeTestListLgth {
logic integer node_lgth{L}(NODE_TEST *node)
reads { nod->next | struct NODE_TEST* nod; nod \in node_to_tset(node) } ;
axiom node_empty_lgth{L}:
\forall NODE_TEST *node;
node == \null ==> node_lgth{L}(node) == 0;
axiom node_t_not_empty_lgth{L}:
\forall NODE_TEST * node;
(node != \null
&& reachable_node_t{L}(node, \null) )
==> node_lgth{L}(node) == node_lgth{L}(node->next) + 1;
}
*/
/**
* Predicates to easy readability
*/
/*@ predicate is_handle_in_list_tset{L}(NODE_TEST *root, int out_handle) =
\exists NODE_TEST *node;
node \in node_to_tset(root) && node->handle == out_handle;
*/
/*@ predicate is_handle_in_list_reach{L}(NODE_TEST *root, int out_handle) =
\exists NODE_TEST *node;
reachable_node_t(root, node) && node->handle == out_handle;
*/
/*****************************************************************/
/*@
requires linked_list != \null && reachable_node_t(linked_list,\null);
requires 0 < node_lgth(linked_list) <= 10000;
behavior handle_in_list:
// assumes is_handle_in_list_tset(linked_list, out_handle); //causes a why3 error when uncommented
assumes is_handle_in_list_reach(linked_list, out_handle);
ensures \result == 616;
behavior handle_not_in_list:
// assumes !(is_handle_in_list_tset(linked_list, out_handle)); //causes a why3 error when uncommented
assumes !(is_handle_in_list_reach(linked_list, out_handle));
ensures \result == 1610;
disjoint behaviors;
complete behaviors;
*/
int getNode(NODE_TEST * linked_list, int out_handle) {
NODE_TEST *temp_node;
/*@ ghost int n = 0;*/
/*@
loop invariant 0 <= n <= node_lgth(linked_list);
loop invariant temp_node \in node_to_tset(linked_list); //causes a why3 error when uncommented
loop invariant reachable_node_t(linked_list, temp_node);
loop invariant reachable_node_t(temp_node, \null);
loop assigns n, temp_node;
loop variant node_lgth(linked_list) + 1 - n;
*/
for (temp_node = linked_list; temp_node != NULL;
temp_node = temp_node->next) {
if (temp_node->handle == out_handle)
return 616;
/*@ghost n++;*/
}
return 1610;
}
```
<!--
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
Proofs of properties ending either successfully or with a timeout.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Most proofs end up failing with a why3 error ``[Why3 Error] Library file not found: vset``, even those pertaining to properties that would be proven without the "problematic" lines.
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: 22.0 (Titanium), 23.0 (Vanadium), 23.1 (Vanadium), *24.0 (Chromium)* and *25.0-beta (Manganese)* (as reported by `frama-c -version`)
- Plug-in used: WP (using Qed and Alt-Ergo)
- OS name: *Ubuntu*
- OS version: *20.04.4 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.
-->
In the case of Frama-C 24, I also did try using both versions 2.3.2 and 2.4.1 of Alt-Ergo, Frama-C 25 was tested using Alt-Ergo 2.4.1, and every other versions of Frama-C used v2.3.2.
FYI @nkosmatovAllan BlanchardAllan Blanchardhttps://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/2609WP - unsoundness with union2024-03-14T22:21:49ZGeoff HuletteWP - unsoundness with union```
/* bug.c */
#include <assert.h>
typedef union {
int a[2];
struct {
int a0, a1;
} s;
} T;
/*@
requires \valid(t);
requires t->a[0] == 0;
requires t->s.a0 == 0;
assigns *t;
ensures t->a[0] == 1;
ensures t->s.a0 == 0;
*/
voi...```
/* bug.c */
#include <assert.h>
typedef union {
int a[2];
struct {
int a0, a1;
} s;
} T;
/*@
requires \valid(t);
requires t->a[0] == 0;
requires t->s.a0 == 0;
assigns *t;
ensures t->a[0] == 1;
ensures t->s.a0 == 0;
*/
void foo(T *t) { t->a[0] = 1; }
/*@
assigns \nothing;
*/
int main() {
T t;
t.a[0] = 0;
t.s.a0 = 0;
foo(&t);
//@ assert t.s.a0 == 0;
assert(t.s.a0 == 0);
return 0;
}
```
In a shell:
```
$ frama-c --version
24.0 (Chromium)
$ frama-c -wp -wp-rte bug.c
[kernel] Parsing bug.c (with preprocessing)
[rte] annotating function foo
[rte] annotating function main
[wp] 18 goals scheduled
[wp] Proved goals: 18 / 18
Qed: 17 (0.74ms-2ms-3ms)
Alt-Ergo 2.3.3: 1 (20ms) (63)
$ clang bug.c
$ ./a.out
a.out: bug.c:29: int main(): Assertion `t.s.a0 == 0' failed.
Aborted (core dumped)
```Allan BlanchardAllan Blanchardhttps://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/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/2596[WP] Type mismatch with Real model2022-03-15T12:28:29ZLélio Brun[WP] Type mismatch with Real model### Steps to reproduce the issue
Here is a minimal example (see [foo.c](/uploads/a0892900e8240b95c1623e300679efa2/foo.c)):
```c
//@ predicate Foo(double y) = y == 0.0;
void foo(double x) {
//@ assert Foo((double) (0.0 + 0.0 * x));
...### Steps to reproduce the issue
Here is a minimal example (see [foo.c](/uploads/a0892900e8240b95c1623e300679efa2/foo.c)):
```c
//@ predicate Foo(double y) = y == 0.0;
void foo(double x) {
//@ assert Foo((double) (0.0 + 0.0 * x));
}
```
Launch Frama-C / WP with Real model: `frama-c -wp -wp-model real foo.c`
### Expected behaviour
No error (as for `frama-c -wp foo.c`):
```
[kernel] Parsing foo.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Cache] found:1
[wp] Proved goals: 1 / 1
Qed: 0
Alt-Ergo 2.4.1: 1 (56ms) (400) (cached: 1)
[wp:pedantic-assigns] foo.c:3: Warning:
No 'assigns' specification for function 'foo'.
Callers assumptions might be imprecise.
```
### Actual behaviour
Type mismatch error:
```
[kernel] Parsing foo.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_real_foo_assert : Failed
[Why3 Error] Type mismatch between real and int
[wp] [Cache] not used
[wp] Proved goals: 0 / 1
Alt-Ergo 2.4.1: 0 (failed: 1)
[wp:pedantic-assigns] foo.c:3: Warning:
No 'assigns' specification for function 'foo'.
Callers assumptions might be imprecise.
```
Indeed, we can see with `frama-c-gui` in Script mode that the expression is simplified to `0`, as we are given the following proof context:
```
Goal Assertion:
Prove: P_Foo(0).
```
### 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
Removing the addition works:
```c
//@ predicate Foo(double y) = y == 0.0;
void foo(double x) {
//@ assert Foo((double) (0.0 * x));
}
```Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2582Frama-C WP crashes with Invalid_argument("Invalid lock on mutex") when trying...2022-09-26T13:52:22ZGuerricChupinFrama-C WP crashes with Invalid_argument("Invalid lock on mutex") when trying to use CoqI'm currently working on a file with WP and RTE where, sometimes, frama-c will crash when using the option `-wp-prover why3:coq -wp-interactive fix`. Note that CVC4, AltErgo and Z3 are also used but disabling them doesn't have an effect....I'm currently working on a file with WP and RTE where, sometimes, frama-c will crash when using the option `-wp-prover why3:coq -wp-interactive fix`. Note that CVC4, AltErgo and Z3 are also used but disabling them doesn't have an effect. The crash happens right after an editor (Emacs with ProofGeneral in my case, but it also happens with CoqIDE) is opened: the editor closes nearly immediately and Frama-C produces the stacktrace below. Modifying the file slightly (e.g. by adding an extra assertion somewhere) will sometime stop Frama-C from crashing, however I can't seem to find a pattern. I'm currently running C-Reduce on my file to extract a MWE, I will post it in the comments as soon as it terminates (if it produces something useful). See below for information on my setup.
I'm wondering if anyone as an idea as to what causes this behaviour and if it can be fixed easily?
```
[kernel] Current source was: FRAMAC_SHARE/libc/stdlib.h:626
The full backtrace is:
Raised at Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 268, characters 41-48
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 269, characters 2-12
Called from Extlib.try_finally in file "src/libraries/stdlib/extlib.ml", line 269, 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 (Invalid_argument("Invalid lock on mutex")).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 23.1 (Vanadium).
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 informations
- Frama-C installation method: opam
- Frama-C version: 23.1
- Plug-in used: WP + RTE
- OS Name: Fedora
- OS Version: 34
- Coq Version: 8.13.2
- Why3 Version: 1.4.0Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2570[frama-clang] Crash parsing compound literals2021-10-06T07:48:17ZEvgenii Kotelnikov[frama-clang] Crash parsing compound literals<!--
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
The following is a valid C++ code that initialises variables `i` and `j` using compound literals.
```cpp
typedef struct A_ { int a; } A;
struct B { int b; };
struct C { A aa; struct B bb; };
struct B i{0};
struct C j{{0}, i};
```
### Expected behaviour
`frama-c struct_fail.cpp` should parse the file.
### Actual behaviour
```
$ frama-c struct_fail.cpp
[kernel] Parsing struct_fail.cpp (external front-end)
Now output intermediate result
[fclang] struct_fail.cpp:6: Failure: Compound init on a scalar type
[kernel] Current source was: struct_fail.cpp:6
The full backtrace is:
Raised at Log.finally_raise in file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 546, characters 24-31
Called from Log.Register.fatal in file "src/kernel_services/plugin_entry_points/log.ml", line 1115, characters 17-55
Called from Log.logwithfinal.(fun) in file "src/kernel_services/plugin_entry_points/log.ml", line 539, characters 9-23
Re-raised at Log.logwithfinal.(fun) in file "src/kernel_services/plugin_entry_points/log.ml", line 542, characters 9-16
Called from Log.Register.fatal in file "src/kernel_services/plugin_entry_points/log.ml", line 1115, characters 4-125
Called from Convert.mk_compound_init.aux.aux_struct in file "convert.ml", line 558, characters 24-44
Called from Convert.mk_compound_init in file "convert.ml", line 563, characters 19-37
Called from Convert.convert_global in file "convert.ml", line 4028, characters 29-62
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Convert.convert_ast in file "convert.ml", line 4120, characters 12-76
Called from Frama_Clang_register.parse_cxx in file "frama_Clang_register.ml", line 175, characters 13-36
Called from File.parse_cabs in file "src/kernel_services/ast_queries/file.ml", line 621, characters 6-49
Called from File.to_cil_cabs in file "src/kernel_services/ast_queries/file.ml", line 630, characters 14-38
Called from File.files_to_cabs_cil.(fun) in file "src/kernel_services/ast_queries/file.ml", line 693, characters 46-72
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from File.files_to_cabs_cil in file "src/kernel_services/ast_queries/file.ml", line 693, characters 17-89
Called from File.prepare_from_c_files in file "src/kernel_services/ast_queries/file.ml", line 1784, characters 24-60
Called from File.init_from_cmdline in file "src/kernel_services/ast_queries/file.ml", line 1861, characters 4-27
Called from Ast.force_compute in file "src/kernel_services/ast_data/ast.ml", line 110, characters 2-28
Called from Ast.compute in file "src/kernel_services/ast_data/ast.ml", line 118, characters 53-71
Called from Boot.play_analysis in file "src/kernel_internals/runtime/boot.ml", line 29, characters 6-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
Plug-in fclang aborted: internal error.
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 23.1 (Vanadium).
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: *23.1 (Vanadium)*
- Plug-in used: *frama-clang-0.0.11*
- OS name: *macOS*
- OS version: *Big Sur 11.5.2*Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2569Known WP limitations on statement contract2022-09-28T11:42:56ZAllan BlanchardKnown WP limitations on statement contractSince [Frama-C 23.0](https://git.frama-c.com/pub/frama-c/-/releases/23.0), statement contract are not supported anymore. Related issues are closed (as duplicates) and listed here.
- pub/frama-c#625
- pub/frama-c#1912
- pub/frama-c#511Since [Frama-C 23.0](https://git.frama-c.com/pub/frama-c/-/releases/23.0), statement contract are not supported anymore. Related issues are closed (as duplicates) and listed here.
- pub/frama-c#625
- pub/frama-c#1912
- pub/frama-c#511Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2568Known WP limitations on the reads clause2021-08-05T09:28:31ZAllan BlanchardKnown WP limitations on the reads clauseThis issue lists known WP issues with the reads clause. Related issues are closed (as duplicates) and listed here.
- [ ] Generate `reads` footprint
- pub/frama-c#1146
- pub/frama-c#410
- [ ] Better handle missing `reads`
- p...This issue lists known WP issues with the reads clause. Related issues are closed (as duplicates) and listed here.
- [ ] Generate `reads` footprint
- pub/frama-c#1146
- pub/frama-c#410
- [ ] Better handle missing `reads`
- pub/frama-c#2172Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2567Known WP limitations on `assigns` handling2022-09-22T08:58:28ZAllan BlanchardKnown WP limitations on `assigns` handlingThis issue lists known WP issues with the handling of `assigns` annotation. Related issues are closed (as duplicates) and listed here.
- [ ] WP assigns verification is stronger than what ACSL specifies
- mitigation: see option `-wp-...This issue lists known WP issues with the handling of `assigns` annotation. Related issues are closed (as duplicates) and listed here.
- [ ] WP assigns verification is stronger than what ACSL specifies
- mitigation: see option `-wp-unfold-assigns`
- pub/frama-c#1018
- pub/frama-c#1002
- pub/frama-c#2584
- [ ] WP does not use per behavior assigns
- pub/frama-c#2104
- pub/frama-c#3
- pub/frama-c#1019
- pub/frama-c#2629
Suggestions:
- pub/frama-c#337Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2562[frama-clang] Cannot parse C++14 variable template2021-06-09T06:23:25ZStefan Gränitz[frama-clang] Cannot parse C++14 variable template<!--
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/b452f30e405c34a0f73e45e7c47049c5/fails.cpp)
[works.cpp](/uploads/f3e16883180db5fcb3d9c7c3f50523a7/works.cpp)
```
> cat fails.cpp
template <class _Tp>
struct in_place_type_t {};
template <class _Tp>
in_place_type_t<_Tp> in_place_type{};
int main() {
return 0;
}
> 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 main:
\result FROM \nothing
[from] ====== END OF DEPENDENCIES ======
```
### Actual output
```
[kernel] Parsing fails.ii (external front-end)
fails.cpp:5:22: Unsupported Type (uninstantiated template specialization):in_place_type_t<_Tp>
Aborting
[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 avoid the unused `in_place_type` variable:
```
> diff -u fails.cpp works.cpp
--- fails.cpp 2021-06-08 22:57:23.374859568 +0000
+++ works.cpp 2021-06-08 23:04:33.305251313 +0000
@@ -1,8 +1,8 @@
template <class _Tp>
struct in_place_type_t {};
-template <class _Tp>
-in_place_type_t<_Tp> in_place_type{};
+//template <class _Tp>
+//in_place_type_t<_Tp> in_place_type{};
int main() {
return 0;
```
### 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
Variable templates are a C++14 language feature:
https://isocpp.org/wiki/faq/cpp14-language#variable-templatesVirgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2560[Plug-in wp] 96-bits floats2021-10-06T07:52:08Zarun-babu[Plug-in wp] 96-bits floatsFeature request, as I get:
```
[kernel] Parsing file.c (with preprocessing)
[kernel] Plug-in wp aborted: unimplemented feature.
You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
'[Plug-in wp] 96-bits...Feature request, as I get:
```
[kernel] Parsing file.c (with preprocessing)
[kernel] Plug-in wp aborted: unimplemented feature.
You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
'[Plug-in wp] 96-bits floats'.
```
I am not sure what this means though!https://git.frama-c.com/pub/frama-c/-/issues/2552Errors when trying to analyze programs including MSVC headers2021-05-18T07:08:10Zmarce9Errors when trying to analyze programs including MSVC headersHi,
We are trying to slice the simple program tst3.cpp (included [tst3.cpp](/uploads/0d081c0cc1fd06079866f667b066e4ff/tst3.cpp)).
The execution command is:
_frama-c tst3.cpp -slice-calls g -slicing-level 1 -slicing-keep-annotations -then...Hi,
We are trying to slice the simple program tst3.cpp (included [tst3.cpp](/uploads/0d081c0cc1fd06079866f667b066e4ff/tst3.cpp)).
The execution command is:
_frama-c tst3.cpp -slice-calls g -slicing-level 1 -slicing-keep-annotations -then-on 'Slicing export' -print -ocode output.cpp_
The slicing succeeds and the output is:
![tst3_no_includes_execution_success](/uploads/769b95a3290e6510fb69486ca4030401/tst3_no_includes_execution_success.PNG)
However, when adding 2 includes <stdio.h> & <string.h> the slicing fails with the following output:
![tst3_with_includes_execution_failure](/uploads/6797417f8fe26d2a127995cff63f6782/tst3_with_includes_execution_failure.PNG)
Moreover, we keep facing failures when trying to slice simple programs with the MinGW's GCC compiler and headers. For example, for tried execution the following command:
**_frama-c -cpp-command 'x86_64-w64-mingw32-gcc -C -E -I /usr/x86_64-w64-mingw32/include' -cpp-frama-c-compliant tst3.cpp -slice-calls g -slicing-level 1 -slicing-keep-annotations -then-on 'Slicing export' -print -ocode output.cpp_**
The errors range from "invalid user input" on header files, to incompatible arch mode (32, 64 bit).
Hope to receive help with the right way of executing things, including the right commands with the right parameters, how to use MinGW in order to slice visual-C++ code (MSVC), etc.https://git.frama-c.com/pub/frama-c/-/issues/2546Problems with a simplest Arduino program, that contain only "Arduino.h" include.2021-10-06T07:49:50ZvarosiProblems with a simplest Arduino program, that contain only "Arduino.h" include.Hello!
I'm trying to evaluate if Frama-C could be used for verification of embedded software.
I have a simple program which just include "Arduino.h".
I run this commands:
```
export FC_COMPILER=$'-Os -mlong-calls -falign-functions=4 -...Hello!
I'm trying to evaluate if Frama-C could be used for verification of embedded software.
I have a simple program which just include "Arduino.h".
I run this commands:
```
export FC_COMPILER=$'-Os -mlong-calls -falign-functions=4 -U__STRICT_ANSI__ -ffunction-sections -fdata-sections -fno-exceptions -DPLATFORMIO=50101 -DESP8266 -DARDUINO_ARCH_ESP8266 -DARDUINO_ESP8266_ESP12 -DF_CPU=160000000L -D__ets__ -DICACHE_FLASH -DARDUINO=10805 -DARDUINO_BOARD=PLATFORMIO_ESP12E -DFLASHMODE_DIO -DLWIP_OPEN_SRC -DNONOSDK22x_190703=1 -DTCP_MSSß=536 -DLWIP_FEATURES=1 -DLWIP_IPV6=0 -DVTABLES_IN_FLASH -I.platformio/packages/framework-arduinoespressif8266/cores/esp8266 -I.platformio/packages/framework-arduinoespressif8266/tools/sdk/include -I.platformio/packages/framework-arduinoespressif8266/tools/sdk/libc/xtensa-lx106-elf/include'
export FC_ERRORS="-kernel-warn-key annot-error=error"
frama-c ${FC_ERRORS} -fclang-cpp-extra-args="${FC_COMPILER}" -machdep x86_32 -wp -wp-rte src/main.cpp
```
in a Docker container varosi/frama-c-clang:21.1
I get a lot of errors such as:
```
In file included from /app/src/main.cpp:4:
In file included from .platformio/packages/framework-arduinoespressif8266/cores/esp8266/Arduino.h:238:
In file included from /usr/local/share/frama-c/frama-clang/libc++/algorithm:26:
In file included from /usr/local/share/frama-c/frama-clang/libc++/functional:27:
In file included from /usr/local/share/frama-c/frama-clang/libc++/utility:28:
/usr/local/share/frama-c/frama-clang/libc++/type_traits:284:46: error: template argument for template type parameter must be a type
using conditional_t = typename conditional<B,T,F>::type;
^
/usr/local/share/frama-c/frama-clang/libc++/type_traits:278:25: note: template parameter is declared here
template <bool, class T, class F> struct conditional;
^
/usr/local/share/frama-c/frama-clang/libc++/type_traits:284:54: error: expected a qualified name after 'typename'
using conditional_t = typename conditional<B,T,F>::type;
^
/usr/local/share/frama-c/frama-clang/libc++/type_traits:284:54: error: type-id cannot have a name
using conditional_t = typename conditional<B,T,F>::type;
----------------
In file included from /app/src/main.cpp:4:
In file included from .platformio/packages/framework-arduinoespressif8266/cores/esp8266/Arduino.h:238:
In file included from /usr/local/share/frama-c/frama-clang/libc++/algorithm:26:
In file included from /usr/local/share/frama-c/frama-clang/libc++/functional:27:
/usr/local/share/frama-c/frama-clang/libc++/utility:33:23: error: unknown type name '_Bool'
template<class T> bool operator!=(const T& x, const T& y) { return !(x == y); }
^
/usr/local/share/frama-c/libc/stdbool.h:25:14: note: expanded from macro 'bool'
#define bool _Bool
----------------
In file included from /app/src/main.cpp:4:
In file included from .platformio/packages/framework-arduinoespressif8266/cores/esp8266/Arduino.h:238:
In file included from /usr/local/share/frama-c/frama-clang/libc++/algorithm:26:
In file included from /usr/local/share/frama-c/frama-clang/libc++/functional:27:
/usr/local/share/frama-c/frama-clang/libc++/utility:68:40: error: expected a qualified name after 'typename'
const T&, T&&>::type
^
/usr/local/share/frama-c/frama-clang/libc++/utility:68:40: warning: variable templates are a C++14 extension
/usr/local/share/frama-c/frama-clang/libc++/utility:68:44: error: expected ';' at end of declaration
const T&, T&&>::type
^
;
/usr/local/share/frama-c/frama-clang/libc++/utility:69:20: error: unknown type name 'T'
move_if_noexcept(T& x) noexcept { return std::move<T&>(x); }
--------------------
In file included from /app/src/main.cpp:4:
In file included from .platformio/packages/framework-arduinoespressif8266/cores/esp8266/Arduino.h:238:
In file included from /usr/local/share/frama-c/frama-clang/libc++/algorithm:26:
In file included from /usr/local/share/frama-c/frama-clang/libc++/functional:27:
/usr/local/share/frama-c/frama-clang/libc++/utility:110:16: error: template argument for template type parameter must be a type; did you forget 'typename'?
__and<
^
typename
/usr/local/share/frama-c/frama-clang/libc++/type_traits:274:25: note: template parameter is declared here
template <bool, class T=void> struct enable_if;
--------------------
```
What can be fixed here?Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2459Frama-C fails to parse a file2022-12-28T10:05:19Zmantis-gitlab-migrationFrama-C fails to parse a fileID0000261:
**This issue was created automatically from Mantis Issue 261. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000261:
**This issue was created automatically from Mantis Issue 261. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000261 | Frama-C | Kernel | public | 2009-10-01 | 2009-10-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jonathan-Christofer Demay | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C Beryllium-20090901 | **Target Version** | - | **Fixed in Version** | - |
### Description :
It compiles fine with "gcc -I. -I./libtomcrypt/src/headers/ -DDROPBEAR_SERVER -DDROPBEAR_CLIENT dbutil.c -c -o dbutil.o"
But when given to Frama-C (CPP is set accordinly), I get the following error:
libtommath/tommath.h:77:[kernel] user error: GCC width mode TI applied to unexpected type, or unexpected mode
In tommath.h line 77 we have a mysterious GCC incantation (>_<):
typedef unsigned long mp_word __attribute__ ((mode(TI)));
### Additional Information :
Uploaded a preprocessed file: "gcc -I. -I./libtomcrypt/src/headers/ -DDROPBEAR_SERVER -DDROPBEAR_CLIENT dbutil.c -C -E -o dbutil.i"
## Attachments
- [dbutil.i](/uploads/ca1ba34059bd1dd4efa823437f09a2c6/dbutil.i)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/2428ghost integer ?2021-02-22T13:58:46ZSylvie Boldoghost integer ?ID0000387:
**This issue was created automatically from Mantis Issue 387. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000387:
**This issue was created automatically from Mantis Issue 387. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000387 | Frama-C | Kernel > ACSL implementation | public | 2010-02-01 | 2010-02-05 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | sboldo | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | feature | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - |
### Description :
Hello,
It is impossible to have a ghost variable of type integer.
I may have an int32 ghost, but I would really prefer having an unbounded integer instead of an int32.Virgile PrevostoVirgile Prevosto