Frama-C:
Plug-ins:
Libraries:

Frama-C API - Parameters

Command-line parameters of the analysis.

Meta-option

Domains

module DomainsFunction : Frama_c_kernel.Parameter_sig.Multiple_map with type key = string and type value = Frama_c_kernel.Kernel_function.t * Eva__.Domain_mode.mode

Precision

State partitioning

module SplitReturnFunction : Frama_c_kernel.Parameter_sig.Map with type key = Frama_c_kernel.Cil_types.kernel_function and type value = Eva__.Split_strategy.split_strategy
module SplitReturn : Frama_c_kernel.Parameter_sig.Custom with type t = Eva__.Split_strategy.split_strategy

Performance

Initial context of the analysis

module InitializationPaddingGlobals : Frama_c_kernel.Parameter_sig.S with type t = [ `Initialized | `Uninitialized | `MaybeInitialized ]

Builtins

Analysis behavior

Non standard alarms

module WarnPointerComparison : Frama_c_kernel.Parameter_sig.S with type t = [ `All | `Pointer | `None ]

Verbosity and outputs

Experimental

type descending_strategy =
  1. | NoIteration
  2. | FullIteration
  3. | ExitIteration

Utility functions

val enabled_domains : unit -> (string * string) list

Returns the list (name, descr) of currently enabled abstract domains.

val use_builtin : Frama_c_kernel.Cil_types.kernel_function -> string -> unit

use_builtin kf name instructs the analysis to use the builtin name to interpret calls to function kf. Raises Not_found if there is no builtin of name name.

val use_global_value_partitioning : Frama_c_kernel.Cil_types.varinfo -> unit

use_global_value_partitioning vi instructs the analysis to use value partitioning on the global variable vi.

val change_correctness : unit -> unit

This function should be called whenever the correctness of the analysis is externally changed through the Eva API, to ensure that the property statuses emitted by Eva are properly reset.

Internal use only

val configure_precision : unit -> unit
val parameters_correctness : Frama_c_kernel.Typed_parameter.t list

List of parameters having an impact on the correctness of the analysis.

val parameters_tuning : Frama_c_kernel.Typed_parameter.t list

List of parameters having an impact only on the analysis precision.

val register_builtin : string -> unit

Registers available cvalue builtins for the -eva-builtin option.

val unregister_builtin : string -> unit

Unregister a cvalue builtin.

val register_domain : name:string -> descr:string -> priority:int -> unit

Registers available domain names for the -eva-domains option.