From b40e056328e183522b50c68aefdbff057bca29cc Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 16 Jun 2013 06:56:02 +0000 Subject: Merge of the "princeton" branch: - Define type "block" as "positive" instead of "Z". - Strengthen mem_unchanged_on so that the permissions are identical, instead of possibly increasing. - Move mem_unchanged_on from Events to Memory.Mem. - Define it in terms of mem_contents rather than in terms of Mem.load. - ExportClight: try to name temporaries introduced by SimplExpr - SimplExpr: avoid reusing temporaries between different functions, instead, thread a single generator through all functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Interp.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'driver') diff --git a/driver/Interp.ml b/driver/Interp.ml index 662baa2..6f9336e 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -155,7 +155,7 @@ let compare_mem m1 m2 = (* Comparing continuations *) -let some_expr = Eval(Vptr(Mem.nullptr, Int.zero), Tvoid) +let some_expr = Eval(Vint Int.zero, Tvoid) let rank_cont = function | Kstop -> 0 @@ -234,7 +234,7 @@ let mem_state = function let compare_state s1 s2 = if s1 == s2 then 0 else - let c = Z.compare (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock in + let c = P.compare (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock in if c <> 0 then c else begin match s1, s2 with | State(f1,s1,k1,e1,m1), State(f2,s2,k2,e2,m2) -> @@ -275,7 +275,7 @@ let rec purge_seen nextblock seen = match min with | None -> seen | Some((s, w) as sw) -> - if Z.le (mem_state s).Mem.nextblock nextblock + if P.le (mem_state s).Mem.nextblock nextblock then purge_seen nextblock (StateSet.remove sw seen) else seen @@ -514,7 +514,7 @@ module PrioQueue = struct let singleton elt = Node(elt, Empty, Empty) let higher_prio (time1, (s1, w1)) (time2, (s2, w2)) = - Z.lt (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock + P.lt (mem_state s1).Mem.nextblock (mem_state s2).Mem.nextblock let rec insert queue elt = match queue with -- cgit v1.2.3