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

    r725 r726  
    22
    33definition myprog := mk_program clight_fundef type
    4   [〈succ_pos_of_nat 0 (* insert *), CL_Internal (
    5      mk_function Tvoid [〈succ_pos_of_nat 2, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ; 〈succ_pos_of_nat 6, (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))〉 ] [〈succ_pos_of_nat 1, (Tint I32 Signed  )〉 ]
     4  [〈ident_of_nat 0 (* insert *), CL_Internal (
     5     mk_function Tvoid [〈ident_of_nat 2, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 6, (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ]
    66       (Ssequence
    77       (Sifthenelse (Expr (Ebinop Oeq
    88                      (Expr (Ederef
    9                         (Expr (Evar (succ_pos_of_nat 6))
    10                           (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    11                         (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
    12                       (Expr (Ecast (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))
     9                        (Expr (Evar (ident_of_nat 6))
     10                          (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     11                        (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
     12                      (Expr (Ecast (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))
    1313                        (Expr (Ecast (Tpointer Any Tvoid)
    1414                          (Expr (Econst_int (repr 0)) (Tint I32 Unsigned)))
    1515                          (Tpointer Any Tvoid)))
    16                         (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
     16                        (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
    1717                      (Tint I32 Signed  ))
    18          (Sassign (Expr (Evar (succ_pos_of_nat 1)) (Tint I32 Signed  ))
     18         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    1919           (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
    20          (Sassign (Expr (Evar (succ_pos_of_nat 1)) (Tint I32 Signed  ))
     20         (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    2121           (Expr (Ebinop One
    2222             (Expr (Ebinop Oge
     
    2424                 (Expr (Efield (Expr (Ederef
    2525                                 (Expr (Ederef
    26                                    (Expr (Evar (succ_pos_of_nat 6))
    27                                      (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    28                                    (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    29                                  (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 4))
     26                                   (Expr (Evar (ident_of_nat 6))
     27                                     (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     28                                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     29                                 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))
    3030                   (Tint I8 Unsigned ))) (Tint I32 Signed  ))
    3131               (Expr (Ecast (Tint I32 Signed  )
    3232                 (Expr (Efield (Expr (Ederef
    33                                  (Expr (Evar (succ_pos_of_nat 2))
    34                                    (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    35                                  (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 4))
     33                                 (Expr (Evar (ident_of_nat 2))
     34                                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     35                                 (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))
    3636                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
    3737               (Tint I32 Signed  ))
    3838             (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    3939             (Tint I32 Signed  ))))
    40        (Sifthenelse (Expr (Evar (succ_pos_of_nat 1)) (Tint I32 Signed  ))
     40       (Sifthenelse (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
    4141         (Ssequence
    4242         (Sassign (Expr (Efield (Expr (Ederef
    43                                   (Expr (Evar (succ_pos_of_nat 2))
    44                                     (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    45                                   (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 5))
    46                     (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     43                                  (Expr (Evar (ident_of_nat 2))
     44                                    (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     45                                  (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
     46                    (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    4747           (Expr (Ederef
    48              (Expr (Evar (succ_pos_of_nat 6))
    49                (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    50              (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
     48             (Expr (Evar (ident_of_nat 6))
     49               (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     50             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
    5151         (Sassign (Expr (Ederef
    52                     (Expr (Evar (succ_pos_of_nat 6))
    53                       (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    54                     (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
    55            (Expr (Evar (succ_pos_of_nat 2))
    56              (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    57          (Scall (None expr) (Expr (Evar (succ_pos_of_nat 0))
    58                               (Tfunction (Tcons (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))) Tnil)) Tvoid))
    59            [(Expr (Evar (succ_pos_of_nat 2))
    60               (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))));
    61            (Expr (Ecast (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     52                    (Expr (Evar (ident_of_nat 6))
     53                      (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     54                    (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
     55           (Expr (Evar (ident_of_nat 2))
     56             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     57         (Scall (None expr) (Expr (Evar (ident_of_nat 0))
     58                              (Tfunction (Tcons (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) Tnil)) Tvoid))
     59           [(Expr (Evar (ident_of_nat 2))
     60              (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))));
     61           (Expr (Ecast (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    6262             (Expr (Eaddrof
    6363               (Expr (Efield (Expr (Ederef
    6464                               (Expr (Ederef
    65                                  (Expr (Evar (succ_pos_of_nat 6))
    66                                    (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    67                                  (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    68                                (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 5))
    69                  (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    70                (Tpointer PData (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    71              (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))])))
     65                                 (Expr (Evar (ident_of_nat 6))
     66                                   (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     67                                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     68                               (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
     69                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     70               (Tpointer PData (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     71             (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))])))
    7272     
    7373     
    7474     
    7575   )〉;
    76   〈succ_pos_of_nat 7 (* sort *), CL_Internal (
    77     mk_function Tvoid [〈succ_pos_of_nat 10, (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))〉 ] [〈succ_pos_of_nat 8, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ; 〈succ_pos_of_nat 5, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ; 〈succ_pos_of_nat 9, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ]
    78       (Ssequence
    79       (Sassign (Expr (Evar (succ_pos_of_nat 5))
    80                  (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     76  〈ident_of_nat 7 (* sort *), CL_Internal (
     77    mk_function Tvoid [〈ident_of_nat 10, (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))〉 ] [〈ident_of_nat 8, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 5, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ; 〈ident_of_nat 9, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ]
     78      (Ssequence
     79      (Sassign (Expr (Evar (ident_of_nat 5))
     80                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    8181        (Expr (Ederef
    82           (Expr (Evar (succ_pos_of_nat 10))
    83             (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    84           (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    85       (Ssequence
    86       (Sassign (Expr (Evar (succ_pos_of_nat 9))
    87                  (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
    88         (Expr (Ecast (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))
     82          (Expr (Evar (ident_of_nat 10))
     83            (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     84          (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     85      (Ssequence
     86      (Sassign (Expr (Evar (ident_of_nat 9))
     87                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
     88        (Expr (Ecast (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))
    8989          (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))
    90           (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    91       (Ssequence
    92       (Ssequence
    93       (Swhile (Expr (Evar (succ_pos_of_nat 5))
    94                 (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     90          (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     91      (Ssequence
     92      (Ssequence
     93      (Swhile (Expr (Evar (ident_of_nat 5))
     94                (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    9595        (Ssequence
    96         (Sassign (Expr (Evar (succ_pos_of_nat 8))
    97                    (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
    98           (Expr (Evar (succ_pos_of_nat 5))
    99             (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
     96        (Sassign (Expr (Evar (ident_of_nat 8))
     97                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
     98          (Expr (Evar (ident_of_nat 5))
     99            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
    100100        (Ssequence
    101         (Sassign (Expr (Evar (succ_pos_of_nat 5))
    102                    (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     101        (Sassign (Expr (Evar (ident_of_nat 5))
     102                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    103103          (Expr (Efield (Expr (Ederef
    104                           (Expr (Evar (succ_pos_of_nat 5))
    105                             (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    106                           (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 5))
    107             (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    108         (Scall (None expr) (Expr (Evar (succ_pos_of_nat 0))
    109                              (Tfunction (Tcons (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))) Tnil)) Tvoid))
    110           [(Expr (Evar (succ_pos_of_nat 8))
    111              (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))));
     104                          (Expr (Evar (ident_of_nat 5))
     105                            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     106                          (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
     107            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     108        (Scall (None expr) (Expr (Evar (ident_of_nat 0))
     109                             (Tfunction (Tcons (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (Tcons (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) Tnil)) Tvoid))
     110          [(Expr (Evar (ident_of_nat 8))
     111             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))));
    112112          (Expr (Eaddrof
    113             (Expr (Evar (succ_pos_of_nat 9))
    114               (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    115             (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))]))))
     113            (Expr (Evar (ident_of_nat 9))
     114              (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     115            (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))]))))
    116116      Sskip)
    117117      (Sassign (Expr (Ederef
    118                  (Expr (Evar (succ_pos_of_nat 10))
    119                    (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))
    120                  (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
    121         (Expr (Evar (succ_pos_of_nat 9))
    122           (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))))))
     118                 (Expr (Evar (ident_of_nat 10))
     119                   (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))
     120                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
     121        (Expr (Evar (ident_of_nat 9))
     122          (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))))))
    123123   
    124124   
    125125   
    126126  )〉;
    127   〈succ_pos_of_nat 11 (* out *), CL_External (succ_pos_of_nat 11) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉;
    128   〈succ_pos_of_nat 12 (* main *), CL_Internal (
    129     mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 13, (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))〉 ]
    130       (Ssequence
    131       (Sassign (Expr (Evar (succ_pos_of_nat 13))
    132                  (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     127  〈ident_of_nat 11 (* out *), CL_External (ident_of_nat 11) (Tcons (Tint I8 Unsigned ) Tnil) Tvoid〉;
     128  〈ident_of_nat 12 (* main *), CL_Internal (
     129    mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 13, (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))〉 ]
     130      (Ssequence
     131      (Sassign (Expr (Evar (ident_of_nat 13))
     132                 (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    133133        (Expr (Eaddrof
    134           (Expr (Evar (succ_pos_of_nat 14))
    135             (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
    136           (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    137       (Ssequence
    138       (Scall (None expr) (Expr (Evar (succ_pos_of_nat 7))
    139                            (Tfunction (Tcons (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))) Tnil) Tvoid))
     134          (Expr (Evar (ident_of_nat 14))
     135            (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
     136          (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     137      (Ssequence
     138      (Scall (None expr) (Expr (Evar (ident_of_nat 7))
     139                           (Tfunction (Tcons (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))) Tnil) Tvoid))
    140140        [(Expr (Eaddrof
    141            (Expr (Evar (succ_pos_of_nat 13))
    142              (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    143            (Tpointer Any (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))])
    144       (Ssequence
    145       (Ssequence
    146       (Swhile (Expr (Evar (succ_pos_of_nat 13))
    147                 (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     141           (Expr (Evar (ident_of_nat 13))
     142             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     143           (Tpointer Any (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))])
     144      (Ssequence
     145      (Ssequence
     146      (Swhile (Expr (Evar (ident_of_nat 13))
     147                (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    148148        (Ssequence
    149         (Scall (None expr) (Expr (Evar (succ_pos_of_nat 11))
     149        (Scall (None expr) (Expr (Evar (ident_of_nat 11))
    150150                             (Tfunction (Tcons (Tint I8 Unsigned ) Tnil) Tvoid))
    151151          [(Expr (Efield (Expr (Ederef
    152                            (Expr (Evar (succ_pos_of_nat 13))
    153                              (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    154                            (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 4))
     152                           (Expr (Evar (ident_of_nat 13))
     153                             (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     154                           (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 4))
    155155             (Tint I8 Unsigned ))])
    156         (Sassign (Expr (Evar (succ_pos_of_nat 13))
    157                    (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))))
     156        (Sassign (Expr (Evar (ident_of_nat 13))
     157                   (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))))
    158158          (Expr (Efield (Expr (Ederef
    159                           (Expr (Evar (succ_pos_of_nat 13))
    160                             (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))
    161                           (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))) (succ_pos_of_nat 5))
    162             (Tpointer PData (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil))))))))
     159                          (Expr (Evar (ident_of_nat 13))
     160                            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))
     161                          (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))) (ident_of_nat 5))
     162            (Tpointer PData (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil))))))))
    163163      Sskip)
    164164      (Sreturn (Some expr (Expr (Econst_int (repr 0)) (Tint I32 Signed  )))))))
     
    167167   
    168168  )〉]
    169   (succ_pos_of_nat 12)
    170   [〈〈〈succ_pos_of_nat 15 (* l6 *),
     169  (ident_of_nat 12)
     170  [〈〈〈ident_of_nat 15 (* l6 *),
    171171     [(Init_int8 (repr 69)) ; (Init_space 3) ; (Init_null PData) ;
    172172     (Init_space 3) ]〉, PData〉,
    173      (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;
    174   〈〈〈succ_pos_of_nat 16 (* l5 *),
     173     (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
     174  〈〈〈ident_of_nat 16 (* l5 *),
    175175    [(Init_int8 (repr 36)) ; (Init_space 3) ;
    176     (Init_addrof PData (succ_pos_of_nat 15) (repr 0))]〉, PData〉,
    177     (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;
    178   〈〈〈succ_pos_of_nat 17 (* l4 *),
     176    (Init_addrof PData (ident_of_nat 15) (repr 0))]〉, PData〉,
     177    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
     178  〈〈〈ident_of_nat 17 (* l4 *),
    179179    [(Init_int8 (repr 136)) ; (Init_space 3) ;
    180     (Init_addrof PData (succ_pos_of_nat 16) (repr 0))]〉, PData〉,
    181     (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;
    182   〈〈〈succ_pos_of_nat 18 (* l3 *),
     180    (Init_addrof PData (ident_of_nat 16) (repr 0))]〉, PData〉,
     181    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
     182  〈〈〈ident_of_nat 18 (* l3 *),
    183183    [(Init_int8 (repr 105)) ; (Init_space 3) ;
    184     (Init_addrof PData (succ_pos_of_nat 17) (repr 0))]〉, PData〉,
    185     (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;
    186   〈〈〈succ_pos_of_nat 19 (* l2 *),
     184    (Init_addrof PData (ident_of_nat 17) (repr 0))]〉, PData〉,
     185    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
     186  〈〈〈ident_of_nat 19 (* l2 *),
    187187    [(Init_int8 (repr 234)) ; (Init_space 3) ;
    188     (Init_addrof PData (succ_pos_of_nat 18) (repr 0))]〉, PData〉,
    189     (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;
    190   〈〈〈succ_pos_of_nat 20 (* l1 *),
     188    (Init_addrof PData (ident_of_nat 18) (repr 0))]〉, PData〉,
     189    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
     190  〈〈〈ident_of_nat 20 (* l1 *),
    191191    [(Init_int8 (repr 240)) ; (Init_space 3) ;
    192     (Init_addrof PData (succ_pos_of_nat 19) (repr 0))]〉, PData〉,
    193     (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉;
    194   〈〈〈succ_pos_of_nat 14 (* l0 *),
     192    (Init_addrof PData (ident_of_nat 19) (repr 0))]〉, PData〉,
     193    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉;
     194  〈〈〈ident_of_nat 14 (* l0 *),
    195195    [(Init_int8 (repr 102)) ; (Init_space 3) ;
    196     (Init_addrof PData (succ_pos_of_nat 20) (repr 0))]〉, PData〉,
    197     (Tstruct (succ_pos_of_nat 3) (Fcons (succ_pos_of_nat 4) (Tint I8 Unsigned ) (Fcons (succ_pos_of_nat 5) (Tcomp_ptr PData (succ_pos_of_nat 3)) Fnil)))〉]
     196    (Init_addrof PData (ident_of_nat 20) (repr 0))]〉, PData〉,
     197    (Tstruct (ident_of_nat 3) (Fcons (ident_of_nat 4) (Tint I8 Unsigned ) (Fcons (ident_of_nat 5) (Tcomp_ptr PData (ident_of_nat 3)) Fnil)))〉]
    198198.
    199199
     
    201201  (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0);EVint (repr 0)];
    202202   OK ? t) = OK ?
    203 [EVextcall (succ_pos_of_nat 11) [EVint (repr 36)] (EVint (repr 0));
    204  EVextcall (succ_pos_of_nat 11) [EVint (repr 69)] (EVint (repr 0));
    205  EVextcall (succ_pos_of_nat 11) [EVint (repr 102)] (EVint (repr 0));
    206  EVextcall (succ_pos_of_nat 11) [EVint (repr 105)] (EVint (repr 0));
    207  EVextcall (succ_pos_of_nat 11) [EVint (repr 136)] (EVint (repr 0));
    208  EVextcall (succ_pos_of_nat 11) [EVint (repr 234)] (EVint (repr 0));
    209  EVextcall (succ_pos_of_nat 11) [EVint (repr 240)] (EVint (repr 0))]
     203[EVextcall (ident_of_nat 11) [EVint (repr 36)] (EVint (repr 0));
     204 EVextcall (ident_of_nat 11) [EVint (repr 69)] (EVint (repr 0));
     205 EVextcall (ident_of_nat 11) [EVint (repr 102)] (EVint (repr 0));
     206 EVextcall (ident_of_nat 11) [EVint (repr 105)] (EVint (repr 0));
     207 EVextcall (ident_of_nat 11) [EVint (repr 136)] (EVint (repr 0));
     208 EVextcall (ident_of_nat 11) [EVint (repr 234)] (EVint (repr 0));
     209 EVextcall (ident_of_nat 11) [EVint (repr 240)] (EVint (repr 0))]
    210210.
    211211normalize  (* you can examine the result here *)
Note: See TracChangeset for help on using the changeset viewer.