From 06345647227c88fd371cf1ef518e3d043821e1ce Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 1 Jun 2022 17:58:16 +0200
Subject: [PATCH] [devguide] blindly update check_api doc oracle

Blindly accept all changes in doc and type of plugin-dev-guide-labelled
values since last time `make check-dev-guide` was successfully launched
---
 doc/developer/check_api/run.oracle | 279 ++++++++++++++++++-----------
 1 file changed, 174 insertions(+), 105 deletions(-)

diff --git a/doc/developer/check_api/run.oracle b/doc/developer/check_api/run.oracle
index c5b9bea960a..ba68feb385a 100644
--- a/doc/developer/check_api/run.oracle
+++ b/doc/developer/check_api/run.oracle
@@ -1,157 +1,193 @@
 
 Cil.cilVisitor.fill_global_tables/unit/fill the global environment tables at the end of a full copy in a  new project./
-Project.load/?selection:State_selection.t -> ?name:string -> string -> t/Load a file into a new project given by its name.  More precisely, load only except name file:  1. creates a new project;2. performs all the registered before_load actions;3. loads the (specified) states of the project according to its  description; and4. performs all the registered after_load actions. raised exception: IOError./
+Project.load/?selection:State_selection.t -> ?name:string -> Filepath.Normalized.t -> t/Load a file into a new project given by its name. More precisely, load only except name file: 1. creates a new project;2. performs all the registered before_load actions;3. loads the (specified) states of the project according to its description; and4. performs all the registered after_load actions. raised exception: IOError./
 Log.Messages.error/'a Log.pretty_printer/user error: syntax/typing error, bad expected input, etc./
-Log.with_log_channel/Log.channel -> (Log.event -> 'b) -> ?kind:Log.kind -> ?prefix:Log.prefix -> ('a, 'b) Log.pretty_aborter/logging function to user-created channel./
 Cil.visitCilFile/Cil.cilVisitor -> Cil_types.file -> unit/Same thing, but the result is ignored. The given visitor must thus be an inplace visitor. Nothing is done if the visitor is a copy visitor./
-Type.t/parameters: 'a, constructors: /Type of type values. For each monomorphic type ty, a value of type ty t dynamically represents the type ty. Such a value is called a type value and should be unique for each static monomorphic type./
-Globals.Functions.get/Cil_types.varinfo -> Cil_types.kernel_function/Globals variables. raised exception: Not_found./
-Log.add_listener/?plugin:string -> ?kind:Log.kind list -> (Log.event -> unit) -> unit/Register a hook that is called each time an event is  emitted. Applies to all channel unless specified,  and all kind of messages unless specified./
+Type.t//Type of type values. For each monomorphic type ty, a value of type ty t dynamically represents the type ty. Such a value is called a type value and should be unique for each static monomorphic type./
+Dgraph_helper.graph_window/parent:GWindow.window -> title:string -> (packing:(GObj.widget -> unit) -> unit -> < adapt_zoom : unit -> unit; .. >) -> unit/Create a new window displaying a graph./
+Globals.Functions.get/Cil_types.varinfo -> Cil_types.kernel_function/Functions. The AST should be computed before using this module (cf. Ast.compute). raised exception: Not_found./
+Log.add_listener/?plugin:string -> ?kind:Log.kind list -> (Log.event -> unit) -> unit/Register a hook that is called each time an event is emitted. Applies to all channel unless specified, and all kind of messages unless specified. Warning: when executing the listener, all listeners will be temporarily deactivated in order to avoid infinite recursion./
 State_builder.Register/string end ) -> State_builder.S with module Datatype = Datatype/Register(Datatype)(State)(Info) registers a new state. Datatype represents the datatype of a state, Local_state explains how to deal with the client-side state and Info are additional required information./
 Parameter_sig.Builder.Zero/functor (X : Parameter_sig.Input_with_arg ) -> Parameter_sig.Int/What is the possible range of values for this parameter./
+Log.Messages.set_warn_status/Log.Messages.warn_category -> Log.warn_status -> unit/returns the warning category name as a string./
 Datatype.Ref/functor (T : Datatype.S ) -> Datatype.S with type t = T.t ref/Deep copy: no possible sharing between x and copy x./
+Datatype.S_with_collections.Hashtbl/Datatype.Hashtbl with type key = t/Deep copy: no possible sharing between x and copy x./
+Cil.visitAction.DoChildren//Continue with the children of this node. Rebuild the node on     return if any of the children changes (use == test)./
 Cil/Cil_types.stmt -> Cil_types.stmt * Cil_types.stmtend /CIL main API. CIL original API documentation is available as an html version at http://manju.cs.berkeley.edu/cil./
-Cil_types.logic_ctor_info/{ctor_name: string; ctor_type: Cil_types.logic_type_info; ctor_params: Cil_types.logic_type list}/Description of a constructor of a logic sum-type./
+Cil_types.stmtkind.Goto/ of Cil_types.stmt Stdlib.ref * Cil_types.location/A goto statement. Appears from actual goto's in the code or from goto's  that have been inserted during elaboration. The reference points to the  statement that is the target of the Goto. This means that you have to  update the reference whenever you replace the target statement. The  target statement MUST have at least a label./
+Cil_types.logic_ctor_info//Description of a constructor of a logic sum-type./
 Cil.cilVisitor.vlogic_var_use/Cil_types.logic_var -> Cil_types.logic_var Cil.visitAction//
 Cmdline.nop/Cmdline.exit//
 State_selection.t//Type of a state selection./
-Cil.register_behavior_extension/string -> (Cil.cilVisitor -> Cil_types.acsl_extension_kind -> Cil_types.acsl_extension_kind Cil.visitAction) -> unit/Indicates how an extended behavior clause is supposed to be visited. The default behavior is DoChildren, which ends up visiting  each identified predicate in the list and leave the id as is./
+Boot/sig end /Main entry point of Frama-C. Nothing is exported./
+Cil_types.stmtkind.UnspecifiedSequence/ of (Cil_types.stmt * Cil_types.lval list * Cil_types.lval list * Cil_types.lval list * Cil_types.stmt Stdlib.ref list)list/statements whose order of execution is not specified by  ISO/C. This is important for the order of side effects  during evaluation of expressions. Each statement comes  together with three list of lval, in this order.- lvals that are written during the sequence and whose future  value depends upon the statement (it is legal to read from them, but  not to write to them)- lvals that are written during the evaluation of the statement itself- lval that are read.- Function calls in the corresponding statement  Note that this include only a subset of the affectations  of the statement. Namely, the  temporary variables generated by cil are excluded (i.e. it  is assumed that the "compilation" is correct). In addition,  side effects caused by function applications are not taken  into account in the list. For a single statement, the written lvals  are supposed to be ordered (or their order of evaluation doesn't  matter), so that an alarm should be emitted only if the lvals read by  a statement overlap with the lvals written (or read) by another  statement of the sequence.  At this time this feature is  experimental and may miss some unspecified sequences.  In case you do not care about this feature just handle it  like a block (see Cil.block_from_unspecified_sequence)./
+Cil_types.stmtkind.Break/ of Cil_types.location/A break to the end of the nearest enclosing Loop or Switch./
 Datatype.unit/unit Type.t/Add sets, maps and hashtables modules to an existing datatype, provided the equal, compare and hash functions are not Datatype.undefined./
-Globals/(Cil_types.stmt -> Cil_types.block) Pervasives.refend /Operations on globals./
-Db.Main/(unit -> unit) Pervasives.refend /Frama-C main interface./
+Globals/(Cil_types.stmt -> Cil_types.kernel_function) Stdlib.refend /Operations on globals./
+Db.Main/(unit -> unit) Stdlib.refend /Frama-C main interface./
+Visitor_behavior.Get/Visitor_behavior.Get/Get operations on behaviors, allows to get the representative of an AST element in the current state of the visitor. Get.ast_element vis e with e of type ast_element gets the representative of e in vis. For example for Cil_types.varinfo: Get.varinfo vis vi./
+Visitor_behavior.Set/Visitor_behavior.Set/Set operations on behaviors, allows to change the representative of a given AST element in the current state of the visitor. Use with care (i.e. makes sure that the old one is not referenced anywhere in the AST, or sharing will be lost). Set.ast_element vis e s with e and s of type ast_element changes the representative of e to s in vis. For example, for Cil_types.varinfo: Set.varinfo vis vi new_representative./
 Db.Properties/Emitter.t -> Cil_types.kernel_function -> Cil_types.stmt -> string -> unitend /Dealing with logical properties./
-Cil_types.enuminfo/{eorig_name: string; mutable ename: string; mutable eitems: Cil_types.enumitem list; mutable eattr: Cil_types.attributes; mutable ereferenced: bool; mutable ekind: Cil_types.ikind}/Information about an enumeration./
+Visitor_behavior.Reset/Visitor_behavior.t -> unitend /Reset operations on behaviors, allows to reset the tables associated to a given kind of AST elements. If you use fresh instances of visitor for each round of transformation, you should not need this module. In place modifications do not need this at all. Reset.ast_element vis resets the tables associated to the considered type of AST elements in vis. For example for Cil_types.varinfo: Reset.varinfo vis./
+Cil_types.enuminfo//Information about an enumeration./
 Datatype.Polymorphic/((Project_skeleton.t -> bool) -> 'a -> bool) -> (Project_skeleton.t -> bool) -> 'a Datatype.t -> bool end ) -> Datatype.Polymorphic with type 'a poly = 'a P.t/Functor for polymorphic types with only 1 type variable./
+Log.Messages.register_warn_category/string -> Log.Messages.warn_category/Returns currently active keys/
+Cil.visitAction.JustCopy//visit the children, but only to make the necessary copies     (only useful for copy visitor)./
+Cil_datatype.Stmt/Stdlib.Format.formatter -> t -> unitend /Pretty print the sid of the statement/
 Datatype.Polymorphic3/((Project_skeleton.t -> bool) -> 'a -> bool) -> ((Project_skeleton.t -> bool) -> 'b -> bool) -> ((Project_skeleton.t -> bool) -> 'c -> bool) -> (Project_skeleton.t -> bool) -> ('a, 'b, 'c) Datatype.t -> bool end ) -> Datatype.Polymorphic3 with type ('a, 'b, 'c) poly = ('a, 'b, 'c) P.t/Functor for polymorphic types with 3 type variables./
 Datatype.string/string Type.t//
