Changeset 1311 for Deliverables/D3.3/id-lookup-branch/ASM

Timestamp:

Oct 6, 2011, 6:45:54 PM (8 years ago)

Author:

campbell

Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

Location:

Deliverables/D3.3/id-lookup-branch

Files:

• . (modified) (1 prop)
• ASM (modified) (1 prop)
• ASM/Arithmetic.ma (modified) (1 diff)
• ASM/Util.ma (modified) (1 diff)

Deliverables/D3.3/id-lookup-branch/ASM/Arithmetic.ma

@@ -319 +319 @@
 alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop".
 
+definition max_u ≝ λn,a,b. if lt_u n a b then b else a.
+definition min_u ≝ λn,a,b. if lt_u n a b then a else b.
+definition max_s ≝ λn,a,b. if lt_s n a b then b else a.
+definition min_s ≝ λn,a,b. if lt_s n a b then a else b.
+
 definition bitvector_of_bool:
       ∀n: nat. ∀b: bool. BitVector (S n) ≝

Deliverables/D3.3/id-lookup-branch/ASM/Util.ma

@@ -40 +40 @@
 definition gtb ≝
   λm, n: nat.
-    leb n m.
+    ltb n m.
 
 (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)