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

Last change on this file since 797 was 797, checked in by campbell, 9 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.