/* Commandline execution:
 *		civl verify pointersBad.cvl
 * */
#include<civlc.cvh>
#include<stdlib.h>

$output int out;
$input int x;
$input int *x_ptr;
void main() {
  int a;
  int* b, *c;
  int * nilPtr = NULL;

  c = (void *)(-1);
  b = (int *)malloc(sizeof(int));
  free(b);
  a = *(&out);
  $choose {
    $when(x == 2) {a = *x_ptr;}
    $when(x == 1) {c = &a + 1; a = *c;}
    $when(x == 0) {a = *c;}
    $when(x >=3 ) {a = *b;}
    $when(x < 0 ) {a = *nilPtr;}
  }
}