Ignore:
Timestamp:
Jun 16, 2011, 1:32:19 PM (9 years ago)
Author:
campbell
Message:

Update remaining Clight examples.

File:
1 moved

Legend:

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

    r975 r978  
    88      (Ssequence
    99      (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    10         (Expr (Evar (ident_of_nat 0))
    11           (Tfunction Tnil (Tint I32 Signed  )))
     10        (Expr (Evar (ident_of_nat 0)) (Tfunction Tnil (Tint I32 Signed  )))
    1211        [])
    1312      (Ssequence
    1413      (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    15         (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    16       (Ssequence
     14        (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    1715      (Ssequence
    1816      (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    19               (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    20         (Expr (Ebinop Ole
    21           (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  ))
    2219          (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    2320          (Tint I32 Signed  ))
     
    2522          (Expr (Ebinop Oadd
    2623            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    27             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     24            (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    2825            (Tint I32 Signed  )))
    2926        (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
     
    3330            (Tint I32 Signed  )))
    3431      )
    35       Sskip)
    36       (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
    37                             (Tint I32 Signed  )))))))
     32      (Sreturn (Some expr (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  )))))))
    3833   
    3934   
     
    4439.
    4540
    46 example exec: finishes_with (repr 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 5)]).
     41example exec: finishes_with (repr I32 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
    4742normalize  (* you can examine the result here *)
    4843@refl qed.
Note: See TracChangeset for help on using the changeset viewer.