frama-c issueshttps://git.frama-c.com/pub/frama-c/-/issues2023-05-16T06:54:01Zhttps://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/2651[WP] Value of 2D-array does not work well2023-03-28T08:47:37ZJim Chen[WP] Value of 2D-array does not work well<!--
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++
#define NUM 5
int x[NUM][NUM];
/*@
@ requires \forall integer i, j; 0 <= i < NUM && 0 <= j < NUM ==> 0 <= x[i][j] < 100;
@*/
void foo()
{
int tmp;
for (int i = 0; i < NUM; i++)
{
for (int j = 0; j < NUM; j++)
{
tmp = x[i][j] + 1;
//@ assert PASS: 1 <= tmp < 101;
//@ assert ASSERTED: tmp < 100;
}
}
if (tmp > 100)
{
tmp = 1;
return;
}
else
{
tmp = 2;
return;
}
}
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
PASS should be pass and ASSERTED should be triggered.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Both of the assertion were triggered in WP
i'm using command:
`frama-c -wp -wp-no-rte -wp-prover z3-nobv,alt-ergo -wp-cache 'rebuild' -wp-model 'Typed' -pp-annot -c11 -kernel-msg-key pp -main foo -lib-entry ./test.c`
### Contextual information
- Frama-C installation mode: *Opam*
- Frama-C version: *26.1* (as reported by `frama-c -version`)
- Plug-in used: *WP*
- OS name: *Ubuntu*
- OS version: *20.04*
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
this 2d-array phenomenon is also observed when I'm writing loop assigns like this:
```c++
#define NUM 5
int x[NUM][NUM];
/*@
@ ;
@*/
void foo()
{
/*@
@ loop assigns x[0 .. NUM - 1][0 .. NUM - 1];
@*/
for (int i = 0; i < NUM; i++)
{
/*@
@ loop assigns x[i][0 .. NUM - 1];
@*/
for (int j = 0; j < NUM; j++)
{
x[i][j] = i * j;
}
}
return;
}
```Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2650Stack overflow using WP in Wp__Register.step_finally2023-03-29T20:08:35ZChristophe GarionStack overflow using WP in Wp__Register.step_finallyFrama-C 26.1 and its WP plugin crash with a stack overflow when trying to prove a function:
```
The full backtrace is:
Raised at Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 834, characters 41-48
Called fro...Frama-C 26.1 and its WP plugin crash with a stack overflow when trying to prove a function:
```
The full backtrace is:
Raised at Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 834, characters 41-48
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Wp__Register.step_finally in file "src/plugins/wp/register.ml", line 835, characters 2-12
Called from Stdlib__Queue.iter.iter in file "queue.ml", line 121, characters 6-15
Called from Frama_c_boot__Boot.play_analysis in file "src/init/boot/boot.ml", line 36, characters 4-20
Called from Frama_c_kernel__Cmdline.play_in_toplevel_one_shot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 850, characters 2-9
Called from Frama_c_kernel__Cmdline.play_in_toplevel in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 880, characters 18-64
Called from Frama_c_kernel__Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 233, characters 4-8
Unexpected error (Stack overflow).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 26.1 (Iron).
```
The function to be proved is part of a rather big C file included in the attached archive. Sorry for the complexity (and maybe the bad quality) of the C code, it is in fact produced by a Lustre compiler we are working on. I will try to produce a real MWE...
Running Frama-C and WP on the whole file causes a stack overflow on `List.map` but I reduce the error when proving the `Arrays1_Arrays1_node_step` function. I use the `ref` and the `real` memory model.
When launching Frama-C on the function, no goal is produced (at least there is no printing of it), only Frama-C is running (there is no process involving Alt-Ergo or Z3 for instance). the crash happens after 13 minutes (!) on my computer (a recent laptop with i9 cores).
### Steps to reproduce the issue
* open the attached archive
* issue the following command:
```
frama-c -wp -wp-model ref,real -wp-fct Arrays1_Arrays1_node_step Arrays1.c
```
### Contextual information
- Frama-C installation mode: opam with an OCaml 4.14.0 switch
- Frama-C version: 26.1 (Iron)
- Plug-in used: WP
- OS name: Linux
- OS version: 22.04
Thanks,
Christophe
[arrays_stack_overflow_wo_optimization.tgz](/uploads/e88a0fcabd4de811d59024517c679f5d/arrays_stack_overflow_wo_optimization.tgz)Loïc CorrensonLoïc Corrensonhttps://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/2648Frama-c-gui does not install on macOS Ventura2023-06-21T08:02:03ZNikolaus HuberFrama-c-gui does not install on macOS VenturaI have tried installing Frama-C through opam on macOS Ventura (13.0.1) for a few days now. I have followed the official installation instructions including the installation of all required tools with brew and setting PKG_CONFIG_PATH. Aft...I have tried installing Frama-C through opam on macOS Ventura (13.0.1) for a few days now. I have followed the official installation instructions including the installation of all required tools with brew and setting PKG_CONFIG_PATH. After issuing `opam install frama-c` Frama-C gets installed, however, whatever I tried frama-c-gui is never available.
When I try
```
opam uninstall frama-c
opam install frama-c.25.0
```
everything works perfectly. I have tried it both on an Intel and an M2 MacBookPro. Does anyone have a similar problem?Loïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2647Frama-C 26 crashes when trying CFG plugin from Frama-C plugin development guide2023-02-10T08:37:41ZChristophe GarionFrama-C 26 crashes when trying CFG plugin from Frama-C plugin development guideHello,
Frama-C 26.0 just crashed when I tried to reproduce the CFG plugin example from the Frama-C plugin development guide. Everything was OK until I tried to use the `bogue` library for the mini-GUI example. Executing Frama-C through ...Hello,
Frama-C 26.0 just crashed when I tried to reproduce the CFG plugin example from the Frama-C plugin development guide. Everything was OK until I tried to use the `bogue` library for the mini-GUI example. Executing Frama-C through dune leads to a crash:
```
Done: 0% (0/0, 0 left) (jobs: 0)[kernel] Current source was: :0
The full backtrace is:
Raised at Dune_site_plugins__Plugins.load_gen in file "otherlibs/site/src/plugins/plugins.ml", line 251, characters 6-89
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Dune_site_plugins__Plugins.load_gen in file "otherlibs/site/src/plugins/plugins.ml", line 255, characters 4-36
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Dune_site_plugins__Plugins.load_gen in file "otherlibs/site/src/plugins/plugins.ml", line 255, characters 4-36
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Dune_site_plugins__Plugins.load_gen in file "otherlibs/site/src/plugins/plugins.ml", line 255, characters 4-36
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Dune_site_plugins__Plugins.load_gen in file "otherlibs/site/src/plugins/plugins.ml", line 255, characters 4-36
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Frama_c_kernel__Kernel.bootstrap_loader in file "src/kernel_services/plugin_entry_points/kernel.ml", line 918, characters 35-62
Called from Frama_c_kernel__Cmdline.parse_and_boot in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 894, characters 2-22
Called from Frama_c_kernel__Cmdline.catch_toplevel_run in file "src/kernel_services/cmdline_parameters/cmdline.ml", line 233, characters 4-8
Unexpected error (It is not possible to dynamically link a plugin which uses the thread library
with an executable not already linked with the thread
library.).
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 26.0 (Iron).
```
### Steps to reproduce the issue
- install both Frama-C and bogue through Opam
- extract the attached archive containing the plugin source (see [view-cfg.tar.gz](/uploads/d9bad096f63e6a429bb7c7683789fa97/view-cfg.tar.gz))
- execute `dune build`
- execute Frama-C through dune with `dune exec -- frama-c`
### Contextual information
- Frama-C installation mode: Opam with an OCaml 4.14.1 switch
- Frama-C version: 26.0 (Iron)
- Plug-in used: "homemade" CFG plugin from the plugin development guide
- OS name: Linux
- OS version: Ubuntu 22.04
### Additional information
I looked through the bugtracker but did not find any related issue. I hope I did not make a stupid mistake by copying the code from the guide!Andre MaronezeAndre Maronezehttps://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/2645Installation in local OPAM switch with dune-project fails2023-02-14T09:11:20ZLélio BrunInstallation in local OPAM switch with dune-project 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.
-->
Create a local OPAM switch, create an empty `dune-project` file, install Frama-C (last version 26).
```
mkdir test
cd test
opam switch create . 4.14.1
eval (opam env)
touch dune-project
opam install frama-c
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Installation succeeds.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Installation fails:
```
[ERROR] The installation of frama-c failed at "make PREFIX=/home/lelio/Projects/test/_opam MANDIR= install".
#=== ERROR while installing frama-c.26.0 ======================================#
# context 2.1.4 | linux/x86_64 | ocaml-base-compiler.4.14.1 | https://opam.ocaml.org#34077df0
# path ~/Projects/test/_opam/.opam-switch/build/frama-c.26.0
# command ~/.opam/opam-init/hooks/sandbox.sh install make PREFIX=/home/lelio/Projects/test/_opam MANDIR= install
# exit-code 2
# env-file ~/.opam/log/frama-c-2744448-3e4244.env
# output-file ~/.opam/log/frama-c-2744448-3e4244.out
### output ###
# Installing Frama-C to current Opam switch
# (copying and relocating files...)
# make: *** [share/Makefile.installation:62: install] Error 1
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ ∗ install frama-c 26.0
└─
╶─ No changes have been performed
```
### Contextual information
- Frama-C installation mode: *local Opam switch with `dune-project` file*
- Frama-C version: *26.0*
- OS name: *Archlinux*
### Additional information (optional)
<!--
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->
I precise that the procedure works well for anterior versions (eg. 24, 25). It works also for version 26 if no `dune-project` file is present.
This is a minimal example, in my use case I didn't even have an error message, Frama-C was reported as successfully installed but the `frama-c` binary was actually not installed (in `_opam/bin/frama-c`).Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2644[WP] Fails to verify left shift by 2 on range2023-01-24T11:13:25ZCostava[WP] Fails to verify left shift by 2 on range<!--
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
/*@
requires a == 1;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_one(const unsigned int a) {
return (a << 2);
}
/*@
requires a == 2;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_two(const unsigned int a) {
return (a << 2);
}
/*@
requires 1 <= a <= 2;
assigns \nothing;
ensures \result == (a << 2);
*/
unsigned int do_some_shift2(const unsigned int a) {
return (a << 2);
}
/*@
requires 1 <= a <= 2;
assigns \nothing;
ensures \result == (a << 1);
*/
unsigned int do_some_shift1(const unsigned int a) {
return (a << 1);
}
```
```sh
$ frama-c -wp -wp-rte fcshift.c
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
All goals verified successfully.
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
```sh
$ frama-c -wp -wp-rte fcshift.c
[kernel] Parsing fcshift.c (with preprocessing)
[rte:annot] annotating function do_one
[rte:annot] annotating function do_some_shift1
[rte:annot] annotating function do_some_shift2
[rte:annot] annotating function do_two
[wp] 8 goals scheduled
[wp] [Alt-Ergo 2.4.1] Goal typed_do_some_shift2_ensures : Timeout (Qed:2ms) (10s)
[wp] Proved goals: 7 / 8
Qed: 6 (0.33ms-0.64ms-2ms)
Alt-Ergo 2.4.1: 1 (10ms) (92) (interrupted: 1)
```
The ensures goal can be verified when `a` has a single value of either `1` or `2` respectively for the `do_one` and `do_two` functions.
But if `a` is `1` or `2` (for function `do_some_shift2`), then the ensures goal fails to verify.
Oddly, the goal succeeds if the left shift is by `1` instead of `2` (function `do_some_shift1`).
[cppreference.com](https://en.cppreference.com/w/c/language/arithmetic_types) is stating that `unsigned int` should always have at least 16 bits, so it is weird to me that changing the amount of the shift is making a difference.
Doubling the timeout to 20 does not make the goal succeed automatically.
Using `frama-c-gui`, I know that I can apply tactic `Logical Shift` on `lsl(a, 2)` in order to make the goal succeed, but a goal that is this specific and simple failing to verify seems like a bug.
### 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.
-->
N/ALoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2643[WP] Isabelle/HOL driver does not work2024-02-27T11:34:19Zkwaxer[WP] Isabelle/HOL driver does not work### Steps to reproduce the issue
1. Make sure Isabelle/HOL is installed and `why3` is configured to use it.
2. Create file `test.h` with the following code:
```
/*@
logic \list<integer> enumeration (integer n) = n == 0 ? \Nil : enum...### Steps to reproduce the issue
1. Make sure Isabelle/HOL is installed and `why3` is configured to use it.
2. Create file `test.h` with the following code:
```
/*@
logic \list<integer> enumeration (integer n) = n == 0 ? \Nil : enumeration (n - 1) ^ [|n - 1|];
lemma enumeration_length: \forall integer n; 0 <= n ==> \length (enumeration (n)) == n;
*/
```
3. Run WP plugin selecting Isabelle/HOL as a backend: `frama-c -wp -wp-prover why3:isabelle test.h`
4. Observe the following output:
```
[wp] 1 goal scheduled
[wp] [Unknown] typed_lemma_enumeration_length (Isabelle)
[wp] Proved goals: 0 / 1
Qed: 0
Unknown: 1
```
5. Observe that no new files or directories are created.
### Expected behavior
Some generated files/directories that can be used to prove the goal in Isabelle/HOL.
### Actual behavior
Nothing is generated, and no errors are reported. The verification fails silently without any clue about what went wrong.
### Contextual information
- Frama-C: 26.0 (Iron) installed with `opam`
- Why3: 1.5.1 installed with `opam`
- Isabelle: 2021-1
- OS: Ubuntu 22.04.1 LTSLoïc CorrensonLoïc Corrensonhttps://git.frama-c.com/pub/frama-c/-/issues/2642Installing Frama-C with opam fails2023-03-12T22:26:44ZHugo GimbertInstalling Frama-C with opam failsHello,
several students of mine were struggling today to install frama-c on their Ubuntu.
Can someone provide some feedback on the following error.
Example on Ubuntu 20.04, standard installation.
```
sudo apt-get remove opam
rm -fr ~...Hello,
several students of mine were struggling today to install frama-c on their Ubuntu.
Can someone provide some feedback on the following error.
Example on Ubuntu 20.04, standard installation.
```
sudo apt-get remove opam
rm -fr ~/.opam
sudo apt-get install opam
opam init
eval $(opam env)
opam install frama-c
```
leads to the following error
```
#=== ERROR while compiling alt-ergo-lib.2.4.2 =================================#
# context 2.0.5 | linux/x86_64 | ocaml-system.4.08.1 | https://opam.ocaml.org#0cd336b3
# path ~/.opam/default/.opam-switch/build/alt-ergo-lib.2.4.2
# command ~/.opam/opam-init/hooks/sandbox.sh build dune build -p alt-ergo-lib -j 1
# exit-code 1
# env-file ~/.opam/log/alt-ergo-lib-66410-e6f851.env
# output-file ~/.opam/log/alt-ergo-lib-66410-e6f851.out
### output ###
# 639 | [@ocaml.ppwarning "TODO: detect when there are no changes "]
# [...]
# Warning 22: TODO: detect when there are no changes
# (cd _build/default && /usr/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -I src/lib/.AltErgoLib.objs/byte -I /home/yussef/.opam/default/lib/ocplib-simplex -I /home/yussef/.opam/default/lib/seq -I /home/yussef/.opam/default/lib/stdlib-shims -I /home/yussef/.opam/default/lib/zarith -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Parsed.cmi -c -intf src/lib/structur[...]
# File "src/lib/structures/parsed.mli", line 32, characters 17-24:
# 32 | | ConstReal of Num.num
# ^^^^^^^
# Error: Unbound module Num
# (cd _build/default && /usr/bin/ocamlc.opt -w -40 -bin-annot -g -bin-annot -I src/lib/.AltErgoLib.objs/byte -I /home/yussef/.opam/default/lib/ocplib-simplex -I /home/yussef/.opam/default/lib/seq -I /home/yussef/.opam/default/lib/stdlib-shims -I /home/yussef/.opam/default/lib/zarith -no-alias-deps -open AltErgoLib -o src/lib/.AltErgoLib.objs/byte/altErgoLib__Typed.cmi -c -intf src/lib/structure[...]
# File "src/lib/structures/typed.mli", line 58, characters 13-20:
# 58 | | Treal of Num.num (** Real constant. *)
# ^^^^^^^
# Error: Unbound module Num
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build alt-ergo-lib 2.4.2
└─
```Andre 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/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/2639Parse-print-reparse error with ranges2024-03-14T16:37:09ZNikolai KosmatovParse-print-reparse error with ranges## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 26.0beta
- MetAcsl 0.4beta
- Alt-Ergo 2.3.2
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, after pa...## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 26.0beta
- MetAcsl 0.4beta
- Alt-Ergo 2.3.2
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, after parsing and printing the code, running frama-c again to parse the code produces an error (due to missing parentheses in ranges).
[f.c](/uploads/dac68b95adf9d3c2c83b7b3ec9ce5898/f.c)
Here is the example
```
// Run frama-c on this file and pretty-print it:
// frama-c f.c -print -no-unicode -ocode f_printed.c
// Run on the resulting pretty-printed file:
// frama-c f_printed.c
typedef unsigned char uchar;
typedef unsigned long ulong;
typedef unsigned char *pchar;
uchar *Ref;
uchar Array[100];
/*@ ghost ulong FCG_Var1[1000]; */
/*@ ensures
sep1:
\let Ref_range = Ref + (0 .. (1 << (size)) - 1);
\let PROP = \forall integer MyNum;
\let myrange = (0 .. (6 - 1));
\let Var2 = &Array[FCG_Var1[MyNum]];
\let CASE_i = 0 <= MyNum < 10;
\let PROP_i =
\separated(Ref_range, Var2 + myrange);
CASE_i ==> PROP_i;
PROP;
*/
static uchar myfun(pchar p_array, short index, uchar size)
{
uchar __retres;
return __retres;
}
```
Here is the error message:
```
[kernel] Parsing f_printed.c (with preprocessing)
[kernel:annot-error] f_printed.c:11: Warning: unexpected token '..'
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "f_printed.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
```https://git.frama-c.com/pub/frama-c/-/issues/2638Parse-print-reparse error with ghost arrays2023-01-17T13:05:30ZNikolai KosmatovParse-print-reparse error with ghost arrays## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 26.0beta
- MetAcsl 0.4beta
- Alt-Ergo 2.3.2
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, after pa...## Contextual information: currently used versions
- Frama-C installation mode: *Opam*
- Frama-C version 26.0beta
- MetAcsl 0.4beta
- Alt-Ergo 2.3.2
- OS name: *Ubuntu*
- OS version: *20.04*
## The issue
On the attached file, after parsing and printing the code, running frama-c again to parse the code produces an error (that disappears after manually removing \ghost attribute).
[f_cut.c](/uploads/90f52009ec5f1412c371349b3fca3659/f_cut.c)
Here is the example
```
// Run frama-c on this file and pretty-print it:
// frama-c f_cut.c -print -no-unicode -ocode f_cut_printed.c
// Run on the resulting pretty-printed file:
// frama-c f_cut_printed.c
typedef unsigned char uint8;
typedef unsigned short uint16;
typedef unsigned long uint32;
uint8 Array[10];
/*@ ghost uint32 FCG_Number; */
/*@ ghost uint32 FCG_Var1[1000]; */
/*@ ghost uint32 FCG_Var2[1000]; */
/*@
predicate mypredl{L}=
(\forall integer MyNum;
0 <= MyNum < FCG_Number ==> FCG_Var2[MyNum] ==
((uint16)(*((uint8 *)(&Array[FCG_Var1[MyNum]] + (1))) * 256 + *((uint8 *)((&Array[FCG_Var1[MyNum]] + (1 + 2)) + 1)))) ) ;
*/
```
Here is the error message:
```
[kernel] Parsing f_cut_printed.c (with preprocessing)
[kernel:annot-error] f_cut_printed.c:14: Warning: unexpected token '\ghost'
[kernel] User Error: warning annot-error treated as fatal error.
[kernel] User Error: stopping on file "f_cut_printed.c" that has errors. Add '-kernel-msg-key pp'
for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
```https://git.frama-c.com/pub/frama-c/-/issues/2637libgnomecanvas disabled in brew2023-06-21T08:15:31ZLaura Titololibgnomecanvas disabled in brewTrying to install frama-c in a Mac machine, when executing
`brew libgnomecanvas`
an error occurs since the library is currently disabled.
The libgnomecanvas repository seems archived since November 29, 2022 (https://formulae.brew.sh/for...Trying to install frama-c in a Mac machine, when executing
`brew libgnomecanvas`
an error occurs since the library is currently disabled.
The libgnomecanvas repository seems archived since November 29, 2022 (https://formulae.brew.sh/formula/libgnomecanvas. https://gitlab.gnome.org/Archive/libgnomecanvas).https://git.frama-c.com/pub/frama-c/-/issues/2636[WP] Builtin \sign(float64) is not defined2022-12-14T12:36:37ZNiksonber[WP] Builtin \sign(float64) is not defined<!--
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
Built-in \\sign is not defined in WP.
`Builtin \sign(float64) not defined`
`[wp] Failure: Logic type 'sign' undefined`
<!--
Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
-->
### Steps To Reproduce
Run: `frama-c -wp -wp-out . -wp-prover coq -wp-model +float -wp-interactive update just_sign.c`
Where `just_sign.c` is:
```
#include <math.h>
/*@
predicate is_same_sign(double X, double Y) = \sign(X) == \sign(Y);
*/
/*@
ensures (is_same_sign(a_double, \result)) ;
assigns \nothing;
*/
double dummy (double a_double) {
return a_double;
}
```
I got the following output:
```
[wp] Warning: Missing RTE guards
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
[wp] 2 goals scheduled
[wp] Failure: Logic type 'sign' undefined
```
### Expected behaviour
Expected a definition for \sign.
<!--
Please explain here what is the expected behaviour.
-->
### Actual behaviour
WP reports:
```
[wp] Failure: Logic type 'sign' undefined
[wp] just_sign.c:4: Warning: Builtin \sign(float64) not defined
```
<!--
Please explain here what is the actual (faulty) behaviour.
-->
### Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 24.0, 25.0 (Manganese), 26.0+dev (Iron) (I tried Several versions)
- Plug-in used: WP
- OS name: Ubuntu
- OS version: 22.04 LTS
<!--
### Additional information (optional)
You may add here any information deemed relevant with regard to this issue,
and tell us if you already tried some workarounds or have some ideas to solve this issue.
-->Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2635e_acsl_assert is not getting added for all given asserts2022-11-09T10:25:29Zamruthabennye_acsl_assert is not getting added for all given assertsI am new to Frama-C. I specifically need to use e-acsl plugin for verification purposes. I used first.i file as
```
int main(void) {
int x = 0;
/∗@ assert x == 0; ∗/
/∗@ assert x == 1; ∗/
return 0;
}
```
Created monitored_first.c ...I am new to Frama-C. I specifically need to use e-acsl plugin for verification purposes. I used first.i file as
```
int main(void) {
int x = 0;
/∗@ assert x == 0; ∗/
/∗@ assert x == 1; ∗/
return 0;
}
```
Created monitored_first.c file from first.i file using the following command.
`$ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.c`
The main function inside the monitored_first.c looks like the one below.
```
int main(void)
{
int __retres;
__e_acsl_memory_init((int *)0,(char ***)0,8UL);
int x = 0;
__retres = 0;
__e_acsl_memory_clean();
return __retres;
}
```
It is not adding e_acsl assertion for x==1.
I tried it using the "e-acsl-gcc.sh" script , which generated the monitored_first.i file. But the main function inside monitored_first.i is same as that in monitored_first.c.
`$ e-acsl-gcc.sh -c -omonitored_first.i first.i`
The above command generated two executable, "a.out.e-acsl" and "a.out". It also generates some warnings when run in ubuntu 22.04 as follows:
```
/home/amrutha/.opam/4.11.1/bin/frama-c -remove-unused-specified-functions -machdep gcc_x86_64 '-cpp-extra-args= -std=c99 -D_DEFAULT_SOURCE -D__NO_CTYPE -D__FC_MACHDEP_X86_64 ' -no-frama-c-stdlib first.i -e-acsl -e-acsl-share=/home/amrutha/.opam/4.11.1/bin/../share/frama-c/e-acsl -then-last -print -ocode monitored_first.i
[kernel] Parsing first.i (no preprocessing)
[e-acsl] beginning translation.
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
/tmp/ppannot15ad34.c:362: warning: "__STDC_IEC_60559_BFP__" redefined
362 | #define __STDC_IEC_60559_BFP__ 201404L
|
In file included from <command-line>:
/usr/include/stdc-predef.h:39: note: this is the location of the previous definition
39 | # define __STDC_IEC_60559_BFP__ 201404L
|
/tmp/ppannot15ad34.c:363: warning: "__STDC_IEC_60559_COMPLEX__" redefined
363 | #define __STDC_IEC_60559_COMPLEX__ 201404L
|
In file included from <command-line>:
/usr/include/stdc-predef.h:49: note: this is the location of the previous definition
49 | # define __STDC_IEC_60559_COMPLEX__ 201404L
|
[e-acsl] translation done in project "e-acsl".
+ gcc -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body first.i -o a.out
+ gcc -DE_ACSL_SEGMENT_MMODEL -std=c99 -m64 -g -O2 -fno-builtin -fno-merge-constants -Wall -Wno-long-long -Wno-attributes -Wno-nonnull -Wno-undef -Wno-unused -Wno-unused-function -Wno-unused-result -Wno-unused-value -Wno-unused-function -Wno-unused-variable -Wno-unused-but-set-variable -Wno-implicit-function-declaration -Wno-empty-body -I/home/amrutha/.opam/4.11.1/bin/../share/frama-c/e-acsl -o a.out.e-acsl monitored_first.i /home/amrutha/.opam/4.11.1/bin/../share/frama-c/e-acsl/e_acsl_rtl.c /home/amrutha/.opam/4.11.1/bin/../lib/frama-c/e-acsl/libeacsl-dlmalloc.a -lgmp -lm
```
In ubuntu 20.04 there is no any warning, only the end part is getting displayed. When run ./a.out.e-acsl , it simply run the code without any message, which is not supposed. The expected output should look like this:
```
$ ./a.out.e-acsl
first.i: In function 'main'
first.i:4: Error: Assertion failed:
The failing predicate is:
x == 1.
Aborted (core dumped)
$ echo $?
134
```
I tried it in ubuntu 22.04 with opam version 2.1.2 and Fragma-C 25.0
and ubuntu 20.04 with opam version 2.0.5 and Fragma-C 25.0https://git.frama-c.com/pub/frama-c/-/issues/2634Installing Frama-C-25.0 with opam fails on Pango interface conflict2022-12-02T09:03:09ZWolfram KahlInstalling Frama-C-25.0 with opam fails on Pango interface conflict<!--
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.
-->
```
opam update # 2022-10-28, created new switch for OCaml-4.14.0
opam reinstall conf-gtk3 conf-cairo conf-pango ocamlgraph ocamlgraph_gtk lablgtk3 frama-c # any number of times
```
### Expected behaviour
<!--
Please explain here what is the expected behaviour.
-->
Successful install of frama-c
### Actual behaviour
<!--
Please explain here what is the actual (faulty) behaviour.
-->
Everything else (re-)installs successfully, but frama-c fails with:
```
# File "src/plugins/gui/dgraph_helper.ml", line 1:
# Error: The files /home/kahl/.opam/default/lib/lablgtk3/gWindow.cmi
# and /home/kahl/.opam/default/lib/ocamlgraph_gtk/graph_gtk__DGraphContainer.cmi
# make inconsistent assumptions over interface Pango
<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build frama-c 25.0
└─
┌─ The following changes have been performed
│ ↻ recompile altgr-ergo 2.4.2
│ ↻ recompile cairo2 0.6.4
│ ↻ recompile conf-cairo 1
│ ↻ recompile conf-gtk3 18
│ ↻ recompile conf-pango 1
│ ↻ recompile lablgtk3 3.1.3
│ ↻ recompile lablgtk3-sourceview3 3.1.3
│ ↻ recompile ocamlgraph 2.0.0
│ ↻ recompile ocamlgraph_gtk 2.0.0
│ ↻ recompile why3 1.5.1
└─
```
### Contextual information
- Frama-C installation mode: opam
- Frama-C version: 25.0
- Plug-in used: *Plug-in used*
- OS name: linux
- OS version: Ubuntu 20.04.5 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.
-->
After the first attempt, I noticed that conf-pango had not even been pulled in automatically.Allan BlanchardAllan Blanchardhttps://git.frama-c.com/pub/frama-c/-/issues/2633Issue while installing Frama-c 25.0.02023-05-15T09:02:22ZOussamaH92Issue while installing Frama-c 25.0.0Hello everyone,
I'm a French student wanting to start using Frama-C.
When I was installing it following the step in Frama-C's website I get this error message after using
`opam install frama-c`
I was stuck with this error : `[ERROR]...Hello everyone,
I'm a French student wanting to start using Frama-C.
When I was installing it following the step in Frama-C's website I get this error message after using
`opam install frama-c`
I was stuck with this error : `[ERROR] The compilation of frama-c.25.0 failed at "make -j7".`
`
Error: Unbound module Cil_typesFile "src/plugins/aorai/promelaoutput.ml", line 26, characters 5-14:
26 | open Cil_types
^^^^^^^^^
Error: Unbound module Cil_types`
I've updated my GNU make version just before the install process with the command `brew install homebrew/core/make`
I hope someone can explain me how to get rid of this problem.
Thanks