Skip to content
Snippets Groups Projects
Commit 8f72e6cc authored by Loïc Correnson's avatar Loïc Correnson Committed by Virgile Prevosto
Browse files

[kernel] fix internal documentation

parent e6ac75ee
No related branches found
No related tags found
No related merge requests found
...@@ -100,7 +100,7 @@ type extension_module_importer = ...@@ -100,7 +100,7 @@ type extension_module_importer =
status or not. status or not.
Here is a basic example: Here is a basic example:
[ {[
let count = ref 0 let count = ref 0
let foo_typer typing_context loc = function let foo_typer typing_context loc = function
| p :: [] -> | p :: [] ->
...@@ -113,7 +113,7 @@ type extension_module_importer = ...@@ -113,7 +113,7 @@ type extension_module_importer =
| _ -> typing_context.error loc "expecting a predicate after keyword FOO" | _ -> typing_context.error loc "expecting a predicate after keyword FOO"
let () = let () =
Acsl_extension.register_behavior ~plugin:"myplugin" "FOO" foo_typer false Acsl_extension.register_behavior ~plugin:"myplugin" "FOO" foo_typer false
] ]}
@before 29.0-Copper parameters [plugin] and [is_same_ext] were not present @before 29.0-Copper parameters [plugin] and [is_same_ext] were not present
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
*) *)
...@@ -160,16 +160,16 @@ val register_code_annot_next_both: register_extension ...@@ -160,16 +160,16 @@ val register_code_annot_next_both: register_extension
(** (**
Module importer extensions allow to extends the import clause with external Module importer extensions allow to extends the import clause with external
loaders. For instance, consider the following declaration: loaders. For instance, consider the following declaration:
[ {[
//@ import A: foo::bar; //@ import A: foo::bar;
] ]}
This import clause will invoke an external module importer named ["A"] This import clause will invoke an external module importer named ["A"]
provided it has been properly registered. provided it has been properly registered.
A module importer extension is a function that receives a [module_builder] A module importer extension is a function that receives a [module_builder]
parameter to be populated with contents of the module. The module name is parameter to be populated with contents of the module. The module name is
provided as list (See {Logic_utils.longident} for details). provided as list (See {!Logic_utils.longident} for details).
New type and function symbols shall be created with `Cil.make_xxx` functions. New type and function symbols shall be created with `Cil.make_xxx` functions.
The registered symbols {i will} be automatically prefixed with the name of The registered symbols {i will} be automatically prefixed with the name of
......
...@@ -141,7 +141,7 @@ type typing_context = { ...@@ -141,7 +141,7 @@ type typing_context = {
} }
(** Functions that can be called when importing external modules into ACSL. (** Functions that can be called when importing external modules into ACSL.
See {Acsl_extension.register_module_importer} for details. See {!Acsl_extension.register_module_importer} for details.
@since Frama-C+dev @since Frama-C+dev
*) *)
type module_builder = { type module_builder = {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment