From 6379f6291eea909426f074db67837b04a1dec9ae Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 1 Apr 2020 14:24:05 +0200 Subject: attempt at compiling --- backend/LICM.v | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 backend/LICM.v (limited to 'backend/LICM.v') diff --git a/backend/LICM.v b/backend/LICM.v new file mode 100644 index 00000000..1b5334ba --- /dev/null +++ b/backend/LICM.v @@ -0,0 +1,9 @@ +Require Import Coqlib Maps Errors Integers Floats Lattice Kildall. +Require Import AST Linking. +Require Import Memory Registers Op RTL. +Require Inject. + +Definition gen_injections (f : function) (max_pc : node) (max_reg : reg): + PTree.t (list Inject.inj_instr) := PTree.empty (list Inject.inj_instr). + +Definition transf_program := Inject.transf_program gen_injections. -- cgit