- Timestamp:
- Mar 4, 2013, 10:03:33 AM (8 years ago)
- Location:
- driver
- Files:
-
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
driver/clightFromC.ml
r2758 r2773 388 388 | C.Oshr -> Oshr 389 389 | C.Oeq -> Oeq 390 | C.One -> One 0390 | C.One -> One 391 391 | C.Olt -> Olt 392 392 | C.Ogt -> Ogt -
driver/clightPrinter.ml
r2759 r2773 76 76 | Oshr -> ">>" 77 77 | Oeq -> "==" 78 | One 0-> "!="78 | One -> "!=" 79 79 | Olt -> "<" 80 80 | Ogt -> ">" … … 176 176 begin match op with 177 177 | Oand | Oor | Oxor -> 75 178 | Oeq | One 0| Olt | Ogt | Ole | Oge -> 70178 | Oeq | One | Olt | Ogt | Ole | Oge -> 70 179 179 | Oadd | Osub | Oshl | Oshr -> 60 180 180 | Omul | Odiv | Omod -> 40 -
driver/error.ml
r2729 r2773 3 3 4 4 let error_to_string = function 5 | AssemblyTooLarge -> "AssemblyTooLarge" 5 6 | MISSING -> "MISSING" 6 7 | EXTERNAL -> "EXTERNAL" -
driver/exec.ml
r2721 r2773 2 2 3 3 let rec run g s = 4 (match Extracted.Cexec.is_final 0s with4 (match Extracted.Cexec.is_final s with 5 5 | Extracted.Types.None -> 6 6 (match Extracted.Cexec.exec_step g s with … … 25 25 let OK mid = Extracted.Compiler.front_end cl in 26 26 let rtlabs = Extracted.Types.snd mid in 27 let g = Extracted.Cexec.make_global 0cl in28 let OK s0 = Extracted.Cexec.make_initial_state 0cl in27 let g = Extracted.Cexec.make_global cl in 28 let OK s0 = Extracted.Cexec.make_initial_state cl in 29 29 let r = run g s0 in 30 30 exit (bv_to_int r) -
driver/frontend.ml
r2721 r2773 25 25 let OK mid = Extracted.Compiler.front_end cl in 26 26 let rtlabs = Extracted.Types.snd mid in 27 let g = Extracted.RTLabs_semantics.make_global 0rtlabs in28 let OK s0 = Extracted.RTLabs_semantics.make_initial_state 0rtlabs in27 let g = Extracted.RTLabs_semantics.make_global rtlabs in 28 let OK s0 = Extracted.RTLabs_semantics.make_initial_state rtlabs in 29 29 let r = run g s0 in 30 30 exit (bv_to_int r)
Note: See TracChangeset
for help on using the changeset viewer.