Changeset 816 for src/Clight/test


Ignore:
Timestamp:
May 19, 2011, 3:06:42 PM (10 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/Clight/test/search.ma

    r748 r816  
    193193@refl
    194194qed.
     195
     196include "Clight/toCminor.ma".
     197include "Cminor/semantics.ma".
     198
     199example e1: finishes_with (repr 3) ? (do p ← clight_to_cminor myprog; exec_up_to Cminor_fullexec p 1000 [ ]).
     200normalize
     201@refl
     202qed.
     203
     204include "Cminor/toRTLabs.ma".
     205include "RTLabs/semantics.ma".
     206
     207example e2: finishes_with (repr 3) ? (
     208do p1 ← clight_to_cminor myprog;
     209do p2 ← cminor_to_rtlabs p1;
     210 exec_up_to RTLabs_fullexec p2 1000 [ ]).
     211normalize
     212@refl
     213qed.
Note: See TracChangeset for help on using the changeset viewer.