run.oracle 47.62 KiB
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./
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./
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./
Datatype.Ref/functor (T : Datatype.S ) -> Datatype.S with type t = T.t ref/Deep copy: no possible sharing between x and copy x./
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.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./
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./
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./
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./
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//
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./
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./
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./
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./
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//
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./
Datatype.func/?label:string * (unit -> 'a) option -> 'a Type.t -> 'b Type.t -> ('a -> 'b) Type.t//
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"./
Datatype.int/int Type.t//
Log.Messages.fatal/('a, 'b) Log.pretty_aborter/internal error of the plug-in. raised exception: AbortFatal./
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./
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./
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./
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./
Cmdline/Cmdline.Group.t -> stringend end /Command line parsing./
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./
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./
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_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./
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./
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./
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.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/
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./
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./
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./
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./
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.)/
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./
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./
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./
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./
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./
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./
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./
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./
Plugin.Register/string end ) -> Plugin.General_services/Functors for registering a new plug-in. It provides access to several services./
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./
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/
Locations.Location_Bits/ module type of Location_Bytes/Association between bases and offsets in bits./
Annotations.add_assert/Emitter.t -> ?kf:Cil_types.kernel_function -> Cil_types.stmt -> Cil_types.predicate -> unit/Add an assertion attached to the given statement. If kf is provided, the function runs faster./
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./
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./
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 ()./
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./
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.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/
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.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./
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./
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/
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./
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./
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./
Datatype.char/char Type.t//
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./
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./
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./
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./
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//
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./
Db/end /Database in which static plugins are registered./
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./
Logic_utils/unit -> boolend /Utilities for ACSL constructs./
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./
Visitor.frama_c_visitor.vglob_aux/Cil_types.global -> Cil_types.global list Cil.visitAction/Replacement of vglob./
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//
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./
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./