+Visitor_behavior.Set_orig/Visitor_behavior.Set/Set operations on behaviors related to original representatives, allows to change the reference of an element of the new AST in the current state of the visitor. Use with care. Set.ast_element vis e s with e and s of type ast_element changes the original representative of e to s in vis. For example, for Cil_types.varinfo: Set_orig.varinfo vis vi new_original_repr./
+Cmdline.stage.Extended//The stage where plug-ins are loaded.     It is also the first stage each time the Frama-C main     loop is run (e.g. after each "-then")./
+Pretty_source.localizable.PVDecl/ of (Cil_types.kernel_function option * Cil_types.kinstr * Cil_types.varinfo)/Declaration and definition of variables and function. Check the type  of the varinfo to distinguish between the various possibilities.  If the varinfo is a global or a local, the kernel_function is the  one in which the variable is declared. The kinstr argument is given  for local variables with an explicit initializer./
 Locations.Location/Datatype.S with type t = location/Misc/
 Parameter_sig.Builder.Int/int end ) -> Parameter_sig.Int/To be used by the plugin to output the results of the option  in a controlled way. See set_output_dependencies details./
 Db.Main.extend/(unit -> unit) -> unit/Register a function to be called by the Frama-C main entry point./
 Annotations/State.tend /Annotations in the AST. The AST should be computed before calling functions of this module./
-Gtk_helper.graph_window/parent:GWindow.window -> title:string -> (packing:(GObj.widget -> unit) -> unit -> < adapt_zoom : unit -> unit; .. >) -> unit/Create a new window displaying a graph./
-Cmdline.run_after_exiting_stage/(unit -> Cmdline.exit) -> unit/Register an action to be executed at the end of the exiting stage.  The guarded action must finish by exit n./
+Cmdline.run_after_exiting_stage/(unit -> Cmdline.exit) -> unit/Register an action to be executed at the end of the exiting stage. The guarded action must finish by exit n./
 Cil.cilVisitor.vvrbl/Cil_types.varinfo -> Cil_types.varinfo Cil.visitAction/Invoked on each variable use. Here only the SkipChildren and  ChangeTo actions make sense since there are no subtrees. Note that  the type and attributes of the variable are not traversed for a  variable use./
-Cil_types.varinfo/{mutable vname: string; vorig_name: string; mutable vtype: Cil_types.typ; mutable vattr: Cil_types.attributes; mutable vstorage: Cil_types.storage; mutable vglob: bool; mutable vdefined: bool; mutable vformal: bool; mutable vinline: bool; mutable vdecl: Cil_types.location; mutable vid: int; mutable vaddrof: bool; mutable vreferenced: bool; vtemp: bool; mutable vdescr: string option; mutable vdescrpure: bool; mutable vghost: bool; vsource: bool; mutable vlogic_var_assoc: Cil_types.logic_var option}/Information about a variable./
+Cil_types.varinfo//Information about a variable./
 Lmap_bitwise/functor (V : Lmap_bitwise.With_default ) -> Lmap_bitwise.Location_map_bitwise with type v = V.tend /Functors making map indexed by zone./
-Cil.cilVisitor.behavior/Cil.visitor_behavior/the kind of behavior expected for the behavior./
+Cil.cilVisitor.behavior/Visitor_behavior.t/the kind of behavior expected for the behavior./
+Eva.Analysis.compute/unit -> unit/Computes the Eva analysis, if not already computed, using the entry point  of the current project. You may set it with Globals.set_entry_point. raised exceptions: , if the entry point is incorrect, if some arguments are  specified for the entry point using Db.Value.fun_set_args, and  an incorrect number of them is given./
 Datatype.Serializable_undefined/Datatype.Undefined/Same as Datatype.Undefined, but the type is supposed to be marshallable by the standard OCaml way (in particular, no hash-consing or projects inside the type)./
-Log.Messages.feedback/?ontty:Log.ontty -> ?level:int -> ?dkey:Log.category -> 'a Log.pretty_printer/Progress and feedback. Level is tested against the verbosity level./
-Log.set_echo/?plugin:string -> ?kind:Log.kind list -> bool -> unit/Turns echo on or off. Applies to all channel unless specified,  and all kind of messages unless specified./
+Log.Messages.feedback/?ontty:Log.ontty -> ?level:int -> ?dkey:Log.Messages.category -> 'a Log.pretty_printer/Progress and feedback. Level is tested against the verbosity level./
+Log.set_echo/?plugin:string -> ?kind:Log.kind list -> bool -> unit/Turns echo on or off. Applies to all channel unless specified, and all kind of messages unless specified./
 Db.Value.self/State.t/Internal state of the value analysis from projects viewpoint./
 Log.new_channel/string -> Log.channel/Send an event over the associated listeners./
-Log.Messages.warning/'a Log.pretty_printer/Hypothesis and restrictions./
-Cil.get_stmt/Cil.visitor_behavior -> Cil_types.stmt -> Cil_types.stmt//
+Log.Messages.warning/?wkey:Log.Messages.warn_category -> 'a Log.pretty_printer/Hypothesis and restrictions./
 Datatype.Undefined/Datatype.Undefined/Sub-signature of Datatype.S./
-Cil_types.fieldinfo/{mutable fcomp: Cil_types.compinfo; forig_name: string; mutable fname: string; mutable ftype: Cil_types.typ; mutable fbitfield: int option; mutable fattr: Cil_types.attributes; mutable floc: Cil_types.location; mutable faddrof: bool; mutable fsize_in_bits: int option; mutable foffset_in_bits: int option; mutable fpadding_in_bits: int option}/Information about a struct/union field./
-Cmdline.is_going_to_load/unit -> unit/To be call if one action is going to run after the loading stage.  It is not necessary to call this function if the running action is set by  an option put on the command line./
+Cil_types.fieldinfo//Information about a struct/union field./
+Cmdline.is_going_to_load/unit -> unit/To be call if one action is going to run after the loading stage. It is not necessary to call this function if the running action is set by an option put on the command line./
 Datatype.func/?label:string * (unit -> 'a) option -> 'a Type.t -> 'b Type.t -> ('a -> 'b) Type.t//
+Cil_types.stmtkind.If/ of Cil_types.exp * Cil_types.block * Cil_types.block * Cil_types.location/A conditional. Two successors, the "then" and the "else" branches (in  this order).  Both branches fall-through to the successor of the If statement./
 Datatype.Function/(string * (unit -> Datatype.t) option) option end ) -> functor (T2 : Datatype.S ) -> Datatype.S with type t = T1.t -> T2.t/Deep copy: no possible sharing between x and copy x./
-Project.clear/?selection:State_selection.t -> ?project:t -> unit -> unit/Clear the given project. Default project is current (). All the  internal states of the given project are now empty (wrt the action  registered with register_todo_on_clear)./
-Kernel.CodeOutput/(Format.formatter -> unit) -> unitend /Behavior of option "-ocode"./
+Project.clear/?selection:State_selection.t -> ?project:t -> unit -> unit/Clear the given project. Default project is current (). All the internal states of the given project are now empty (wrt the action registered with register_todo_on_clear)./
+Kernel.CodeOutput/(Stdlib.Format.formatter -> unit) -> unitend /Behavior of option "-ocode"./
+Datatype.S_with_collections.Set/Datatype.Set with type elt = t/Datatype with alternative ordering, where properties are ordered according the following criteria: 1. Kf name (global properties ranked first) 2. Kinstr 3. kind of property 4. id of the property/
 Datatype.int/int Type.t//
+Cil.visitAction.ChangeTo/ of 'a/Replace the expression with the given one./
 Log.Messages.fatal/('a, 'b) Log.pretty_aborter/internal error of the plug-in. raised exception: AbortFatal./
+Dataflow2/Cil_types.fundec -> Cil_types.stmt list * Cil_types.stmt listend /Implementation of data flow analyses over user-supplied domains./
 Cil.cilVisitor.vexpr/Cil_types.exp -> Cil_types.exp Cil.visitAction/Invoked on each expression occurrence. The subtrees are the  subexpressions, the types (for a Cast or SizeOf expression) or the  variable use./
 Parameter_customize/(string -> Cil_datatype.Kf.Set.t) -> unitend /Configuration of command line options. You can apply the functions below just before applying one of the functors provided by the functor Plugin.Register and generating a new parameter./
 Cmdline.run_during_extending_stage/(unit -> unit) -> unit/Register an action to be executed during the extending stage./
