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

Last change on this file since 731 was 731, checked in by campbell, 9 years ago

Common definition for animation semantics, and factor out IO definitions.

File size: 1.1 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.
Note: See TracBrowser for help on using the repository browser.