diff options
Diffstat (limited to 'backend/CSE3analysis.v')
| -rw-r--r-- | backend/CSE3analysis.v | 2 |
1 files changed, 2 insertions, 0 deletions
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 := |