Commit 75d5210e authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Removing a few misplaced usage of `syntax converter`

parent 2c43796b
...@@ -10,9 +10,8 @@ module ref.Ref ...@@ -10,9 +10,8 @@ module ref.Ref
syntax type ref "%1" syntax type ref "%1"
syntax val ref "%1" syntax val ref "%1"
syntax val (!_) "%1" syntax val (!_) "%1"
syntax converter (!_) "%1"
syntax val (:=) "%1 = %2" syntax val (:=) "%1 = %2"
syntax converter contents "%1" syntax val contents "%1"
end end
module mach.int.Unsigned module mach.int.Unsigned
...@@ -23,7 +22,6 @@ end ...@@ -23,7 +22,6 @@ end
module mach.int.Int32 module mach.int.Int32
syntax val of_int "%1" syntax val of_int "%1"
syntax converter of_int "%1"
syntax type int32 "int32_t" syntax type int32 "int32_t"
...@@ -44,8 +42,8 @@ module mach.int.UInt32Gen ...@@ -44,8 +42,8 @@ module mach.int.UInt32Gen
syntax type uint32 "uint32_t" syntax type uint32 "uint32_t"
syntax converter max_uint32 "0xffffffff" syntax val max_uint32 "0xffffffff"
syntax converter length "32" syntax val length "32"
end end
...@@ -223,7 +221,6 @@ end ...@@ -223,7 +221,6 @@ end
module mach.int.Int64 module mach.int.Int64
syntax val of_int "%1" syntax val of_int "%1"
syntax converter of_int "%1"
syntax type int64 "int64_t" syntax type int64 "int64_t"
...@@ -244,8 +241,8 @@ module mach.int.UInt64Gen ...@@ -244,8 +241,8 @@ module mach.int.UInt64Gen
syntax type uint64 "uint64_t" syntax type uint64 "uint64_t"
syntax converter max_uint64 "0xffffffffffffffff" syntax val max_uint64 "0xffffffffffffffff"
syntax converter length "64" syntax val length "64"
end end
......
...@@ -386,10 +386,12 @@ module Int63 ...@@ -386,10 +386,12 @@ module Int63
lemma to_int_in_bounds, lemma to_int_in_bounds,
lemma extensionality lemma extensionality
let constant zero = of_int 0 let constant zero = (0:int63)
let constant one = of_int 1 let constant one = (1:int63)
let constant max_int = of_int max_int63 val constant max_int:int63
let constant min_int = of_int min_int63 ensures { int63'int result = max_int63)
val constant min_int:int63
ensures { int63'int result = min_int63
(* use bv.BV63 as BV63 (* use bv.BV63 as BV63
...@@ -409,11 +411,11 @@ module Refint63 ...@@ -409,11 +411,11 @@ module Refint63
let incr (r: ref int63) : unit let incr (r: ref int63) : unit
requires { [@expl:integer overflow] to_int !r < max_int63 } requires { [@expl:integer overflow] to_int !r < max_int63 }
ensures { to_int !r = to_int (old !r) + 1 } ensures { to_int !r = to_int (old !r) + 1 }
= r := !r + of_int 1 = r := !r + (1:int63)
let decr (r: ref int63) : unit let decr (r: ref int63) : unit
requires { [@expl:integer overflow] min_int63 < to_int !r } requires { [@expl:integer overflow] min_int63 < to_int !r }
ensures { to_int !r = to_int (old !r) - 1 } ensures { to_int !r = to_int (old !r) - 1 }
= r := !r - of_int 1 = r := !r - (1:int63)
let (+=) (r: ref int63) (v: int63) : unit let (+=) (r: ref int63) (v: int63) : unit
requires { [@expl:integer overflow] in_bounds (to_int !r + to_int v) } requires { [@expl:integer overflow] in_bounds (to_int !r + to_int v) }
......
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