-File.init_project_from_cil_file/Project.t -> Cil_types.file -> unit/Initialize the cil file representation with the given file for the  given project from the current one.  Should be called at most once per project. raised exception: File_types.Bad_Initialization./
-Datatype.func2/?label1:string * (unit -> 'a) option -> 'a Type.t -> ?label2:string * (unit -> 'b) option -> 'b Type.t -> 'c Type.t -> ('a -> 'b -> 'c) Type.t/optlabel_func lab dft ty1 ty2 is equivalent to  func ~label:(lab, Some dft) ty1 ty2/
-Cil.visitAction/parameters: 'a, constructors: | SkipChildren/Do not visit the children. Return the node as it is./
-Log.Messages/Log.Messages/Returns currently active keys/
-Extlib.the/?exn:exn -> 'a option -> 'a/opt_bind f x returns None if x is None and f y if is Some y (monadic bind) raised exceptions: , if the value is None and exn is specified., if the value is None and exn is not specified./
+File.init_project_from_cil_file/Project.t -> Cil_types.file -> unit/Initialize the cil file representation with the given file for the given project from the current one. Should be called at most once per project. raised exception: File_types.Bad_Initialization./
+Datatype.func2/?label1:string * (unit -> 'a) option -> 'a Type.t -> ?label2:string * (unit -> 'b) option -> 'b Type.t -> 'c Type.t -> ('a -> 'b -> 'c) Type.t/optlabel_func lab dft ty1 ty2 is equivalent to func ~label:(lab, Some dft) ty1 ty2/
+Cil.visitAction//Different visiting actions. 'a will be instantiated with exp, instr, etc./
+Log.Messages/Log.Messages//
+Cil_types.code_annotation_node.AExtended/ of string list * bool * Cil_types.acsl_extension/extension in a code or loop annotation.  Boolean flag is true for loop extensions and false for code extensions/
 Parameter_sig.Builder.String_set/functor (X : Parameter_sig.Input_with_arg ) -> Parameter_sig.String_set/Is there some element satisfying the given predicate?/
-Cil.inplace_visit/unit -> Cil.visitor_behavior/In-place modification. Behavior of the original cil visitor./
 Cmdline.Exit///
 Cil_state_builder.Stmt_hashtbl/functor (Data : Datatype.S ) -> functor (Info : State_builder.Info_with_size ) -> State_builder.Hashtbl with type key = Cil_types.stmt and type data = Data.t/Return the list of all data associated with the given key./
-State_builder.Hashtbl/functor (H : Datatype.Hashtbl ) -> functor (Data : Datatype.S ) -> functor (Info : State_builder.Info_with_size ) -> State_builder.Hashtbl with type key = H.key and type data = Data.t   and module Datatype = H.Make(Data)/remove x removes from the table one instance of x. Does nothing if  there is no instance of x./
+State_builder.Hashtbl/functor (H : Datatype.Hashtbl ) -> functor (Data : Datatype.S ) -> functor (Info : State_builder.Info_with_size ) -> State_builder.Hashtbl with type key = H.key and type data = Data.t        and module Datatype = H.Make(Data)/remove x removes from the table one instance of x. Does nothing if  there is no instance of x./
 Parameter_sig.Builder.True/functor (X : Parameter_sig.Input ) -> Parameter_sig.Bool/Set the boolean to false./
 Parameter_sig.Builder/Parameter_sig.Builder/Signatures containing the different functors which may be used to generate new command line options./
+Acsl_extension.register_global_block/string -> ?preprocessor:Acsl_extension.extension_preprocessor_block -> Acsl_extension.extension_typer_block -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/Registers extension for global block annotation. See register_behavior./
+Typed_parameter/t -> stringend /Parameter settable through a command line option. This is a low level API, internally used by the kernel. As a plug-in developer, you certainly prefer to use the API of Plugin instead./
 Log.Messages.abort/('a, 'b) Log.pretty_aborter/user error stopping the plugin. raised exception: AbortError./
 Kernel_function/State.tend /Operations to get info from a kernel function. This module does not give access to information about the set of all the registered kernel functions (like iterators over kernel functions). This kind of operations is stored in module Globals.Functions./
 Datatype.String/Datatype.S_with_collections with type t = string/Deep copy: no possible sharing between x and copy x./
 File.init_from_cmdline/unit -> unit/Initialize the cil file representation with the file given on the command line. Should be called at most once per project. raised exception: File_types.Bad_Initialization./
-File.init_from_c_files/t list -> unit/Initialize the cil file representation of the current project.  Should be called at most once per project. raised exception: File_types.Bad_Initialization./
-Cil_types.mach/{sizeof_short: int; sizeof_int: int; sizeof_long: int; sizeof_longlong: int; sizeof_ptr: int; sizeof_float: int; sizeof_double: int; sizeof_longdouble: int; sizeof_void: int; sizeof_fun: int; size_t: string; wchar_t: string; ptrdiff_t: string; alignof_short: int; alignof_int: int; alignof_long: int; alignof_longlong: int; alignof_ptr: int; alignof_float: int; alignof_double: int; alignof_longdouble: int; alignof_str: int; alignof_fun: int; char_is_unsigned: bool; underscore_name: bool; const_string_literals: bool; little_endian: bool; alignof_aligned: int; has__builtin_va_list: bool; __thread_is_keyword: bool; compiler: string; cpp_arch_flags: string list; version: string}/Definition of a machine model (architecture + compiler)./
-Ast.mark_as_grown/unit -> unit/call this function whenever you have added something to the AST,  without modifying the existing nodes/
-Globals.set_entry_point/string -> bool -> unit/set_entry_point name lib sets Kernel.MainFunction to name and  Kernel.LibEntry to lib. Moreover, clear the results of all the analysis which depend on Kernel.MainFunction or Kernel.LibEntry./
+File.init_from_c_files/t list -> unit/Initialize the cil file representation of the current project. Should be called at most once per project. raised exception: File_types.Bad_Initialization./
+Cil_types.mach//Definition of a machine model (architecture + compiler)./
+Ast.mark_as_grown/unit -> unit/call this function whenever you have added something to the AST, without modifying the existing nodes/
+Globals.set_entry_point/string -> bool -> unit/set_entry_point name lib sets Kernel.MainFunction to name and Kernel.LibEntry to lib. Moreover, clear the results of all the analysis which depend on Kernel.MainFunction or Kernel.LibEntry./
+State_selection.only_dependencies/State.t -> State_selection.t/The selection containing all the dependencies of the given state (but not this state itself)./
 Cmdline/Cmdline.Group.t -> stringend end /Command line parsing./
+Datatype.Ty.t//A type with its type value./
 Design.main_window_extension_points.register_source_selector/(GMenu.menu GMenu.factory -> Design.main_window_extension_points -> button:int -> Pretty_source.localizable -> unit) -> unit/register an action to perform when button is released on a given  localizable.  If the button 3 is released, the first argument is popped as a  contextual menu./
 Frontc.add_syntactic_transformation/(Cabs.file -> Cabs.file) -> unit/add a syntactic transformation that will be applied to all freshly parsed C files./
 Project/unit -> unitend end /Projects management. A project groups together all the internal states of Frama-C. An internal state is roughly the result of a computation which depends of an AST. It is possible to have many projects at the same time. For registering a new state in the Frama-C projects, apply the functor State_builder.Register./
 Visitor.frama_c_visitor.current_kf/Cil_types.kernel_function option/link to the kernel function currently being visited.  NB: for copy visitors, the link is to the original kf (anyway,  the new kf is created only after the visit is over)./
 Datatype.undefined/'a -> 'b/Must be used if you don't want to implement a required function./
+Cil_types.stmtkind.TryExcept/ of Cil_types.block * (Cil_types.instr list * Cil_types.exp) * Cil_types.block * Cil_types.location/On MSVC we support structured exception handling. The try/except  statement is a bit tricky:    __try { blk } __except (e) { handler }   The argument to __except must be an expression. However, we keep a  list of instructions AND an expression in case you need to make  function calls. We'll print those as a comma expression. The control  can get to the __except expression only if an exception is thrown.  After that, depending on the value of the expression the control  goes to the handler, propagates the exception, or retries the  exception. The location corresponds to the try keyword./
 Log.Messages.failure/'a Log.pretty_printer/internal error of the plug-in./
 Logic_const.prel/?loc:Cil_types.location -> Cil_types.relation * Cil_types.term * Cil_types.term -> Cil_types.predicate/Binary relation./
+Cil.visitAction.ChangeDoChildrenPost/ of 'a * ('a -> 'a)/First consider that the entire exp is replaced by the first parameter. Then  continue with the children. On return rebuild the node if any of the  children has changed and then apply the function on the node./
 Locations.Zone/Locations.Zone.map_t -> Int_Intervals.t Hptmap.Shape(Base.Base).tend /Association between bases and ranges of bits./
-Cil.cilVisitor.get_filling_actions/(unit -> unit) Queue.t/get the queue of actions to be performed at the end of a full copy./
-Locations.location/{loc: Locations.Location_Bits.t; size: Int_Base.t}/A Location_Bits.t and a size in bits./
+Cil.cilVisitor.get_filling_actions/(unit -> unit) Stdlib.Queue.t/get the queue of actions to be performed at the end of a full copy./
+Locations.location//A Location_Bits.t and a size in bits./
 Cil_types/end /The Abstract Syntax of CIL./
 Visitor.frama_c_visitor.vstmt_aux/Cil_types.stmt -> Cil_types.stmt Cil.visitAction/Replacement of vstmt./
-File.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./
+File.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./
 Datatype.Polymorphic4/((Project_skeleton.t -> bool) -> 'a -> bool) -> ((Project_skeleton.t -> bool) -> 'b -> bool) -> ((Project_skeleton.t -> bool) -> 'c -> bool) -> ((Project_skeleton.t -> bool) -> 'd -> bool) -> (Project_skeleton.t -> bool) -> ('a, 'b, 'c, 'd) Datatype.t -> bool end ) -> Datatype.Polymorphic4 with type ('a, 'b, 'c, 'd) poly = ('a, 'b, 'c, 'd) P.t/Functor for polymorphic types with 4 type variables./
 Datatype.List/functor (T : Datatype.S ) -> Datatype.S with type t = T.t list/Deep copy: no possible sharing between x and copy x./
 Structural_descr.pack/Structural_descr.t -> Structural_descr.pack/Pack a structural descriptor in order to embed it inside another one./
 Log.set_output/?isatty:bool -> (string -> int -> int -> unit) -> (unit -> unit) -> unit/This function has the same parameters as Format.make_formatter./
-Cil.reset_behavior_varinfo/Cil.visitor_behavior -> unit/resets the internal tables used by the given visitor_behavior. If you use fresh instances of visitor for each round of transformation, this should not be needed. In place modifications do not need that at all./
-Logic_utils.expr_to_term/cast:bool -> Cil_types.exp -> Cil_types.term/translates a C expression into an "equivalent" logical term. cast specifies how C arithmetic operators are translated.  When cast is true, the translation returns a logic term having the  same semantics of the C expr by introducing casts (i.e. the C expr a+b  can be translated as (char)(((char)a)+(char)b) to preserve the modulo  feature of the C addition). Otherwise, no such casts are introduced and the C arithmetic operators are  translated into perfect mathematical operators (i.e. a floating point  addition is translated into an addition of real numbers)./
-Journal/(string -> string) Pervasives.refend /Journalization of functions./
+Log.Messages.logwith/(Log.event option -> 'b) -> ?wkey:Log.Messages.warn_category -> ?emitwith:(Log.event -> unit) -> ?once:bool -> ('a, 'b) Log.pretty_aborter/Recommanded generic log routine using warn_category instead of kind.  logwith continuation ?wkey fmt similar to warning ?wkey fmt  and then calling the continuation.  The optional continuation argument refers to the corresponding event.  None is used iff no message is logged.  In case the wkey is considered as a Failure, the continution is not called.  This kind of message denotes a fatal error aborting Frama-C.  Notice that the ~emitwith action is called iff a message is logged./
+Logic_utils.expr_to_term/?coerce:bool -> Cil_types.exp -> Cil_types.term/Returns a logic term that has exactly the same semantics as the original C-expression. The type of the resulting term is determined by the ~coerce flag as follows:- when ~coerce:false is given (the default) the term has the same  c-type as the original expression.- when ~coerce:true is given, if the original expression has an int or  float type, then the returned term is coerced into the integer or real  logic type, respectively. Remark: when the original expression is a comparison, it is evaluated as an int or an integer depending on the ~coerce flag. To obtain a boolean or predicate, use expr_to_boolean or expr_to_predicate instead./
+Journal/(string -> Datatype.Filepath.t) Stdlib.refend /Journalization of functions./
 Cil.cilVisitor.vstmt/Cil_types.stmt -> Cil_types.stmt Cil.visitAction/Control-flow statement. The default DoChildren action does not create a  new statement when the components change. Instead it updates the contents  of the original statement. This is done to preserve the sharing with  Goto and Case statements that point to the original statement. If you  use the ChangeTo action then you should take care of preserving that  sharing yourself./
-Cil.get_varinfo/Cil.visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo/retrieve the representative of a given varinfo in the current state of the visitor/
-Eva.Analysis.is_computed/unit -> bool/Return true iff the value analysis has been done./
+Db.Value.is_computed/unit -> bool/Return true iff the value analysis has been done./
 Kernel.Unicode/('a -> 'b) -> 'a -> 'bend /Behavior of option "-unicode"./
 Design.register_extension/(Design.main_window_extension_points -> unit) -> unit/Register an extension to the main GUI. It will be invoked at initialization time./
-Cil_types.global/ | GType of Cil_types.typeinfo * Cil_types.location | GCompTag of Cil_types.compinfo * Cil_types.location | GCompTagDecl of Cil_types.compinfo * Cil_types.location | GEnumTag of Cil_types.enuminfo * Cil_types.location | GEnumTagDecl of Cil_types.enuminfo * Cil_types.location | GVarDecl of Cil_types.varinfo * Cil_types.location | GFunDecl of Cil_types.funspec * Cil_types.varinfo * Cil_types.location | GVar of Cil_types.varinfo * Cil_types.initinfo * Cil_types.location | GFun of Cil_types.fundec * Cil_types.location | GAsm of string * Cil_types.location | GPragma of Cil_types.attribute * Cil_types.location | GText of string | GAnnot of Cil_types.global_annotation * Cil_types.location/The main type for representing global declarations and definitions. A list of these form a CIL file. The order of globals in the file is generally important./
+Cil_types.global//The main type for representing global declarations and definitions. A list of these form a CIL file. The order of globals in the file is generally important./
 Cil.dummyStmt/Cil_types.stmt/A statement consisting of just dummyInstr./
 Datatype.func3/?label1:string * (unit -> 'a) option -> 'a Type.t -> ?label2:string * (unit -> 'b) option -> 'b Type.t -> ?label3:string * (unit -> 'c) option -> 'c Type.t -> 'd Type.t -> ('a -> 'b -> 'c -> 'd) Type.t//
-Cil.cilVisitor//A visitor interface for traversing CIL trees. Create instantiations of this type by specializing the class Cil.nopCilVisitor. Each of the specialized visiting functions can also call the queueInstr to specify that some instructions should be inserted before the current instruction or statement. Use syntax like self#queueInstr to call a method associated with the current object. Important Note for Frama-C Users: Unless you really know what you are doing, you should probably inherit from the Visitor.generic_frama_c_visitor instead of Cil.genericCilVisitor or Cil.nopCilVisitor/
+Cmdline.stage.Loading//After Extended, the stage where a previous Frama-C     internal states is restored (e.g. the one specified by     -load or by running the journal)./
+Cil.cilVisitor//A visitor interface for traversing CIL trees. Create instantiations of this type by specializing the class Cil.nopCilVisitor. Each of the specialized visiting functions can also call the queueInstr to specify that some instructions should be inserted before the current statement. Use syntax like self#queueInstr to call a method associated with the current object. Important Note for Frama-C Users: Unless you really know what you are doing, you should probably inherit from the Visitor.generic_frama_c_visitor instead of Cil.genericCilVisitor or Cil.nopCilVisitor/
 Cil.lzero/?loc:Cil_types.location -> unit -> Cil_types.term/The constant logic term zero./
 Db.Value.is_reachable/Db.Value.state -> bool/add_formals_to_state state kf exps evaluates exps in state  and binds them to the formal arguments of kf in the resulting  state/
-Cil_types.compinfo/{mutable cstruct: bool; corig_name: string; mutable cname: string; mutable ckey: int; mutable cfields: Cil_types.fieldinfo list; mutable cattr: Cil_types.attributes; mutable cdefined: bool; mutable creferenced: bool}/The definition of a structure or union type. Use Cil.mkCompInfo to make one and use Cil.copyCompInfo to copy one (this ensures that a new key is assigned and that the fields have the right pointers to parents.)./
-Cil_types.logic_type_info/{lt_name: string; lt_params: string list; mutable lt_def: Cil_types.logic_type_def option; mutable lt_attr: Cil_types.attributes}/Description of a logic type./
+Cil_types.compinfo//The definition of a structure or union type. Use Cil.mkCompInfo to make one and use Cil.copyCompInfo to copy one (this ensures that a new key is assigned and that the fields have the right pointers to parents.)./
+Cil_types.logic_type_info//Description of a logic type./
 Cmdline.run_after_loading_stage/(unit -> unit) -> unit/Register an action to be executed at the end of the loading stage./
 Locations/Base.t -> Cil_types.typ -> Cil_types.offset -> Locations.locationend /Memory locations./
-File.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./
+Logic_const.new_acsl_extension/string -> Cil_types.location -> bool -> Cil_types.acsl_extension_kind -> Cil_types.acsl_extension/creates a new acsl_extension with a fresh id./
+Acsl_extension.register_code_annot_next_stmt/string -> ?preprocessor:Acsl_extension.extension_preprocessor -> Acsl_extension.extension_typer -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/Registers extension for code annotation to be evaluated for the _next_ statement. See register_behavior./
+File.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./
 Parameter_sig.Builder.Kernel_function_set/functor (X : Parameter_sig.Input_with_arg ) -> Parameter_sig.Kernel_function_set/Is there some element satisfying the given predicate?/
 Ast.add_monotonic_state/State.t -> unit/indicates that the given state (which must depend on Ast.self) is robust against additions to the AST, that is, it will be able to compute information on the new nodes whenever needed. Ast.mark_as_grown will not erase such states, while Ast.mark_as_changed and clearing Ast.self itself will./
 Visitor.visitFramacFunction/Visitor.frama_c_visitor -> Cil_types.fundec -> Cil_types.fundec/Visit a function definition./
-File.create_project_from_visitor/?reorder:bool -> ?last:bool -> string -> (Project.t -> Visitor.frama_c_visitor) -> Project.t/Return a new project with a new cil file representation by visiting the  file of the current project. If 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). raised exception: File_types.Bad_Initialization./
+File.create_project_from_visitor/?reorder:bool -> ?last:bool -> string -> (Project.t -> Visitor.frama_c_visitor) -> Project.t/Return a new project with a new cil file representation by visiting the file of the current project. If 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). raised exception: File_types.Bad_Initialization./
+Cil_types.binop.Div////
 Parameter_sig.Bool/Parameter_sig.Bool/Signature for a boolean parameter./
-Visitor.generic_frama_c_visitor/Cil.visitor_behavior -> /Generic class that abstracts over frama_c_inplace and frama_c_copy./
-Db.Value.get_stmt_state/Cil_types.stmt -> Db.Value.state/Initial state used by the analysis/
-Logic_typing.typing_context/{is_loop: unit -> bool; anonCompFieldName: string; conditionalConversion: Cil_types.typ -> Cil_types.typ -> Cil_types.typ; find_macro: string -> Logic_ptree.lexpr; find_var: string -> Cil_types.logic_var; find_enum_tag: string -> Cil_types.exp * Cil_types.typ; find_comp_field: Cil_types.compinfo -> string -> Cil_types.offset; find_type: Logic_typing.type_namespace -> string -> Cil_types.typ; find_label: string -> Cil_types.stmt Pervasives.ref; remove_logic_function: string -> unit; remove_logic_type: string -> unit; remove_logic_ctor: string -> unit; add_logic_function: Cil_types.logic_info -> unit; add_logic_type: string -> Cil_types.logic_type_info -> unit; add_logic_ctor: string -> Cil_types.logic_ctor_info -> unit; find_all_logic_functions: string -> Cil_types.logic_info list; find_logic_type: string -> Cil_types.logic_type_info; find_logic_ctor: string -> Cil_types.logic_ctor_info; pre_state: Logic_typing.Lenv.t; post_state: Cil_types.termination_kind list -> Logic_typing.Lenv.t; assigns_env: Logic_typing.Lenv.t; silent: bool; type_predicate: Logic_typing.typing_context -> Logic_typing.Lenv.t -> Logic_ptree.lexpr -> Cil_types.predicate/typechecks a predicate. Note that the first argument is itself a  typing_context, which allows for open recursion. Namely, it is  possible for the extension to change the type-checking functions for  the sub-nodes of the parsed tree, and not only for the toplevel lexpr./
+Cil_types.stmtkind.Instr/ of Cil_types.instr/An instruction that does not contain control flow. Control implicitly  falls through./
+Visitor.generic_frama_c_visitor/Visitor_behavior.t -> /Generic class that abstracts over frama_c_inplace and frama_c_copy./
+Db.Value.get_stmt_state/?after:bool -> Cil_types.stmt -> Db.Value.state/after is false by default./
+Logic_typing.typing_context//Functions that can be called when type-checking an extension of ACSL./
 Parameter_sig.Builder.False/functor (X : Parameter_sig.Input ) -> Parameter_sig.Bool/Set the boolean to false./
 Cil.cilVisitor.vglob/Cil_types.global -> Cil_types.global list Cil.visitAction/Global (vars, types, etc.)/
+Cil_types.ext_category//Where are we expected to find corresponding extension keyword./
 Parameter_sig.Builder.String/string end ) -> Parameter_sig.String/What is the possible range of values for this parameter./
 State/t -> unitend /A state is a project-compliant mutable value./
 Type.name/'a Type.t -> string/Apply this functor to access to the abstract type of the given name./
-Log.Messages.debug/?level:int -> ?dkey:Log.category -> 'a Log.pretty_printer/Debugging information dedicated to Plugin developers.  Default level is 1. The debugging key is used in message headers.	See also set_debug_keys and set_debug_keyset./
+Log.Messages.debug/?level:int -> ?dkey:Log.Messages.category -> 'a Log.pretty_printer/Debugging information dedicated to Plugin developers.  Default level is 1. The debugging key is used in message headers.  See also set_debug_keys and set_debug_keyset./
 Cil_state_builder/functor (Data : Datatype.S ) -> functor (Info : State_builder.Info_with_size ) -> State_builder.Hashtbl with type key = Cil_types.kernel_function       and type data = Data.tend /Functors for building computations which use kernel datatypes./
-Cil_printer.register_behavior_extension/string -> (Printer_api.extensible_printer_type -> Format.formatter -> Cil_types.acsl_extension_kind -> unit) -> unit/Register a pretty-printer used for behavior extension./
+Log.Messages.warn_category//Same as above, but for warnings/
 Structural_descr.p_int/Structural_descr.pack/Equivalent to pack Abstract/
-Lmap/V.t Lmap.default_contents end ) -> module type of Lmap_sig with type v = V.t and type widen_hint_base = V.generic_widen_hint and type offsetmap = Offsetmap.tend /Maps from bases to memory maps. The memory maps are those of the Offsetmap module./
-Dynamic/string list -> unitend /Value accesses through dynamic typing./
-Kernel_function.dummy/unit -> t/callsites f collect the statements where f is called. Same  complexity as find_from_sid./
-Design/GSourceView2.source_buffer -> offset:int -> Property_status.Feedback.t -> unitend end /The extensible GUI./
+Lmap/V.t Lmap.default_contents end ) -> module type of Lmap_sig with type v = V.t and type widen_hint_base = V.numerical_widen_hint and type offsetmap = Offsetmap.tend /Maps from bases to memory maps. The memory maps are those of the Offsetmap module./
+Dynamic/string -> boolend /Value accesses through dynamic typing./
+Kernel_function.dummy/unit -> t/is_between b s1 s2 s3 returns true if the statement s2 appears strictly between s1 and s3 inside the b.bstmts list. All three statements must actually occur in b.bstmts, either directly or indirectly (see Kernel_function.find_enclosing_stmt_in_block). raised exception: AbortFatal./
+Design/GSourceView.source_buffer -> ?call_site:Cil_types.stmt -> offset:int -> Property_status.Feedback.t -> unitend end /The extensible GUI./
+Structural_descr.structure.Sum/ of Structural_descr.pack array array/Sum c describes a non-array type where c is an array describing  the non-constant constructors of the type being described (in the order  of their declarations in that type). Each element of this latter array  is an array of t that describes (in order) the fields of the  corresponding constructor./
+Visitor_behavior.inplace/unit -> Visitor_behavior.t/In-place modification. Behavior of the original cil visitor./
 Datatype.list/'a Type.t -> 'a list Type.t/Functor for polymorphic types with 4 type variables./
 Cil.cilVisitor.vlogic_var_decl/Cil_types.logic_var -> Cil_types.logic_var Cil.visitAction//
-Cil_types.typeinfo/{torig_name: string; mutable tname: string; mutable ttype: Cil_types.typ; mutable treferenced: bool}/Information about a defined type./
+Cil_types.typeinfo//Information about a defined type./
 Ast.self/State.t/The state kind associated to the cil AST./
 Type.AlreadyExists/string/May be raised by Type.register./
 Property_status/Property.t -> boolend /Status of properties./
 Datatype.never_any_project/(Project_skeleton.t -> bool) -> 'a -> bool/Must be used for mem_project if values of your type does never contain any project./
-Property/string -> stringend end /ACSL comparable property./
-Cil_datatype/unit -> unitend /Datatypes of some useful CIL types./
+Property/?truncate:int -> Property.identified_property -> stringend end /ACSL comparable property./
+Cil_datatype/S with type t = Logic_ptree.lexprend /Datatypes of some useful CIL types./
+Cmdline.stage.Early//Initial stage for very specific almost hard-coded     options. Do not use it./
+Acsl_extension.register_behavior/string -> ?preprocessor:Acsl_extension.extension_preprocessor -> Acsl_extension.extension_typer -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/register_behavior name ~preprocessor typer ~visitor ~printer ~short_printer status registers new ACSL extension to be used in function contracts with name name. The optional preprocessor is a function to be applied by the parser on the untyped content of the extension before parsing the rest of the processed file. By default, this function is the identity. The typer is applied when transforming the untyped AST to Cil. It recieves the typing context of the annotation that can be used to type the received logic expressions (see Logic_typing.typing_context), and the location of the annotation. The optional visitor allows changing the way the ACSL extension is visited. By default, the behavior is Cil.DoChildren, which ends up visiting each identified predicate/term in the list and leave the id as is. The optional printer allows changing the way the ACSL extension is pretty printed. By default, it prints the name of the extension followed by the formatted predicates, terms or identifier according to the Cil_types.acsl_extension_kind. The optional short_printer allows changing the Printer.pp_short_extended behavior for the ACSL extension. By default, it just prints the name. It is for example used for the filetree in the GUI. The status indicates whether the extension can be assigned a property status or not. Here is a basic example:  let count = ref 0 let foo_typer typing_context loc = function  | p :: [] ->  Ext_preds  [ (typing_context.type_predicate    typing_context    (typing_context.post_state [Normal])    p)])  | [] -> let id = !count in incr count; Ext_id id  | _ -> typing_context.error loc "expecting a predicate after keyword FOO" let () = Acsl_extension.register_behavior "FOO" foo_typer false /
 Datatype.Int/Datatype.S_with_collections with type t = int/Deep copy: no possible sharing between x and copy x./
 Datatype.Make/functor (X : Datatype.Make_input ) -> Datatype.S with type t = X.t/Generic datatype builder./
