Changeset 750 for src/RTLabs/test


Ignore:
Timestamp:
Apr 12, 2011, 12:32:33 PM (9 years ago)
Author:
campbell
Message:

Track some of the changes to the prototype in RTLabs.

Just one register in each place now, f_ptrs is present but not checked.
The changes to memory quantities have been glossed over for now.
A new difference from the prototype: return registers are optional.

File:
1 edited

Legend:

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

    r737 r750  
    66
    77  definition id_search := ident_of_nat 0.
    8   definition search9 := 40.
    9   definition search8 := 39.
    10   definition search7 := 38.
    11   definition search6 := 37.
    12   definition search5 := 36.
     8  definition search9 := 53.
     9  definition search8 := 52.
     10  definition search7 := 51.
     11  definition search6 := 50.
     12  definition search53 := 49.
     13  definition search52 := 48.
     14  definition search51 := 47.
     15  definition search50 := 46.
     16  definition search5 := 45.
     17  definition search49 := 44.
     18  definition search48 := 43.
     19  definition search47 := 42.
     20  definition search46 := 41.
     21  definition search45 := 40.
     22  definition search44 := 39.
     23  definition search43 := 38.
     24  definition search42 := 37.
     25  definition search41 := 36.
    1326  definition search40 := 35.
    1427  definition search4 := 34.
     
    4861  definition search0 := 0.
    4962  definition C_cost0 := costlabel_of_nat 8.
    50   definition C_cost1 := costlabel_of_nat 7.
    51   definition C_cost8 := costlabel_of_nat 6.
     63  definition C_cost8 := costlabel_of_nat 7.
     64  definition C_cost1 := costlabel_of_nat 6.
    5265  definition C_cost6 := costlabel_of_nat 5.
    53   definition C_cost7 := costlabel_of_nat 4.
    54   definition C_cost4 := costlabel_of_nat 3.
     66  definition C_cost4 := costlabel_of_nat 4.
     67  definition C_cost7 := costlabel_of_nat 3.
    5568  definition C_cost5 := costlabel_of_nat 2.
    5669  definition C_cost2 := costlabel_of_nat 1.
     
    6073  definition pre_search := mk_pre_internal_function
    6174    (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint))
    62     (dp ?? 1 [[10]])
    63     [(dp ?? 2 [[9 ; 8]]); (dp ?? 1 [[2]]); (dp ?? 1 [[3]])]
    64     [(dp ?? 1 [[4]]); (dp ?? 1 [[5]]); (dp ?? 1 [[6]]); (dp ?? 1 [[7]]); (dp ?? 2 [[9 ; 8]]); (dp ?? 1 [[10]]); (dp ?? 1 [[11]]); (dp ?? 1 [[12]]); (dp ?? 1 [[13]]); (dp ?? 2 [[15 ; 14]]); (dp ?? 1 [[16]]); (dp ?? 1 [[17]]); (dp ?? 1 [[18]]); (dp ?? 1 [[19]]); (dp ?? 2 [[21 ; 20]]); (dp ?? 1 [[22]]); (dp ?? 1 [[23]]); (dp ?? 1 [[24]]); (dp ?? 2 [[26 ; 25]]); (dp ?? 1 [[27]]); (dp ?? 1 [[28]]); (dp ?? 1 [[29]]); (dp ?? 1 [[30]]); (dp ?? 1 [[31]]); (dp ?? 1 [[32]])]
     75    (Some ? 8)
     76    [7; 1; 2]
     77    [3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18; 19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34; 35; 36; 37; 38; 39; 40]
     78    [7; 15; 23; 29]
    6579    0
    6680    [
    67     (pair ?? search9 (make_St_cond2 (Ocmp Clt) (dp ?? 1 [[13]]) (dp ?? 1 [[3]]) search8 search5));
    68     (pair ?? search8 (make_St_cost C_cost0 search7));
    69     (pair ?? search7 (make_St_const (dp ?? 1 [[12]]) (Ointconst (repr 1)) search6));
    70     (pair ?? search6 (make_St_op2 Oadd (dp ?? 1 [[5]]) (dp ?? 1 [[7]]) (dp ?? 1 [[12]]) search4));
     81    (pair ?? search9 (make_St_cost C_cost0 search8));
     82    (pair ?? search8 (make_St_op1 Ocast8unsigned 10 6 search7));
     83    (pair ?? search7 (make_St_const 11 (Ointconst (repr 1)) search6));
     84    (pair ?? search6 (make_St_op2 Oadd 4 10 11 search4));
     85    (pair ?? search53 (make_St_cost C_cost8 search52));
     86    (pair ?? search52 (make_St_const 4 (Ointconst (repr 0)) search51));
     87    (pair ?? search51 (make_St_op1 Ocast8unsigned 39 1 search50));
     88    (pair ?? search50 (make_St_const 40 (Ointconst (repr 1)) search49));
    7189    (pair ?? search5 (make_St_cost C_cost1 search4));
    72     (pair ?? search40 (make_St_cost C_cost8 search39));
    73     (pair ?? search4 (make_St_skip search36));
    74     (pair ?? search39 (make_St_const (dp ?? 1 [[5]]) (Ointconst (repr 0)) search38));
    75     (pair ?? search38 (make_St_const (dp ?? 1 [[32]]) (Ointconst (repr 1)) search37));
    76     (pair ?? search37 (make_St_op2 Osub (dp ?? 1 [[6]]) (dp ?? 1 [[2]]) (dp ?? 1 [[32]]) search4));
    77     (pair ?? search36 (make_St_op2 (Ocmp Cge) (dp ?? 1 [[31]]) (dp ?? 1 [[6]]) (dp ?? 1 [[5]]) search35));
    78     (pair ?? search35 (make_St_cond1 Onotbool (dp ?? 1 [[31]]) search3 search34));
    79     (pair ?? search34 (make_St_cost C_cost6 search33));
    80     (pair ?? search33 (make_St_op2 Oadd (dp ?? 1 [[29]]) (dp ?? 1 [[6]]) (dp ?? 1 [[5]]) search32));
    81     (pair ?? search32 (make_St_const (dp ?? 1 [[30]]) (Ointconst (repr 2)) search31));
    82     (pair ?? search31 (make_St_op2 Odivu (dp ?? 1 [[7]]) (dp ?? 1 [[29]]) (dp ?? 1 [[30]]) search30));
    83     (pair ?? search30 (make_St_const (dp ?? 1 [[28]]) (Ointconst (repr 1)) search29));
     90    (pair ?? search49 (make_St_op2 Osub 5 39 40 search4));
     91    (pair ?? search48 (make_St_op1 Ocast8unsigned 37 5 search47));
     92    (pair ?? search47 (make_St_op1 Ocast8unsigned 38 4 search46));
     93    (pair ?? search46 (make_St_op2 (Ocmp Cge) 36 37 38 search45));
     94    (pair ?? search45 (make_St_cond1 Onotbool 36 search3 search44));
     95    (pair ?? search44 (make_St_cost C_cost6 search43));
     96    (pair ?? search43 (make_St_op1 Ocast8unsigned 34 5 search42));
     97    (pair ?? search42 (make_St_op1 Ocast8unsigned 35 4 search41));
     98    (pair ?? search41 (make_St_op2 Oadd 32 34 35 search40));
     99    (pair ?? search40 (make_St_const 33 (Ointconst (repr 2)) search39));
     100    (pair ?? search4 (make_St_skip search48));
     101    (pair ?? search39 (make_St_op2 Odiv 6 32 33 search38));
     102    (pair ?? search38 (make_St_const 31 (Ointconst (repr 1)) search37));
     103    (pair ?? search37 (make_St_op2 Omul 30 6 31 search36));
     104    (pair ?? search36 (make_St_op2 Oaddp 29 7 30 search35));
     105    (pair ?? search35 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[29]] 28 search34));
     106    (pair ?? search34 (make_St_op1 Ocast8unsigned 26 28 search33));
     107    (pair ?? search33 (make_St_op1 Ocast8unsigned 27 2 search32));
     108    (pair ?? search32 (make_St_cond2 (Ocmp Ceq) 26 27 search31 search29));
     109    (pair ?? search31 (make_St_cost C_cost4 search30));
     110    (pair ?? search30 (make_St_op1 Oid 8 6 search0));
    84111    (pair ?? search3 (make_St_cost C_cost7 search2));
    85     (pair ?? search29 (make_St_op2 Omul (dp ?? 1 [[27]]) (dp ?? 1 [[7]]) (dp ?? 1 [[28]]) search28));
    86     (pair ?? search28 (make_St_op2 Oaddp (dp ?? 2 [[26 ; 25]]) (dp ?? 2 [[9 ; 8]]) (dp ?? 1 [[27]]) search27));
    87     (pair ?? search27 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[26 ; 25]])]] (dp ?? 1 [[24]]) search26));
    88     (pair ?? search26 (make_St_cond2 (Ocmp Ceq) (dp ?? 1 [[24]]) (dp ?? 1 [[3]]) search25 search23));
    89     (pair ?? search25 (make_St_cost C_cost4 search24));
    90     (pair ?? search24 (make_St_op1 Oid (dp ?? 1 [[10]]) (dp ?? 1 [[7]]) search0));
    91     (pair ?? search23 (make_St_cost C_cost5 search22));
    92     (pair ?? search22 (make_St_const (dp ?? 1 [[23]]) (Ointconst (repr 1)) search21));
    93     (pair ?? search21 (make_St_op2 Omul (dp ?? 1 [[22]]) (dp ?? 1 [[7]]) (dp ?? 1 [[23]]) search20));
    94     (pair ?? search20 (make_St_op2 Oaddp (dp ?? 2 [[21 ; 20]]) (dp ?? 2 [[9 ; 8]]) (dp ?? 1 [[22]]) search19));
    95     (pair ?? search2 (make_St_const (dp ?? 1 [[11]]) (Ointconst (repr 1)) search1));
    96     (pair ?? search19 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[21 ; 20]])]] (dp ?? 1 [[19]]) search18));
    97     (pair ?? search18 (make_St_cond2 (Ocmp Cgt) (dp ?? 1 [[19]]) (dp ?? 1 [[3]]) search17 search14));
    98     (pair ?? search17 (make_St_cost C_cost2 search16));
    99     (pair ?? search16 (make_St_const (dp ?? 1 [[18]]) (Ointconst (repr 1)) search15));
    100     (pair ?? search15 (make_St_op2 Osub (dp ?? 1 [[6]]) (dp ?? 1 [[7]]) (dp ?? 1 [[18]]) search13));
    101     (pair ?? search14 (make_St_cost C_cost3 search13));
    102     (pair ?? search13 (make_St_const (dp ?? 1 [[17]]) (Ointconst (repr 1)) search12));
    103     (pair ?? search12 (make_St_op2 Omul (dp ?? 1 [[16]]) (dp ?? 1 [[7]]) (dp ?? 1 [[17]]) search11));
    104     (pair ?? search11 (make_St_op2 Oaddp (dp ?? 2 [[15 ; 14]]) (dp ?? 2 [[9 ; 8]]) (dp ?? 1 [[16]]) search10));
    105     (pair ?? search10 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[15 ; 14]])]] (dp ?? 1 [[13]]) search9));
    106     (pair ?? search1 (make_St_op1 Onegint (dp ?? 1 [[10]]) (dp ?? 1 [[11]]) search0));
    107     (pair ?? search0 (make_St_return (dp ?? 1 [[10]])))
     112    (pair ?? search29 (make_St_cost C_cost5 search28));
     113    (pair ?? search28 (make_St_const 25 (Ointconst (repr 1)) search27));
     114    (pair ?? search27 (make_St_op2 Omul 24 6 25 search26));
     115    (pair ?? search26 (make_St_op2 Oaddp 23 7 24 search25));
     116    (pair ?? search25 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[23]] 22 search24));
     117    (pair ?? search24 (make_St_op1 Ocast8unsigned 20 22 search23));
     118    (pair ?? search23 (make_St_op1 Ocast8unsigned 21 2 search22));
     119    (pair ?? search22 (make_St_cond2 (Ocmp Cgt) 20 21 search21 search17));
     120    (pair ?? search21 (make_St_cost C_cost2 search20));
     121    (pair ?? search20 (make_St_op1 Ocast8unsigned 18 6 search19));
     122    (pair ?? search2 (make_St_const 9 (Ointconst (repr 1)) search1));
     123    (pair ?? search19 (make_St_const 19 (Ointconst (repr 1)) search18));
     124    (pair ?? search18 (make_St_op2 Osub 5 18 19 search16));
     125    (pair ?? search17 (make_St_cost C_cost3 search16));
     126    (pair ?? search16 (make_St_const 17 (Ointconst (repr 1)) search15));
     127    (pair ?? search15 (make_St_op2 Omul 16 6 17 search14));
     128    (pair ?? search14 (make_St_op2 Oaddp 15 7 16 search13));
     129    (pair ?? search13 (make_St_load Mint8unsigned (Aindexed (repr 0)) [[15]] 14 search12));
     130    (pair ?? search12 (make_St_op1 Ocast8unsigned 12 14 search11));
     131    (pair ?? search11 (make_St_op1 Ocast8unsigned 13 2 search10));
     132    (pair ?? search10 (make_St_cond2 (Ocmp Clt) 12 13 search9 search5));
     133    (pair ?? search1 (make_St_op1 Onegint 8 9 search0));
     134    (pair ?? search0 (make_St_return 8))
    108135]
    109136
    110     search40
     137    search53
    111138    search0.
    112139
     
    159186  definition pre_main := mk_pre_internal_function
    160187    (mk_signature [] (Some ? ASTint))
    161     (dp ?? 1 [[2]])
     188    (Some ? 2)
    162189    []
    163     [(dp ?? 1 [[0]]); (dp ?? 1 [[1]]); (dp ?? 1 [[2]]); (dp ?? 2 [[4 ; 3]]); (dp ?? 1 [[5]]); (dp ?? 1 [[6]]); (dp ?? 2 [[8 ; 7]]); (dp ?? 1 [[9]]); (dp ?? 2 [[11 ; 10]]); (dp ?? 1 [[12]]); (dp ?? 1 [[13]]); (dp ?? 1 [[14]]); (dp ?? 2 [[16 ; 15]]); (dp ?? 1 [[17]]); (dp ?? 2 [[19 ; 18]]); (dp ?? 1 [[20]]); (dp ?? 1 [[21]]); (dp ?? 1 [[22]]); (dp ?? 2 [[24 ; 23]]); (dp ?? 1 [[25]]); (dp ?? 2 [[27 ; 26]]); (dp ?? 1 [[28]]); (dp ?? 1 [[29]]); (dp ?? 1 [[30]]); (dp ?? 2 [[32 ; 31]]); (dp ?? 1 [[33]]); (dp ?? 2 [[35 ; 34]]); (dp ?? 1 [[36]]); (dp ?? 1 [[37]]); (dp ?? 1 [[38]]); (dp ?? 2 [[40 ; 39]]); (dp ?? 1 [[41]]); (dp ?? 2 [[43 ; 42]]); (dp ?? 1 [[44]]); (dp ?? 1 [[45]]); (dp ?? 1 [[46]])]
     190    [0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18; 19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34; 35]
     191    [3; 6; 8; 12; 14; 18; 20; 24; 26; 30; 32]
    164192    5
    165193    [
    166     (pair ?? main9 (make_St_op2 Omul (dp ?? 1 [[12]]) (dp ?? 1 [[13]]) (dp ?? 1 [[14]]) main8));
    167     (pair ?? main8 (make_St_op2 Oaddp (dp ?? 2 [[8 ; 7]]) (dp ?? 2 [[11 ; 10]]) (dp ?? 1 [[12]]) main7));
    168     (pair ?? main7 (make_St_const (dp ?? 1 [[9]]) (Ointconst (repr 120)) main6));
    169     (pair ?? main6 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[8 ; 7]])]] (dp ?? 1 [[9]]) main5));
    170     (pair ?? main5 (make_St_const (dp ?? 2 [[4 ; 3]]) (Oaddrstack (repr 0)) main4));
     194    (pair ?? main9 (make_St_op2 Omul 9 10 11 main8));
     195    (pair ?? main8 (make_St_op2 Oaddp 6 8 9 main7));
     196    (pair ?? main7 (make_St_const 7 (Ointconst (repr 120)) main6));
     197    (pair ?? main6 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[6]] 7 main5));
     198    (pair ?? main5 (make_St_const 3 (Oaddrstack (repr 0)) main4));
    171199    (pair ?? main41 (make_St_cost C_cost9 main40));
    172     (pair ?? main40 (make_St_const (dp ?? 2 [[43 ; 42]]) (Oaddrstack (repr 0)) main39));
    173     (pair ?? main4 (make_St_const (dp ?? 1 [[5]]) (Ointconst (repr 5)) main3));
    174     (pair ?? main39 (make_St_const (dp ?? 1 [[45]]) (Ointconst (repr 0)) main38));
    175     (pair ?? main38 (make_St_const (dp ?? 1 [[46]]) (Ointconst (repr 1)) main37));
    176     (pair ?? main37 (make_St_op2 Omul (dp ?? 1 [[44]]) (dp ?? 1 [[45]]) (dp ?? 1 [[46]]) main36));
    177     (pair ?? main36 (make_St_op2 Oaddp (dp ?? 2 [[40 ; 39]]) (dp ?? 2 [[43 ; 42]]) (dp ?? 1 [[44]]) main35));
    178     (pair ?? main35 (make_St_const (dp ?? 1 [[41]]) (Ointconst (repr 0)) main34));
    179     (pair ?? main34 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[40 ; 39]])]] (dp ?? 1 [[41]]) main33));
    180     (pair ?? main33 (make_St_const (dp ?? 2 [[35 ; 34]]) (Oaddrstack (repr 0)) main32));
    181     (pair ?? main32 (make_St_const (dp ?? 1 [[37]]) (Ointconst (repr 1)) main31));
    182     (pair ?? main31 (make_St_const (dp ?? 1 [[38]]) (Ointconst (repr 1)) main30));
    183     (pair ?? main30 (make_St_op2 Omul (dp ?? 1 [[36]]) (dp ?? 1 [[37]]) (dp ?? 1 [[38]]) main29));
    184     (pair ?? main3 (make_St_const (dp ?? 1 [[6]]) (Ointconst (repr 57)) main2));
    185     (pair ?? main29 (make_St_op2 Oaddp (dp ?? 2 [[32 ; 31]]) (dp ?? 2 [[35 ; 34]]) (dp ?? 1 [[36]]) main28));
    186     (pair ?? main28 (make_St_const (dp ?? 1 [[33]]) (Ointconst (repr 18)) main27));
    187     (pair ?? main27 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[32 ; 31]])]] (dp ?? 1 [[33]]) main26));
    188     (pair ?? main26 (make_St_const (dp ?? 2 [[27 ; 26]]) (Oaddrstack (repr 0)) main25));
    189     (pair ?? main25 (make_St_const (dp ?? 1 [[29]]) (Ointconst (repr 2)) main24));
    190     (pair ?? main24 (make_St_const (dp ?? 1 [[30]]) (Ointconst (repr 1)) main23));
    191     (pair ?? main23 (make_St_op2 Omul (dp ?? 1 [[28]]) (dp ?? 1 [[29]]) (dp ?? 1 [[30]]) main22));
    192     (pair ?? main22 (make_St_op2 Oaddp (dp ?? 2 [[24 ; 23]]) (dp ?? 2 [[27 ; 26]]) (dp ?? 1 [[28]]) main21));
    193     (pair ?? main21 (make_St_const (dp ?? 1 [[25]]) (Ointconst (repr 23)) main20));
    194     (pair ?? main20 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[24 ; 23]])]] (dp ?? 1 [[25]]) main19));
    195     (pair ?? main2 (make_St_call_id id_search [(dp ?? 2 [[4 ; 3]]); (dp ?? 1 [[5]]); (dp ?? 1 [[6]])] (dp ?? 1 [[1]]) (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint)) main1));
    196     (pair ?? main19 (make_St_const (dp ?? 2 [[19 ; 18]]) (Oaddrstack (repr 0)) main18));
    197     (pair ?? main18 (make_St_const (dp ?? 1 [[21]]) (Ointconst (repr 3)) main17));
    198     (pair ?? main17 (make_St_const (dp ?? 1 [[22]]) (Ointconst (repr 1)) main16));
    199     (pair ?? main16 (make_St_op2 Omul (dp ?? 1 [[20]]) (dp ?? 1 [[21]]) (dp ?? 1 [[22]]) main15));
    200     (pair ?? main15 (make_St_op2 Oaddp (dp ?? 2 [[16 ; 15]]) (dp ?? 2 [[19 ; 18]]) (dp ?? 1 [[20]]) main14));
    201     (pair ?? main14 (make_St_const (dp ?? 1 [[17]]) (Ointconst (repr 57)) main13));
    202     (pair ?? main13 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[(dp ?? 2 [[16 ; 15]])]] (dp ?? 1 [[17]]) main12));
    203     (pair ?? main12 (make_St_const (dp ?? 2 [[11 ; 10]]) (Oaddrstack (repr 0)) main11));
    204     (pair ?? main11 (make_St_const (dp ?? 1 [[13]]) (Ointconst (repr 4)) main10));
    205     (pair ?? main10 (make_St_const (dp ?? 1 [[14]]) (Ointconst (repr 1)) main9));
    206     (pair ?? main1 (make_St_op1 Oid (dp ?? 1 [[2]]) (dp ?? 1 [[1]]) main0));
    207     (pair ?? main0 (make_St_return (dp ?? 1 [[2]])))
     200    (pair ?? main40 (make_St_const 32 (Oaddrstack (repr 0)) main39));
     201    (pair ?? main4 (make_St_const 4 (Ointconst (repr 5)) main3));
     202    (pair ?? main39 (make_St_const 34 (Ointconst (repr 0)) main38));
     203    (pair ?? main38 (make_St_const 35 (Ointconst (repr 1)) main37));
     204    (pair ?? main37 (make_St_op2 Omul 33 34 35 main36));
     205    (pair ?? main36 (make_St_op2 Oaddp 30 32 33 main35));
     206    (pair ?? main35 (make_St_const 31 (Ointconst (repr 0)) main34));
     207    (pair ?? main34 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[30]] 31 main33));
     208    (pair ?? main33 (make_St_const 26 (Oaddrstack (repr 0)) main32));
     209    (pair ?? main32 (make_St_const 28 (Ointconst (repr 1)) main31));
     210    (pair ?? main31 (make_St_const 29 (Ointconst (repr 1)) main30));
     211    (pair ?? main30 (make_St_op2 Omul 27 28 29 main29));
     212    (pair ?? main3 (make_St_const 5 (Ointconst (repr 57)) main2));
     213    (pair ?? main29 (make_St_op2 Oaddp 24 26 27 main28));
     214    (pair ?? main28 (make_St_const 25 (Ointconst (repr 18)) main27));
     215    (pair ?? main27 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[24]] 25 main26));
     216    (pair ?? main26 (make_St_const 20 (Oaddrstack (repr 0)) main25));
     217    (pair ?? main25 (make_St_const 22 (Ointconst (repr 2)) main24));
     218    (pair ?? main24 (make_St_const 23 (Ointconst (repr 1)) main23));
     219    (pair ?? main23 (make_St_op2 Omul 21 22 23 main22));
     220    (pair ?? main22 (make_St_op2 Oaddp 18 20 21 main21));
     221    (pair ?? main21 (make_St_const 19 (Ointconst (repr 23)) main20));
     222    (pair ?? main20 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[18]] 19 main19));
     223    (pair ?? main2 (make_St_call_id id_search [3; 4; 5] (Some ? 1) (mk_signature [ASTptr Any; ASTint; ASTint] (Some ? ASTint)) main1));
     224    (pair ?? main19 (make_St_const 14 (Oaddrstack (repr 0)) main18));
     225    (pair ?? main18 (make_St_const 16 (Ointconst (repr 3)) main17));
     226    (pair ?? main17 (make_St_const 17 (Ointconst (repr 1)) main16));
     227    (pair ?? main16 (make_St_op2 Omul 15 16 17 main15));
     228    (pair ?? main15 (make_St_op2 Oaddp 12 14 15 main14));
     229    (pair ?? main14 (make_St_const 13 (Ointconst (repr 57)) main13));
     230    (pair ?? main13 (make_St_store Mint8unsigned (Aindexed (repr 0)) [[12]] 13 main12));
     231    (pair ?? main12 (make_St_const 8 (Oaddrstack (repr 0)) main11));
     232    (pair ?? main11 (make_St_const 10 (Ointconst (repr 4)) main10));
     233    (pair ?? main10 (make_St_const 11 (Ointconst (repr 1)) main9));
     234    (pair ?? main1 (make_St_op1 Ocast8unsigned 2 1 main0));
     235    (pair ?? main0 (make_St_return 2))
    208236]
    209237
     
    226254).
    227255
    228    example exec: result ? (do p ← prog; do r ← exec_up_to RTLabs_fullexec p 100 [ ]; OK ? r).
     256   example exec: finishes_with (repr 3) ? (do p ← prog; do r ← exec_up_to RTLabs_fullexec p 1000 [ ]; OK ? r).
    229257   normalize  (* you can examine the result here *)
    230    % qed.
     258   @refl qed.
Note: See TracChangeset for help on using the changeset viewer.