From 0f9018baabe8feeed19d8f7e14f8480e898b5a84 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 8 Dec 2020 19:56:28 +0100 Subject: CSE3 now runs on its own fixpoint iterator not based on Kildall.v --- backend/CSE3analysis.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'backend/CSE3analysis.v') diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v index 390f6d26..bcdebca7 100644 --- a/backend/CSE3analysis.v +++ b/backend/CSE3analysis.v @@ -509,12 +509,14 @@ Definition check_inductiveness (fn : RTL.function) (tenv: typing_env) (inv: inva (fun pc' => relb_leb rel' (PMap.get pc' inv)) (RTL.successors_instr instr) end). +(* No longer used. Incompatible with transfer functions that yield a different result depending on the successor. Definition internal_analysis (tenv : typing_env) (f : RTL.function) : option invariants := DS.fixpoint (RTL.fn_code f) RTL.successors_instr (apply_instr' tenv (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). +*) End OPERATIONS. Record analysis_hints := -- cgit