diff options
Diffstat (limited to 'backend/LICM.v')
| -rw-r--r-- | backend/LICM.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/backend/LICM.v b/backend/LICM.v new file mode 100644 index 00000000..787ce256 --- /dev/null +++ b/backend/LICM.v @@ -0,0 +1,21 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL. +Require Inject. + +Axiom gen_injections : function -> node -> reg -> PTree.t (list Inject.inj_instr). + +Definition transf_program : program -> res program := + Inject.transf_program gen_injections. |