Last change
on this file since 717 was
717,
checked in by campbell, 10 years ago
|
Clean up Clight examples; better temporary definition of multiply.
|
File size:
1.5 KB
|
Rev | Line | |
---|
[717] | 1 | include "Clight/Animation.ma". |
---|
| 2 | |
---|
| 3 | definition myprog := mk_program fundef type |
---|
| 4 | [〈succ_pos_of_nat 0 (* dosomething *), External (succ_pos_of_nat 0) (Tcons (Tint I32 Signed ) Tnil) (Tint I32 Signed )〉; |
---|
| 5 | 〈succ_pos_of_nat 1 (* main *), 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 | |
---|
| 31 | example 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〉. |
---|
| 34 | normalize (* you can examine the result here *) |
---|
| 35 | @refl |
---|
| 36 | qed. |
---|
Note: See
TracBrowser
for help on using the repository browser.