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/RTLabs/RTLabsMatitaPrinter.ml

    r765 r816  
    167167        lbl
    168168  | RTLabs.St_call_id (f, args, res, sg, lbl) ->
    169       Printf.sprintf "make_St_call_id id_%s %s (Some ? %s) (%s) %s"
     169      Printf.sprintf "make_St_call_id id_%s %s (Some ? %s) %s"
    170170        f
    171171        (print_params args)
    172172        (Register.print res)
    173         (print_sig sg)
    174173        lbl
    175174  | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
    176       Printf.sprintf "make_St_call_ptr %s %s (Some ? %s) (%s) %s"
     175      Printf.sprintf "make_St_call_ptr %s %s (Some ? %s) %s"
    177176        (Register.print f)
    178177        (print_params args)
    179178        (Register.print res)
    180         (print_sig sg)
    181179        lbl
    182180  | RTLabs.St_tailcall_id (f, args, sg) ->
    183       Printf.sprintf "make_St_tailcall_id id_%s %s (%s)"
     181      Printf.sprintf "make_St_tailcall_id id_%s %s"
    184182        f
    185183        (print_params args)
    186         (print_sig sg)
    187184  | RTLabs.St_tailcall_ptr (f, args, sg) ->
    188       Printf.sprintf "make_St_tailcall_ptr %s %s (%s)"
     185      Printf.sprintf "make_St_tailcall_ptr %s %s"
    189186        (Register.print f)
    190187        (print_params args)
    191         (print_sig sg)
    192188  | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
    193189      Printf.sprintf "make_St_condcst (%s) %s %s"
Note: See TracChangeset for help on using the changeset viewer.