-Cil.set_varinfo/Cil.visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo -> unit/change the representative of a given varinfo in the current  state of the visitor. Use with care (i.e. makes sure that the old one  is not referenced anywhere in the AST, or sharing will be lost./
+Acsl_extension.register_code_annot_next_loop/string -> ?preprocessor:Acsl_extension.extension_preprocessor -> Acsl_extension.extension_typer -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/Registers extension for loop annotation. See register_behavior./
 Cmdline.run_after_setting_files/(string list -> unit) -> unit/Register an action to be executed just after setting the files put on the command line. The argument of the function is the list of files./
 Dynamic.register/?comment:string -> plugin:string -> string -> 'a Type.t -> journalize:bool -> 'a -> 'a/register ~plugin name ty v registers v with the name name, the type ty and the plug-in plugin. raised exception: Type.AlreadyExists./
+Cil_types.ext_code_annot_context//can be found both as normal code annot or loop annot./
+Acsl_extension.register_code_annot/string -> ?preprocessor:Acsl_extension.extension_preprocessor -> Acsl_extension.extension_typer -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/Registers extension for code annotation to be evaluated at _current_ program point. See register_behavior./
 Kernel/Parameter_sig.Boolend /Provided services for kernel developers./
 Emitter.create/string -> Emitter.kind list -> correctness:Typed_parameter.t list -> tuning:Typed_parameter.t list -> t/Emitter.create name kind ~correctness ~tuning creates a new emitter with the given name. The given parameters are the ones which impact the generated annotations/status. A "correctness" parameter may fully change a generated element when its value changes (for instance, a valid status may become invalid and conversely). A "tuning" parameter may improve a generated element when its value changes (for instance, a "dont_know" status may become valid or invalid, but a valid status cannot become invalid). The given name must be unique. raised exception: Invalid_argument./
+Type.precedence.Call//Instantiation of polymorphic type/
 Plugin.Register/string end ) -> Plugin.General_services/Functors for registering a new plug-in. It provides access to several services./
