diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-16 07:52:57 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-16 07:52:57 +0200 |
commit | 6e4f49f7b8154d21c2c42f9978e6829d7a22a1de (patch) | |
tree | 71bd99acff0d01fe5a81def039ac011d0b7339dd /kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli | |
parent | 2e54a9c599ef13e4fe84ec80fac4c1835a052241 (diff) | |
download | compcert-kvx-6e4f49f7b8154d21c2c42f9978e6829d7a22a1de.tar.gz compcert-kvx-6e4f49f7b8154d21c2c42f9978e6829d7a22a1de.zip |
starting to move common files
Diffstat (limited to 'kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli')
-rw-r--r-- | kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli | 33 |
1 files changed, 0 insertions, 33 deletions
diff --git a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli b/kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli deleted file mode 100644 index 6064286a..00000000 --- a/kvx/abstractbb/Impure/ocaml/ImpIOOracles.mli +++ /dev/null @@ -1,33 +0,0 @@ -open ImpPrelude - - -(* -Memoized version of translation from int -> BinNums.positive. -The first arg is an indicative bound on the max int translated: -it pre-computes all positives lower or equal to this bound. -*) -val memo_int2pos: int -> int -> BinNums.positive - -val read_line: unit -> pstring - -val print: pstring -> unit - -val println: pstring -> unit - -val string_of_Z: BinNums.coq_Z -> pstring - -val timer : (('a -> 'b ) * 'a) -> 'b - -val new_exit_observer: (unit -> unit) -> (unit -> unit) ref - -val set_exit_observer: (unit -> unit) ref * (unit -> unit) -> unit - -val exn2string: exn -> pstring - -val fail: pstring -> 'a - -exception ImpureFail of pstring;; - -val try_with_fail: (unit -> 'a) * (pstring -> exn -> 'a) -> 'a - -val try_with_any: (unit -> 'a) * (exn -> 'a) -> 'a |