From a72af8d92cb7a8df6eec553b2b573c9b6ea0cf3d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 25 Jun 2024 18:56:38 +0200
Subject: [PATCH] Removes references to removed pragma in some comments.
---
src/kernel_services/ast_data/property.mli | 4 ++--
src/kernel_services/ast_queries/cil.mli | 10 +++++-----
src/plugins/sparecode/Sparecode.mli | 2 +-
src/plugins/sparecode/register.mli | 2 +-
4 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 2b86486b245..f957ff21d99 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -479,7 +479,7 @@ val ip_of_code_annot:
(** Builds the IP related to the code annotation.
should be used only on code annotations returning a single ip, i.e.
- assert, invariant, variant, pragma.
+ assert, invariant, variant.
@raise Invalid_argument if the resulting code annotation has an empty set
of identified property
@since Carbon-20110201 *)
@@ -499,7 +499,7 @@ val ip_of_global_annotation_single:
val has_status: identified_property -> bool
(** Does the property has a logical status (which may be Never_tried)?
- False for pragma, assumes clauses and some ACSL extensions.
+ False for assumes clauses and some ACSL extensions.
@since 19.0-Potassium *)
val get_kinstr: identified_property -> kinstr
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index e54b77b2f41..11091f7b462 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2040,11 +2040,11 @@ val visitCilBlock: cilVisitor -> block -> block
(** Mark the given block as candidate to be flattened into its parent block,
after returning from its visit. This is not systematic, as the environment
might prevent it (e.g. if the preceding statement is a statement contract
- or a slicing/pragma annotation, or if there are labels involved). Use
- that whenever you're creating a block in order to hold multiple statements
- as a result of visiting a single statement. If the block contains local
- variables, it will not be marked as transient, since removing it will
- change the scope of those variables.
+ or if there are labels involved).
+ Use that whenever you're creating a block in order to hold multiple
+ statements as a result of visiting a single statement. If the block
+ contains local variables, it will not be marked as transient, since
+ removing it will change the scope of those variables.
@raise Fatal error if the given block attempts to declare local variables
and contain definitions of local variables that are not part of the block.
diff --git a/src/plugins/sparecode/Sparecode.mli b/src/plugins/sparecode/Sparecode.mli
index 2487a7f1405..e98a84689e1 100644
--- a/src/plugins/sparecode/Sparecode.mli
+++ b/src/plugins/sparecode/Sparecode.mli
@@ -27,7 +27,7 @@ module Register: sig
val get: select_annot:bool -> select_slice_annot:bool -> Project.t
(** Remove in each function what isn't used to compute its outputs,
or its annotations when [select_annot] is true,
- or its slicing pragmas when [select_slice_annot] is true.
+ or its slicing annotations when [select_slice_annot] is true.
@return a new project where the sparecode has been removed.
*)
diff --git a/src/plugins/sparecode/register.mli b/src/plugins/sparecode/register.mli
index f912136d53e..df9ac76e7f5 100644
--- a/src/plugins/sparecode/register.mli
+++ b/src/plugins/sparecode/register.mli
@@ -23,7 +23,7 @@
val get: select_annot:bool -> select_slice_annot:bool -> Project.t
(** Remove in each function what isn't used to compute its outputs,
or its annotations when [select_annot] is true,
- or its slicing pragmas when [select_slice_annot] is true.
+ or its slicing annotations when [select_slice_annot] is true.
@return a new project where the sparecode has been removed. *)
val rm_unused_globals : ?new_proj_name:string -> ?project:Project.t -> unit -> Project.t
--
GitLab