Ignore:
Timestamp:
Nov 17, 2011, 4:50:46 PM (9 years ago)
Author:
campbell
Message:

Fix up Clight examples.

File:
1 edited

Legend:

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

    r1157 r1513  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef ((list init_data) × type)
    5   [〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) 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  )〉 ; 〈ident_of_nat 4, (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)) (Tfunction Tnil (Tint I32 Signed  )))
    11         [])
    12       (Ssequence
    13       (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    14         (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    15       (Ssequence
    16       (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    17               (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
    18         (Expr (Ebinop Ole (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    19           (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    20           (Tint I32 Signed  ))
    21         (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    22           (Expr (Ebinop Oadd
     4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
     5  [][〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) 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  )〉 ; 〈ident_of_nat 4, (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)) (Tfunction Tnil (Tint I32 Signed  )))
     11          [])
     12        (Ssequence
     13        (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
     14          (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     15        (Ssequence
     16        (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
     17                (Expr (Econst_int I32 (repr ? 2)) (Tint I32 Signed  )))
     18          (Expr (Ebinop Ole
    2319            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    24             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    25             (Tint I32 Signed  )))
    26         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    27           (Expr (Ebinop Omul
    28             (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    29             (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  )))
    30             (Tint I32 Signed  )))
    31       )
    32       (Sreturn (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))))))
    33    
    34    
    35    
    36   )〉]
     20            (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
     21            (Tint I32 Signed  ))
     22          (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
     23            (Expr (Ebinop Oadd
     24              (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
     25              (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
     26              (Tint I32 Signed  )))
     27          (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
     28            (Expr (Ebinop Omul
     29              (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
     30              (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  )))
     31              (Tint I32 Signed  )))
     32        )
     33        (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
     34                              (Tint I32 Signed  )))))))
     35     
     36     
     37     
     38    )〉]
    3739  (ident_of_nat 1)
    38   []
     40 
    3941.
    4042
    41 example exec: finishes_with (repr I32 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
     43(*
     44example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    4245normalize  (* you can examine the result here *)
    43 @refl
    44 qed.
     46*)
Note: See TracChangeset for help on using the changeset viewer.