Changeset 4 for C-semantics/Csyntax.ma


Ignore:
Timestamp:
Jun 2, 2010, 7:11:14 PM (10 years ago)
Author:
campbell
Message:

Some experimental work on executable Clight semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Csyntax.ma

    r3 r4  
    278278  match t return λ_.Z (* XXX appears to infer nat otherwise *) with
    279279  [ Tvoid ⇒ 1
    280   | Tint sz _ ⇒ match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    281   | Tfloat sz ⇒ match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ]
     280  | Tint sz _ ⇒ match sz return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
     281  | Tfloat sz ⇒ match sz return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    282282  | Tpointer _ ⇒ 4
    283283  | Tarray t' n ⇒ alignof t'
     
    363363  match t return λ_.Z with
    364364  [ Tvoid ⇒ 1
    365   | Tint i _ ⇒ match i with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    366   | Tfloat f ⇒ match f with [ F32 ⇒ 4 | F64 ⇒ 8 ]
     365  | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
     366  | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    367367  | Tpointer _ ⇒ 4
    368368  | Tarray t' n ⇒ sizeof t' * Zmax 1 n
Note: See TracChangeset for help on using the changeset viewer.