/* This file gives prototypes and specifications for three functions:
	strcpy, strcmp, and strlen
*/

/*
spec strcpy(cpTo, cpFrom)
{
  requires $valid(cpTo):
		"the first argument must be a valid pointer"
  requires $string(cpFrom):
		"the second argument must be a valid string"
  requires $length(cpTo) > $string_length(cpFrom):
          	 "the array must be large enough to hold the entire string"

  modifies $elems(cpTo)

  ensures forall(i) ((i >= 0 && i <= $string_length(cpFrom)) implies
                     $final(cpTo[i]) == cpFrom[i])

  // next item is true but not necessary for the spec
  //ensures $string_length(cpTo) == $string_length(cpFrom)
}
*/
void strcpy(char* cpTo, char* cpFrom);


/*
spec strcmp(str1, str2)
{
  requires $string(str1): "the first argument must be a string"
  requires $string(str2): "the second argument must be a string"

  // if return is greater than zero, str1 is greater than str2
  ensures ($return > 0) iff
            ((str1[$return - 1] > str2[$return - 1]) &&
             forall (i) ((i >= 0 && i < $return - 1) implies
                         (str1[i] == str2[i])))

  // if return is less than zero, str1 is less than str2
  ensures ($return < 0) iff
            ((str1[$abs($return) - 1] < str2[$abs($return) - 1]) &&
             forall (i) ((i >= 0 && i < $abs($return) - 1) implies
                         (str1[i] == str2[i])))

  // if return is zero, the strings match all the way through the
  // terminating zero.
  ensures ($return == 0) iff
          forall (i) ((i >= 0 && i <= $string_length(str1)) implies
                      (str1[i] == str2[i]))

  // the return value must be within the length of the strings
  // (do we really need these?  I doubt it, but it doesn't hurt.)
  ensures $abs($return) <= $string_length(str1)
  ensures $abs($return) <= $string_length(str2)
}
*/
int strcmp(char* str1, char* str2);


/*
spec strlen(str1)
{
  requires $string(str1): "arg must be a valid string"
  ensures  $return == $string_length(str1)
}
*/
int strlen(char* str1);