Changeset 2619


Ignore:
Timestamp:
Feb 6, 2013, 5:03:19 PM (6 years ago)
Author:
campbell
Message:

Update some test cases.

Location:
src/Clight/test
Files:
12 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/addptrcharboth.test.ma

    r2569 r2619  
    1414
    1515include "Clight/toCminor.ma".
    16 include "Cminor/semantics.ma".
     16include "Cminor/Cminor_semantics.ma".
    1717
    1818example e1: finishes_with (repr I32 266) ?
     
    2424
    2525include "Cminor/toRTLabs.ma".
    26 include "RTLabs/semantics.ma".
     26include "RTLabs/RTLabs_semantics.ma".
    2727include "Clight/label.ma".
    2828
  • src/Clight/test/badconditional.test.ma

    r2576 r2619  
    1515
    1616include "Clight/toCminor.ma".
    17 include "Cminor/semantics.ma".
     17include "Cminor/Cminor_semantics.ma".
    1818
    1919example e1: finishes_with (repr I32 15) ?
     
    2525
    2626include "Cminor/toRTLabs.ma".
    27 include "RTLabs/semantics.ma".
     27include "RTLabs/RTLabs_semantics.ma".
    2828include "Clight/label.ma".
    2929
  • src/Clight/test/controlflow.test.ma

    r2388 r2619  
    1414
    1515include "Clight/toCminor.ma".
    16 include "Cminor/semantics.ma".
     16include "Cminor/Cminor_semantics.ma".
    1717
    1818example e1: finishes_with (repr I32 38) ?
     
    2424
    2525include "Cminor/toRTLabs.ma".
    26 include "RTLabs/semantics.ma".
     26include "RTLabs/RTLabs_semantics.ma".
    2727include "Clight/label.ma".
    2828
  • src/Clight/test/endptr.test.ma

    r2395 r2619  
    88include "Clight/SimplifyCasts.ma".
    99include "Clight/toCminor.ma".
    10 include "Cminor/semantics.ma".
     10include "Cminor/Cminor_semantics.ma".
    1111
    1212(* This succeeds because the variables have been arranged in the stack frame. *)
     
    2020
    2121include "Cminor/toRTLabs.ma".
    22 include "RTLabs/semantics.ma".
     22include "RTLabs/RTLabs_semantics.ma".
    2323include "Clight/label.ma".
    2424
  • src/Clight/test/endptr2.test.ma

    r2395 r2619  
    88include "Clight/SimplifyCasts.ma".
    99include "Clight/toCminor.ma".
    10 include "Cminor/semantics.ma".
     10include "Cminor/Cminor_semantics.ma".
    1111
    1212example e1:
     
    1919
    2020include "Cminor/toRTLabs.ma".
    21 include "RTLabs/semantics.ma".
     21include "RTLabs/RTLabs_semantics.ma".
    2222include "Clight/label.ma".
    2323
  • src/Clight/test/forcont.test.ma

    r2407 r2619  
    1414
    1515include "Clight/toCminor.ma".
    16 include "Cminor/semantics.ma".
     16include "Cminor/Cminor_semantics.ma".
    1717
    1818example e1: finishes_with (repr I32 9) ?
     
    2424
    2525include "Cminor/toRTLabs.ma".
    26 include "RTLabs/semantics.ma".
     26include "RTLabs/RTLabs_semantics.ma".
    2727include "Clight/label.ma".
    2828
  • src/Clight/test/goto-if.test.ma

    r2353 r2619  
    2323
    2424include "Clight/toCminor.ma".
    25 include "Cminor/semantics.ma".
     25include "Cminor/Cminor_semantics.ma".
    2626
    2727example e1: finishes_with (repr I32 0) ?
     
    3333
    3434include "Cminor/toRTLabs.ma".
    35 include "RTLabs/semantics.ma".
     35include "RTLabs/RTLabs_semantics.ma".
    3636
    3737example e2: finishes_with (repr I32 0) ? (
  • src/Clight/test/implicit.test.ma

    r2568 r2619  
    1414
    1515include "Clight/toCminor.ma".
    16 include "Cminor/semantics.ma".
     16include "Cminor/Cminor_semantics.ma".
    1717
    1818example e1: finishes_with (repr I32 10) ?
     
    2424
    2525include "Cminor/toRTLabs.ma".
    26 include "RTLabs/semantics.ma".
     26include "RTLabs/RTLabs_semantics.ma".
    2727include "Clight/label.ma".
    2828
  • src/Clight/test/implicitcond.test.ma

    r2568 r2619  
    1414
    1515include "Clight/toCminor.ma".
    16 include "Cminor/semantics.ma".
     16include "Cminor/Cminor_semantics.ma".
    1717
    1818example e1: finishes_with (repr I32 2) ?
     
    2424
    2525include "Cminor/toRTLabs.ma".
    26 include "RTLabs/semantics.ma".
     26include "RTLabs/RTLabs_semantics.ma".
    2727include "Clight/label.ma".
    2828
  • src/Clight/test/search.test.ma

    r2385 r2619  
    1212(* Check some individual passes. *)
    1313
    14 include "Cminor/semantics.ma".
     14include "Cminor/Cminor_semantics.ma".
    1515
    1616example e1: finishes_with (repr I32 3) ? (bind ? (snapshot state) (clight_to_cminor myprog) (λp. exec_up_to Cminor_fullexec p 1000 [ ])).
     
    1919qed.
    2020
    21 include "RTLabs/semantics.ma".
     21include "RTLabs/RTLabs_semantics.ma".
    2222
    2323example e2: finishes_with (repr 3) ? (
  • src/Clight/test/sum.test.ma

    r2353 r2619  
    1414
    1515include "Clight/toCminor.ma".
    16 include "Cminor/semantics.ma".
     16include "Cminor/Cminor_semantics.ma".
    1717
    1818example e1: finishes_with (repr I32 74) ?
     
    2424
    2525include "Cminor/toRTLabs.ma".
    26 include "RTLabs/semantics.ma".
     26include "RTLabs/RTLabs_semantics.ma".
    2727include "Clight/label.ma".
    2828
  • src/Clight/test/trivial.test.ma

    r2535 r2619  
    1414
    1515include "Clight/toCminor.ma".
    16 include "Cminor/semantics.ma".
     16include "Cminor/Cminor_semantics.ma".
    1717
    1818example e1: finishes_with (repr I32 0) ?
     
    2424
    2525include "Cminor/toRTLabs.ma".
    26 include "RTLabs/semantics.ma".
     26include "RTLabs/RTLabs_semantics.ma".
    2727include "Clight/label.ma".
    2828
     
    101101
    102102include "common/Measurable.ma".
    103 include "Clight/abstract.ma".
     103include "Clight/Clight_abstract.ma".
    104104
    105105definition Clight_pcs : preclassified_system ≝
     
    107107  clight_fullexec
    108108  (λ_.Clight_labelled)
    109   (λ_.Clight_classify).
     109  (λ_.Clight_classify)
     110  (λcosts,g,s,H. 1).
    110111
    111112lemma poke : ∀A,B:Prop. A → (A → B) → A ∧ B.
     
    115116example ms :
    116117 let 〈p0,init〉 ≝ clight_label myprog in
    117  measurable Clight_pcs p0 1 4 (λs,H. 1) 1.
     118 measurable Clight_pcs p0 1 4 (λfn. 1) 1.
    118119whd whd in match (state ????);
    119120% [2: % [2: % [2: % [2:
Note: See TracChangeset for help on using the changeset viewer.