Ignore:
Timestamp:
Mar 30, 2011, 4:16:08 PM (9 years ago)
Author:
campbell
Message:

Do some light manual disambiguation to make Clight examples go through more
easily.

File:
1 edited

Legend:

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

    r717 r725  
    11include "Clight/Animation.ma".
    22
    3 definition myprog := mk_program fundef type
    4   [〈succ_pos_of_nat 0 (* search *), Internal (
     3definition myprog := mk_program clight_fundef type
     4  [〈succ_pos_of_nat 0 (* search *), CL_Internal (
    55     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 )〉 ]
    66       (Ssequence
     
    114114     
    115115   )〉;
    116   〈succ_pos_of_nat 7 (* main *), Internal (
     116  〈succ_pos_of_nat 7 (* main *), CL_Internal (
    117117    mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 4, (Tarray Any (Tint I8 Unsigned ) 5)〉 ; 〈succ_pos_of_nat 8, (Tint I8 Unsigned )〉 ]
    118118      (Ssequence
Note: See TracChangeset for help on using the changeset viewer.