mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
60 lines
1.1 KiB
Plaintext
60 lines
1.1 KiB
Plaintext
(** {1 General functions related to OCaml extraction} *)
|
|
|
|
module Sys
|
|
|
|
use int.Int
|
|
use mach.int.Int63
|
|
|
|
val constant max_array_length : int63
|
|
axiom non_neg_max_array_length : 0 <= max_array_length
|
|
|
|
end
|
|
|
|
module Exceptions
|
|
|
|
exception Exit
|
|
exception Not_found
|
|
exception Invalid_argument string
|
|
|
|
end
|
|
|
|
module Pervasives
|
|
|
|
use int.Int
|
|
use mach.int.Int63
|
|
|
|
use export Exceptions
|
|
|
|
val succ (x: int63) : int63
|
|
requires { [@expl:integer overflow] in_bounds (to_int x + 1) }
|
|
ensures { to_int result = to_int x + 1 }
|
|
|
|
val pred (x: int63) : int63
|
|
requires { [@expl:integer overflow] in_bounds (to_int x - 1) }
|
|
ensures { to_int result = to_int x - 1 }
|
|
|
|
exception AssertFailure
|
|
|
|
val ocaml_assert (_b: bool) : unit
|
|
raises { AssertFailure }
|
|
|
|
end
|
|
|
|
module OCaml
|
|
|
|
use export int.Int
|
|
use mach.int.Int63 as Int63
|
|
use export int.MinMax
|
|
use export option.Option
|
|
use export Pervasives
|
|
use Sys
|
|
|
|
use mach.array.Array63 as Array
|
|
type array 'a = Array.array 'a
|
|
|
|
type int63 = Int63.int63
|
|
|
|
let function to_int (n: Int63.int63) : int = Int63.to_int n
|
|
|
|
end
|