From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Tue, 20 Oct 2015 13:32:18 +0200
Subject: Updated PR by removing whitespaces. Bug 17450.

---
 common/Memtype.v | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'common/Memtype.v')

diff --git a/common/Memtype.v b/common/Memtype.v
index 43fc708f..5dbb66dc 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -376,7 +376,7 @@ Axiom loadbytes_split:
   loadbytes m b ofs (n1 + n2) = Some bytes ->
   n1 >= 0 -> n2 >= 0 ->
   exists bytes1, exists bytes2,
-     loadbytes m b ofs n1 = Some bytes1 
+     loadbytes m b ofs n1 = Some bytes1
   /\ loadbytes m b (ofs + n1) n2 = Some bytes2
   /\ bytes = bytes1 ++ bytes2.
 
@@ -636,7 +636,7 @@ Axiom perm_alloc_4:
   forall b' ofs k p, perm m2 b' ofs k p -> b' <> b -> perm m1 b' ofs k p.
 Axiom perm_alloc_inv:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
-  forall b' ofs k p, 
+  forall b' ofs k p,
   perm m2 b' ofs k p ->
   if eq_block b' b then lo <= ofs < hi else perm m1 b' ofs k p.
 
@@ -729,7 +729,7 @@ Axiom perm_free_3:
 Axiom valid_access_free_1:
   forall m1 bf lo hi m2, free m1 bf lo hi = Some m2 ->
   forall chunk b ofs p,
-  valid_access m1 chunk b ofs p -> 
+  valid_access m1 chunk b ofs p ->
   b <> bf \/ lo >= hi \/ ofs + size_chunk chunk <= lo \/ hi <= ofs ->
   valid_access m2 chunk b ofs p.
 Axiom valid_access_free_2:
@@ -790,7 +790,7 @@ Axiom perm_drop_4:
 
 Axiom load_drop:
   forall m b lo hi p m', drop_perm m b lo hi p = Some m' ->
-  forall chunk b' ofs, 
+  forall chunk b' ofs,
   b' <> b \/ ofs + size_chunk chunk <= lo \/ hi <= ofs \/ perm_order p Readable ->
   load chunk m' b' ofs = load chunk m b' ofs.
 
@@ -928,10 +928,10 @@ Axiom weak_valid_pointer_extends:
   a sub-block at offset [ofs] of the block [b'] in [m2].
 
 A memory injection [f] defines a relation [Val.inject] between values
-that is the identity for integer and float values, and relocates pointer 
+that is the identity for integer and float values, and relocates pointer
 values as prescribed by [f].  (See module [Values].)
 
-Likewise, a memory injection [f] defines a relation between memory states 
+Likewise, a memory injection [f] defines a relation between memory states
 that we now axiomatize. *)
 
 Parameter inject: meminj -> mem -> mem -> Prop.
@@ -1146,7 +1146,7 @@ Axiom alloc_left_mapped_inject:
   (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) ->
   inj_offset_aligned delta (hi-lo) ->
   (forall b delta' ofs k p,
-   f b = Some (b2, delta') -> 
+   f b = Some (b2, delta') ->
    perm m1 b ofs k p ->
    lo + delta <= ofs + delta' < hi + delta -> False) ->
   exists f',
@@ -1188,8 +1188,8 @@ Axiom free_parallel_inject:
 
 Axiom drop_outside_inject:
   forall f m1 m2 b lo hi p m2',
-  inject f m1 m2 -> 
-  drop_perm m2 b lo hi p = Some m2' -> 
+  inject f m1 m2 ->
+  drop_perm m2 b lo hi p = Some m2' ->
   (forall b' delta ofs k p,
     f b' = Some(b, delta) ->
     perm m1 b' ofs k p -> lo <= ofs + delta < hi -> False) ->
-- 
cgit