+Visitor_behavior.copy/Project.t -> Visitor_behavior.t/Makes fresh copies of the mutable structures.- preserves sharing for varinfo.- makes fresh copy of varinfo only for declarations. Variables that are  only used in the visited AST are thus still shared with the original  AST. This allows for instance to copy a function with its  formals and local variables, and to keep the references to other  globals in the function's body./
 Cil.cilVisitor.vlogic_type_info_decl/Cil_types.logic_type_info -> Cil_types.logic_type_info Cil.visitAction//
 Dynamic.Parameter.Bool/string -> unit -> unitend /Boolean parameters./
 Datatype/functor (W : Datatype.Sub_caml_weak_hashtbl ) -> functor (D : Datatype.S with type t = W.data ) -> Datatype.S with type t = W.tend /A datatype provides useful values for types. It is a high-level API on top of module Type./
-Lattice_type/Lattice_type.Lattice_Hashconsed_Setend /Lattice signatures./
+Lattice_type/Lattice_type.Lattice_Setend /Lattice signatures./
 Cabs2cil.convFile/Cabs.file -> Cil_types.file/new hook that will be called when processing a for loop. Argument is the increment part of the loop./
 Datatype.Pair/functor (T1 : Datatype.S ) -> functor (T2 : Datatype.S ) -> Datatype.S with type t = T1.t * T2.t/Deep copy: no possible sharing between x and copy x./
 Dynamic.get/plugin:string -> string -> 'a Type.t -> 'a/get ~plugin name ty returns the value registered with the name name, the type ty and the plug-in plugin. This plug-in will be loaded if required. raised exceptions: , if the name is not registered, if the name is not registered with a compatible type, _ in the -no-obj mode/
