Module Core.Codex_options

This file registers in the Frama-C kernel the options for Frama-C/Codex. If needed, see the Frama-C plugin development guide for a description.

val help_msg : string

type category

type warn_category

val verbose_atleast : int -> bool

val debug_atleast : int -> bool

val printf : ?level:int -> ?dkey:category -> ?current:bool -> ?source:Frama_c_kernel.Filepath.position -> ?append:(Stdlib.Format.formatter -> unit) -> ?header:(Stdlib.Format.formatter -> unit) -> ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a

val result : ?level:int -> ?dkey:category -> 'a Frama_c_kernel__Log.pretty_printer

val has_tty : unit -> bool

val feedback : ?ontty:Frama_c_kernel__Log.ontty -> ?level:int -> ?dkey:category -> 'a Frama_c_kernel__Log.pretty_printer

val debug : ?level:int -> ?dkey:category -> 'a Frama_c_kernel__Log.pretty_printer

val warning : ?wkey:warn_category -> 'a Frama_c_kernel__Log.pretty_printer

val error : 'a Frama_c_kernel__Log.pretty_printer

val abort : ('a, 'b) Frama_c_kernel__Log.pretty_aborter

val failure : 'a Frama_c_kernel__Log.pretty_printer

val fatal : ('a, 'b) Frama_c_kernel__Log.pretty_aborter

