// frama-c-gui -eva pointeurs_eva.c
#include <stdlib.h>
#include <assert.h>

int *q;

/*@assigns \result \from \nothing;*/
extern int *input();

int main() {
  int *p;
  p = input();
  if (p != NULL) {
    q = p;
    *p = 42;
    assert(*q == 42); // <- validé par EVA
    free(p);
    *q = 7; // <- UAF signalé par EVA
  }
  return 0;
}