Changeset 251 for C-semantics/Csyntax.ma


Ignore:
Timestamp:
Nov 22, 2010, 2:40:26 PM (9 years ago)
Author:
campbell
Message:

Separate out soundness of exec_expr from definition.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Csyntax.ma

    r250 r251  
    192192  | Efield: expr → ident → expr_descr  (**r access to a member of a struct or union *)
    193193  | Ecost: costlabel → expr → expr_descr.
     194
     195
     196
    194197
    195198(* * Extract the type part of a type-annotated Clight expression. *)
Note: See TracChangeset for help on using the changeset viewer.