stdlib: added a function length in mach.c.String

parent 3ae7cf75
......@@ -501,6 +501,7 @@ module mach.c.String
syntax val big_z "'Z'" prec 0
syntax val minus_char "'-'" prec 0
syntax val code "%1" prec 0
syntax val length "strlen"
syntax val strlen "strlen"
syntax val (=) "%1 == %2" prec 7 7 6
......
......@@ -317,6 +317,9 @@ module String [@W:non_conservative_extension:N]
use mach.int.UInt32
val length (s: string) : uint32
ensures { result = String.length s }
val strlen (p: ptr char) : uint32
requires { valid_string p }
ensures { result = strlen (pelts p) (offset p) }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment