Changeset 124 for C-semantics/test


Ignore:
Timestamp:
Sep 24, 2010, 10:31:32 AM (10 years ago)
Author:
campbell
Message:

Initial work on Clight semantics with 8051 memory spaces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/test/io2.c.ma

    r20 r124  
    3636interpretation "hide memory" 'mem = (mk_mem ???).
    3737
     38ninductive result (T:Type) : T → Prop ≝
     39| witness : ∀t:T. result T t.
     40
    3841(* The trick to being able to normalize the term is to avoid looking at the
    3942   continuations! *)
    4043nremark foo:
    41     match match s with [ Interact f args k ⇒ k (EVint (repr 10))
    42                  | Value v ⇒ Wrong ?
    43                  | Wrong ⇒ Wrong ? ] with
    44     [ Interact _ _ _ ⇒ False
    45     | Value v ⇒ v = v
     44    match match s with [ Interact call k ⇒ k (EVint (repr 10))
     45                 | Value v ⇒ Wrong ???
     46                 | Wrong ⇒ Wrong ??? ] with
     47    [ Interact _ _ ⇒ False
     48    | Value v ⇒ result ? v
    4649    | Wrong ⇒ False
    4750    ].
Note: See TracChangeset for help on using the changeset viewer.