Ignore:
Timestamp:
Mar 15, 2013, 1:32:50 AM (7 years ago)
Author:
sacerdot
Message:

Pretty printing of object code integrated too.
A couple of axioms make execution via the preclassified_system
raise assert false.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/semantics.ml

    r2873 r2875  
    316316
    317317open LIN_semantics
     318
     319open Interpret2
    318320
    319321type preclassified_system_pass =
     
    324326    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    325327    preclassified_system_pass -> 'a1 **)
    326 let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_26392 =
    327   let pcs_pcs = x_26392 in h_mk_preclassified_system_pass pcs_pcs __
     328let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_3 =
     329  let pcs_pcs = x_3 in h_mk_preclassified_system_pass pcs_pcs __
    328330
    329331(** val preclassified_system_pass_rect_Type5 :
    330332    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    331333    preclassified_system_pass -> 'a1 **)
    332 let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_26394 =
    333   let pcs_pcs = x_26394 in h_mk_preclassified_system_pass pcs_pcs __
     334let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_5 =
     335  let pcs_pcs = x_5 in h_mk_preclassified_system_pass pcs_pcs __
    334336
    335337(** val preclassified_system_pass_rect_Type3 :
    336338    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    337339    preclassified_system_pass -> 'a1 **)
    338 let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_26396 =
    339   let pcs_pcs = x_26396 in h_mk_preclassified_system_pass pcs_pcs __
     340let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_7 =
     341  let pcs_pcs = x_7 in h_mk_preclassified_system_pass pcs_pcs __
    340342
    341343(** val preclassified_system_pass_rect_Type2 :
    342344    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    343345    preclassified_system_pass -> 'a1 **)
    344 let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_26398 =
    345   let pcs_pcs = x_26398 in h_mk_preclassified_system_pass pcs_pcs __
     346let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_9 =
     347  let pcs_pcs = x_9 in h_mk_preclassified_system_pass pcs_pcs __
    346348
    347349(** val preclassified_system_pass_rect_Type1 :
    348350    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    349351    preclassified_system_pass -> 'a1 **)
    350 let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_26400 =
    351   let pcs_pcs = x_26400 in h_mk_preclassified_system_pass pcs_pcs __
     352let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_11 =
     353  let pcs_pcs = x_11 in h_mk_preclassified_system_pass pcs_pcs __
    352354
    353355(** val preclassified_system_pass_rect_Type0 :
    354356    Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
    355357    preclassified_system_pass -> 'a1 **)
    356 let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_26402 =
    357   let pcs_pcs = x_26402 in h_mk_preclassified_system_pass pcs_pcs __
     358let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_13 =
     359  let pcs_pcs = x_13 in h_mk_preclassified_system_pass pcs_pcs __
    358360
    359361(** val pcs_pcs :
     
    405407  Measurable.pcs_exec__o__es1 (pcs_pcs x0 x1)
    406408
     409exception NotImplementedYet
     410
    407411(** val preclassified_system_of_pass :
    408     Compiler.pass -> preclassified_system_pass **)
     412    Compiler.pass -> Compiler.syntax_of_pass -> preclassified_system_pass **)
    409413let preclassified_system_of_pass = function
    410 | Compiler.Clight_pass -> Clight_classified_system.clight_pcs
    411 | Compiler.Clight_switch_removed_pass -> Clight_classified_system.clight_pcs
    412 | Compiler.Clight_label_pass -> Clight_classified_system.clight_pcs
    413 | Compiler.Clight_simplified_pass -> Clight_classified_system.clight_pcs
    414 | Compiler.Cminor_pass -> Cminor_classified_system.cminor_pcs
    415 | Compiler.Rtlabs_pass -> RTLabs_classified_system.rTLabs_pcs
     414| Compiler.Clight_pass -> (fun x -> Clight_classified_system.clight_pcs)
     415| Compiler.Clight_switch_removed_pass ->
     416  (fun x -> Clight_classified_system.clight_pcs)
     417| Compiler.Clight_label_pass ->
     418  (fun x -> Clight_classified_system.clight_pcs)
     419| Compiler.Clight_simplified_pass ->
     420  (fun x -> Clight_classified_system.clight_pcs)
     421| Compiler.Cminor_pass -> (fun x -> Cminor_classified_system.cminor_pcs)
     422| Compiler.Rtlabs_pass -> (fun x -> RTLabs_classified_system.rTLabs_pcs)
    416423| Compiler.Rtl_separate_pass ->
    417   Joint_fullexec.joint_preclassified_system
    418     (SemanticsUtils.sem_graph_params_to_sem_params
    419       RTL_semantics.rTL_semantics_separate)
     424  (fun x ->
     425    Joint_fullexec.joint_preclassified_system
     426      (SemanticsUtils.sem_graph_params_to_sem_params
     427        RTL_semantics.rTL_semantics_separate))
    420428| Compiler.Rtl_uniq_pass ->
    421   Joint_fullexec.joint_preclassified_system
    422     (SemanticsUtils.sem_graph_params_to_sem_params
    423       RTL_semantics.rTL_semantics_unique)
     429  (fun x ->
     430    Joint_fullexec.joint_preclassified_system
     431      (SemanticsUtils.sem_graph_params_to_sem_params
     432        RTL_semantics.rTL_semantics_unique))
    424433| Compiler.Ertl_pass ->
    425   Joint_fullexec.joint_preclassified_system
    426     (SemanticsUtils.sem_graph_params_to_sem_params
    427       ERTL_semantics.eRTL_semantics)
     434  (fun x ->
     435    Joint_fullexec.joint_preclassified_system
     436      (SemanticsUtils.sem_graph_params_to_sem_params
     437        ERTL_semantics.eRTL_semantics))
    428438| Compiler.Ertlptr_pass ->
    429   Joint_fullexec.joint_preclassified_system
    430     (SemanticsUtils.sem_graph_params_to_sem_params
    431       ERTLptr_semantics.eRTLptr_semantics)
     439  (fun x ->
     440    Joint_fullexec.joint_preclassified_system
     441      (SemanticsUtils.sem_graph_params_to_sem_params
     442        ERTLptr_semantics.eRTLptr_semantics))
    432443| Compiler.Ltl_pass ->
    433   Joint_fullexec.joint_preclassified_system
    434     (SemanticsUtils.sem_graph_params_to_sem_params
    435       LTL_semantics.lTL_semantics)
     444  (fun x ->
     445    Joint_fullexec.joint_preclassified_system
     446      (SemanticsUtils.sem_graph_params_to_sem_params
     447        LTL_semantics.lTL_semantics))
    436448| Compiler.Lin_pass ->
    437   Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics
     449  (fun x ->
     450    Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics)
     451| Compiler.Assembly_pass -> (fun prog -> raise NotImplementedYet)
     452| Compiler.Object_code_pass ->
     453  (fun prog -> Interpret2.oC_preclassified_system (Obj.magic prog))
    438454
    439455(** val run_and_print :
     
    443459    Types.unit0 **)
    444460let run_and_print pass prog n print_pass print_event print_error print_exit =
    445   let pcs = preclassified_system_of_pass pass in
     461 try
     462  let pcs = preclassified_system_of_pass pass prog in
    446463  let prog0 = prog in
    447464  let g = (pcs_pcs__o__pcs_exec pass pcs).SmallstepExec.make_global prog0 in
     
    460477      | Errors.Error msg -> print_error msg)
    461478   | Errors.Error msg -> print_error msg)
    462 
     479 with
     480  NotImplementedYet -> Types.It
     481
Note: See TracChangeset for help on using the changeset viewer.