diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-12 19:31:42 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-12 19:31:42 +0100 |
| commit | 7ead22b0a04fbea3fb0ef99ba3528460f0d6bd67 (patch) | |
| tree | 6700f03c7ff29d2ff7afedb7f42828b07ac98ba2 /backend/CSE3analysis.v | |
| parent | 560c9837eee2145e3a9763aa2e37a6eb34c7e9ac (diff) | |
| download | compcert-kvx-7ead22b0a04fbea3fb0ef99ba3528460f0d6bd67.tar.gz compcert-kvx-7ead22b0a04fbea3fb0ef99ba3528460f0d6bd67.zip | |
CSE3 analysis
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 10 |
1 files changed, 5 insertions, 5 deletions
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). |