module File:sig
..end
type
cpp_opt_kind =
| |
Gnu |
| |
Not_gnu |
| |
Unknown |
type
file =
| |
NeedCPP of |
(* |
The first string is the filename of the
.c to preprocess.
The second one is the preprocessor command (filename.c -o will be appended at the end). | *) |
| |
NoCPP of |
(* |
Already pre-processed file
.i | *) |
| |
External of |
(* |
file that can be translated into a Cil AST through an external
function, together with the recognized suffix.
| *) |
include Datatype.S
val new_file_type : string -> (string -> Cil_types.file * Cabs.file) -> unit
new_file_type suffix func funcname
registers a new type of files (with
corresponding suffix) as recognized by Frama-C through func
.val new_machdep : string -> Cil_types.mach -> unit
new_machdep name module
registers a new machdep name as recognized by
Frama-C through The usual uses is
Cmdline.run_after_loading_stage
(fun () -> File.new_machdep "my_machdep" my_machdep_implem)
Invalid_argument
if the given name already existsval machdep_macro : string -> string
machdep_macro machine
returns the name of a macro __FC_MACHDEP_XXX so
that the preprocessor can select std lib definition consistent with
the selected machdep. This function will emit a warning if machine
is
not known by default by the kernel and return __FC_MACHDEP_MACHINE in that
case.type
code_transformation_category
val register_code_transformation_category : string -> code_transformation_category
val add_code_transformation_before_cleanup : ?deps:(module Parameter_sig.S) list ->
?before:code_transformation_category list ->
?after:code_transformation_category list ->
code_transformation_category -> (Cil_types.file -> unit) -> unit
add_code_transformation_before_cleanup name hook
adds an hook in the corresponding category
that will be called during the normalization of a linked
file, before clean up and removal of temps and unused declarations.
If this transformation involves changing statements of a function f
,
f
must be flagged with File.must_recompute_cfg
.
The optional before
(resp after
) categories indicates that current
transformation must be executed before (resp after)
the corresponding ones, if they exist. In case of dependencies cycle,
an arbitrary order will be chosen for the transformations involved in
the cycle.
The optional deps
argument gives the list of options whose change
(e.g. after a -then
) will trigger the transformation over the already
computed AST. If several transformations are triggered by the same
option, their relative order is preserved.
At this level, globals and ACSL annotations have not been registered.
Since Neon-20140301
Consult the Plugin Development Guide for additional details.
val add_code_transformation_after_cleanup : ?deps:(module Parameter_sig.S) list ->
?before:code_transformation_category list ->
?after:code_transformation_category list ->
code_transformation_category -> (Cil_types.file -> unit) -> unit
Ast.mark_as_changed
or Ast.mark_as_grown
whenever it is the case.val constfold : code_transformation_category
val must_recompute_cfg : Cil_types.fundec -> unit
must_recompute_cfg f
must be called by code transformation hooks
when they modify statements in function f
. This will trigger a
recomputation of the cfg of f
after the transformation.val get_suffixes : unit -> string list
val get_name : t -> string
val get_preprocessor_command : unit -> string * cpp_opt_kind
val pre_register : t -> unit
val get_all : unit -> t list
val from_filename : ?cpp:string -> string -> t
!get_preprocessor_command ()
.val prepare_from_c_files : unit -> unit
File_types.Bad_Initialization
if called more than once.val init_from_c_files : t list -> unit
File_types.Bad_Initialization
if called more than once.val init_project_from_cil_file : Project.t -> Cil_types.file -> unit
File_types.Bad_Initialization
if called more than once.val init_project_from_visitor : ?reorder:bool -> Project.t -> Visitor.frama_c_visitor -> unit
init_project_from_visitor prj vis
initialize the cil file
representation of prj
. prj
must be essentially empty: it can have
some options set, but not an existing cil file; proj
is filled using
vis
, which must be a copy visitor that puts its results in prj
.
if reorder
is true
(default is false
) the new AST in prj
will be reordered.val create_project_from_visitor : ?reorder:bool ->
?last:bool -> string -> (Project.t -> Visitor.frama_c_visitor) -> Project.t
reorder
is true
, the globals in the
AST of the new project are reordered (default is false
). If last
is
true
(by default), remember than the returned project is the last
created one.
The visitor is responsible to avoid sharing between old file and new
file (i.e. it should use Cil.copy_visit
at some point).File_types.Bad_Initialization
if called more than once.reorder
optional argumentlast
optional argumentval create_rebuilt_project_from_visitor : ?reorder:bool ->
?last:bool ->
?preprocess:bool ->
string -> (Project.t -> Visitor.frama_c_visitor) -> Project.t
File.create_project_from_visitor
, but the new generated cil file is
generated into a temp .i or .c file according to preprocess
, then re-built
by Frama-C in the returned project. For instance, use this function if the
new cil file contains a constructor GText
as global.
Note that the generation of a preprocessed C file may fail in some cases
(e.g. if it includes headers already included). Thus the generated file is
NOT preprocessed by default.
Since Nitrogen-20111001
Raises File_types.Bad_Initialization
if called more than once.
Change in Fluorine-20130401: added reorder optional argument
val init_from_cmdline : unit -> unit
File_types.Bad_Initialization
if called more than once.val reorder_ast : unit -> unit
val reorder_custom_ast : Cil_types.file -> unit
val pretty_machdep : ?fmt:Format.formatter -> ?machdep:Cil_types.mach -> unit -> unit
machdep
, or the current one in current project
by default. Default output formatter is Log.print_on_output
.val pretty_ast : ?prj:Project.t -> ?fmt:Format.formatter -> unit -> unit
Kernel.CodeOutput.get_fmt ()
.File_types.Bad_Initialization
if the file is not initialized.