Frama-C API - LoopVar
A set is a collection.
include Frama_c_kernel.Parameter_sig.Collection with type elt = Frama_c_kernel.Cil_types.kernel_function with type t = Frama_c_kernel.Cil_datatype.Kf.Set.t
A collection is a standard command line parameter.
include Frama_c_kernel.Parameter_sig.S with type t = Frama_c_kernel.Cil_datatype.Kf.Set.t
include Frama_c_kernel.Parameter_sig.S_no_parameter with type t = Frama_c_kernel.Cil_datatype.Kf.Set.t
type t = Frama_c_kernel.Cil_datatype.Kf.Set.t
Type of the parameter (an int, a string, etc). It is concrete for each module implementing this signature.
val set : t -> unit
Set the option.
Add a hook to be called after the function set
is called. The first parameter of the hook is the old value of the parameter while the second one is the new value.
Add a hook to be called when the value of the parameter changes (by calling set
or indirectly by the project library. The first parameter of the hook is the old value of the parameter while the second one is the new value. Note that it is **not** specified if the hook is applied just before or just after the effective change.
val get : unit -> t
Option value (not necessarily set on the current command line).
Set the option to its default value, that is the value if set
was never called.
val get_default : unit -> t
Get the default value for the option.
Print the help of the parameter in the given formatter as it would be printed on the command line by -<plugin>-help. For invisible parameters, the string corresponds to the one returned if it would be not invisible.
include Frama_c_kernel.State_builder.S
val self : Frama_c_kernel.State.t
The kind of the registered state.
val mark_as_computed : ?project:Frama_c_kernel.Project.t -> unit -> unit
Indicate that the registered state will not change again for the given project (default is current ()
).
val is_computed : ?project:Frama_c_kernel.Project.t -> unit -> bool
Returns true
iff the registered state will not change again for the given project (default is current ()
).
Exportation of some inputs (easier use of State_builder.Register
).
module Datatype : Frama_c_kernel.Datatype.S
val add_hook_on_update : (Datatype.t -> unit) -> unit
Add an hook which is applied each time (just before) the project library changes the local value of the state.
val howto_marshal : (Datatype.t -> 'a) -> ('a -> Datatype.t) -> unit
howto_marshal marshal unmarshal
registers a custom couple of functions (marshal, unmarshal)
to be used for serialization. Default functions are identities. In particular, this function must be used if Datatype.t
is not marshallable and do_not_save
is not called.
Add some aliases for this option. That is other option names which have exactly the same semantics that the initial option. If visible
is set to false, the aliases do not appear in help messages. If deprecated
is set to true, the use of the aliases emits a warning.
val parameter : Frama_c_kernel.Typed_parameter.t
type elt = Frama_c_kernel.Cil_types.kernel_function
Element in the collection.
val iter : (elt -> unit) -> unit
Iterate over all the elements of the collection.
val fold : (elt -> 'a -> 'a) -> 'a -> 'a
Fold over all the elements of the collection.
val add : elt -> unit
Add an element to the collection
A collection is a standard string parameter
module Category : Frama_c_kernel.Parameter_sig.Collection_category with type elt = elt
Categories for this collection.
Additional accessors to the set.
val mem : elt -> bool
Does the given element belong to the set?
val exists : (elt -> bool) -> bool
Is there some element satisfying the given predicate?