frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2024-01-17T11:25:46Zhttps://git.frama-c.com/pub/frama-c/-/issues/2681[kernel] Conflicting types error for enum & typedef enum2024-01-17T11:25:46ZT-Gruber[kernel] Conflicting types error for enum & typedef enumI have encountered a problem that leads to an error when parsing. This occurs when an enum is defined multiple times as shown below. The expectation would be that it works as with the struct shown:
- forward declaration of struct/enum
- ...I have encountered a problem that leads to an error when parsing. This occurs when an enum is defined multiple times as shown below. The expectation would be that it works as with the struct shown:
- forward declaration of struct/enum
- introducing an alias via typedef
- both in one
```C
// test.c
// works
struct my_struct;
typedef struct my_struct my_struct;
typedef struct my_struct {
int val;
} my_struct;
// fails
enum my_enum;
typedef enum my_enum my_enum;
typedef enum my_enum {
VAL
} my_enum;
```
### Steps to reproduce the issue
Parse source file:
```
frama-c test.c
```
### Expected behaviour
Output:
```
[kernel] Parsing test.c
```
### Actual behaviour
Output:
```
[kernel] Parsing test.c
[kernel] test.c:14: User Error:
redefinition of type 'my_enum' in the same scope with conflicting type.
Previous declaration was at test.c:10
[kernel] User Error: stopping on file "test.c" that has errors.
[kernel] Frama-C aborted: invalid user input.
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 27.0 (Cobalt)
- OS: Ubuntu 22.04.2 LTS (WSL)https://git.frama-c.com/pub/frama-c/-/issues/2652Unproven validity of memory access2023-05-16T06:54:01ZYani ZIANIUnproven validity of memory access<!--
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]…
-->
### Description
According to the ACSL language implementation p.67 for Frama-C v26.0 and 26.1 (modulo potential alignment constraints), the ``valid {L}(p) <==> \valid{L}(((char *)p)+(0 .. sizeof(*p)-1))`` equivalence should hold true for any pointer ``p`` (and would be in line with C's behavior when trying to access any pointer as an array of bytes). But I've run into trouble trying to prove it in simple cases, be it using the ``Typed`` memory model, or its extension using ``+cast``.
### 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.
-->
Running Frama-C with WP on the minimal code inlined below, or running ``frama-c-gui char_ptr.c -wp `` and ``frama-c-gui char_ptr.c -wp -wp-model Typed+cast`` using the attachments.
```C
#include <stdio.h>
typedef struct {
int test_buffer[5];
} test_type;
int * test_ptr;
test_type * _test_type_ptr;
int dummy_valid()
{
/*@ check \valid(test_ptr) ==> \valid(((char *) test_ptr) + (0 .. (size_t) sizeof(*test_ptr) -
/*@ check \valid(((char *) test_ptr) + (0 .. (size_t) sizeof(*test_ptr) - 1)) ==> \valid(
/*@ check \valid(_test_type_ptr) ==> \valid(((char *) _test_type_ptr) + (0 .. (size_t) sizeof(*_test_type_ptr) -
/*@ check \valid((char *) _test_type_ptr + (0 .. (size_t) sizeof(*_test_type_ptr) - 1)) ==> \valid(_test_type_ptr);*/
return 0;
}
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
All check clauses should be proved when using the ``+cast`` variant of ``Typed``.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
None of the check clauses extending the validity of the original pointer to the validity of the corresponding byte array are proved.
My understanding/guess would be that it may be due to WP's ability to translate the cast to ``char *`` to byte accesses, but I'm really not clear on what's actually happening there.
```
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: 26.0 (Iron)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 20.04.4 LTS
### Additional information (optional)
- Alt-Ergo version : 2.4.2
<!--
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.
-->
FYI @nkosmatov
[char_ptr.c](/uploads/8ebaf1fac5f9a9c8de2e0367ef0cd628/char_ptr.c)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2649[WP] no trivial separation of the allocation status of heap and local variabl...2023-02-15T07:38:06ZYani ZIANI[WP] no trivial separation of the allocation status of heap and local variables whose address are taken<!--
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]…
-->
### Description
I'm currently working on specifying and proving functions focused on linked list structures using previous works based on ACSL logic lists (cf this [paper](https://nikolai-kosmatov.eu/publications/blanchard_kl_sac_2019.pdf)), and I've encountered some issues proving relatively simple assertions when certain types of memory separation between pointers are involved.
### 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.
-->
Running Frama-C with WP on the minimal code inlined below, or running ``frama-c-gui linked_ll_dptr_proof.c -wp -wp-rte -wp-prover altergo,cvc4,cvc4-ce -wp-smoke-tests -wp-fct="dummyCaller, dummyCaller_bis" &`` using the attachments.
I've also taken the liberty of attaching an extended version of the code below in ``linked_ll_dptr_proof.c`` including all the logic definitions (modulo name changes) used in the "Logic against Ghosts" paper, as well as the corresponding lemmas in ``lemmas_list.h``, but I'm not really sure of their relevance, as the issue also occurs on variants of the original logic definitions of the paper that are not used by said lemmas.
```C
#include <stdlib.h>
typedef struct LIST {
int handle;
struct LIST * next;
} LIST;
/**** Logic definitions from the "Logic against Ghosts" paper (modulo renaming for node_to_ll) ****/
/*@
predicate ptr_separated_from_range{L}
(LIST* e, \list<LIST*> ll, integer beg, integer end) =
\forall integer n ; 0 <= beg <= n < end <= \length(ll) ==> \separated(\nth(ll, n), e);
predicate dptr_separated_from_range{L}
(LIST** e, \list<LIST*> ll, integer beg, integer end) =
\forall integer n ; 0 <= beg <= n < end <= \length(ll) ==> \separated(\nth(ll, n), e);
predicate ptr_separated_from_list{L}(LIST* e, \list<LIST*> ll) =
ptr_separated_from_range(e, ll, 0, \length(ll));
predicate dptr_separated_from_list{L}(LIST** e, \list<LIST*> ll) =
dptr_separated_from_range(e, ll, 0, \length(ll));
*/
/*@
predicate in_list{L}(LIST* e, \list<LIST*> ll) =
\exists integer n ; 0 <= n < \length(ll) && \nth(ll, n) == e ;
*/
/*@
inductive linked_ll{L}(LIST *bl, LIST *el, \list<LIST*> ll) {
case linked_ll_nil{L}:
\forall LIST *el ; linked_ll{L}(el, el, \Nil);
case linked_ll_cons{L}:
\forall LIST *bl, *el, \list<LIST*> tail ;
\separated(bl, el) ==> \valid(bl) ==>
linked_ll{L}(bl->next, el, tail) ==>
ptr_separated_from_list(bl, tail) ==>
linked_ll{L}(bl, el, \Cons(bl, tail)) ;
}
*/
/*@
axiomatic Node_To_ll {
logic \list<LIST*> node_to_ll{L}(LIST* beg_node, LIST* end_node)
reads { node->next | LIST* node ; \valid(node) && in_list(node, node_to_ll(beg_node, end_node)) } ;
axiom to_ll_nil{L}:
\forall LIST *node ; node_to_ll{L}(node, node) == \Nil ;
axiom to_ll_cons{L}:
\forall LIST *beg_node, *end_node ;
\separated(beg_node, end_node) ==>
\valid{L}(beg_node) ==>
ptr_separated_from_list{L}(beg_node, node_to_ll{L}(beg_node->next, end_node)) ==>
node_to_ll{L}(beg_node, end_node) == (\Cons(beg_node, node_to_ll{L}(beg_node->next, end_node))) ;
}
*/
/*******************************************************************/
/*@
requires node_separation_to_list : dptr_separated_from_list(out_node, node_to_ll(rsrc_list, NULL)); //if uncommented, linked_assert cannot be proved
assigns \nothing;
ensures \result == 616;
*/
int dummyCallee(LIST * rsrc_list, LIST ** out_node);
/*@
requires linked_ll(rsrc_list, NULL, node_to_ll(rsrc_list, NULL));
assigns \nothing;
ensures \result == 616;
*/
int dummyCaller(LIST * rsrc_list, LIST ** out_node)
{
/*@ assert linked_assert : linked_ll(rsrc_list, NULL, node_to_ll(rsrc_list, NULL));*/ // should be proved from the precondition
int r;
LIST *test_node;
r = dummyCallee(rsrc_list, &test_node);
return r;
}
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
The ``linked_assert`` assertion in dummyCaller (or dummyCaller_bis in the attached files) should be always proved, even when the ``node_separation_to_list`` (and/or ``int_separation_to_list`` in attachments) preconditions are uncommented.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
None of the linked_assert assertions are proved.
The situation depicted by ``dummyCaller`` and ``dummyCallee``, using ``node_separation_to_list`` as a precondition, is the closest to the code I'm currently working on.
In the code in attachments, I also tried using ``node_separation_to_nil`` as precondition to test whether the issue also occured using a ``\Nil`` logic list, and the ``dummyCaller_bis`` and ``dummyCallee_bis`` functions to test if eliminating lemmas, or changing the datatype used for separation in ``dummyCallees``, had any influence on the issue, but they don't seem to.
```
```
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: 26.0 (Iron) (As well as version 25.0)
- Plug-in used: WP and RTE
- OS name: Ubuntu
- OS version: 20.04.4 LTS
### Additional information (optional)
- Alt-Ergo version : 2.4.2
- CVC4 version : 1.7
<!--
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.
-->
FYI @nkosmatov @floulergue
Edit: I completely forgot to add those attachments earlier :
[linked_ll_dptr_proof.c](/uploads/dd969cc3ce822db1c89e21fa939d0d48/linked_ll_dptr_proof.c)
[lemmas_list.h](/uploads/a9620641f45aa49d32cf7234f2d4ccfd/lemmas_list.h)Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2646OPAM installation on macOS fails2023-05-16T06:53:50ZvarosiOPAM installation on macOS fails<!--
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
To install correctly using OPAM on macOS Ventura 13.2 on x64 following - https://frama-c.com/html/get-frama-c.html
### Actual behaviour
After running **opam install frama-c**, I got:
```
> <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
> -> removed conf-gtk2.1
> -> installed conf-gtk2.1
> -> retrieved frama-c.21.1 (cached)
> [ERROR] The compilation of frama-c.21.1 failed at "make -j11".
>
> #=== ERROR while compiling frama-c.21.1 =======================================#
> # context 2.1.4 | macos/x86_64 | ocaml-base-compiler.4.07.1 | https://opam.ocaml.org#0c15cf29
> # path ~/.opam/default/.opam-switch/build/frama-c.21.1
> # command ~/.opam/opam-init/hooks/sandbox.sh build make -j11
> # exit-code 2
> # env-file ~/.opam/log/frama-c-37505-febf41.env
> # output-file ~/.opam/log/frama-c-37505-febf41.out
> ### output ###
> # [...]
> # Ocamlc src/plugins/qed/hcons.cmo
> # Ocamlc src/plugins/qed/listmap.cmo
> # Ocamlc src/plugins/qed/listset.cmo
> # Ocamlc src/plugins/qed/intmap.cmo
> # Ocamlc src/plugins/qed/intset.cmo
> # File "src/plugins/markdown-report/sarif.ml", line 31, characters 17-30:
> # Error: Unbound type constructor Yojson.Safe.t
> # make: *** [src/plugins/markdown-report/sarif.cmo] Error 2
> # make: *** Waiting for unfinished jobs....
> # Ocamlc src/plugins/qed/idxmap.cmo
> # AR src/plugins/e-acsl/lib/libeacsl-dlmalloc.a
> # RANLIB src/plugins/e-acsl/lib/libeacsl-dlmalloc.a
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: not installed previously
- OS name: macOS
- OS version: Ventura 13.2 on x64Andre MaronezeAndre Maronezehttps://git.frama-c.com/pub/frama-c/-/issues/2641can't parse __int1282023-05-16T06:53:28ZYurii Rashkovskiican't parse __int128<!--
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.
-->
Expect this to be processed:
```c
__int128 i;
```
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Get a syntax error:
```
syntax error:
Location: between <unknown> and 1:9, before or at token: v
1 __int128 v;
```
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 26
- Plug-in used: WP
- OS name: macOS
- OS version: 13.1
### 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.
-->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/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/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/2347Parse error when using a wide string literal to initialize uint16 array2021-02-22T13:56:58Zmantis-gitlab-migrationParse error when using a wide string literal to initialize uint16 arrayID0000593:
**This issue was created automatically from Mantis Issue 593. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- ...ID0000593:
**This issue was created automatically from Mantis Issue 593. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0000593 | Frama-C | Kernel | public | 2010-09-30 | 2010-10-01 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Maria | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
I'm trying to analyze Brew with Frama-C. OS - windows XP.
I've created simple Brew project(see attach), preprocessed it with Visual Studio and after it try to analyze with Frama-C:
C:\Frama-C\bin>frama-c.exe "\Program Files\BREW 3.1.5\sdk\examples\helloworld"\*.i
Also, I've tried to add files to project, using user interface, but nothing happened.
## Attachments
- [helloworld.zip](/uploads/e1faf5861730eaa7d75da589b90c18c6/helloworld.zip)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/906exception identifier from catch() statement unknown in contracts, but not in ...2021-02-22T13:28:04ZJochen Burghardtexception identifier from catch() statement unknown in contracts, but not in codeID0002071:
**This issue was created automatically from Mantis Issue 2071. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002071:
**This issue was created automatically from Mantis Issue 2071. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002071 | Frama-Clang | Plug-in > clang | public | 2015-02-02 | 2015-02-13 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 447.cpp (external front-end)
447.cpp:6:17: unknown identifier 'e'
Now output intermediate result
The message disappears if the "assert" in line 6 is deactivated.
## Attachments
- [447.cpp](/uploads/25b6f25f7846390e808821adc8820019/447.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/903can't compare pointer and reference for equality in contract2021-02-22T13:14:31ZJochen Burghardtcan't compare pointer and reference for equality in contractID0002060:
**This issue was created automatically from Mantis Issue 2060. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002060:
**This issue was created automatically from Mantis Issue 2060. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002060 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 441.cpp (external front-end)
441.cpp:2:22: invalid implicit conversion
441.cpp:2:22: unknown type comparison for the operator ==
Now output intermediate result
When line 2 is commented out, the comparison in C++ code in line 3 is accepted.
## Attachments
- [441.cpp](/uploads/da2cc8f3623d5563d069827341da0b18/441.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/900type def'd as template typename causes SEGV when used in logic functions2021-02-22T13:14:28ZJochen Burghardttype def'd as template typename causes SEGV when used in logic functionsID0002057:
**This issue was created automatically from Mantis Issue 2057. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002057:
**This issue was created automatically from Mantis Issue 2057. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002057 | Frama-Clang | Plug-in > clang | public | 2015-01-22 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | fvedrine | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
In its current version, the program apparently causes a SEGV of the front-end:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 438.cpp (external front-end)
Segmentation fault (core dumped)
[kernel] user error: Failed to parse C++ file. See Clang messages for more information
Several variations cause different behaviors, such as:
(1) changing "integer" to "int " in line 8:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 438.cpp (external front-end)
438.cpp:8:51: invalid implicit conversion
438.cpp:8:51: expecting a term as body of function
Now output intermediate result
(2) omitting the template parameter, and changing "T" to "int" in line 3:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 438.cpp (external front-end)
Now output intermediate result
[fclang] failure: Cannot understand intermediate AST: line 799: unexpected unknown constructor 39702768 (Unknown constructor for term_node)
[kernel] Current source was: FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i:43
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/frama_Clang_register.ml", line 83, characters 6-75
Called from file "src/kernel/file.ml", line 1248, characters 8-41
Called from file "src/kernel/file.ml", line 1296, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1293, characters 6-864
Called from file "src/kernel/file.ml", line 2287, characters 12-30
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-STANCE.
(3) changing "pointer" to "T*" in line 7:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 438.cpp (external front-end)
438.cpp:8:55: predicates do not support binary '+' operation
Now output intermediate result
438.cpp:7:[fclang] failure: predicate definition with a term as body
[kernel] Current source was: 438.cpp:7
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_acsl.ml", line 622, characters 12-76
Called from file "src/frama-clang/convert.ml", line 2393, characters 18-54
Called from file "src/frama-clang/convert.ml", line 2554, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2558, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1248, characters 8-41
Called from file "src/kernel/file.ml", line 1296, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1293, characters 6-864
Called from file "src/kernel/file.ml", line 2287, characters 12-30
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-STANCE.
## Attachments
- [438.cpp](/uploads/4ab4dc04efdff7cdadbd1e41d15d47e0/438.cpp)
- [438a.cpp](/uploads/957036da370283dcaa88f2713cd9f18a/438a.cpp)Franck VedrineFranck Vedrinehttps://git.frama-c.com/pub/frama-c/-/issues/898catching a superclass causes crash2021-02-22T13:14:26ZJochen Burghardtcatching a superclass causes crashID0002051:
**This issue was created automatically from Mantis Issue 2051. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002051:
**This issue was created automatically from Mantis Issue 2051. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002051 | Frama-Clang | Plug-in > clang | public | 2015-01-15 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
[fclang] failure: Did not find struct for mangled class name _Z9Underflow
[kernel] Current source was: 432.cpp:6
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_link.ml", line 71, characters 36-53
Called from file "src/lib/FCSet.ml", line 332, characters 37-58
Called from file "src/frama-clang/convert_link.ml", line 86, characters 16-112
Called from file "src/frama-clang/convert_link.ml", line 104, characters 16-62
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert_link.ml", line 102, characters 12-142
Called from file "src/kernel/visitor.ml", line 75, characters 14-33
Called from file "cil/src/cil.ml", line 2046, characters 15-31
Called from file "cil/src/cil.ml", line 3095, characters 5-86
Called from file "cil/src/cil.ml", line 2085, characters 13-16
Called from file "cil/src/cil.ml", line 3255, characters 16-40
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 3484, characters 14-39
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 3446, characters 5-91
Called from file "cil/src/cil.ml", line 3538, characters 16-38
Called from file "cil/src/cil.ml", line 2085, characters 13-16
Called from file "cil/src/cil.ml", line 2130, characters 24-57
Called from file "cil/src/cil.ml", line 3532, characters 5-53
Called from file "cil/src/cil.ml", line 6151, characters 16-36
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/cil.ml", line 5741, characters 3-30
Called from file "cil/src/cil.ml", line 6152, characters 2-420
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 6185, characters 7-84
Called from file "src/kernel/file.ml", line 1803, characters 2-8
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/file.ml", line 1880, characters 2-36
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-STANCE.
The problem remains if some member variable (e.g. "int x;") is added to the body of class "Matherr" in line 2 or/and the body of class "Underflow" in line 3.
The problem disappears if either:
(1) the definition of "Underflow" in line 3 is deleted,
(2) the definition of "foo" in line 5-10 is deleted,
(3) "Matherr" is changed to "Underflow" in the catch statement in line 8, or
(4) "public" is changed to "private" in line 3.
## Attachments
- [432.cpp](/uploads/c3a89685372790a4946ec88f8e54c293/432.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/897recursive logic integer function definition causes error2021-02-22T13:27:11ZJochen Burghardtrecursive logic integer function definition causes errorID0002050:
**This issue was created automatically from Mantis Issue 2050. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002050:
**This issue was created automatically from Mantis Issue 2050. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002050 | Frama-Clang | Plug-in > clang | public | 2015-01-15 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
431.cpp:2:56: unknown identifier 'fac'
Now output intermediate result
The problem disappears when the file is renamed to "431.c".
## Attachments
- [431.cpp](/uploads/50a3448bd9c7ec87a3c7205370803f6e/431.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/896ACSL comment rejected in function template2021-02-22T13:27:13ZJochen BurghardtACSL comment rejected in function templateID0002048:
**This issue was created automatically from Mantis Issue 2048. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002048:
**This issue was created automatically from Mantis Issue 2048. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002048 | Frama-Clang | Plug-in > clang | public | 2015-01-12 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | minor | **Reproducibility** | always |
| **Platform** | Neon-20140301+dev-STANCE-Jan2015 | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing 430.cpp (external front-end)
inadequate comment at 430.cpp:5:2
If line 2 is commented-in and line 3 is commented-out, the error message disappears.
## Attachments
- [430.cpp](/uploads/fb7c1b9a2c7e740eb0e5c7200661ce99/430.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/895unprovable obligation generated for "ensures" in presence of exceptions2021-02-22T13:14:24ZJochen Burghardtunprovable obligation generated for "ensures" in presence of exceptionsID0002046:
**This issue was created automatically from Mantis Issue 2046. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002046:
**This issue was created automatically from Mantis Issue 2046. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002046 | Frama-Clang | Plug-in > clang | public | 2015-01-08 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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 :
Running "frama-c -wp 429.cpp" on the attached program, the goal "typed__Z3bari_post_part1" cannot be proven by Alt-Ergo, i.e. it can't be proven that the postcondition of "foo" implies that of "bar" if the former doesn't throw an exception.
The goal in the file "_Z3bari_post_part1_Alt-Ergo.mlw" reads:
585 goal _Z3bari_post_part1:
586 forall i : int.
587 forall f : S___fc_exn_struct.
588 let x = (f.F___fc_exn_struct_exn_uncaught) : int in
589 (1 <> x) ->
590 is_sint32(i) ->
591 is_sint32(f.F___fc_exn_struct_exn_kind) ->
592 is_sint32(x) ->
593 ((0 = x) -> (42 <= i)) ->
594 (24 <= i)
If line 589 is changed to "(0 = x) ->", Alt-Ergo can prove it without problems; likewise if line 593 is changed to "((1 <> x) -> (42 <= i)) ->".
## Attachments
- [429.cpp](/uploads/8924b97702a6b0ba13c4daf1f56285ca/429.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/894throw without argument causes crash2021-02-22T13:41:11ZJochen Burghardtthrow without argument causes crashID0002045:
**This issue was created automatically from Mantis Issue 2045. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0002045:
**This issue was created automatically from Mantis Issue 2045. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0002045 | Frama-Clang | Plug-in > clang | public | 2015-01-08 | 2015-02-14 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **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:
Now output intermediate result
[kernel] Current source was: 428.cpp:2
The full backtrace is:
Raised at file "stack.ml", line 36, characters 20-25
Called from file "src/kernel/exn_flow.ml", line 98, characters 23-44
Called from file "src/kernel/visitor.ml", line 75, characters 14-33
Called from file "cil/src/cil.ml", line 2046, characters 15-31
Called from file "cil/src/cil.ml", line 3095, characters 5-86
Called from file "cil/src/cil.ml", line 2085, characters 13-16
Called from file "cil/src/cil.ml", line 3255, characters 16-40
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 3484, characters 14-39
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 3446, characters 5-91
Called from file "cil/src/cil.ml", line 3538, characters 16-38
Called from file "cil/src/cil.ml", line 2085, characters 13-16
Called from file "cil/src/cil.ml", line 2130, characters 24-57
Called from file "cil/src/cil.ml", line 3532, characters 5-53
Called from file "cil/src/cil.ml", line 6151, characters 16-36
Called from file "list.ml", line 69, characters 12-15
Called from file "cil/src/cil.ml", line 5741, characters 3-30
Called from file "cil/src/cil.ml", line 6152, characters 2-420
Called from file "cil/src/cil.ml", line 2061, characters 21-41
Called from file "cil/src/cil.ml", line 6185, characters 7-84
Called from file "src/kernel/visitor.ml", line 827, characters 2-45
Called from file "src/kernel/file.ml", line 1803, characters 2-8
Called from file "queue.ml", line 134, characters 6-20
Called from file "src/kernel/file.ml", line 1880, characters 2-36
Called from file "src/kernel/file.ml", line 2372, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Unexpected error (Stack.Empty).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-STANCE.
## Attachments
- [428.cpp](/uploads/ec15e3525df0c4c9340947fc89b631c9/428.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/889use of template class in default template argument in namespace causes crash2021-02-22T13:14:16ZJochen Burghardtuse of template class in default template argument in namespace causes crashID0001970:
**This issue was created automatically from Mantis Issue 1970. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001970:
**This issue was created automatically from Mantis Issue 1970. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001970 | Frama-Clang | Plug-in > clang | public | 2014-11-17 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | - | **OS** | - | **OS Version** | - |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
135.cpp:6:[fclang] failure: Unknown aggregate type std::vector<...,...>
[kernel] Current source was: 135.cpp:6
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert_env.ml", line 269, characters 43-71
Called from file "src/frama-clang/convert.ml", line 162, characters 17-69
Called from file "src/frama-clang/convert.ml", line 170, characters 17-52
Called from file "list.ml", line 57, characters 20-23
Called from file "src/frama-clang/convert.ml", line 1283, characters 13-45
Called from file "src/frama-clang/convert.ml", line 1910, characters 8-66
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1998, characters 19-78
Called from file "src/frama-clang/convert.ml", line 2262, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2266, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
The problem remains if the "std::" prefix is removed in line 5.
However, the problem disappears if no namespaces are used at all, i.e. if line 2 and 7 are deleted, and the "std::" prefixes are removed in line 5 and 9.
(Importance: this code is used via #include <vector>.)
## Attachments
- [135.cpp](/uploads/ea988c45a4d3e96baf392b9da299f9f7/135.cpp)Virgile PrevostoVirgile Prevostohttps://git.frama-c.com/pub/frama-c/-/issues/887use of initialized array causes crash2021-02-22T13:27:04ZJochen Burghardtuse of initialized array causes crashID0001986:
**This issue was created automatically from Mantis Issue 1986. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | ---...ID0001986:
**This issue was created automatically from Mantis Issue 1986. Further discussion may take place here.**
---
| **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** |
| --- | --- | --- | --- | --- | --- |
| ID0001986 | Frama-Clang | Plug-in > clang | public | 2014-11-24 | 2015-02-15 |
| | | | | | |
| --- | --- | --- | --- | --- | --- |
| **Reporter** | Jochen | **Assigned To** | virgile | **Resolution** | open |
| **Priority** | normal | **Severity** | crash | **Reproducibility** | always |
| **Platform** | frama-c-Neon-20140301+dev-stance | **OS** | - | **OS Version** | xubuntu-cfe13.10 |
| **Product Version** | - | **Target Version** | - | **Fixed in Version** | - |
### Description :
output:
Now output intermediate result
149.cpp:4:[fclang] failure: Unknown local variable a
[kernel] Current source was: 149.cpp:4
The full backtrace is:
Raised at file "src/kernel/log.ml", line 524, characters 30-31
Called from file "src/kernel/log.ml", line 518, characters 9-16
Re-raised at file "src/kernel/log.ml", line 521, characters 15-16
Called from file "src/frama-clang/convert.ml", line 210, characters 8-39
Called from file "src/frama-clang/convert.ml", line 387, characters 33-55
Called from file "src/frama-clang/convert.ml", line 434, characters 29-52
Called from file "src/frama-clang/convert.ml", line 567, characters 29-52
Called from file "src/frama-clang/convert.ml", line 421, characters 29-52
Called from file "src/frama-clang/convert.ml", line 1082, characters 25-48
Called from file "src/frama-clang/convert.ml", line 1275, characters 20-46
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 1265, characters 17-40
Called from file "src/frama-clang/convert.ml", line 2151, characters 21-44
Called from file "src/frama-clang/convert.ml", line 2262, characters 21-48
Called from file "list.ml", line 74, characters 24-34
Called from file "src/frama-clang/convert.ml", line 2266, characters 4-79
Called from file "src/frama-clang/frama_Clang_register.ml", line 86, characters 13-36
Called from file "src/kernel/file.ml", line 1073, characters 10-43
Called from file "src/kernel/file.ml", line 1117, characters 23-30
Called from file "list.ml", line 74, characters 24-34
Called from file "src/kernel/file.ml", line 1114, characters 6-520
Called from file "src/kernel/file.ml", line 2179, characters 12-30
Called from file "src/kernel/file.ml", line 2264, characters 4-27
Called from file "src/kernel/ast.ml", line 111, characters 2-28
Called from file "src/kernel/ast.ml", line 123, characters 53-71
Called from file "src/kernel/boot.ml", line 29, characters 6-20
Called from file "src/kernel/cmdline.ml", line 761, characters 2-9
Called from file "src/kernel/cmdline.ml", line 216, characters 4-8
Plug-in fclang aborted: internal error.
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Neon-20140301+dev-stance.
The problem disappears if "a" isn't initialized in line 3, i.e. if "= {11,22,33}" is removed there.
## Attachments
- [149.cpp](/uploads/51ab1c38b8c7d36f3e7e7306fef9b130/149.cpp)Virgile PrevostoVirgile Prevosto