Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: PVS

Original von: Coq^©

(** Some architectures may have a native ocaml compiler but no native
    dynlink.cmxa (e.g. ARM). If you still want to build a native coqtop
    there, you'll need this dummy implementation of Dynlink.
    Compile it and install with:

      ocamlopt -a -o dynlink.cmxa dynlink.ml
      sudo cp -i dynlink.cmxa `ocamlopt -where`

    Then build coq this way: ./configure -natdynlink no && make world
*)

let is_native = true (* This file will only be given to the native compiler *)

type linking_error =
| Undefined_global of string
| Unavailable_primitive of string
| Uninitialized_global of string

type error =
| Not_a_bytecode_file of string
| Inconsistent_import of string
| Unavailable_unit of string
| Unsafe_file
| Linking_error of string * linking_error
| Corrupted_interface of string
| File_not_found of string
| Cannot_open_dll of string
| Inconsistent_implementation of string

exception Error of error

let error_message = function
  | Not_a_bytecode_file s -> "Native dynamic link not supported (module "^s^")"
  | _ -> "Native dynamic link not supported"

let loadfile : string -> unit = fun s -> raise (Error (Not_a_bytecode_file s))
let loadfile_private = loadfile

let adapt_filename s = s

let init () = ()
let allow_only : string list -> unit = fun _ -> ()
let prohibit : string list -> unit = fun _ -> ()
let default_available_units : unit -> unit = fun _ -> ()
let allow_unsafe_modules : bool -> unit = fun _ -> ()
let add_interfaces : string list -> string list -> unit = fun _ _ -> ()
let add_available_units : (string * Digest.t) list -> unit = fun _ -> ()
let clear_available_units : unit -> unit = fun _ -> ()
let digest_interface : string -> string list -> Digest.t =
fun _ _ -> failwith "digest_interface"

¤ Dauer der Verarbeitung: 0.27 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.