test/simplebufferConstraintTests/sizeof.c

   1
   2 extern void /*@alt char * @*/
   3   mystrncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2,
   4 size_t n)
   5   /*@modifies *s1@*/      /*@requires MaxSet(s1) >= ( n - 1) /\ MaxRead (s2) >= ( n - 1 ); @*/ /*@ensures MaxRead (s1) ==
   6 MaxRead (s2) /\ MaxRead (s1) <= n; @*/;
   7
   8
   9  void f(char *z) /*@requires MaxRead(z) >= 2; @*/
  10 {
  11 char x[3];
  12 char y[3];
  13
  14 mystrncpy (x, z, 3);
  15 mystrncpy (y, z, 3);
  16
  17 x[(sizeof x)] = 'i';
  18 y[((sizeof y) - 1)] = '0';
  19
  20 }