--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on February 2020 ---
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.