Changeset 13 for C-semantics/Csem.ma


Ignore:
Timestamp:
Jul 19, 2010, 4:30:09 PM (10 years ago)
Author:
campbell
Message:

Minor syntactic changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Csem.ma

    r3 r13  
    444444ndefinition env ≝ (tree_t ? PTree) block. (* map variable -> location *)
    445445
    446 ndefinition empty_env: env ≝ (empty ? PTree block).
     446ndefinition empty_env: env ≝ (empty ).
    447447
    448448(* * [load_value_of_type ty m b ofs] computes the value of a datum
     
    487487      ∀e,m,id,ty,vars,m1,b1,m2,e2.
    488488      alloc m 0 (sizeof ty) = 〈m1, b1〉 →
    489       alloc_variables (set ? PTree ? id b1 e) m1 vars e2 m2 →
     489      alloc_variables (set id b1 e) m1 vars e2 m2 →
    490490      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.
    491491
     
    503503  | bind_parameters_cons:
    504504      ∀e,m,id,ty,params,v1,vl,b,m1,m2.
    505       get ? PTree ? id e = Some ? b →
     505      get ??? id e = Some ? b →
    506506      store_value_of_type ty m b zero v1 = Some ? m1 →
    507507      bind_parameters e m1 params vl m2 →
     
    511511
    512512ndefinition blocks_of_env : env → list block ≝ λe.
    513   map ?? (snd ident block) (elements ? PTree ? e).
     513  map ?? (snd ident block) (elements ??? e).
    514514
    515515(* * Selection of the appropriate case of a [switch], given the value [n]
     
    611611with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr -> block -> int -> Prop ≝
    612612  | eval_Evar_local:   ∀id,l,ty.
    613       (* XXX notation? e!id*) get ? PTree ? id e = Some ? l ->
     613      (* XXX notation? e!id*) get ??? id e = Some ? l ->
    614614      eval_lvalue ge e m (Expr (Evar id) ty) l zero
    615615  | eval_Evar_global: ∀id,l,ty.
    616       (* XXX e!id *) get ? PTree ? id e = None ? ->
    617       find_symbol Genv ? ge id = Some ? l ->
     616      (* XXX e!id *) get ??? id e = None ? ->
     617      find_symbol ?? ge id = Some ? l ->
    618618      eval_lvalue ge e m (Expr (Evar id) ty) l zero
    619619  | eval_Ederef: ∀a,ty,l,ofs.
     
    774774      eval_expr ge e m a vf ->
    775775      eval_exprlist ge e m al vargs ->
    776       find_funct Genv ? ge vf = Some ? fd ->
     776      find_funct ?? ge vf = Some ? fd ->
    777777      type_of_fundef fd = typeof a ->
    778778      step ge (State f (Scall (None ?) a al) k e m)
     
    783783      eval_expr ge e m a vf ->
    784784      eval_exprlist ge e m al vargs ->
    785       find_funct Genv ? ge vf = Some ? fd ->
     785      find_funct ?? ge vf = Some ? fd ->
    786786      type_of_fundef fd = typeof a ->
    787787      step ge (State f (Scall (Some ? lhs) a al) k e m)
     
    12451245      let ge := globalenv Genv ?? p in
    12461246      let m0 := init_mem Genv ?? p in
    1247       find_symbol Genv ? ge (prog_main ?? p) = Some ? b ->
    1248       find_funct_ptr Genv ? ge b = Some ? f ->
     1247      find_symbol ?? ge (prog_main ?? p) = Some ? b ->
     1248      find_funct_ptr ?? ge b = Some ? f ->
    12491249      initial_state p (Callstate f (nil ?) Kstop m0).
    12501250
     
    12611261
    12621262ndefinition exec_program : program → program_behavior → Prop ≝ λp,beh.
    1263   program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv Genv ?? p) beh.
     1263  program_behaves (mk_transrel ?? step) (initial_state p) final_state (globalenv ??? p) beh.
    12641264(*
    12651265(** Big-step execution of a whole program.  *)
Note: See TracChangeset for help on using the changeset viewer.