Changeset 2773 for driver


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
Location:
driver
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • driver/clightFromC.ml

    r2758 r2773  
    388388        | C.Oshr -> Oshr
    389389        | C.Oeq  -> Oeq
    390         | C.One  -> One0
     390        | C.One  -> One
    391391        | C.Olt  -> Olt
    392392        | C.Ogt  -> Ogt
  • driver/clightPrinter.ml

    r2759 r2773  
    7676  | Oshr -> ">>"
    7777  | Oeq  -> "=="
    78   | One0  -> "!="
     78  | One  -> "!="
    7979  | Olt  -> "<"
    8080  | Ogt  -> ">"
     
    176176      begin match op with
    177177      | Oand | Oor | Oxor -> 75
    178       | Oeq | One0 | Olt | Ogt | Ole | Oge -> 70
     178      | Oeq | One | Olt | Ogt | Ole | Oge -> 70
    179179      | Oadd | Osub | Oshl | Oshr -> 60
    180180      | Omul | Odiv | Omod -> 40
  • driver/error.ml

    r2729 r2773  
    33
    44let error_to_string = function
     5| AssemblyTooLarge -> "AssemblyTooLarge"
    56| MISSING -> "MISSING"
    67| EXTERNAL -> "EXTERNAL"
  • driver/exec.ml

    r2721 r2773  
    22
    33let rec run g s =
    4   (match Extracted.Cexec.is_final0 s with
     4  (match Extracted.Cexec.is_final s with
    55  | Extracted.Types.None ->
    66    (match Extracted.Cexec.exec_step g s with
     
    2525let OK mid = Extracted.Compiler.front_end cl in
    2626let rtlabs = Extracted.Types.snd mid in
    27 let g = Extracted.Cexec.make_global0 cl in
    28 let OK s0 = Extracted.Cexec.make_initial_state0 cl in
     27let g = Extracted.Cexec.make_global cl in
     28let OK s0 = Extracted.Cexec.make_initial_state cl in
    2929let r = run g s0 in
    3030exit (bv_to_int r)
  • driver/frontend.ml

    r2721 r2773  
    2525let OK mid = Extracted.Compiler.front_end cl in
    2626let rtlabs = Extracted.Types.snd mid in
    27 let g = Extracted.RTLabs_semantics.make_global0 rtlabs in
    28 let OK s0 = Extracted.RTLabs_semantics.make_initial_state0 rtlabs in
     27let g = Extracted.RTLabs_semantics.make_global rtlabs in
     28let OK s0 = Extracted.RTLabs_semantics.make_initial_state rtlabs in
    2929let r = run g s0 in
    3030exit (bv_to_int r)
Note: See TracChangeset for help on using the changeset viewer.