Changeset 816 for src/common


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/common/Identifiers.ma

    r797 r816  
    114114λtag,s,s'. an_id_set tag (merge unit 16 (match s with [ an_id_set s0 ⇒ s0 ])
    115115                                        (match s' with [ an_id_set s1 ⇒ s1 ])).
     116
     117interpretation "identifier set union" 'union a b = (union_set ? a b).
     118notation "∅" non associative with precedence 90 for @{ 'empty }.
     119interpretation "empty identifier set" 'empty = (empty_set ?).
     120interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
Note: See TracChangeset for help on using the changeset viewer.