Ignore:
Timestamp:
Mar 29, 2011, 5:54:36 PM (9 years ago)
Author:
campbell
Message:

Clean up Clight examples; better temporary definition of multiply.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/test/factorial.ma

    r415 r717  
    1 include "Animation.ma".
     1include "Clight/Animation.ma".
    22
    3 ndefinition myprog := mk_program fundef type
    4  [mk_pair ?? (succ_pos_of_nat 132 (* get_input *)) (External (succ_pos_of_nat 132) Tnil (Tint I32 Signed  ));
    5   mk_pair ?? (succ_pos_of_nat 133 (* main *)) (Internal (
    6     mk_function (Tint I32 Signed  ) [] [mk_pair ?? (succ_pos_of_nat 134) (Tint I32 Signed  ); mk_pair ?? (succ_pos_of_nat 135) (Tint I32 Signed  ); mk_pair ?? (succ_pos_of_nat 136) (Tint I32 Signed  )]
     3definition myprog := mk_program fundef type
     4  [〈succ_pos_of_nat 0 (* get_input *), External (succ_pos_of_nat 0) 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  )〉 ; 〈succ_pos_of_nat 4, (Tint I32 Signed  )〉 ]
    77      (Ssequence
    8       (Scall (Some ? (Expr (Evar (succ_pos_of_nat 134)) (Tint I32 Signed  )))
    9         (Expr (Evar (succ_pos_of_nat 132))
     8      (Scall (Some expr (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  )))
     9        (Expr (Evar (succ_pos_of_nat 0))
    1010          (Tfunction Tnil (Tint I32 Signed  )))
    1111        [])
    1212      (Ssequence
    13       (Sassign (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed  ))
     13      (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
    1414        (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    1515      (Ssequence
    16       (Sfor (Sassign (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  ))
     16      (Ssequence
     17      (Sfor (Sassign (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
    1718              (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    1819        (Expr (Ebinop Ole
    19           (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  ))
    20           (Expr (Evar (succ_pos_of_nat 134)) (Tint I32 Signed  )))
     20          (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
     21          (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  )))
    2122          (Tint I32 Signed  ))
    22         (Sassign (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  ))
     23        (Sassign (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
    2324          (Expr (Ebinop Oadd
    24             (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  ))
     25            (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
    2526            (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    2627            (Tint I32 Signed  )))
    27         (Sassign (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed  ))
     28        (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
    2829          (Expr (Ebinop Omul
    29             (Expr (Evar (succ_pos_of_nat 135)) (Tint I32 Signed  ))
    30             (Expr (Evar (succ_pos_of_nat 136)) (Tint I32 Signed  )))
     30            (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
     31            (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  )))
    3132            (Tint I32 Signed  )))
    3233      )
    33       (Sreturn (Some ? (Expr (Evar (succ_pos_of_nat 135))
    34                          (Tint I32 Signed  )))))))
     34      Sskip)
     35      (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 3))
     36                            (Tint I32 Signed  )))))))
    3537   
    3638   
    3739   
    38   ))]
    39   (succ_pos_of_nat 133)
     40  )]
     41  (succ_pos_of_nat 1)
    4042  []
    4143.
    4244
    43 nremark exec: result ? (exec_up_to myprog 40 [EVint (repr 5)]).
    44 nnormalize;  (* you can examine the result here *)
    45 @; nqed.
     45example exec:
     46  (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 5)]; OK ? (is_final s)) = OK ? (Some ? (repr 120)).
     47normalize  (* you can examine the result here *)
     48@refl qed.
Note: See TracChangeset for help on using the changeset viewer.