Commit e540cdd7 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Update API doc for 22.0-Titanium

parent 218bcaf2
......@@ -74,7 +74,7 @@ val pp_context_from_file:
?ctx:int -> ?start_line:int -> Format.formatter -> Filepath.position -> unit
(** prints a readable description of a location
@since Frama-C+dev *)
@since 22.0-Titanium *)
val pp_location: Format.formatter -> Cil_types.location -> unit
(** Parse errors are usually fatal, but their reporting is sometimes
......
......@@ -69,7 +69,7 @@ val funspec:
val has_funspec: kernel_function -> bool
(** @return [true] iff the function has a non-empty specification.
@since Frama-C+dev *)
@since 22.0-Titanium *)
val behaviors:
?emitter:Emitter.t -> ?populate:bool -> kernel_function -> funbehavior list
......@@ -284,7 +284,7 @@ val add_code_annot:
There can be at most one loop variant registered per statement.
Attempting to register a second one will result in a fatal error.
@modify Frama-C+dev: add keep_empty argument
@modify 22.0-Titanium: add keep_empty argument
*)
val add_assert:
......@@ -411,7 +411,7 @@ val add_allocates:
keep_empty:bool -> allocation behavior_component_addition
(** Add new allocates into the given behavior.
See {!Annotations.add_assigns} for the signification of [keep_empty]
@modify Frama-C+dev add keep_empty argument
@modify 22.0-Titanium add keep_empty argument
*)
val add_extended: acsl_extension behavior_component_addition
......
......@@ -107,15 +107,15 @@ module Functions: sig
val mem_name: string -> bool
(** @return [true] iff there is a function with such a name
@since Frama-C+dev *)
@since 22.0-Titanium *)
val mem_def_name: string -> bool
(** @return [true] iff there is a function definition with such a name
@since Frama-C+dev *)
@since 22.0-Titanium *)
val mem_decl_name: string -> bool
(** @return [true] iff there is a function declaration with such a name
@since Frama-C+dev *)
@since 22.0-Titanium *)
(** {2 Searching} *)
......@@ -236,7 +236,7 @@ module Types : sig
val mem_enum_tag: string -> bool
(** @return [true] iff there is an enum constant with the given name in the
AST.
@since Frama-C+dev *)
@since 22.0-Titanium *)
val find_enum_tag: string -> exp * typ
(** Find an enum constant from its name in the AST.
......@@ -245,7 +245,7 @@ module Types : sig
val mem_type: Logic_typing.type_namespace -> string -> bool
(** @return [true] iff there is a type with the given name in the given
namespace in the AST.
@since Frama-C+dev *)
@since 22.0-Titanium *)
val find_type: Logic_typing.type_namespace -> string -> typ
(** Find a type from its name in the AST.
......
......@@ -453,7 +453,7 @@ module type S_pp = sig
val pp_predicate_node: Format.formatter -> predicate_node -> unit
val pp_predicate: Format.formatter -> predicate -> unit
val pp_toplevel_predicate: Format.formatter -> toplevel_predicate -> unit
(** @since Frama-C+dev *)
(** @since 22.0-Titanium *)
val pp_identified_predicate: Format.formatter -> identified_predicate -> unit
val pp_code_annotation: Format.formatter -> code_annotation -> unit
val pp_funspec: Format.formatter -> funspec -> unit
......
......@@ -548,12 +548,12 @@ val isArithmeticType: typ -> bool
(** True if the argument is a scalar type (i.e. integral, enum,
floating point or pointer
@since Frama-C+dev
@since 22.0-Titanium
*)
val isScalarType: typ -> bool
(** alias of isScalarType.
@deprecated Frama-C+dev use isScalarType instead
@deprecated 22.0-Titanium use isScalarType instead
*)
val isArithmeticOrPointerType: typ -> bool
......
......@@ -73,7 +73,7 @@ module Location: sig
(** Pretty-print both location start and end, including file, line and
character offset.
@since Frama-C+dev
@since 22.0-Titanium
*)
val pretty_debug: t Pretty_utils.formatter
......@@ -85,7 +85,7 @@ module Location: sig
starting position. Compares normalized filenames, lines and columns,
but no absolute character offsets.
@since Frama-C+dev
@since 22.0-Titanium
*)
val equal_start_semantic : location -> location -> bool
......
......@@ -73,7 +73,7 @@ val list_available_machdeps: unit -> string list
(** [list_available_machdeps ()] gives the list of the names of available
machdeps, starting with the ones added with new_machdep and ending with
the list of default machdeps.
@since Frama-C+dev *)
@since 22.0-Titanium *)
type code_transformation_category
(** type of registered code transformations
......
......@@ -27,6 +27,6 @@ val get_flags : Datatype.Filepath.t -> string list
(** [has_entry f] returns true iff [f] has an entry in the JSON compilation
database. Must only be called if a JCDB file has been specified.
@since Frama-C+dev
@since 22.0-Titanium
*)
val has_entry : Datatype.Filepath.t -> bool
......@@ -51,12 +51,12 @@ val refresh_spec: funspec -> funspec
to check a property, without adding it as hypothesis for the rest of the
verification. See {!Cil_types.toplevel_predicate} for more information.
Default is [false], i.e. use standard ACSL semantics.
@since Frama-C+dev
@since 22.0-Titanium
*)
val toplevel_predicate: ?only_check:bool -> predicate -> toplevel_predicate
(** creates a new identified predicate with a fresh id.
@modify Frama-C+dev add [only_check] optional parameter
@modify 22.0-Titanium add [only_check] optional parameter
*)
val new_predicate: ?only_check:bool -> predicate -> identified_predicate
......
......@@ -315,12 +315,12 @@ val add_attribute_glob_annot:
(** {2 Contracts } *)
(** [true] if the behavior has only an assigns clause.
@since Frama-C+dev
@since 22.0-Titanium
*)
val behavior_has_only_assigns: behavior -> bool
(** [true] if the only non-empty fields of the contract are assigns clauses
@since Frama-C+dev
@since 22.0-Titanium
*)
val funspec_has_only_assigns: funspec -> bool
......
......@@ -319,7 +319,7 @@ val add_aliases:
If [deprecated] is set to true, the use of the aliases emits a warning.
@Invalid_argument if an alias name is the empty string
@since Carbon-20110201
@modify Frama-c+dev add [visible] and [deprecated] arguments. *)
@modify 22.0-Titanium add [visible] and [deprecated] arguments. *)
val replace_option_setting:
string -> plugin:string -> group:Group.t -> option_setting -> unit
......@@ -396,7 +396,7 @@ val permissive: bool
unknown option names and invalid values for some options
(e.g. non-existent function names).
@since Frama-C+dev *)
@since 22.0-Titanium *)
val last_project_created_by_copy: (unit -> string option) ref
......
......@@ -129,7 +129,7 @@ val is_reconfigurable: unit -> unit
only parameters corresponding to options registered at the
{!Cmdline.Configuring} stage are reconfigurable.
@since Nitrogen-20111001
@modify Frama-C+dev [do_iterate] renamed to [is_reconfigurable]
@modify 22.0-Titanium [do_iterate] renamed to [is_reconfigurable]
*)
val is_not_reconfigurable: unit -> unit
......@@ -137,7 +137,7 @@ val is_not_reconfigurable: unit -> unit
parameters corresponding to options registered at the
{!Cmdline.Configuring} stage are reconfigurable.
@since Nitrogen-20111001
@modify Frama-C+dev [do_iterate] renamed to [is_reconfigurable]
@modify 22.0-Titanium [do_iterate] renamed to [is_reconfigurable]
*)
val no_category: unit -> unit
......
......@@ -185,7 +185,7 @@ module type S_no_parameter = sig
If [visible] is set to false, the aliases do not appear in help messages.
If [deprecated] is set to true, the use of the aliases emits a warning.
@raise Invalid_argument if one of the strings is empty
@modify Frama-c+dev add [visible] and [deprecated] arguments. *)
@modify 22.0-Titanium add [visible] and [deprecated] arguments. *)
(**/**)
val is_set: unit -> bool
......
......@@ -71,7 +71,7 @@ val orphan: t
emitter that is no longer available (in particular, annotations loaded
from a state that was generated from a different set of plug-ins than
in current session). Should not be used outside of the kernel.
@since Frama-C+dev
@since 22.0-Titanium
*)
(** Usable emitters are the ones which can really emit something. *)
......
......@@ -240,7 +240,7 @@ module AutocompleteHelp: Parameter_sig.String_set
module PrintConfigJson: Parameter_sig.Bool
(** Behavior of option "-print-config-json"
@since Frama-C+dev *)
@since 22.0-Titanium *)
(* ************************************************************************* *)
(** {2 Output Messages} *)
......
......@@ -71,7 +71,7 @@ module type S_no_log = sig
[add_plugin_output_aliases [alias]] adds the aliases -alias-help,
-alias-verbose, etc.
@since 18.0-Argon
@modify Frama-c+dev add [visible] and [deprecated] arguments. *)
@modify 22.0-Titanium add [visible] and [deprecated] arguments. *)
end
(** Provided plug-general services for plug-ins.
......@@ -90,7 +90,7 @@ type plugin = private
p_help: string;
p_parameters: (string, Typed_parameter.t list) Hashtbl.t }
(** @since Beryllium-20090901
@modify Frama-C+dev previously only "iterable" parameters were included,
@modify 22.0-Titanium previously only "iterable" parameters were included,
now all parameters are.
*)
......@@ -175,7 +175,7 @@ val iter_on_plugins: (plugin -> unit) -> unit
val fold_on_plugins: (plugin -> 'a -> 'a) -> 'a -> 'a
(** Fold [f] on each registered plug-in.
@since Frama-C+dev *)
@since 22.0-Titanium *)
(**/**)
(* ************************************************************************* *)
......
......@@ -323,7 +323,7 @@ val html_escape: string -> string
(** [format_string_of_stag stag] returns the string corresponding to [stag],
or raises an exception if the tag extension is unsupported.
@since Frama-C+dev
@since 22.0-Titanium
*)
val format_string_of_stag: Format.stag -> string
......
......@@ -92,7 +92,7 @@ val add_symbolic_dir: string -> string -> unit
(** Returns the list of symbolic dirs added via [add_symbolic_dir], plus
preexisting ones (e.g. FRAMAC_SHARE), as pairs (name, dir).
@since Frama-C+dev
@since 22.0-Titanium
*)
val all_symbolic_dirs: unit -> (string * string) list
......@@ -114,7 +114,7 @@ module Normalized: sig
resulting from the concatenation of [dir] ^ "/" ^ [file].
The resulting path must respect [existence].
@since Frama-C+dev
@since 22.0-Titanium
*)
val concat: ?existence:existence -> t -> string -> t
......@@ -159,7 +159,7 @@ module Normalized: sig
(** [is_file f] returns [true] iff [f] points to a regular file
(or a symbolic link pointing to a file).
Returns [false] if any errors happen when [stat]'ing the file.
@since Frama-C+dev *)
@since 22.0-Titanium *)
val is_file: t -> bool
(** [to_base_uri path] returns a pair [prefix, rest], according to the
......@@ -171,7 +171,7 @@ module Normalized: sig
E.g. for the path "FRAMAC_SHARE/libc/string.h", returns
("FRAMAC_SHARE", "libc/string.h").
@since Frama-C+dev
@since 22.0-Titanium
*)
val to_base_uri: t -> string option * string
end
......
......@@ -432,7 +432,7 @@ sig
The [force] parameters defaults to [false], when it is [true], if there
exist another builtin, it is replaced with the new one. Use with care.
@modify Frama-C+dev add optional [force] parameter
@modify 22.0-Titanium add optional [force] parameter
*)
val set_builtin' :
......@@ -448,7 +448,7 @@ sig
The [force] parameters defaults to [false], when it is [true], if there
exist another builtin, it is replaced with the new one. Use with care.
@modify Frama-C+dev add optional [force] parameter
@modify 22.0-Titanium add optional [force] parameter
*)
val set_builtin_get :
......@@ -460,7 +460,7 @@ sig
The [force] parameters defaults to [false], when it is [true], if there
exist another builtin, it is replaced with the new one. Use with care.
@modify Frama-C+dev add optional [force] parameter
@modify 22.0-Titanium add optional [force] parameter
*)
val set_builtin_eq :
......@@ -475,7 +475,7 @@ sig
The [force] parameters defaults to [false], when it is [true], if there
exist another builtin, it is replaced with the new one. Use with care.
@modify Frama-C+dev add optional [force] parameter
@modify 22.0-Titanium add optional [force] parameter
*)
val set_builtin_leq :
......@@ -491,7 +491,7 @@ sig
The [force] parameters defaults to [false], when it is [true], if there
exist another builtin, it is replaced with the new one. Use with care.
@modify Frama-C+dev add optional [force] parameter
@modify 22.0-Titanium add optional [force] parameter
*)
(** {3 Specific Patterns} *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment