Changeset 1157 for src/Clight


Ignore:
Timestamp:
Aug 31, 2011, 12:15:39 PM (9 years ago)
Author:
campbell
Message:

Update pretty printers and examples.

Location:
src/Clight
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/clightPrintMatita.ml

    r965 r1157  
    367367
    368368let print_globvar p (((id, init), ty)) =
    369   fprintf p "@[<hov 2>〈〈〈ident_of_nat %i (* %s *),@ %a〉,@ Any〉,@ %s〉@]"
     369  fprintf p "@[<hov 2>〈〈ident_of_nat %i (* %s *),@ Any〉,@ 〈%a,@ %s〉〉@]"
    370370    (id_i id)
    371371    id
     
    466466  collect_program prog;
    467467  fprintf p "include \"Clight/Cexec.ma\".@\ninclude \"common/Animation.ma\".@\n@\n";
    468   fprintf p "@[<v 2>definition myprog := mk_program clight_fundef type@ ";
     468  fprintf p "@[<v 2>definition myprog := mk_program clight_fundef ((list init_data) × type)@ ";
    469469(*  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
    470470  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
  • src/Clight/test/duff.c.ma

    r965 r1157  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef type
     4definition myprog := mk_program clight_fundef ((list init_data) × type)
    55  [〈ident_of_nat 0 (* copy *), CL_Internal (
    66     mk_function Tvoid [〈ident_of_nat 19, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 20, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 21, (Tint I32 Signed  )〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 4, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 5, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 7, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 8, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 9, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 10, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 11, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 12, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 13, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 14, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 15, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 16, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 17, (Tpointer Any (Tint I16 Signed  ))〉 ; 〈ident_of_nat 18, (Tpointer Any (Tint I16 Signed  ))〉 ]
     
    409409
    410410example exec: finishes_with (repr I32 6) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    411 normalize @refl
     411normalize  (* you can examine the result here *)
     412@refl
    412413qed.
  • src/Clight/test/factorial.c.ma

    r978 r1157  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef type
     4definition myprog := mk_program clight_fundef ((list init_data) × type)
    55  [〈ident_of_nat 0 (* get_input *), CL_External (ident_of_nat 0) Tnil (Tint I32 Signed  )〉;
    66  〈ident_of_nat 1 (* main *), CL_Internal (
     
    4141example exec: finishes_with (repr I32 120) ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr ? 5)]).
    4242normalize  (* you can examine the result here *)
    43 @refl qed.
     43@refl
     44qed.
Note: See TracChangeset for help on using the changeset viewer.