@@ -160,85 +196,118 @@ Annotations.add_assert/Emitter.t -> ?kf:Cil_types.kernel_function -> Cil_types.s
 Cil.visitCilFileCopy/Cil.cilVisitor -> Cil_types.file -> Cil_types.file/Visit a file. This will re-cons all globals TWICE (so that it is tail-recursive). Use Cil.visitCilFileSameGlobals if your visitor will not change the list of globals./
 Parameter_sig.Kernel_function_set/Parameter_sig.Set with type elt = Cil_types.kernel_function  and type t = Cil_datatype.Kf.Set.t/Set of defined kernel functions. If you want to also include pure prototype, use Parameter_customize.argument_may_be_fundecl./
 Parameter_sig.Builder.Empty_string/functor (X : Parameter_sig.Input_with_arg ) -> Parameter_sig.String/always return the argument, even if the argument is not a function name./
-Ast.mark_as_changed/unit -> unit/call this function whenever you've made some changes in place  inside the AST/
-Log.Messages.result/?level:int -> ?dkey:Log.category -> 'a Log.pretty_printer/Results of analysis. Default level is 1./
+Ast.mark_as_changed/unit -> unit/call this function whenever you've made some changes in place inside the AST/
+Log.Messages.result/?level:int -> ?dkey:Log.Messages.category -> 'a Log.pretty_printer/Results of analysis. Default level is 1./
 Kernel.SafeArrays/Parameter_sig.Bool/Behavior of option "-safe-arrays"./
-Cil_types.stmt/{mutable labels: Cil_types.label list; mutable skind: Cil_types.stmtkind; mutable sid: int; mutable succs: Cil_types.stmt list; mutable preds: Cil_types.stmt list; mutable ghost: bool}/Statements./
-Cil.visitCilFileSameGlobals/Cil.cilVisitor -> Cil_types.file -> unit/A visitor for the whole file that does not change the globals (but maybe changes things inside the globals). Use this function instead of Cil.visitCilFile whenever appropriate because it is more efficient for long files./
+Cil_types.stmt//Statements./
+Cil.visitCilFileSameGlobals/Cil.cilVisitor -> Cil_types.file -> unit/A visitor for the whole file that does not *physically* change the globals (but maybe changes things inside the globals through side-effects). Use this function instead of Cil.visitCilFile whenever appropriate because it is more efficient for long files./
+Datatype.S_with_collections/Datatype.S_with_collections/A datatype for a type t extended with predefined set, map and hashtbl over t./
 Cmdline.run_after_extended_stage/(unit -> unit) -> unit/Register an action to be executed at the end of the extended stage./
-Db.Value.compute/(unit -> unit) Pervasives.ref/Compute the value analysis using the entry point of the current  project. You may set it with Globals.set_entry_point. raised exceptions: , if the entry point is incorrect, if some arguments are  specified for the entry point using Db.Value.fun_set_args, and  an incorrect number of them is given./
-Cil_types.logic_info/{mutable l_var_info: Cil_types.logic_var; mutable l_labels: Cil_types.logic_label list; mutable l_tparams: string list; mutable l_type: Cil_types.logic_type option; mutable l_profile: Cil_types.logic_var list; mutable l_body: Cil_types.logic_body}/description of a logic function or predicate./
-Cil_types.fundec/{mutable svar: Cil_types.varinfo; mutable sformals: Cil_types.varinfo list; mutable slocals: Cil_types.varinfo list; mutable smaxid: int; mutable sbody: Cil_types.block; mutable smaxstmtid: int option; mutable sallstmts: Cil_types.stmt list; mutable sspec: Cil_types.funspec}/Function definitions./
-Locations.Location_Bytes/bool -> unitend /Association between bases and offsets in byte./
-Project.on/?selection:State_selection.t -> t -> ('a -> 'b) -> 'a -> 'b/on p f x sets the current project to p, computes f x then  restores the current project. You should use this function if you use a  project different of current ()./
+Db.Value.compute/(unit -> unit) Stdlib.ref/Compute the value analysis using the entry point of the current  project. You may set it with Globals.set_entry_point. raised exceptions: , if the entry point is incorrect, if some arguments are  specified for the entry point using Db.Value.fun_set_args, and  an incorrect number of them is given./
+Visitor_behavior.Get_orig/Visitor_behavior.Get/Get operations on behaviors, allows to get the original representative of an element of the new AST in the curent state of the visitor. Get_orig.ast_element vis new_e with new_e of type ast_element gets the original representative of new_e in vis. For example for Cil_types.varinfo: Get_orig.varinfo vis new_vi./
+Cil_types.stmtkind.TryFinally/ of Cil_types.block * Cil_types.block * Cil_types.location/On MSVC we support structured exception handling. This is what you might  expect. Control can get into the finally block either from the end of the  body block, or if an exception is thrown./
+Cil_types.logic_info//description of a logic function or predicate./
+Cil_types.fundec//Function definitions./
+Locations.Location_Bytes/Locations.Location_Bytes.t -> Locations.Location_Bytes.tend /Association between bases and offsets in byte./
+Project.on/?selection:State_selection.t -> t -> ('a -> 'b) -> 'a -> 'b/on p f x sets the current project to p, computes f x then restores the current project. You should use this function if you use a project different of current ()./
 Cabs/end /Untyped AST./
 Design.main_window_extension_points//This is the type of extension points for the GUI./
 Pretty_utils/?align:Pretty_utils.align -> ?pp:string Pretty_utils.formatter -> Pretty_utils.marger -> string Pretty_utils.formatterend /Pretty-printer utilities./
+Cil_types.binop.Mod//%/
 Dynamic.Parameter/string -> (string -> unit) -> unitend end /Module to use for accessing parameters of plug-ins. Assume that the plug-in is already loaded./
 Datatype.Polymorphic2/((Project_skeleton.t -> bool) -> 'a -> bool) -> ((Project_skeleton.t -> bool) -> 'b -> bool) -> (Project_skeleton.t -> bool) -> ('a, 'b) Datatype.t -> bool end ) -> Datatype.Polymorphic2 with type ('a, 'b) poly = ('a, 'b) P.t/Functor for polymorphic types with 2 type variables./
-Parameter_customize.set_negative_option_name/string -> unit/For boolean parameters, set the name of the negative  option generating automatically from the positive one (the given option  name). The default used value prefixes the given option name by "-no".  Assume that the given string is a valid option name or empty.  If it is empty, no negative option is created./
-Parameter_state.get_selection/?is_set:bool -> unit -> State_selection.t/Selection of all the settable parameters.  is_set is true by default (for backward compatibility): in such a  case, for each option, the extra internal state indicating whether it is  set also belongs to the selection./
+Cil_types.stmtkind.Block/ of Cil_types.block/Just a block of statements. Use it as a way to keep some block attributes  local./
+Cil.visitAction.JustCopyPost/ of ('a -> 'a)/same as JustCopy + applies the given function to the result./
+Parameter_customize.set_negative_option_name/string -> unit/For boolean parameters, set the name of the negative option generating automatically from the positive one (the given option name). The default used value prefixes the given option name by "-no". Assume that the given string is a valid option name or empty. If it is empty, no negative option is created./
+Parameter_state.get_selection/?is_set:bool -> unit -> State_selection.t/Selection of all the settable parameters. is_set is true by default (for backward compatibility): in such a case, for each option, the extra internal state indicating whether it is set also belongs to the selection./
 Cil.cilVisitor.vlogic_ctor_info_decl/Cil_types.logic_ctor_info -> Cil_types.logic_ctor_info Cil.visitAction//
-Project.save/?selection:State_selection.t -> ?project:t -> string -> unit/Save a given project in a file. Default project is current (). raised exception: IOError./
-Plugin/(Plugin.plugin -> unit) -> unitend /Provided plug-general services for plug-ins./
-Cil.get_original_varinfo/Cil.visitor_behavior -> Cil_types.varinfo -> Cil_types.varinfo/retrieve the original representative of a given copy of a varinfo  in the current state of the visitor./
-Cil_types.acsl_extension_kind/ | Ext_id of int | Ext_terms of Cil_types.term list | Ext_preds of Cil_types.predicate list/a list of predicates, the most common case of for extensions/
-Cabs.file//the string is a file name, and then the list of toplevel forms./
-Cil_datatype.Varinfo/tend /Identity of a key. Must verify id k >= 0 and       equal k1 k2 ==> id k1 = id k2/
+Project.save/?selection:State_selection.t -> ?project:t -> Filepath.Normalized.t -> unit/Save a given project in a file. Default project is current (). raised exception: IOError./
+Plugin/(Plugin.plugin -> 'a -> 'a) -> 'a -> 'aend /Plugin registration and general services./
+Datatype.Ty.ty/Datatype.Ty.t Type.t//
+Cil_types.acsl_extension_kind//a list of predicates, the most common case of for extensions/
+Cabs.file//the file name, and then the list of toplevel forms./
+State_selection.with_dependencies/State.t -> State_selection.t/The selection containing the given state and all its dependencies./
+Cil_datatype.Varinfo/tend /Identity of a key. Must verify id k >= 0 and      equal k1 k2 ==> id k1 = id k2/
+Analysis.is_computed/unit -> bool/Return true iff the Eva analysis has been done./
+Cil_types.global.GFun/ of Cil_types.fundec * Cil_types.location/A function definition./
 Cil.cilVisitor.vfile/Cil_types.file -> Cil_types.file Cil.visitAction/visit a whole file./
-Cil.copy_visit/Project.t -> Cil.visitor_behavior/Makes fresh copies of the mutable structures.- preserves sharing for varinfo.- makes fresh copy of varinfo only for declarations. Variables that are  only used in the visited AST are thus still shared with the original  AST. This allows for instance to copy a function with its  formals and local variables, and to keep the references to other  globals in the function's body./
-Log.print_delayed/(Format.formatter -> unit) -> unit/Direct printing on output. Same as print_on_output, except  that message echo is not delayed until text material is actually  written. This gives an chance for formatters to emit messages  before actual pretty printing.  Can not be recursively invoked./
+Cil_types.global_annotation.Dextended/ of Cil_types.acsl_extension * Cil_types.attributes * Cil_types.location/Extended global clause./
+Log.print_delayed/(Stdlib.Format.formatter -> unit) -> unit/Direct printing on output. Same as print_on_output, except that message echo is not delayed until text material is actually written. This gives an chance for formatters to emit messages before actual pretty printing. Can not be recursively invoked./
 Cil.cilVisitor.vvdec/Cil_types.varinfo -> Cil_types.varinfo Cil.visitAction/Invoked for each variable declaration. The children to be traversed  are those corresponding to the type and attributes of the variable.  Note that variable declarations are GVar, GVarDecl, GFun and  GFunDecl globals, the formals of functions prototypes, and the  formals and locals of function definitions. This means that the list  of formals of a function may be traversed multiple times if there exists  both a declaration and a definition, or multiple declarations./
