Commit c4b0dbb3 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Added a tiny [Sys] module.

parent 4c657cd0
(* TEMPORARY
(* [big_endian] and [word_size] are defined as external *constants* here.
In OCaml they are external *functions* and they are invoked once on
startup. *)
external big_endian : (* unit -> *) bool = "%big_endian"
external word_size : (* unit -> *) int = "%word_size"
let max_array_length = (1 lsl (word_size - 10)) - 1
let max_string_length = word_size / 8 * max_array_length - 1
*)
let big_endian = false
let word_size = 64
let max_array_length = 18014398509481983
let max_string_length = 144115188075855863
Set Implicit Arguments.
Require Import CFLib.
Require Import Sys_ml.
Parameter word_size_spec :
word_size = 32 \/ word_size = 64.
Parameter max_array_length_spec :
0 < max_array_length.
Parameter max_string_length_spec :
0 < max_string_length.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment