Changeset 816 for src/Clight/Csyntax.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/Clight/Csyntax.ma

    r797 r816  
    830830inductive classify_cmp_cases : Type[0] ≝
    831831  | cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *)
    832   | cmp_case_ipip: classify_cmp_cases  (**r int|ptr|array , int|ptr|array*)
     832  | cmp_case_ii: classify_cmp_cases  (**r int, int*)
     833  | cmp_case_pp: classify_cmp_cases  (**r ptr|array , ptr|array*)
    833834  | cmp_case_ff: classify_cmp_cases  (**r float , float *)
    834835  | cmp_default: classify_cmp_cases . (**r other *)
     
    840841    [ Tint i2 s2 ⇒
    841842      classify_32un_aux ? i1 s1 cmp_case_I32unsi
    842         (classify_32un_aux ? i2 s2 cmp_case_I32unsi cmp_case_ipip)
     843        (classify_32un_aux ? i2 s2 cmp_case_I32unsi cmp_case_ii)
    843844    | _ ⇒ cmp_default ]
    844845  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff | _ ⇒ cmp_default ]
    845846  | Tpointer _ _ ⇒
    846847    match ty2 with
    847     [ Tint _ _ ⇒ cmp_case_ipip
    848     | Tpointer _ _ ⇒ cmp_case_ipip
    849     | Tarray _ _ _ ⇒ cmp_case_ipip
     848    [ Tpointer _ _ ⇒ cmp_case_pp
     849    | Tarray _ _ _ ⇒ cmp_case_pp
    850850    | _ ⇒ cmp_default ]
    851851  | Tarray _ _ _ ⇒
    852852    match ty2 with
    853     [ Tint _ _ ⇒ cmp_case_ipip
    854     | Tpointer _ _ ⇒ cmp_case_ipip
    855     | Tarray _ _ _ ⇒ cmp_case_ipip
     853    [ Tpointer _ _ ⇒ cmp_case_pp
     854    | Tarray _ _ _ ⇒ cmp_case_pp
    856855    | _ ⇒ cmp_default ]
    857856  | _ ⇒ cmp_default
Note: See TracChangeset for help on using the changeset viewer.