|
typedef _Bool bool;
|
|
|
|
enum {
|
|
false = 0,
|
|
true = 1
|
|
};
|
|
|
|
/*@ axiomatic Un_Space {
|
|
logic char unescape_space (integer ch);
|
|
axiom N: unescape_space ('n') == '\n';
|
|
axiom R: unescape_space ('r') == '\r';
|
|
axiom T: unescape_space ('t') == '\t';
|
|
axiom V: unescape_space ('v') == '\v';
|
|
axiom F: unescape_space ('f') == '\f';
|
|
}
|
|
*/
|
|
|
|
/*@
|
|
requires \valid (src) && \valid (dst) &&
|
|
\valid (*src) && \valid(*dst);
|
|
assigns (**dst), *src, *dst;
|
|
|
|
behavior is_space:
|
|
assumes (**src) == 'n' || (**src) == 't' ||
|
|
(**src) == 'r' || (**src) == 'v' ||
|
|
(**src) == 'f';
|
|
ensures \result == true;
|
|
ensures *dst == \old(*dst + 1);
|
|
ensures *src == \old(*src + 1);
|
|
ensures (*(*dst - 1)) == unescape_space(*(*src - 1));
|
|
|
|
behavior fail:
|
|
assumes (**src) != 'n' && (**src) != 't' &&
|
|
(**src) != 'r' && (**src) != 'v' &&
|
|
(**src) != 'f';
|
|
ensures \result == false;
|
|
complete behaviors;
|
|
disjoint behaviors;
|
|
*/
|
|
|
|
static bool unescape_space(char **src, char **dst)
|
|
{
|
|
char *p = *dst, *q = *src;
|
|
|
|
switch (*q) {
|
|
case 'n':
|
|
*p = '\n';
|
|
break;
|
|
case 'r':
|
|
*p = '\r';
|
|
break;
|
|
case 't':
|
|
*p = '\t';
|
|
break;
|
|
case 'v':
|
|
*p = '\v';
|
|
break;
|
|
case 'f':
|
|
*p = '\f';
|
|
break;
|
|
default:
|
|
return false;
|
|
}
|
|
*dst += 1;
|
|
*src += 1;
|
|
return true;
|
|
}
|
|
|
|
/*@ axiomatic Un_Special {
|
|
logic char unescape_special (char ch);
|
|
axiom S: unescape_special ('\"') == '\"';
|
|
axiom SS: unescape_special ('\\') == '\\';
|
|
axiom E: unescape_special ('e') == '\e';
|
|
axiom A: unescape_special ('a') == '\a';
|
|
}
|
|
*/
|
|
|
|
/*@ predicate is_special(integer c) = (c == '\"' || c == '\\'
|
|
|| c == 'e' || c == 'a'); */
|
|
|
|
/*@
|
|
requires \valid (src) && \valid (dst) &&
|
|
\valid (*src) && \valid(*dst);
|
|
assigns (**dst), *dst, *src;
|
|
|
|
behavior is_special:
|
|
assumes (**src) == '\"' || (**src) == '\\' ||
|
|
(**src) == 'e' || (**src) == 'a';
|
|
ensures \result == true;
|
|
ensures *dst == \old(*dst + 1);
|
|
ensures *src == \old(*src + 1);
|
|
ensures (*(*dst - 1)) == unescape_special(*(*src - 1));
|
|
|
|
behavior fail:
|
|
assumes (**src) != '\"' && (**src) != '\\' &&
|
|
(**src) != 'e' && (**src) != 'a'; // '\e' !!
|
|
ensures \result == false;
|
|
complete behaviors;
|
|
disjoint behaviors;
|
|
*/
|
|
|
|
static bool unescape_special(char **src, char **dst)
|
|
{
|
|
char *p = *dst, *q = *src;
|
|
|
|
switch (*q) {
|
|
case '\"':
|
|
*p = '\"';
|
|
break;
|
|
case '\\':
|
|
*p = '\\';
|
|
break;
|
|
case 'a':
|
|
*p = '\a';
|
|
break;
|
|
case 'e':
|
|
*p = '\e';
|
|
break;
|
|
default:
|
|
return false;
|
|
}
|
|
*dst += 1;
|
|
*src += 1;
|
|
return true;
|
|
}
|