language-ats-1.7.10.0: test/data/str.out
abst@ype strlen(n: int) viewdef string_v(n: int, l: addr) = strlen(n) @ l vtypedef string_vt(n: int, l: addr) = (string_v(n, l) | ptr(l)) vtypedef String_vt = [n:nat][ l : addr | l > null ] string_vt(n, l)
abst@ype strlen(n: int) viewdef string_v(n: int, l: addr) = strlen(n) @ l vtypedef string_vt(n: int, l: addr) = (string_v(n, l) | ptr(l)) vtypedef String_vt = [n:nat][ l : addr | l > null ] string_vt(n, l)