diff options
Diffstat (limited to 'arm')
-rw-r--r-- | arm/Asmgen.v | 4 | ||||
-rw-r--r-- | arm/Asmgenretaddr.v | 4 | ||||
-rw-r--r-- | arm/ConstpropOp.vp | 1 | ||||
-rw-r--r-- | arm/PrintAsm.ml | 5 | ||||
-rw-r--r-- | arm/SelectOp.vp | 5 | ||||
-rw-r--r-- | arm/SelectOpproof.v | 2 |
6 files changed, 3 insertions, 18 deletions
diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 4200c11b..b78dfb66 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -13,14 +13,10 @@ (** Translation from Mach to ARM. *) Require Import Coqlib. -Require Import Maps. Require Import Errors. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Mach. diff --git a/arm/Asmgenretaddr.v b/arm/Asmgenretaddr.v index 48b6328c..2d3c72d3 100644 --- a/arm/Asmgenretaddr.v +++ b/arm/Asmgenretaddr.v @@ -17,13 +17,9 @@ return addresses that are stored in activation records. *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Mach. diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index 0f06703c..a9cbad5d 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -17,7 +17,6 @@ Require Import Coqlib. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. Require Import Op. Require Import Registers. diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 0cee7865..64152487 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -640,7 +640,8 @@ let print_instruction oc = function | EF_inline_asm txt -> fprintf oc "%s begin inline assembly\n" comment; fprintf oc " %s\n" (extern_atom txt); - fprintf oc "%s end inline assembly\n" comment + fprintf oc "%s end inline assembly\n" comment; + 5 (* hoping this is an upper bound... *) | _ -> assert false end @@ -754,13 +755,13 @@ let print_var oc name v = fprintf oc " .size %a, . - %a\n" print_symb name print_symb name let print_globdef oc (name, gdef) = + match gdef with | Gfun(Internal f) -> print_function oc name f | Gfun(External ef) -> () | Gvar v -> print_var oc name v let print_program oc p = (* fprintf oc " .fpu vfp\n"; *) - List.iter (print_var oc) p.prog_vars; List.iter (print_globdef oc) p.prog_defs diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index 255c97c1..22ef88d2 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -37,14 +37,9 @@ *) Require Import Coqlib. -Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Cminor. Require Import Op. Require Import CminorSel. diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index a72913d3..e25fb0c7 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -19,9 +19,7 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import Memory. -Require Import Events. Require Import Globalenvs. -Require Import Smallstep. Require Import Cminor. Require Import Op. Require Import CminorSel. |