diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli index fcee9704a38fabe6317d8b77311421a9d4e4bb36..ebc5c3c6a928a43a1e14f1d8f0758762c134c95b 100644 --- a/src/kernel_services/ast_queries/acsl_extension.mli +++ b/src/kernel_services/ast_queries/acsl_extension.mli @@ -100,7 +100,7 @@ type extension_module_importer = status or not. Here is a basic example: - [ + {[ let count = ref 0 let foo_typer typing_context loc = function | p :: [] -> @@ -113,7 +113,7 @@ type extension_module_importer = | _ -> typing_context.error loc "expecting a predicate after keyword FOO" let () = Acsl_extension.register_behavior ~plugin:"myplugin" "FOO" foo_typer false - ] + ]} @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> *) @@ -160,16 +160,16 @@ val register_code_annot_next_both: register_extension (** Module importer extensions allow to extends the import clause with external loaders. For instance, consider the following declaration: - [ + {[ //@ import A: foo::bar; - ] + ]} This import clause will invoke an external module importer named ["A"] provided it has been properly registered. 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 - 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. The registered symbols {i will} be automatically prefixed with the name of diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli index 7726e105af6a5baaf224efd2bcee25eaa698a932..9af8714ecb2ca12f85a57bb16a813ff12c4c252b 100644 --- a/src/kernel_services/ast_queries/logic_typing.mli +++ b/src/kernel_services/ast_queries/logic_typing.mli @@ -141,7 +141,7 @@ type typing_context = { } (** 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 *) type module_builder = {