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/factorial.ma

    r725 r726  
    22
    33definition myprog := mk_program clight_fundef type
    4   [〈succ_pos_of_nat 0 (* get_input *), CL_External (succ_pos_of_nat 0) Tnil (Tint I32 Signed  )〉;
    5   〈succ_pos_of_nat 1 (* main *), CL_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  )〉 ]
     4  [〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
     5  〈ident_of_nat 1 (* main *), CL_Internal (
     6    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  )〉 ]
    77      (Ssequence
    8       (Scall (Some expr (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  )))
    9         (Expr (Evar (succ_pos_of_nat 0))
     8      (Scall (Some expr (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
     9        (Expr (Evar (ident_of_nat 0))
    1010          (Tfunction Tnil (Tint I32 Signed  )))
    1111        [])
    1212      (Ssequence
    13       (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
     13      (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    1414        (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    1515      (Ssequence
    1616      (Ssequence
    17       (Sfor (Sassign (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
     17      (Sfor (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    1818              (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
    1919        (Expr (Ebinop Ole
    20           (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
    21           (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  )))
     20          (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
     21          (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    2222          (Tint I32 Signed  ))
    23         (Sassign (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
     23        (Sassign (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    2424          (Expr (Ebinop Oadd
    25             (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
     25            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  ))
    2626            (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    2727            (Tint I32 Signed  )))
    28         (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
     28        (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
    2929          (Expr (Ebinop Omul
    30             (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
    31             (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  )))
     30            (Expr (Evar (ident_of_nat 3)) (Tint I32 Signed  ))
     31            (Expr (Evar (ident_of_nat 4)) (Tint I32 Signed  )))
    3232            (Tint I32 Signed  )))
    3333      )
    3434      Sskip)
    35       (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 3))
     35      (Sreturn (Some expr (Expr (Evar (ident_of_nat 3))
    3636                            (Tint I32 Signed  )))))))
    3737   
     
    3939   
    4040  )〉]
    41   (succ_pos_of_nat 1)
     41  (ident_of_nat 1)
    4242  []
    4343.
Note: See TracChangeset for help on using the changeset viewer.