Changeset 726 for src/Clight/test/io.ma


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

    r725 r726  
    22
    33definition myprog := mk_program clight_fundef type
    4   [〈succ_pos_of_nat 0 (* dosomething *), CL_External (succ_pos_of_nat 0) (Tcons (Tint I32 Signed  ) 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  )〉 ]
     4  [〈ident_of_nat 0 (* dosomething *), CL_External (ident_of_nat 0) (Tcons (Tint I32 Signed  ) 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  )〉 ]
    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 (Tcons (Tint I32 Signed  ) Tnil) (Tint I32 Signed  )))
    1111        [(Expr (Econst_int (repr 10)) (Tint I32 Signed  ))])
    12       (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 2))
     12      (Sreturn (Some expr (Expr (Evar (ident_of_nat 2))
    1313                            (Tint I32 Signed  )))))
    1414   
     
    1616   
    1717  )〉]
    18   (succ_pos_of_nat 1)
     18  (ident_of_nat 1)
    1919  []
    2020.
     
    2222example exec:
    2323 (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 7)]; do r ← opt_to_res … (is_final s); OK ? 〈t,r〉) =
    24  OK ? 〈[EVextcall (succ_pos_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
     24 OK ? 〈[EVextcall (ident_of_nat 0) [EVint (repr 10)] (EVint (repr 7))], repr 7〉.
    2525normalize  (* you can examine the result here *)
    2626@refl
Note: See TracChangeset for help on using the changeset viewer.