}
/*@out@*/ void *dimalloc (size_t size, const char *name, int line)
+ /*@ensures maxSet(result) == (size - 1); @*/
{
/*
static void *lastaddr = 0;
}
extern
-char *mstring_copy (char *s1)
+char *mstring_copy (char *s1) /*@ensures maxRead(result) == maxRead(s1) /\ maxSet(result) == maxSet(s1) @*/
{
if (s1 == NULL)
{
check (fputc ('\n', out) == (int) '\n');
}
-unsigned int int_toNonNegative (int x)
+unsigned int int_toNonNegative (int x) /*@*/
{
llassert (x >= 0);
return (unsigned) x;
return (long unsigned) x;
}
-size_t size_fromInt (int x)
+size_t size_fromInt (int x) /*@ensures result==x@*/
{
size_t res = (size_t) x;