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/semantics.ma

    r797 r816  
    142142      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
    143143      ret ? 〈E0, build_state f fs m' l〉
    144   | St_call_id id args dst sig l ⇒ (* XXX: haven't used sig *)
     144  | St_call_id id args dst l ⇒
    145145      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    146146      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    147147      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    148148      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    149   | St_call_ptr frs args dst sig l ⇒  (* XXX: haven't used sig *)
     149  | St_call_ptr frs args dst l ⇒
    150150      ! fv ← reg_retrieve (locals f) frs;
    151151      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    152152      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    153153      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    154   | St_tailcall_id id args sig ⇒ (* XXX: haven't used sig *)
     154  | St_tailcall_id id args
    155155      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    156156      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    157157      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    158158      ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    159   | St_tailcall_ptr frs args sig ⇒  (* XXX: haven't used sig *)
     159  | St_tailcall_ptr frs args
    160160      ! fv ← reg_retrieve (locals f) frs;
    161161      ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
Note: See TracChangeset for help on using the changeset viewer.