diff options
Diffstat (limited to 'backend/Linear.v')
| -rw-r--r-- | backend/Linear.v | 19 |
1 files changed, 5 insertions, 14 deletions
diff --git a/backend/Linear.v b/backend/Linear.v index da1b4c04..55f92d16 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -17,17 +17,8 @@ instructions with explicit labels and ``goto'' instructions. *) Require Import Coqlib. -Require Import AST. -Require Import Integers. -Require Import Values. -Require Import Memory. -Require Import Events. -Require Import Globalenvs. -Require Import Smallstep. -Require Import Op. -Require Import Locations. -Require Import LTL. -Require Import Conventions. +Require Import AST Integers Values Memory Events Globalenvs Smallstep. +Require Import Op Locations LTL Conventions. (** * Abstract syntax *) @@ -194,7 +185,7 @@ Inductive step: state -> trace -> state -> Prop := find_function ros rs' = Some f' -> sig = funsig f' -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - step (State s f (Vptr stk Int.zero) (Ltailcall sig ros :: b) rs m) + step (State s f (Vptr stk Ptrofs.zero) (Ltailcall sig ros :: b) rs m) E0 (Callstate s f' rs' m') | exec_Lbuiltin: forall s f sp rs m ef args res b vargs t vres rs' m', @@ -236,14 +227,14 @@ Inductive step: state -> trace -> state -> Prop := | exec_Lreturn: forall s f stk b rs m m', Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - step (State s f (Vptr stk Int.zero) (Lreturn :: b) rs m) + step (State s f (Vptr stk Ptrofs.zero) (Lreturn :: b) rs m) E0 (Returnstate s (return_regs (parent_locset s) rs) m') | exec_function_internal: forall s f rs m rs' m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> rs' = undef_regs destroyed_at_function_entry (call_regs rs) -> step (Callstate s (Internal f) rs m) - E0 (State s f (Vptr stk Int.zero) f.(fn_code) rs' m') + E0 (State s f (Vptr stk Ptrofs.zero) f.(fn_code) rs' m') | exec_function_external: forall s ef args res rs1 rs2 m t m', args = map (fun p => Locmap.getpair p rs1) (loc_arguments (ef_sig ef)) -> |