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

Last change on this file since 881 was 881, checked in by campbell, 9 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.