+Datatype.S_no_copy.pretty/Stdlib.Format.formatter -> Datatype.t -> unit/Pretty print each value in an user-friendly way./
 Visitor.frama_c_inplace//in-place visitor; always act in the current project./
 Abstract_interp/functor (L1 : Lattice_type.AI_Lattice_with_cardinal_one ) -> functor (L2 : Lattice_type.AI_Lattice_with_cardinal_one ) -> Lattice_Sum with type t1 = L1.t and type t2 = L2.tend /Functors for generic lattices implementations./
+Eva.Analysis.is_computed/unit -> bool/Return true iff the Eva analysis has been done./
 Log.Messages.verify/bool -> ('a, bool) Log.pretty_aborter/If the first argument is true, return true and do nothing else,  otherwise, send the message on the fatal channel and return  false.  The intended usage is: assert (verify e "Bla...") ;./
-Ast.get/unit -> Cil_types.file/Get the cil file representation.  One of the initialisation function of module File has to be called  before using this function. raised exception: Bad_Initialization./
-Locations.enumerate_valid_bits/for_writing:bool -> Locations.location -> Locations.Zone.t/Is the valid part of the location bottom or a singleton?/
-File.add_code_transformation_after_cleanup/?deps:(module Parameter_sig.S) list -> ?before:File.code_transformation_category list -> ?after:File.code_transformation_category list -> File.code_transformation_category -> (Cil_types.file -> unit) -> unit/Same as above, but the hook is applied after clean up.  At this level, globals and ACSL annotations have been registered. If  the hook adds some new globals or annotations, it must take care of  adding them in the appropriate tables.  Note that it is the responsibility of the hook to use  Ast.mark_as_changed or Ast.mark_as_grown whenever it is the case./
-Cil_types.file/{mutable fileName: string; mutable globals: Cil_types.global list; mutable globinit: Cil_types.fundec option; mutable globinitcalled: bool}/The top-level representation of a CIL source file (and the result of the parsing and elaboration). Its main contents is the list of global declarations and definitions. You can iterate over the globals in a Cil_types.file using the following iterators: Cil.mapGlobals, Cil.iterGlobals and Cil.foldGlobals. You can also use the Cil.dummyFile when you need a Cil_types.file as a placeholder. For each global item CIL stores the source location where it appears (using the type Cil_types.location)/
-Type.par/Type.precedence -> Type.precedence -> Format.formatter -> (Format.formatter -> unit) -> unit/par context myself fmt pp puts parenthesis around the verbatim prints by pp according to the precedence myself of the verbatim and to the precedence context of the caller of the pretty printer. fmt is the output formatter. The typical use is the following: let pretty_print p_caller fmt x = let pp fmt = Format.fprintf "..." ... x ... in let myself = Call in par p_caller myself fmt pp/
-Logic_typing.register_behavior_extension/string -> (typing_context:Logic_typing.typing_context -> loc:Cil_types.location -> Logic_ptree.lexpr list -> Cil_types.acsl_extension_kind) -> unit/register_behavior_extension name f registers a typing function f to be used to type clause with name name. Here is a basic example: let count = ref 0 in let foo_typer ~typing_context ~loc ps = match ps with p::[] ->  Ext_preds     (typing_context.type_predicate    typing_context    (typing_context.post_state [Normal])    p))  | [] -> let id = !count in incr count; Ext_id id  | _ -> typing_context.error loc "expecting a predicate after keyword FOO" let () = register_behavior_extension "FOO" foo_typer/
+Cil.visitAction.SkipChildren//Do not visit the children. Return the node as it is./
+Ast.get/unit -> Cil_types.file/Get the cil file representation. One of the initialization function of module File has to be called before using this function. raised exception: Bad_Initialization./
+Cil_types.stmtkind.Switch/ of Cil_types.exp * Cil_types.block * Cil_types.stmt list * Cil_types.location/A switch statement. exp is the index of the switch. block is  the body of the switch. stmt list contains the set of  statements whose labels are cases of the switch (i.e. for each  case, the corresponding statement is in stmt list, a statement  cannot appear more than once in the list, and statements in  stmt list can have several labels corresponding to several  cases./
+Locations.enumerate_valid_bits/Locations.access -> Locations.location -> Locations.Zone.t/Is there a possibly non-empty intersection between two given locations? If partial is true, returns true if the two locations may be overlapping without being equal. If partial is false, also returns true if the two locations may be equal. Returns false when the two locations cannot be overlapping./
+File.add_code_transformation_after_cleanup/?deps:(module Parameter_sig.S) list -> ?before:File.code_transformation_category list -> ?after:File.code_transformation_category list -> File.code_transformation_category -> (Cil_types.file -> unit) -> unit/Same as above, but the hook is applied after clean up. At this level, globals and ACSL annotations have been registered. If the hook adds some new globals or annotations, it must take care of adding them in the appropriate tables. Note that it is the responsibility of the hook to use Ast.mark_as_changed or Ast.mark_as_grown whenever it is the case./
+Cil_types.file//The top-level representation of a CIL source file (and the result of the parsing and elaboration). Its main contents is the list of global declarations and definitions. You can iterate over the globals in a Cil_types.file using the following iterators: Cil.mapGlobals, Cil.iterGlobals and Cil.foldGlobals. You can also use the Cil.dummyFile when you need a Cil_types.file as a placeholder. For each global item CIL stores the source location where it appears (using the type Cil_types.location)/
+Type.par/Type.precedence -> Type.precedence -> Stdlib.Format.formatter -> (Stdlib.Format.formatter -> unit) -> unit/par context myself fmt pp puts parenthesis around the verbatim prints by pp according to the precedence myself of the verbatim and to the precedence context of the caller of the pretty printer. fmt is the output formatter. The typical use is the following: let pretty_print p_caller fmt x = let pp fmt = Format.fprintf "..." ... x ... in let myself = Call in par p_caller myself fmt pp/
 Datatype.bool/bool Type.t//
-Datatype.pp_fail/Type.precedence -> Format.formatter -> 'a -> unit/Must be used for internal_pretty_code if this pretty-printer must fail only when called./
+Datatype.pp_fail/Type.precedence -> Stdlib.Format.formatter -> 'a -> unit/Must be used for internal_pretty_code if this pretty-printer must fail only when called./
 Visitor.visitFramacFileSameGlobals/Visitor.frama_c_visitor -> Cil_types.file -> unit/A visitor for the whole file that does not change the globals (but maybe changes things inside the globals). Use this function instead of Visitor.visitFramacFile whenever appropriate because it is more efficient for long files./
-Log.Messages.with_log/(Log.event -> 'b) -> ?kind:Log.kind -> ('a, 'b) Log.pretty_aborter//
-Cil.visitor_behavior//Visitor behaviorHow the visitor should behave in front of mutable fields: in  place modification or copy of the structure. This type is abstract.  Use one of the two values below in your classes./
+Structural_descr.t.Structure/ of Structural_descr.structure/Provide a description of the representation of data./
+Cil_types.relation.Rneq//Different/
+Cil_types.stmtkind.Return/ of Cil_types.exp option * Cil_types.location/The return statement. This is a leaf in the CFG./
 Cmdline.run_after_early_stage/(unit -> unit) -> unit/Register an action to be executed at the end of the early stage./
-Cil_types.logic_var/{mutable lv_name: string; mutable lv_id: int; mutable lv_type: Cil_types.logic_type; mutable lv_kind: Cil_types.logic_var_kind; mutable lv_origin: Cil_types.varinfo option; mutable lv_attr: Cil_types.attributes}/description of a logic variable/
-Dataflow/Cil_types.fundec -> Cil_types.stmt list * Cil_types.stmt listend /Deprecated: use Dataflows instead. A framework for implementing data flow analysis./
-Log.log_channel/Log.channel -> ?kind:Log.kind -> ?prefix:Log.prefix -> 'a Log.pretty_printer/logging function to user-created channel./
-Db.progress/(unit -> unit) Pervasives.ref/This function should be called from time to time by all analysers taking time. In GUI mode, this will make the interface reactive./
-Kernel_function.get_definition/t -> Cil_types.fundec/For functions with a declaration and a definition, returns the definition. raised exception: No_Definition./
+Cil.visitAction.ChangeToPost/ of 'a * ('a -> 'a)/applies the expression to the function and gives back the result.  Useful to insert some actions in an inheritance chain./
+Cil_types.logic_var//description of a logic variable/
+Cil_types.exp_node.BinOp/ of Cil_types.binop * Cil_types.exp * Cil_types.exp * Cil_types.typ/Binary operation. Includes the type of the result. The arithmetic  conversions are made explicit for the arguments./
+Log.log_channel/Log.channel -> ?kind:Log.kind -> 'a Log.pretty_printer/logging function to user-created channel./
+Cil_types.stmtkind.Loop/ of Cil_types.code_annotation list * Cil_types.block * Cil_types.location * Cil_types.stmt option * Cil_types.stmt option/A while(1) loop. The termination test is implemented in the body of a  loop using a Break statement. If Cfg.prepareCFG has been called, the  first stmt option will point to the stmt containing the continue label  for this loop and the second will point to the stmt containing the break  label for this loop./
+Db.progress/(unit -> unit) Stdlib.ref/This function should be called from time to time by all analysers taking time. In GUI mode, this will make the interface reactive./
+Kernel_function.get_definition/t -> Cil_types.fundec/Returns the list of static variables declared inside the function. raised exception: No_Definition./
 Datatype.char/char Type.t//
+Visitor_behavior.Get.stmt/Visitor_behavior.t -> Cil_types.stmt -> Cil_types.stmt/Fold operations on table of a given type of AST elements. Fold.ast_element vis f, folds f over each pair of ast_element registered in vis. The ast_element in the old AST is presented to f first (that is, f looks like: let f old_e new_e acc = .... For example for Cil_types.varinfo: Fold.varinfo vis (fun old_vi new_vi acc -> ... )./
 Cil.cilVisitor.vlogic_info_decl/Cil_types.logic_info -> Cil_types.logic_info Cil.visitAction/link to the current function being visited.  NB: for copy visitors, the fundec is the original one./
-Cil_types.acsl_extension//extension to standard ACSL clause. Each extension is associated to a keyword. An extension can be registered through the following functions:- Logic_typing.register_behavior_extension for parsing and type-checking- Cil_printer.register_behavior_extension for pretty-printing an  extended clause- Cil.register_behavior_extension for visiting an extended clause/
-Cil_types.offset/ | NoOffset | Field of Cil_types.fieldinfo * Cil_types.offset | Index of Cil_types.exp * Cil_types.offset/The offset part of an Cil_types.lval. Each offset can be applied to certain kinds of lvalues and its effect is that it advances the starting address of the lvalue and changes the denoted type, essentially focussing to some smaller lvalue that is contained in the original one./
+Cil_types.acsl_extension//Extension to standard ACSL clause with an unique identifier. The integer is a (unique) identifier. The boolean flag is true if the annotation can be assigned a property status. Use Logic_const.new_acsl_extension to create new acsl extension with a fresh id. Each extension is associated with a keyword, and can be either a global annotation, the clause of a function contract, a code annotation, or a loop annotation. An extension can be registered through the function Acsl_extension.register_xxx. It is _not_ possible to register the same keyword for annotations at two different levels (e.g. global and behavior), as this would make the grammar ambiguous./
+Cil_types.offset//The offset part of an Cil_types.lval. Each offset can be applied to certain kinds of lvalues and its effect is that it advances the starting address of the lvalue and changes the denoted type, essentially focussing to some smaller lvalue that is contained in the original one./
+Cil.visitAction.DoChildrenPost/ of ('a -> 'a)/visit the children, and apply the given function to the result./
 Datatype.Bool/Datatype.S_with_collections with type t = bool/Deep copy: no possible sharing between x and copy x./
 Cil.cilVisitor.vlogic_info_use/Cil_types.logic_info -> Cil_types.logic_info Cil.visitAction//
-File.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./
+File.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./
 Log.Messages.log/?kind:Log.kind -> ?verbose:int -> ?debug:int -> 'a Log.pretty_printer/Generic log routine. The default kind is Result. Use cases (with  n,m > 0):- log ~verbose:n: emit the message only when verbosity level is  at least n.- log ~debug:n: emit the message only when debugging level is  at least n.- log ~verbose:n ~debug:m: any debugging or verbosity level is  sufficient./
 Type/'b Type.Obj_tbl.t -> ('a Type.ty -> 'a -> 'b -> unit) -> unitend end /Type value. A type value is a value representing a static ML monomorphic type. This API is quite low level. Prefer to use module Datatype instead whenever possible./
+Cmdline.stage.Exiting//Run once when exiting Frama-C./
 Datatype.identity/'a -> 'a/Must be used if you want to implement a required function by fun x -> x. Only useful for implementing rehash and copy./
-State_selection/end /A state selection is a set of states with operations for easy handling of state dependencies./
-Project.set_current/?on:bool -> ?selection:State_selection.t -> t -> unit/Set the current project with the given one.  The flag on is not for casual users. raised exception: Invalid_argument./
+State_selection/(State.t -> 'a -> 'a) -> State_selection.t -> 'a -> 'aend /A state selection is a set of states with operations for easy handling of state dependencies./
+Project.set_current/?on:bool -> ?selection:State_selection.t -> t -> unit/Set the current project with the given one. The flag on is not for casual users. raised exception: Invalid_argument./
 Logic_const/Cil_types.term_offset -> Cil_types.term_lval -> Cil_types.term_lvalend /Smart constructors for logic annotations./
 Cil.cilVisitor.vlogic_type_info_use/Cil_types.logic_type_info -> Cil_types.logic_type_info Cil.visitAction//
+Project.IOError/string/register_before_remove_hook f adds a hook called just before removing a project./
 Kernel_function.Make_Table/functor (Data : Datatype.S ) -> functor (Info : State_builder.Info_with_size ) -> State_builder.Hashtbl with type key = t and type data = Data.t/Hashtable indexed by kernel functions and dealing with project./
-State_builder.Ref/unit -> Data.t end ) -> State_builder.Ref with type data = Data.t/Deep copy: no possible sharing between x and copy x./
-File.add_code_transformation_before_cleanup/?deps:(module Parameter_sig.S) list -> ?before:File.code_transformation_category list -> ?after:File.code_transformation_category list -> File.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./
+State_builder.Ref/unit -> Data.t end ) -> State_builder.Ref with type data = Data.t and type Datatype.t = Data.t ref/Deep copy: no possible sharing between x and copy x./
+Visitor_behavior.Get.kernel_function/Visitor_behavior.t -> Cil_types.kernel_function -> Cil_types.kernel_function//
+Cmdline.stage.Configuring//The stage where all the parameters which were not already     set may be modified to take into account cmdline options.     Just after this stage, Frama-C will run the plug-in mains./
+Acsl_extension.register_global/string -> ?preprocessor:Acsl_extension.extension_preprocessor -> Acsl_extension.extension_typer -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/Registers extension for global annotation. See register_behavior./
+File.add_code_transformation_before_cleanup/?deps:(module Parameter_sig.S) list -> ?before:File.code_transformation_category list -> ?after:File.code_transformation_category list -> File.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./
 Db/end /Database in which static plugins are registered./
