test/simplebufferConstraintTests/m.c

   1 extern /*@null@*/ /*@out@*/ /*@only@*/ void *mymalloc (size_t size) /*@*/
   2      /*@ensuresConstraint MaxSet(result) == (size - 1); @*/ ;
   3
   4 void t()
   5 {
   6 char *f;
   7
   8 f = mymalloc (3);
   9 f[2] = '2';
  10 free (f);
  11 }