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

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

Clean up Clight examples; better temporary definition of multiply.

File size: 1.0 KB
RevLine 
[717]1include "Clight/Animation.ma".
2
3definition myprog := mk_program fundef type
4  [〈succ_pos_of_nat 0 (* dosomething *), External (succ_pos_of_nat 0) (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )〉;
5  〈succ_pos_of_nat 1 (* main *), Internal (
6    mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 2, (Tint I32 Signed  )〉 ]
7      (Ssequence
8      (Scall (Some expr (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  )))
9        (Expr (Evar (succ_pos_of_nat 0))
10          (Tfunction (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )))
11        [(Expr (Econst_int (repr 10)) (Tint I32 Signed  ))])
12      (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 2))
13                            (Tint I32 Signed  )))))
14   
15   
16   
17  )〉]
18  (succ_pos_of_nat 1)
19  []
20.
21
22example exec:
23 (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 7)]; do r ← opt_to_res … (is_final s); OK ? 〈t,r〉) =
24 OK ? 〈[EVextcall (succ_pos_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
25normalize  (* you can examine the result here *)
26@refl
27qed.
Note: See TracBrowser for help on using the repository browser.