Changeset 3043 for extracted/lTL.ml


Ignore:
Timestamp:
Mar 29, 2013, 6:38:26 PM (7 years ago)
Author:
sacerdot
Message:

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/lTL.ml

    r3001 r3043  
    191191  in
    192192  let res0 =
    193     Joint.add_graph lTL (AST.prog_var_names p.Joint.joint_prog) l1
     193    Joint.add_graph lTL
     194      (Joint.prog_names (Joint.graph_params_to_params lTL) p) l1
    194195      (Joint.Sequential ((Joint.COST_LABEL p.Joint.init_cost_label),
    195196      (Obj.magic l2))) res
    196197  in
    197198  let res1 =
    198     Joint.add_graph lTL (AST.prog_var_names p.Joint.joint_prog) l2
     199    Joint.add_graph lTL
     200      (Joint.prog_names (Joint.graph_params_to_params lTL) p) l2
    199201      (Joint.Sequential ((Joint.CALL ((Types.Inl
    200       (AST.prog_main p.Joint.joint_prog)), (Obj.magic Nat.O),
     202      p.Joint.joint_prog.AST.prog_main), (Obj.magic Nat.O),
    201203      (Obj.magic Types.It))), (Obj.magic l3))) res0
    202204  in
    203205  let res2 =
    204     Joint.add_graph lTL (AST.prog_var_names p.Joint.joint_prog) l3
    205       (Joint.Final (Joint.GOTO l3)) res1
     206    Joint.add_graph lTL
     207      (Joint.prog_names (Joint.graph_params_to_params lTL) p) l3 (Joint.Final
     208      (Joint.GOTO l3)) res1
    206209  in
    207210  res2
Note: See TracChangeset for help on using the changeset viewer.