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

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

Do some light manual disambiguation to make Clight examples go through more
easily.

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