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

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

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

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