diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-05 12:27:33 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-03-05 12:27:33 +0100 |
| commit | f8ae73357fd7650bc2409b9eddb5816d4025747e (patch) | |
| tree | e5196e7ec1f5326e661b5731e532e9b4de4dba70 | |
| parent | 264637042f4e648888307af28392aea21e2f28b8 (diff) | |
| download | compcert-kvx-f8ae73357fd7650bc2409b9eddb5816d4025747e.tar.gz compcert-kvx-f8ae73357fd7650bc2409b9eddb5816d4025747e.zip | |
compilation of ImpIOOracles
| -rw-r--r-- | Makefile.extr | 2 | ||||
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml | 11 | ||||
| -rw-r--r-- | mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.mli | 1 |
3 files changed, 9 insertions, 5 deletions
diff --git a/Makefile.extr b/Makefile.extr index 3d54f61f..d6a94d2e 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -43,7 +43,7 @@ cparser/pre_parser_messages.ml: DIRS=extraction \ lib common $(ARCH) backend cfrontend cparser driver \ - exportclight debug mppa_k1c/unittest + exportclight debug mppa_k1c/unittest mppa_k1c/abstractbb/Impure/ocaml INCLUDES=$(patsubst %,-I %, $(DIRS)) diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml index e5ec8e87..0e5cf434 100644 --- a/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml +++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml @@ -6,8 +6,10 @@ These oracles assumes the following extraction directives: *) open ImpPrelude +(* open BinNums open Datatypes +*) (* two auxiliary functions, for efficient mapping of "int" to "BinNums.positive" *) exception Overflow @@ -52,12 +54,13 @@ let memo_int2pos: int -> int -> BinNums.positive pi in find;; - +(* let string_coq2caml: char list -> string = fun l -> let buf = Buffer.create (List.length l) in List.iter (fun c -> Buffer.add_char buf c) l; Buffer.contents buf;; +*) let new_exit_observer: (unit -> unit) -> (unit -> unit) ref = fun f -> @@ -120,16 +123,18 @@ let zTr: BinNums.coq_Z -> int let ten = BinNums.Zpos (BinNums.Coq_xO (BinNums.Coq_xI (BinNums.Coq_xO BinNums.Coq_xH))) let rec string_of_pos (p:BinNums.positive) (acc: pstring): pstring -= let (q,r) = BinIntDef.Z.pos_div_eucl p ten in += let (q,r) = BinInt.Z.pos_div_eucl p ten in let acc0 = Concat (CamlStr (string_of_int (zTr r)), acc) in match q with | BinNums.Z0 -> acc0 | BinNums.Zpos p0 -> string_of_pos p0 acc0 | _ -> assert false +(* let string_of_Z_debug: BinNums.coq_Z -> pstring = fun p -> CamlStr (string_of_int (zTr p)) - +*) + let string_of_Z: BinNums.coq_Z -> pstring = function | BinNums.Z0 -> CamlStr "0" diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.mli b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.mli index 29db881b..6064286a 100644 --- a/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.mli +++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.mli @@ -1,5 +1,4 @@ open ImpPrelude -open Datatypes (* |