products/sources/formale sprachen/Coq/dev/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Prinzipien der Anforderungsanalyse sigma_swap.pvs   Sprache: SML

Untersuchung 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"

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.22Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Begriffe der Konzeptbildung
Was zu einem Entwurf gehört
Begriffe der Konzeptbildung
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff