From 7ead22b0a04fbea3fb0ef99ba3528460f0d6bd67 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 12 Mar 2020 19:31:42 +0100 Subject: CSE3 analysis --- backend/CSE3analysis.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'backend/CSE3analysis.v') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 43c44ccd..76723f40 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -331,16 +331,16 @@ Definition apply_instr' (tenv : typing_env) code (pc : node) (ro : RB.t) : RB.t Definition invariants := PMap.t RB.t. -Definition rel_le (x y : RELATION.t) : bool := (PSet.is_subset y x). +Definition rel_leb (x y : RELATION.t) : bool := (PSet.is_subset y x). -Definition relb_le (x y : RB.t) : bool := +Definition relb_leb (x y : RB.t) : bool := match x, y with | None, _ => true | (Some _), None => false - | (Some x), (Some y) => rel_le x y + | (Some x), (Some y) => rel_leb x y end. -Definition check_inductiveness (tenv: typing_env) (inv: invariants) (fn : RTL.function) := +Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: invariants) := (RB.beq (Some RELATION.top) (PMap.get (fn_entrypoint fn) inv)) && PTree_Properties.for_all (fn_code fn) (fun pc instr => @@ -349,7 +349,7 @@ Definition check_inductiveness (tenv: typing_env) (inv: invariants) (fn : RTL.fu | Some rel => let rel' := apply_instr pc tenv instr rel in List.forallb - (fun pc' => relb_le rel' (PMap.get pc' inv)) + (fun pc' => relb_leb rel' (PMap.get pc' inv)) (RTL.successors_instr instr) end). -- cgit