diff options
| author | Kathy Gray | 2014-11-19 14:06:00 +0000 |
|---|---|---|
| committer | Kathy Gray | 2014-11-19 14:06:00 +0000 |
| commit | c34462722ec2b17353784cd4e7caa42ac5dddf04 (patch) | |
| tree | 512a7b3316372625f7a5dbce82f461cc22dc34ce /src/lem_interp | |
| parent | 33a6b4216a5cfba56e2c17eddb8f4242d1317a6f (diff) | |
add value compare functions
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 5c77e807..91ef3d7f 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -32,7 +32,7 @@ type value = | Unknown (*To add: an abstract value representing an unknown but named memory address?*) -instance (Ord value) +instance (Ord bool) let compare = defaultCompare let (<) = defaultLess let (<=) = defaultLessEq @@ -40,6 +40,25 @@ instance (Ord value) let (>=) = defaultGreaterEq end +let valueCompare v1 v2 = + match (v1,v2) with + | (Bitvector bits1 inc1 start1, Bitvector bits2 inc2 start2) -> + tripleCompare compare compare compare (bits1,inc1,start1) (bits2,inc2,start2) + | (Bytevector words1, Bytevector words2) -> compare words1 words2 + | (Unknown,Unknown) -> EQ + | (Bitvector _ _ _, _) -> LT + | (Bytevector _, _) -> LT + | (_, _) -> GT + end + +instance (Ord value) + let compare = valueCompare + let (<) v1 v2 = (valueCompare v1 v2) = LT + let (<=) v1 v2 = (valueCompare v1 v2) <> GT + let (>) v1 v2 = (valueCompare v1 v2) = GT + let (>=) v1 v2 = (valueCompare v1 v2) <> LT +end + type slice = (integer * integer) |