Changeset 886 for src/Clight/toCminor.ma


Ignore:
Timestamp:
Jun 6, 2011, 1:27:59 PM (9 years ago)
Author:
campbell
Message:

Put types into parameter and variable lists in Cminor.
Temporarily breaks translation to RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r882 r886  
    698698
    699699
    700 definition is_pointer : type → bool ≝
    701 λty.
    702   match ty with
    703   [ Tpointer _ _ ⇒ true
    704   | Tfunction _ _ ⇒ true
    705   | _ ⇒ false
    706   ].
    707 
    708700definition bigid1 ≝ an_identifier SymbolTag [[
    709701false;true;false;false;
     
    717709false;false;false;true]].
    718710
     711(* FIXME: the temporary handling is nonsense, I'm afraid. *)
    719712definition translate_function : list (ident×region) → function → res internal_function ≝
    720713λglobals, f.
     
    722715  let tmp ≝ bigid1 in (* FIXME *)
    723716  let tmpp ≝ bigid2 in (* FIXME *)
    724   let p_ptrs ≝ filter ? (λx. is_pointer (\snd x)) (fn_params f) in
    725   let v_ptrs ≝ (filter ? (λx. is_pointer (\snd x)) (fn_vars f)) in
    726717  do s ← translate_statement vartypes tmp tmpp (fn_body f);
    727718  OK ? (mk_internal_function
    728     (signature_of_type (type_of_params (fn_params f)) (fn_return f))
    729     (map ?? (fst ??) (fn_params f))
    730     (tmp::tmpp::(map ?? (fst ??) (fn_vars f)))
    731     (tmpp::(map ?? (fst ??) p_ptrs) @ (map ?? (fst ??) v_ptrs))
     719    (opttyp_of_type (fn_return f))
     720    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
     721    (〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
    732722    stacksize
    733723    s).
Note: See TracChangeset for help on using the changeset viewer.