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

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

Change identifiers to Words in Clight and RTLabs semantics.

File size: 1.5 KB
Line 
1include "Clight/Animation.ma".
2
3definition myprog := mk_program clight_fundef type
4  [〈ident_of_nat 0 (* dosomething *), CL_External (ident_of_nat 0) (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )〉;
5  〈ident_of_nat 1 (* main *), CL_Internal (
6    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I32 Signed  )〉 ]
7      (Ssequence
8      (Sassign (Expr (Evar (ident_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 (ident_of_nat 3)) (Tint I32 Signed  )))
13        (Expr (Evar (ident_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 (ident_of_nat 2)) (Tint I32 Signed  ))
17        (Expr (Ebinop Oadd
18          (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
19          (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))
20          (Tint I32 Signed  ))))
21      (Sreturn (Some expr (Expr (Evar (ident_of_nat 2))
22                            (Tint I32 Signed  ))))))
23   
24   
25   
26  )〉]
27  (ident_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 (ident_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.