generalized_check.i

/* run.config
OPT: -wp-fct f,main -wp -wp-prover qed -wp-msg-key strategy,no-time-info -print
*/
/*@ check lemma easy_proof: \false; */ // should not be put in any environment

/*@ check requires f_valid_x: \valid(x);
    assigns *x;
    check ensures f_init_x: *x == 0;
*/
void f(int* x) {
  /*@ check f_valid_ko: \valid(x); */
  *x = 0;
}

int main() {
  int a = 4;
  volatile int c;
  int* p = (void*)0;
  if (c) p = &a;
  f(p);
  /*@ check main_valid_ko: \valid(p); */
  /*@ check main_p_content_ko: *p == 0; */
}

void loop () {
  /*@ check loop invariant \true; */
  for (int i = 0; i< 10; i++);
  int j = 0;
 l: /*@ check invariant \true; */ ;
  if (j >= 10) goto l1;
  j++;
  goto l;
 l1 : ;
}