//@ ensures *p >= 0 void abs1(int *p) { if (*p < 0) *p = -*p; } /*@ requires \valid(p) @ ensures *p >= 0 @*/ void abs2(int *p) { if (*p < 0) *p = -*p; }
//@ ensures *p >= 0 void abs1(int *p) { if (*p < 0) *p = -*p; } /*@ requires \valid(p) @ ensures *p >= 0 @*/ void abs2(int *p) { if (*p < 0) *p = -*p; }