- Timestamp:
- Aug 26, 2011, 7:08:07 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/semantics.ma
r1117 r1118 18 18 (* CSC: I have a byte, I need a value, but it is complex to do so *) 19 19 axiom val_of_Byte: Byte → val. 20 (* Map from the front-end memory model to the back-end memory model *) 21 axiom represent_block: block → val × val. 20 22 (* CSC: fixed size chunk *) 21 23 axiom chunk: memory_chunk. … … 170 172 ! locals ← reg_store dst v' (locals f); 171 173 ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉 *) 174 172 175 (* CSC: Removed: St_jumptable *) 173 176 (* CSC: Added: *) 174 | rtl_st_addr ldest hdest id l ⇒ ? 175 | rtl_st_stack_addr ldest hdest l ⇒ ? 176 (* CSC: St_const splitted into rtl_st_int *) 177 178 (* CSC: St_const splitted into rtl_st_int, rtl_st_addr and rt_st_stack_addr; *) 179 | rtl_st_addr ldest hdest id l ⇒ 180 ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id); 181 let 〈laddr,haddr〉 ≝ represent_block addr in 182 ! locals ← reg_store ldest laddr (locals f); 183 ! locals ← reg_store hdest haddr locals; 184 ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉 185 | rtl_st_stack_addr ldest hdest l ⇒ 186 let 〈laddr,haddr〉 ≝ represent_block (sp f) in 187 ! locals ← reg_store ldest laddr (locals f); 188 ! locals ← reg_store hdest haddr locals; 189 ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉 177 190 | rtl_st_int dest v l ⇒ 178 191 ! locals ← reg_store dest (val_of_Byte v) (locals f); 179 192 ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f) (carry f)) fs m〉 193 180 194 | rtl_st_move dreg sreg l ⇒ ? 181 195 | rtl_st_opaccs op dacc dbacc sacc sbacc l ⇒ ?
Note: See TracChangeset
for help on using the changeset viewer.