Changeset 879 for src/Cminor


Ignore:
Timestamp:
Jun 3, 2011, 5:35:30 PM (8 years ago)
Author:
campbell
Message:

Refine "AST" types to include size/signedness information.

Location:
src/Cminor
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/semantics.ma

    r816 r879  
    226226    | External fn ⇒
    227227        ! evargs ← check_eventval_list args (sig_args (ef_sig fn));
    228         ! evres ← do_io (ef_id fn) evargs (match (sig_res (ef_sig fn)) with [ None ⇒ ASTint | Some t ⇒ t ]);  (* XXX hack, should allow none *)
     228        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    229229        let res ≝ match (sig_res (ef_sig fn)) with [ None ⇒ None ? | Some _ ⇒ Some ? (mk_val ? evres) ] in
    230230        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate res m k〉
  • src/Cminor/test/factorial.ma

    r816 r879  
    33
    44definition id_get_input := ident_of_nat 0.
    5 definition f_get_input := External internal_function (mk_external_function id_get_input (mk_signature [] (Some ? ASTint))).
     5definition f_get_input := External internal_function (mk_external_function id_get_input (mk_signature [] (Some ? (ASTint I32 Signed)))).
    66definition id_main := ident_of_nat 1.
    77definition id_main_tmp0 := ident_of_nat 5.
     
    1313definition C_cost1 := costlabel_of_nat 2.
    1414definition f_main := Internal ? (mk_internal_function
    15   (mk_signature [] (Some ? ASTint))
     15  (mk_signature [] (Some ? (ASTint I32 Signed)))
    1616  []
    1717  [id_main_tmp0; id_main_r; id_main_j; id_main_i]
  • src/Cminor/test/null-op.ma

    r776 r879  
    1717definition C_cost1 := costlabel_of_nat 1.
    1818definition f_main := Internal ? (mk_internal_function
    19   (mk_signature [] (Some ? ASTint))
     19  (mk_signature [] (Some ? (ASTint I32 Signed)))
    2020  []
    2121  [id_main_tmp0; id_main_q; id_main_p; id_main_c]
  • src/Cminor/test/search.ma

    r816 r879  
    2020definition C_cost7 := costlabel_of_nat 1.
    2121definition f_search := Internal ? (mk_internal_function
    22   (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint))
     22  (mk_signature [ASTptr Any; ASTint I8 Signed; ASTint I8 Signed] (Some ? (ASTint I8 Signed)))
    2323  [id_search_tab; id_search_size; id_search_to_find]
    2424  [id_search_tmp0; id_search_low; id_search_high; id_search_i]
     
    101101definition C_cost9 := costlabel_of_nat 18.
    102102definition f_main := Internal ? (mk_internal_function
    103   (mk_signature [] (Some ? ASTint))
     103  (mk_signature [] (Some ? (ASTint I32 Signed)))
    104104  []
    105105  [id_main_tmp0; id_main_res]
  • src/Cminor/test/sum-bad.ma

    r797 r879  
    1616definition C_cost1 := costlabel_of_nat 1.
    1717definition f_main := Internal ? (mk_internal_function
    18   (mk_signature [] (Some ? ASTint))
     18  (mk_signature [] (Some ? (ASTint I32 Signed)))
    1919  []
    2020  [id_main_tmp0; id_main_total(*; id_main_i*)]
  • src/Cminor/test/sum.ma

    r768 r879  
    1313definition C_cost1 := costlabel_of_nat 1.
    1414definition f_main := Internal ? (mk_internal_function
    15   (mk_signature [] (Some ? ASTint))
     15  (mk_signature [] (Some ? (ASTint I32 Signed)))
    1616  []
    1717  [id_main_tmp0; id_main_total; id_main_i]
  • src/Cminor/test/switcher.ma

    r816 r879  
    77
    88definition id_get := ident_of_nat 99.
    9 definition f_get := External internal_function (mk_external_function id_get (mk_signature [] (Some ? ASTint))).
     9definition f_get := External internal_function (mk_external_function id_get (mk_signature [] (Some ? (ASTint I32 Signed)))).
    1010
    1111
     
    1414definition id_main_x1 := ident_of_nat 2.
    1515definition f_main := Internal ? (mk_internal_function
    16   (mk_signature [] (Some ? ASTint))
     16  (mk_signature [] (Some ? (ASTint I32 Signed)))
    1717  []
    1818  [id_main_i; id_main_x1]
Note: See TracChangeset for help on using the changeset viewer.