diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-05-24 09:46:07 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-05-24 09:46:07 +0000 |
commit | 3fa79790e617d87584598746296e626e0ce3b256 (patch) | |
tree | dcdc926130d9ed8d302eedf8215d065c0e787eed /arm/Asm.v | |
parent | 285d908c5dbd90bff7f03618c7a9e0fa5e287c94 (diff) | |
download | compcert-kvx-3fa79790e617d87584598746296e626e0ce3b256.tar.gz compcert-kvx-3fa79790e617d87584598746296e626e0ce3b256.zip |
Refactoring: move symbol_offset into Genv.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/Asm.v')
-rw-r--r-- | arm/Asm.v | 14 |
1 files changed, 4 insertions, 10 deletions
@@ -493,12 +493,6 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool := must survive the execution of the pseudo-instruction. *) -Definition symbol_offset (id: ident) (ofs: int) : val := - match Genv.find_symbol ge id with - | Some b => Vptr b ofs - | None => Vundef - end. - Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome := match i with | Padd r1 r2 so => @@ -514,11 +508,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | None => Stuck end | Pbsymb id sg => - Next (rs#PC <- (symbol_offset id Int.zero)) m + Next (rs#PC <- (Genv.symbol_address ge id Int.zero)) m | Pbreg r sg => Next (rs#PC <- (rs#r)) m | Pblsymb id sg => - Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (symbol_offset id Int.zero)) m + Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (Genv.symbol_address ge id Int.zero)) m | Pblreg r sg => Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (rs#r)) m | Pbic r1 r2 so => @@ -649,7 +643,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Plabel lbl => Next (nextinstr rs) m | Ploadsymbol r1 lbl ofs => - Next (nextinstr (rs#r1 <- (symbol_offset lbl ofs))) m + Next (nextinstr (rs#r1 <- (Genv.symbol_address ge lbl ofs))) m | Pbtbl r tbl => match rs#r with | Vint n => @@ -763,7 +757,7 @@ Inductive initial_state (p: program): state -> Prop := let ge := Genv.globalenv p in let rs0 := (Pregmap.init Vundef) - # PC <- (symbol_offset ge p.(prog_main) Int.zero) + # PC <- (Genv.symbol_address ge p.(prog_main) Int.zero) # IR14 <- Vzero # IR13 <- Vzero in Genv.init_mem p = Some m0 -> |