|
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.1 KB
|
| Line | |
|---|
| 1 | include "Clight/Cexec.ma". |
|---|
| 2 | include "common/Animation.ma". |
|---|
| 3 | |
|---|
| 4 | definition 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 )〉 ] |
|---|
| 8 | (Ssequence |
|---|
| 9 | (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed ))) |
|---|
| 10 | (Expr (Evar (ident_of_nat 0)) |
|---|
| 11 | (Tfunction (Tcons (Tint I32 Signed ) Tnil) (Tint I32 Signed ))) |
|---|
| 12 | [(Expr (Econst_int (repr 10)) (Tint I32 Signed ))]) |
|---|
| 13 | (Sreturn (Some expr (Expr (Evar (ident_of_nat 2)) |
|---|
| 14 | (Tint I32 Signed ))))) |
|---|
| 15 | |
|---|
| 16 | |
|---|
| 17 | |
|---|
| 18 | )〉] |
|---|
| 19 | (ident_of_nat 1) |
|---|
| 20 | [] |
|---|
| 21 | . |
|---|
| 22 | |
|---|
| 23 | example exec: |
|---|
| 24 | (do r ← exec_up_to clight_fullexec myprog 1000 [EVint (repr 7)]; |
|---|
| 25 | match r with [ finished t r _ ⇒ OK ? 〈t,r〉 | _ ⇒ Error ? [ ] ]) = |
|---|
| 26 | OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉. |
|---|
| 27 | normalize (* you can examine the result here *) |
|---|
| 28 | @refl |
|---|
| 29 | qed. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