val verify : bool -> ('a, bool) Frama_c_kernel__Log.pretty_aborter

val not_yet_implemented : ?current:bool -> ?source:Frama_c_kernel.Filepath.position -> ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a

val deprecated : string -> now:string -> ('a -> 'b) -> 'a -> 'b

val with_result : (Frama_c_kernel__Log.event option -> 'b) -> ('a, 'b) Frama_c_kernel__Log.pretty_aborter

val with_warning : (Frama_c_kernel__Log.event option -> 'b) -> ('a, 'b) Frama_c_kernel__Log.pretty_aborter

val with_error : (Frama_c_kernel__Log.event option -> 'b) -> ('a, 'b) Frama_c_kernel__Log.pretty_aborter

val with_failure : (Frama_c_kernel__Log.event option -> 'b) -> ('a, 'b) Frama_c_kernel__Log.pretty_aborter

val log : ?kind:Frama_c_kernel__Log.kind -> ?verbose:int -> ?debug:int -> 'a Frama_c_kernel__Log.pretty_printer

val logwith : (Frama_c_kernel__Log.event option -> 'b) -> ?wkey:warn_category -> ?emitwith:(Frama_c_kernel__Log.event -> unit) -> ?once:bool -> ('a, 'b) Frama_c_kernel__Log.pretty_aborter

val register : Frama_c_kernel__Log.kind -> (Frama_c_kernel__Log.event -> unit) -> unit

val register_tag_handlers : ((string -> string) * (string -> string)) -> unit

val register_category : ?help:string -> string -> category

val pp_category : Stdlib.Format.formatter -> category -> unit

val pp_all_categories : unit -> unit

val dkey_name : category -> string

val is_registered_category : string -> bool

val get_category : string -> category option

val get_all_categories : unit -> category list

val add_debug_keys : category -> unit

val del_debug_keys : category -> unit

val get_debug_keys : unit -> category list

val is_debug_key_enabled : category -> bool

val register_warn_category : ?help:string -> string -> warn_category

val is_warn_category : string -> bool

val pp_warn_category : Stdlib.Format.formatter -> warn_category -> unit

val pp_all_warn_categories_status : unit -> unit

val wkey_name : warn_category -> string

val get_warn_category : string -> warn_category option

val get_all_warn_categories : unit -> warn_category list

val get_all_warn_categories_status : unit -> (warn_category * Frama_c_kernel__Log.warn_status) list

val set_warn_status : warn_category -> Frama_c_kernel__Log.warn_status -> unit

val get_warn_status : warn_category -> Frama_c_kernel__Log.warn_status

val add_group : ?memo:bool -> string -> Frama_c_kernel.Cmdline.Group.t

module Verbose : Frama_c_kernel.Parameter_sig.Int

module Debug : Frama_c_kernel.Parameter_sig.Int

module Share : Frama_c_kernel.Parameter_sig.Site_root

module Session : Frama_c_kernel.Parameter_sig.User_dir_opt

module Cache_dir () : Frama_c_kernel.Parameter_sig.User_dir_opt

module Config_dir () : Frama_c_kernel.Parameter_sig.User_dir_opt

module State_dir () : Frama_c_kernel.Parameter_sig.User_dir_opt

val help : Frama_c_kernel.Cmdline.Group.t

val messages : Frama_c_kernel.Cmdline.Group.t

val add_plugin_output_aliases : ?visible:bool -> ?deprecated:bool -> string list -> unit

module Bool (_ : sig ... end) : sig ... end

module Action (_ : sig ... end) : sig ... end

module False (_ : sig ... end) : sig ... end

module True (_ : sig ... end) : sig ... end

module WithOutput (_ : sig ... end) : sig ... end

module Int (_ : sig ... end) : sig ... end

module Zero (_ : sig ... end) : sig ... end

module Float (_ : sig ... end) : sig ... end

module String (_ : sig ... end) : sig ... end

module Empty_string (_ : sig ... end) : sig ... end

module Fc_Filepath = Frama_c_kernel.Filepath

module Filepath (_ : sig ... end) : sig ... end

module Make_site_dir (_ : sig ... end) (_ : sig ... end) : sig ... end

module Make_user_dir (_ : sig ... end) (_ : sig ... end) : sig ... end

module Make_user_dir_opt (_ : sig ... end) (_ : sig ... end) : sig ... end

module Custom (V : sig ... end) (_ : sig ... end) : sig ... end

module Enum (X : sig ... end) : sig ... end

exception Cannot_build of string

module Make_set (E : sig ... end) (_ : sig ... end) : sig ... end

module String_set (_ : sig ... end) : sig ... end

module Filled_string_set (_ : sig ... end) : sig ... end

module Kernel_function_set (_ : sig ... end) : sig ... end

module Fundec_set (_ : sig ... end) : sig ... end

module Make_list (E : sig ... end) (_ : sig ... end) : sig ... end

module String_list (_ : sig ... end) : sig ... end

module Filepath_list (_ : sig ... end) : sig ... end

module Value_int : sig ... end

module Value_string : sig ... end

module Filepath_map (V : sig ... end) (_ : sig ... end) : sig ... end

module Make_map (K : sig ... end) (V : sig ... end) (_ : sig ... end) : sig ... end

module String_map (V : sig ... end) (_ : sig ... end) : sig ... end

module Kernel_function_map (V : sig ... end) (_ : sig ... end) : sig ... end

module Make_multiple_map (K : sig ... end) (V : sig ... end) (_ : sig ... end) : sig ... end

module String_multiple_map (V : sig ... end) (_ : sig ... end) : sig ... end

module Kernel_function_multiple_map (V : sig ... end) (_ : sig ... end) : sig ... end

val parameters : unit -> Frama_c_kernel.Typed_parameter.t list

module Enabled : sig ... end

module TypeConfigurationFile : sig ... end

module HtmlDump : sig ... end

module ExpDump : sig ... end

module OutputPrefix : sig ... end

module UseTypeDomain : sig ... end

module CompareWithValue : sig ... end

val needs_exp_term_mapping : unit -> bool

type svcomp_property =

1. | No_overflow
2. | Valid_memsafety
3. | Valid_memcleanup
4. | Termination
5. | Def_behavior
6. | No_data_race
7. | Unreach_call of {
   1. suffix : string option;
   }
8. | Coverage_error_call
9. | Coverage_branches
10. | Coverage_statements
11. | Coverage_conditions

val pp_svcomp_property : Stdlib.Format.formatter -> svcomp_property -> unit

module SVComp_expected_properties : sig ... end

module Print_Force_Lazyness : sig ... end

module UnknownUninitialized : sig ... end

module Focusing : sig ... end

module UseLoopDomain : sig ... end

module FixpointUseRegexp : sig ... end

module SparseNonRelationalDomain : sig ... end

module BitwiseDomain : sig ... end

module SerializeCache : sig ... end

module UseWeakTypes : sig ... end

module OverflowAlarms : sig ... end

module TryHard : sig ... end

module AnalyzeFunctions : sig ... end

module InferTypes : sig ... end

module UseUnionFind : sig ... end

module ExtraMetrics : sig ... end

module GcStats : sig ... end

module BackPropagationLimit : sig ... end

module VariableDisplay : sig ... end

val performance : category

val performance_warning : ('a, Stdlib.Format.formatter, unit) Stdlib.format -> 'a

val emitter : Frama_c_kernel.Emitter.t

module Location : sig ... end

TODO: We should have a "callstack" or "Location" module.