--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on February 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] WP and Allocations



I'm using Frama-C 20.0, alt-ergo 2.3.0, why3 1.2.1.

Is there any reasonable way to deal with dynamic allocation with
ACSL and WP? Here's a small sample program:

> #include <stdlib.h>
>
> int
> main(void)
> {
>         char *p = malloc(10);
>         if (!p)
>                 return 1;
>         //@ assert \valid(p);
>         return 0;
> }

When I run `frama-c -wp [filename]`, none of the provers are able to
prove the assertion, while running `frama-c -eva [filename]` says
that it's valid.