blob: d45eef43e135d0aad3368bdca15a8a163b075c6c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
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).
Opaque gen_injections.
Definition transf_program : program -> res program :=
Inject.transf_program gen_injections.
|
