Changeset 961 for src/Clight/Csyntax.ma


Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csyntax.ma

    r879 r961  
    156156
    157157with expr_descr : Type[0] ≝
    158   | Econst_int: int → expr_descr       (**r integer literal *)
     158  | Econst_int: ∀sz:intsize. bvint sz → expr_descr       (**r integer literal *)
    159159  | Econst_float: float → expr_descr   (**r float literal *)
    160160  | Evar: ident → expr_descr           (**r variable *)
     
    207207with labeled_statements : Type[0] ≝            (**r cases of a [switch] *)
    208208  | LSdefault: statement → labeled_statements
    209   | LScase: int → statement → labeled_statements → labeled_statements.
     209  | LScase: ∀sz:intsize. bvint sz → statement → labeled_statements → labeled_statements.
    210210
    211211let rec statement_ind2
     
    227227  (Scs:∀l,s. P s → P (Scost l s))
    228228  (LSd:∀s. P s → Q (LSdefault s))
    229   (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
     229  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
    230230  (s:statement) on s : P s ≝
    231231match s with
     
    276276  (Scs:∀l,s. P s → P (Scost l s))
    277277  (LSd:∀s. P s → Q (LSdefault s))
    278   (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
     278  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
    279279  (ls:labeled_statements) on ls : Q ls ≝
    280280match ls with
    281281[ LSdefault s ⇒ LSd s
    282282    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    283 | LScase i s t ⇒ LSc i s t
     283| LScase sz i s t ⇒ LSc sz i s t
    284284    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    285285    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t)
     
    288288definition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo,Scs.
    289289  statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs
    290   (λ_,_. I) (λ_,_,_,_,_.I).
     290  (λ_,_. I) (λ_,_,_,_,_,_.I).
    291291
    292292(* * ** Functions *)
Note: See TracChangeset for help on using the changeset viewer.