package frama-c
Install
dune-project
Dependency
Authors
-
MMichele Alberti
-
TThibaud Antignac
-
GGergö Barany
-
PPatrick Baudin
-
NNicolas Bellec
-
TThibaut Benjamin
-
AAllan Blanchard
-
LLionel Blatter
-
FFrançois Bobot
-
RRichard Bonichon
-
VVincent Botbol
-
QQuentin Bouillaguet
-
DDavid Bühler
-
ZZakaria Chihani
-
SSylvain Chiron
-
LLoïc Correnson
-
JJulien Crétin
-
PPascal Cuoq
-
ZZaynah Dargaye
-
BBasile Desloges
-
JJean-Christophe Filliâtre
-
PPhilippe Herrmann
-
JJordan Ischard
-
MMaxime Jacquemin
-
BBenjamin Jorge
-
FFlorent Kirchner
-
AAlexander Kogtenkov
-
RRemi Lazarini
-
TTristan Le Gall
-
KKilyan Le Gallic
-
JJean-Christophe Léchenet
-
MMatthieu Lemerre
-
DDara Ly
-
DDavid Maison
-
CClaude Marché
-
AAndré Maroneze
-
TThibault Martin
-
FFonenantsoa Maurica
-
MMelody Méaulle
-
BBenjamin Monate
-
NNicky Mouha
-
YYannick Moy
-
PPierre Nigron
-
AAnne Pacalet
-
VValentin Perrelle
-
GGuillaume Petiot
-
DDario Pinto
-
VVirgile Prevosto
-
AArmand Puccetti
-
FFélix Ridoux
-
VVirgile Robles
-
JJan Rochel
-
MMuriel Roger
-
CCécile Ruet-Cros
-
JJulien Signoles
-
FFabien Siron
-
NNicolas Stouls
-
HHugo Thievenaz
-
KKostyantyn Vorobyov
-
BBoris Yakobowski
Maintainers
Sources
sha256=9c1cbffd28bb33c17a668107e39c96e4ae7378a3d8249f69b47afc7ee964e9b8
doc/frama-c-slicing.core/Slicing/SlicingParameters/Config_dir/index.html
Module SlicingParameters.Config_dir
Handle the specific `config' directory of the plug-in.
Parameters
Signature
include Frama_c_kernel.Parameter_sig.User_dir
val get_dir : ?create_path:bool -> string -> Frama_c_kernel.Filepath.tget_dir ~create_path name tries to get the directory name. The function aborts if:
- a file named
nameexists, - creating a the directory fails.
Otherwise returns the path, and creates it if create_path is true (it defaults to false). Subdirectories modules can be created with Builder.Make_user_dir and Builder.Make_user_dir_opt.
val get_file : ?create_path:bool -> string -> Frama_c_kernel.Filepath.tget_file ~create_path name tries to get the file name. The function aborts if:
- a directory named
nameexists, - creating the path to the file fails.
Otherwise returns the path, and creates the directories that lead to the file if create_path is true (it defaults to false). The file is *not* created by the function.
include Frama_c_kernel.Parameter_sig.S with type t = Frama_c_kernel.Filepath.t
include Frama_c_kernel.Parameter_sig.S_no_parameter
with type t = Frama_c_kernel.Filepath.t
type t = Frama_c_kernel.Filepath.tType of the parameter (an int, a string, etc). It is concrete for each module implementing this signature.
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.
Set the option to its default value, that is the value if set was never called.
val get_default : unit -> tGet the default value for the option.
val print_help : Format.formatter -> unitPrint 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.tThe kind of the registered state.
val mark_as_computed : ?project:Frama_c_kernel.Project.t -> unit -> unitIndicate 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 -> boolReturns 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.Sval add_hook_on_update : (Datatype.t -> unit) -> unitAdd 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) -> unithowto_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.tval set : Frama_c_kernel.Filepath.t -> unitSets the <user-dir> directory (without creating it).
val get : unit -> Frama_c_kernel.Filepath.t