Changeset 1058 for src/Clight/Csem.ma
- Timestamp:
- Jul 6, 2011, 1:29:58 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Csem.ma
r964 r1058 25 25 include "common/Globalenvs.ma". 26 26 include "Clight/Csyntax.ma". 27 include "common/Maps.ma".28 27 (*include "Events.ma".*) 29 28 include "common/Smallstep.ma". … … 482 481 block. *) 483 482 484 definition env ≝ (tree_t ? PTree)block. (* map variable -> location *)485 486 definition empty_env: env ≝ (empty …).483 definition env ≝ identifier_map SymbolTag block. (* map variable -> location *) 484 485 definition empty_env: env ≝ (empty_map …). 487 486 488 487 (* * [load_value_of_type ty m b ofs] computes the value of a datum … … 535 534 ∀e,m,id,ty,vars,m1,b1,m2,e2. 536 535 alloc m 0 (sizeof ty) Any = 〈m1, b1〉 → 537 alloc_variables ( set … id b1 e) m1 vars e2 m2 →536 alloc_variables (add … e id b1) m1 vars e2 m2 → 538 537 alloc_variables e m (〈id, ty〉 :: vars) e2 m2. 539 538 … … 551 550 | bind_parameters_cons: 552 551 ∀e,m,id,ty,params,v1,vl,b,m1,m2. 553 get ??? id e= Some ? b →552 lookup ?? e id = Some ? b → 554 553 store_value_of_type ty m b zero_offset v1 = Some ? m1 → 555 554 bind_parameters e m1 params vl m2 → … … 559 558 560 559 definition blocks_of_env : env → list block ≝ λe. 561 map ?? (λx. snd ?? x) (elements ?? ?e).560 map ?? (λx. snd ?? x) (elements ?? e). 562 561 563 562 (* * Selection of the appropriate case of a [switch], given the value [n] … … 666 665 with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → offset → trace → Prop ≝ 667 666 | eval_Evar_local: ∀id,l,ty. 668 (* XXX notation? e!id*) get ??? id e= Some ? l →667 (* XXX notation? e!id*) lookup ?? e id = Some ? l → 669 668 eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0 670 669 | eval_Evar_global: ∀id,l,ty. 671 (* XXX e!id *) get ??? id e= None ? →670 (* XXX e!id *) lookup ?? e id = None ? → 672 671 find_symbol ?? ge id = Some ? l → 673 672 eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
Note: See TracChangeset
for help on using the changeset viewer.