module Wp_error: sig
.. end
To be raised a feature of C/ACSL cannot be supported by a memory model
or is not implemented, or ...
exception Error of string * string
To be raised a feature of C/ACSL cannot be supported by a memory model
or is not implemented, or ...
val current : string Pervasives.ref
val set_model : string -> unit
val unsupported : ?model:string -> ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
val not_yet_implemented : ?model:string -> ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
val pp_logic_label : Format.formatter -> Cil_types.logic_label -> unit
val pp_assigns : Format.formatter -> Cil_types.identified_term Cil_types.assigns -> unit
val pp_string_list : ?sep:(unit, Format.formatter, unit, unit, unit, unit) Pervasives.format6 ->
empty:string -> Format.formatter -> string list -> unit
type 'a
cc =
| |
Result of 'a |
| |
Warning of string * string |
val protected : exn -> (string * string) option
val protect : exn -> string * string
val protect_warning : exn -> 'a cc
val protect_function : ('a -> 'b) -> 'a -> 'b cc
val protect_translation : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c cc
val protect_translation3 : ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd cc
val protect_translation4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> 'e cc
val protect_translation5 : ('a -> 'b -> 'c -> 'd -> 'e -> 'f) ->
'a -> 'b -> 'c -> 'd -> 'e -> 'f cc
val protect_map : ('a -> 'b cc) -> 'a list -> 'b list cc
val name : string list -> string