source: src/Clight/test/io2.ma @ 781

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

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

File size: 1.5 KB
RevLine 
[731]1include "Clight/Cexec.ma".
2include "common/Animation.ma".
[717]3
[725]4definition myprog := mk_program clight_fundef type
[726]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  )〉 ; 〈ident_of_nat 3, (Tint I32 Signed  )〉 ]
[717]8      (Ssequence
[726]9      (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
[717]10        (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
11      (Ssequence
12      (Ssequence
[726]13      (Scall (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))
14        (Expr (Evar (ident_of_nat 0))
[717]15          (Tfunction (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )))
16        [(Expr (Econst_int (repr 10)) (Tint I32 Signed  ))])
[726]17      (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
[717]18        (Expr (Ebinop Oadd
[726]19          (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
20          (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))
[717]21          (Tint I32 Signed  ))))
[726]22      (Sreturn (Some expr (Expr (Evar (ident_of_nat 2))
[717]23                            (Tint I32 Signed  ))))))
24   
25   
26   
27  )〉]
[726]28  (ident_of_nat 1)
[717]29  []
30.
31
32example exec:
[731]33 (do r ← exec_up_to clight_fullexec myprog 1000 [EVint (repr 7)];
34   match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? ]) =
[726]35 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 9〉.
[717]36normalize  (* you can examine the result here *)
37@refl
38qed.
Note: See TracBrowser for help on using the repository browser.