Ignore:
Timestamp:
Mar 30, 2011, 6:47:35 PM (10 years ago)
Author:
campbell
Message:

Change identifiers to Words in Clight and RTLabs semantics.

File:
1 edited

Legend:

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

    r725 r726  
    22
    33definition myprog := mk_program clight_fundef type
    4   [〈succ_pos_of_nat 0 (* search *), CL_Internal (
    5      mk_function (Tint I8 Unsigned ) [〈succ_pos_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈succ_pos_of_nat 5, (Tint I8 Unsigned )〉 ; 〈succ_pos_of_nat 6, (Tint I8 Unsigned )〉 ] [〈succ_pos_of_nat 1, (Tint I8 Unsigned )〉 ; 〈succ_pos_of_nat 2, (Tint I8 Unsigned )〉 ; 〈succ_pos_of_nat 3, (Tint I8 Unsigned )〉 ]
     4  [〈ident_of_nat 0 (* search *), CL_Internal (
     5     mk_function (Tint I8 Unsigned ) [〈ident_of_nat 4, (Tpointer Any (Tint I8 Unsigned ))〉 ; 〈ident_of_nat 5, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 6, (Tint I8 Unsigned )〉 ] [〈ident_of_nat 1, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
    66       (Ssequence
    7        (Sassign (Expr (Evar (succ_pos_of_nat 1)) (Tint I8 Unsigned ))
     7       (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
    88         (Expr (Ecast (Tint I8 Unsigned )
    99           (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    1010           (Tint I8 Unsigned )))
    1111       (Ssequence
    12        (Sassign (Expr (Evar (succ_pos_of_nat 2)) (Tint I8 Unsigned ))
     12       (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    1313         (Expr (Ecast (Tint I8 Unsigned )
    1414           (Expr (Ebinop Osub
    1515             (Expr (Ecast (Tint I32 Signed  )
    16                (Expr (Evar (succ_pos_of_nat 5)) (Tint I8 Unsigned )))
     16               (Expr (Evar (ident_of_nat 5)) (Tint I8 Unsigned )))
    1717               (Tint I32 Signed  ))
    1818             (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     
    2222       (Swhile (Expr (Ebinop Oge
    2323                 (Expr (Ecast (Tint I32 Signed  )
    24                    (Expr (Evar (succ_pos_of_nat 2)) (Tint I8 Unsigned )))
     24                   (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    2525                   (Tint I32 Signed  ))
    2626                 (Expr (Ecast (Tint I32 Signed  )
    27                    (Expr (Evar (succ_pos_of_nat 1)) (Tint I8 Unsigned )))
     27                   (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    2828                   (Tint I32 Signed  ))) (Tint I32 Signed  ))
    2929         (Ssequence
    30          (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I8 Unsigned ))
     30         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    3131           (Expr (Ecast (Tint I8 Unsigned )
    3232             (Expr (Ebinop Odiv
    3333               (Expr (Ebinop Oadd
    3434                 (Expr (Ecast (Tint I32 Signed  )
    35                    (Expr (Evar (succ_pos_of_nat 2)) (Tint I8 Unsigned )))
     35                   (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
    3636                   (Tint I32 Signed  ))
    3737                 (Expr (Ecast (Tint I32 Signed  )
    38                    (Expr (Evar (succ_pos_of_nat 1)) (Tint I8 Unsigned )))
     38                   (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned )))
    3939                   (Tint I32 Signed  ))) (Tint I32 Signed  ))
    4040               (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
     
    4545                          (Expr (Ederef
    4646                            (Expr (Ebinop Oadd
    47                               (Expr (Evar (succ_pos_of_nat 4))
     47                              (Expr (Evar (ident_of_nat 4))
    4848                                (Tpointer Any (Tint I8 Unsigned )))
    49                               (Expr (Evar (succ_pos_of_nat 3))
     49                              (Expr (Evar (ident_of_nat 3))
    5050                                (Tint I8 Unsigned )))
    5151                              (Tpointer Any (Tint I8 Unsigned ))))
    5252                            (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    5353                        (Expr (Ecast (Tint I32 Signed  )
    54                           (Expr (Evar (succ_pos_of_nat 6))
     54                          (Expr (Evar (ident_of_nat 6))
    5555                            (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    5656                        (Tint I32 Signed  ))
    57            (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 3))
     57           (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
    5858                                 (Tint I8 Unsigned ))))
    5959           Sskip)
     
    6363                          (Expr (Ederef
    6464                            (Expr (Ebinop Oadd
    65                               (Expr (Evar (succ_pos_of_nat 4))
     65                              (Expr (Evar (ident_of_nat 4))
    6666                                (Tpointer Any (Tint I8 Unsigned )))
    67                               (Expr (Evar (succ_pos_of_nat 3))
     67                              (Expr (Evar (ident_of_nat 3))
    6868                                (Tint I8 Unsigned )))
    6969                              (Tpointer Any (Tint I8 Unsigned ))))
    7070                            (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    7171                        (Expr (Ecast (Tint I32 Signed  )
    72                           (Expr (Evar (succ_pos_of_nat 6))
     72                          (Expr (Evar (ident_of_nat 6))
    7373                            (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    7474                        (Tint I32 Signed  ))
    75            (Sassign (Expr (Evar (succ_pos_of_nat 2)) (Tint I8 Unsigned ))
     75           (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
    7676             (Expr (Ecast (Tint I8 Unsigned )
    7777               (Expr (Ebinop Osub
    7878                 (Expr (Ecast (Tint I32 Signed  )
    79                    (Expr (Evar (succ_pos_of_nat 3)) (Tint I8 Unsigned )))
     79                   (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    8080                   (Tint I32 Signed  ))
    8181                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     
    8686                          (Expr (Ederef
    8787                            (Expr (Ebinop Oadd
    88                               (Expr (Evar (succ_pos_of_nat 4))
     88                              (Expr (Evar (ident_of_nat 4))
    8989                                (Tpointer Any (Tint I8 Unsigned )))
    90                               (Expr (Evar (succ_pos_of_nat 3))
     90                              (Expr (Evar (ident_of_nat 3))
    9191                                (Tint I8 Unsigned )))
    9292                              (Tpointer Any (Tint I8 Unsigned ))))
    9393                            (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    9494                        (Expr (Ecast (Tint I32 Signed  )
    95                           (Expr (Evar (succ_pos_of_nat 6))
     95                          (Expr (Evar (ident_of_nat 6))
    9696                            (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    9797                        (Tint I32 Signed  ))
    98            (Sassign (Expr (Evar (succ_pos_of_nat 1)) (Tint I8 Unsigned ))
     98           (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I8 Unsigned ))
    9999             (Expr (Ecast (Tint I8 Unsigned )
    100100               (Expr (Ebinop Oadd
    101101                 (Expr (Ecast (Tint I32 Signed  )
    102                    (Expr (Evar (succ_pos_of_nat 3)) (Tint I8 Unsigned )))
     102                   (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    103103                   (Tint I32 Signed  ))
    104104                 (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     
    114114     
    115115   )〉;
    116   〈succ_pos_of_nat 7 (* main *), CL_Internal (
    117     mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈succ_pos_of_nat 8, (Tint I8 Unsigned )〉 ]
     116  〈ident_of_nat 7 (* main *), CL_Internal (
     117    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈ident_of_nat 8, (Tint I8 Unsigned )〉 ]
    118118      (Ssequence
    119119      (Sassign (Expr (Ederef
    120120                 (Expr (Ebinop Oadd
    121                    (Expr (Evar (succ_pos_of_nat 4))
     121                   (Expr (Evar (ident_of_nat 4))
    122122                     (Tarray Any (Tint I8 Unsigned ) 5))
    123123                   (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
     
    129129      (Sassign (Expr (Ederef
    130130                 (Expr (Ebinop Oadd
    131                    (Expr (Evar (succ_pos_of_nat 4))
     131                   (Expr (Evar (ident_of_nat 4))
    132132                     (Tarray Any (Tint I8 Unsigned ) 5))
    133133                   (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
     
    139139      (Sassign (Expr (Ederef
    140140                 (Expr (Ebinop Oadd
    141                    (Expr (Evar (succ_pos_of_nat 4))
     141                   (Expr (Evar (ident_of_nat 4))
    142142                     (Tarray Any (Tint I8 Unsigned ) 5))
    143143                   (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
     
    149149      (Sassign (Expr (Ederef
    150150                 (Expr (Ebinop Oadd
    151                    (Expr (Evar (succ_pos_of_nat 4))
     151                   (Expr (Evar (ident_of_nat 4))
    152152                     (Tarray Any (Tint I8 Unsigned ) 5))
    153153                   (Expr (Econst_int (repr 3)) (Tint I32 Signed  )))
     
    159159      (Sassign (Expr (Ederef
    160160                 (Expr (Ebinop Oadd
    161                    (Expr (Evar (succ_pos_of_nat 4))
     161                   (Expr (Evar (ident_of_nat 4))
    162162                     (Tarray Any (Tint I8 Unsigned ) 5))
    163163                   (Expr (Econst_int (repr 4)) (Tint I32 Signed  )))
     
    167167          (Tint I8 Unsigned )))
    168168      (Ssequence
    169       (Scall (Some expr (Expr (Evar (succ_pos_of_nat 8)) (Tint I8 Unsigned )))
    170         (Expr (Evar (succ_pos_of_nat 0))
     169      (Scall (Some expr (Expr (Evar (ident_of_nat 8)) (Tint I8 Unsigned )))
     170        (Expr (Evar (ident_of_nat 0))
    171171          (Tfunction (Tcons (Tpointer Any (Tint I8 Unsigned )) (Tcons (Tint I8 Unsigned ) (Tcons (Tint I8 Unsigned ) Tnil))) (Tint I8 Unsigned )))
    172         [(Expr (Evar (succ_pos_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5));
     172        [(Expr (Evar (ident_of_nat 4)) (Tarray Any (Tint I8 Unsigned ) 5));
    173173        (Expr (Ecast (Tint I8 Unsigned )
    174174          (Expr (Econst_int (repr 5)) (Tint I32 Signed  )))
     
    178178          (Tint I8 Unsigned ))])
    179179      (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
    180                             (Expr (Evar (succ_pos_of_nat 8))
     180                            (Expr (Evar (ident_of_nat 8))
    181181                              (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))))))
    182182   
     
    184184   
    185185  )〉]
    186   (succ_pos_of_nat 7)
     186  (ident_of_nat 7)
    187187  []
    188188.
     
    190190example exec: result ? (exec_up_to myprog 1000 [EVint (repr 0)]).
    191191normalize  (* you can examine the result here *)
     192%
     193qed.
Note: See TracChangeset for help on using the changeset viewer.