Ignore:
Timestamp:
Oct 6, 2011, 6:45:54 PM (10 years ago)
Author:
campbell
Message:

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/ERTL/semantics.ma

    r1197 r1311  
    4949axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
    5050
    51 definition genv ≝ λglobals. (genv_t Genv) (fundef (ertl_internal_function globals)).
     51definition genv ≝ λglobals. (genv_t Genv) (fundef (joint_internal_function globals … (ertl_sem_params_ globals))).
    5252
    5353(* CSC: frame reduced to this *)
     
    139139
    140140axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals).
    141 axiom fetch_function: ∀globals: list ident. state → res (ertl_internal_function globals).
     141axiom fetch_function: ∀globals: list ident. state → res (joint_internal_function globals … (ertl_sem_params_ globals)).
    142142
    143143definition init_locals : list register → register_env val ≝
     
    191191  (* CSC: monadic notation missing here *)
    192192    bind ?? (fetch_function globals st) (λf.
    193     OK ? (ertl_if_stacksize globals f)).
     193    OK ? (joint_if_stacksize globals … f)).
    194194
    195195definition get_hwsp : state → res address ≝
Note: See TracChangeset for help on using the changeset viewer.