Changeset 2468 for src/Clight/Csyntax.ma


Ignore:
Timestamp:
Nov 15, 2012, 6:12:57 PM (7 years ago)
Author:
garnier
Message:

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csyntax.ma

    r2391 r2468  
    6464  | Tvoid: type                         (**r the [void] type *)
    6565  | Tint: intsize → signedness → type   (**r integer types *)
    66   | Tfloat: floatsize → type            (**r floating-point types *)
    6766  | Tpointer: (*region →*) type → type      (**r pointer types ([*ty]) *)
    6867  | Tarray: (*region →*) type → nat → type  (**r array types ([ty[len]]) *)
     
    8584  (vo:P Tvoid)
    8685  (it:∀i,s. P (Tint i s))
    87   (fl:∀f. P (Tfloat f))
    8886  (pt:∀t. P t → P (Tpointer t))
    8987  (ar:∀t,n. P t → P (Tarray t n))
     
    9694  [ Tvoid ⇒ vo
    9795  | Tint i s ⇒ it i s
    98   | Tfloat s ⇒ fl s
    99   | Tpointer t' ⇒ pt t' (type_ind P vo it fl pt ar fn st un cp t')
    100   | Tarray t' n ⇒ ar t' n (type_ind P vo it fl pt ar fn st un cp t')
    101   | Tfunction tl t' ⇒ fn tl t' (type_ind P vo it fl pt ar fn st un cp t')
     96  | Tpointer t' ⇒ pt t' (type_ind P vo it pt ar fn st un cp t')
     97  | Tarray t' n ⇒ ar t' n (type_ind P vo it pt ar fn st un cp t')
     98  | Tfunction tl t' ⇒ fn tl t' (type_ind P vo it pt ar fn st un cp t')
    10299  | Tstruct i fs ⇒ st i fs
    103100  | Tunion i fs ⇒ un i fs
     
    157154with expr_descr : Type[0] ≝
    158155  | Econst_int: ∀sz:intsize. bvint sz → expr_descr       (**r integer literal *)
    159   | Econst_float: float → expr_descr   (**r float literal *)
    160156  | Evar: ident → expr_descr           (**r variable *)
    161157  | Ederef: expr → expr_descr          (**r pointer dereference (unary [*]) *)
     
    355351  [ Tvoid ⇒ 1
    356352  | Tint sz _ ⇒ match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    357   | Tfloat sz ⇒ match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    358353  | Tpointer _ ⇒ 4
    359354  | Tarray t' n ⇒ alignof t'
     
    380375  (vo:P Tvoid)
    381376  (it:∀i,s. P (Tint i s))
    382   (fl:∀f. P (Tfloat f))
    383377  (pt:∀t. P t → P (Tpointer t))
    384378  (ar:∀t,n. P t → P (Tarray t n))
     
    393387  [ Tvoid ⇒ vo
    394388  | Tint i s ⇒ it i s
    395   | Tfloat s ⇒ fl s
    396   | Tpointer t' ⇒ pt t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    397   | Tarray t' n ⇒ ar t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    398   | Tfunction tl t' ⇒ fn tl t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
    399   | Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
    400   | Tunion i fs ⇒ un i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
     389  | Tpointer t' ⇒ pt t' (type_ind2 P Q vo it pt ar fn st un cp nl cs t')
     390  | Tarray t' n ⇒ ar t' n (type_ind2 P Q vo it pt ar fn st un cp nl cs t')
     391  | Tfunction tl t' ⇒ fn tl t' (type_ind2 P Q vo it pt ar fn st un cp nl cs t')
     392  | Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it pt ar fn st un cp nl cs fs)
     393  | Tunion i fs ⇒ un i fs (fieldlist_ind2 P Q vo it pt ar fn st un cp nl cs fs)
    401394  | Tcomp_ptr i ⇒ cp i
    402395  ]
     
    405398  (vo:P Tvoid)
    406399  (it:∀i,s. P (Tint i s))
    407   (fl:∀f. P (Tfloat f))
    408400  (pt:∀t. P t → P (Tpointer t))
    409401  (ar:∀t,n. P t → P (Tarray t n))
     
    417409  match fs return λfs'.Q fs' with
    418410  [ Fnil ⇒ nl
    419   | Fcons i t f' ⇒ cs i t f' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t)
    420                         (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs f')
     411  | Fcons i t f' ⇒ cs i t f' (type_ind2 P Q vo it pt ar fn st un cp nl cs t)
     412                        (fieldlist_ind2 P Q vo it pt ar fn st un cp nl cs f')
    421413  ].
    422414
     
    439431  [ Tvoid ⇒ 1
    440432  | Tint i _ ⇒ match i with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
    441   | Tfloat f ⇒ match f with [ F32 ⇒ 4 | F64 ⇒ 8 ]
    442433  | Tpointer _ ⇒ size_pointer
    443434  | Tarray t' n ⇒ sizeof t' * max 1 n
     
    610601  [ Tvoid ⇒ ASTint I32 Unsigned
    611602  | Tint sz sg ⇒ ASTint sz sg
    612   | Tfloat sz ⇒ ASTfloat sz
    613603  | Tpointer _ ⇒ ASTptr
    614604  | Tarray _ _ ⇒ ASTptr
     
    622612  [ Tvoid ⇒ None ?
    623613  | Tint sz sg ⇒ Some ? (ASTint sz sg)
    624   | Tfloat sz ⇒ Some ? (ASTfloat sz)
    625614  | Tpointer _ ⇒ Some ? ASTptr
    626615  | Tarray _ _ ⇒ Some ? ASTptr
     
    657646  match ty return λty. mode (typ_of_type ty) with
    658647  [ Tint i s ⇒ By_value (ASTint i s)
    659   | Tfloat sz ⇒ By_value (ASTfloat sz)
    660648  | Tvoid ⇒ By_nothing …
    661649  | Tpointer _ ⇒ By_value ASTptr
Note: See TracChangeset for help on using the changeset viewer.