Changeset 816 for src/Cminor/toRTLabs.ma


Ignore:
Timestamp:
May 19, 2011, 3:06:42 PM (9 years ago)
Author:
campbell
Message:

Clight to Cminor compilation, modulo switch statements, temporary
generation, 32 to 8 bit translation and miscellaneous bugs.

Also, remove (unused) signatures from function call statements in Cminor
and RTLabs; and separate comparison of integers and pointers in Clight
semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r797 r816  
    251251    do f ← add_with_addressing env e1 (λm,rs. St_store q m rs val_reg) ptrs f;
    252252    add_expr env e2 val_reg ptrs f
    253 | St_call return_opt_id e args sig
     253| St_call return_opt_id e args
    254254    do return_opt_reg ←
    255255      match return_opt_id with
     
    260260    do f ←
    261261      match e with
    262       [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f
     262      [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg) f
    263263      | _ ⇒
    264264        do 〈fnr, f〉 ← choose_reg env e ptrs f;
    265         do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) f;
     265        do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg) f;
    266266        add_expr env e fnr ptrs f
    267267      ];
    268268    add_exprs env args args_regs ptrs f
    269 | St_tailcall e args sig
     269| St_tailcall e args
    270270    do 〈args_regs, f〉 ← choose_regs env args ptrs f;
    271271    do f ←
    272272      match e with
    273       [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f
     273      [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs) f
    274274      | _ ⇒
    275275        do 〈fnr, f〉 ← choose_reg env e ptrs f;
    276         do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) f;
     276        do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs) f;
    277277        add_expr env e fnr ptrs f
    278278      ];
Note: See TracChangeset for help on using the changeset viewer.