source: src/Clight/test/io.ma @ 881

Last change on this file since 881 was 881, checked in by campbell, 10 years ago

Sort out regions in Cminor to fix Clight to Cminor translation of Ederef.

File size: 1.9 KB
Line 
1include "Clight/Cexec.ma".
2include "common/Animation.ma".
3
4definition myprog := mk_program clight_fundef type
5  [〈ident_of_nat 0 (* dosomething *), CL_External (ident_of_nat 0) (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )〉;
6  〈ident_of_nat 1 (* main *), CL_Internal (
7    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ]
8      (Ssequence
9      (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
10        (Expr (Evar (ident_of_nat 0))
11          (Tfunction (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )))
12        [(Expr (Econst_int (repr 10)) (Tint I32 Signed  ))])
13      (Sreturn (Some expr (Expr (Evar (ident_of_nat 2))
14                            (Tint I32 Signed  )))))
15   
16   
17   
18  )〉]
19  (ident_of_nat 1)
20  []
21.
22
23example exec:
24 (do r ← exec_up_to clight_fullexec myprog 1000 [EVint (repr 7)];
25  match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? [ ] ]) =
26 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
27normalize  (* you can examine the result here *)
28@refl
29qed.
30
31
32include "Clight/toCminor.ma".
33include "Cminor/semantics.ma".
34
35example e1: (do p ← clight_to_cminor myprog;
36             do r ← exec_up_to Cminor_fullexec p 1000 [EVint (repr 7) ];
37             match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? [ ] ]) =
38 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
39normalize
40@refl
41qed.
42
43include "Cminor/toRTLabs.ma".
44include "RTLabs/semantics.ma".
45
46example e2: (do p1 ← clight_to_cminor myprog;
47             do p2 ← cminor_to_rtlabs p1;
48             do r ← exec_up_to RTLabs_fullexec p2 1000 [EVint (repr 7) ];
49             match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? [ ] ]) =
50 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
51normalize
52@refl
53qed.
Note: See TracBrowser for help on using the repository browser.