+Cmdline.stage.Extending//Before loading plug-ins. Run only once./
+Analysis.compute/unit -> unit/Computes the Eva analysis, if not already computed, using the entry point of the current project. You may set it with Globals.set_entry_point. raised exceptions: , if the entry point is incorrect, if some arguments are specified for the entry point using Db.Value.fun_set_args, and an incorrect number of them is given./
+Type.precedence.Basic//Normal precedence/
+FCHashtbl/int -> int -> 'a -> intend /Extension of OCaml's Hashtbl module./
+Cil_datatype.Fundec/Cil_datatype.S_with_collections_pretty with type t = fundec//
+Acsl_extension.register_code_annot_next_both/string -> ?preprocessor:Acsl_extension.extension_preprocessor -> Acsl_extension.extension_typer -> ?visitor:Acsl_extension.extension_visitor -> ?printer:Acsl_extension.extension_printer -> ?short_printer:Acsl_extension.extension_printer -> bool -> unit/Registers extension both for code and loop annotations. See register_behavior./
+From_parameters.ForceCallDeps/Parameter_sig.With_output/Option -calldeps./
 Type.Abstract/Type.Abstract.t Type.tyend /Apply this functor to access to the abstract type of the given name. raised exception: No_abstract_type./
+Cil_types.behavior//Behavior of a function or statement. This type shares the name of its constructors with Logic_ptree.behavior./
 Logic_utils/unit -> boolend /Utilities for ACSL constructs./
+Cil_types.stmtkind.Continue/ of Cil_types.location/A continue to the start of the nearest enclosing Loop./
 Cil.cilVisitor.voffs/Cil_types.offset -> Cil_types.offset Cil.visitAction/Invoked on each offset occurrence that is *not* as part of an  initializer list specification, i.e. in an lval or recursively inside an  offset./
 Cil.cilVisitor.vlogic_ctor_info_use/Cil_types.logic_ctor_info -> Cil_types.logic_ctor_info Cil.visitAction//
-Log.print_on_output/(Format.formatter -> unit) -> unit/Direct printing on output.  Message echo is delayed until the output is finished.  Then, the output is flushed and all pending message are echoed.  Notification of listeners is not delayed, however.  Can not be recursively invoked./
+Log.print_on_output/(Stdlib.Format.formatter -> unit) -> unit/Direct printing on output. Message echo is delayed until the output is finished. Then, the output is flushed and all pending message are echoed. Notification of listeners is not delayed, however. Can not be recursively invoked./
 Visitor.frama_c_visitor.vglob_aux/Cil_types.global -> Cil_types.global list Cil.visitAction/Replacement of vglob./
+Visitor_behavior.t//How the visitor should behave in front of mutable fields: in place modification or copy of the structure. This type is abstract. Use one of the two values below in your classes./
 Cmdline.run_after_configuring_stage/(unit -> unit) -> unit/Register an action to be executed at the end of the configuring stage./
 Project.current/unit -> t/The current project. raised exception: NoProject./
 State.dummy/t/A dummy state./
-Project_skeleton.t/{pid: int; mutable name: string; mutable unique_name: string}/No function is exported.  Extension of the GUI in order to support project switching./
-Cil.get_kernel_function/Cil.visitor_behavior -> Cil_types.kernel_function -> Cil_types.kernel_function//
+Project_skeleton.t//This module should not be used outside of the Project library./
 File.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) raised exception: Invalid_argument./
 State_builder/?prj:Project.t -> string -> 'a Type.t -> 'a * boolend end /State builders. Provide ways to implement signature State_builder.S. Depending on the builder, also provide some additional useful information./
+Datatype.S_no_copy.equal/Datatype.t -> Datatype.t -> bool/Equality: same spec than Stdlib.(=)./
 Cil.cilVisitor.current_kinstr/Cil_types.kinstr/Kstmt stmt when visiting statement stmt, Kglobal when called outside  of a statement./
-Parameter_sig.Int/Parameter_sig.Int/Signature for an integer parameter./
\ No newline at end of file
+Parameter_sig.Int/Parameter_sig.Int/Signature for an integer parameter./
+Visitor_behavior.Memo/Visitor_behavior.Get/Memo operations on behaviors, allows to get a binding in the new project for the given AST element, creating one if it does not already exists. Memo.ast_element vis e with e of type ast_element tries to find a binding to a e in the new project created using vis in the current state, if it does not exist this binding is created. For example for Cil_types.varinfo: Memo.varinfo vis vi./
\ No newline at end of file
-- 
GitLab