From e40cbf496b6f5b3c09f3064aa27f1427b7b62ca6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 17 Jan 2025 17:32:27 +0100
Subject: [PATCH] [Eva] Updates headers and fixes documentation of Export.
---
src/plugins/eva/Eva.mli | 7 +++----
src/plugins/eva/utils/export.ml | 2 +-
src/plugins/eva/utils/export.mli | 9 ++++-----
3 files changed, 8 insertions(+), 10 deletions(-)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 25d2834bf98..ae2a20ae829 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -977,7 +977,7 @@ module Export: sig
instruction or the branching condition of the statement. Other kinds of
statements, like loops, blocks and exceptions are not visited.
- More precisely, for set and call instructions: the writen l-values from
+ More precisely, for set and call instructions: the written l-values from
left-hand-side are not visited, but their inner l-values are visited; any
l-value from the right-hand-side of the instruction is also visited.
*)
@@ -990,14 +990,13 @@ module Export: sig
(**
Creates a visitor that can be used to generate new annotations for all
visited instructions. The generated assertions are associated with the local
- {!generated} emitter. They are all assigned a valid status by
- {!Analysis.emitter}.
+ {!emitter}. They are all assigned a valid status by {!Analysis.emitter}.
*)
val generator : unit -> Visitor.frama_c_inplace
(**
Creates a visitor that can be used to remove all generated annotations from
- {!generated} emitter. This will also remove their associated status.
+ {!emitter}. This will also remove their associated status.
*)
val cleaner : unit -> Visitor.frama_c_inplace
end
diff --git a/src/plugins/eva/utils/export.ml b/src/plugins/eva/utils/export.ml
index 3f84f2a1f85..4a99475717b 100644
--- a/src/plugins/eva/utils/export.ml
+++ b/src/plugins/eva/utils/export.ml
@@ -2,7 +2,7 @@
(* *)
(* This file is part of Frama-C. *)
(* *)
-(* Copyright (C) 2007-2024 *)
+(* Copyright (C) 2007-2025 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src/plugins/eva/utils/export.mli b/src/plugins/eva/utils/export.mli
index 574bf6e4329..a4a148071e1 100644
--- a/src/plugins/eva/utils/export.mli
+++ b/src/plugins/eva/utils/export.mli
@@ -2,7 +2,7 @@
(* *)
(* This file is part of Frama-C. *)
(* *)
-(* Copyright (C) 2007-2024 *)
+(* Copyright (C) 2007-2025 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
@@ -37,7 +37,7 @@ val export_value :
instruction or the branching condition of the statement. Other kinds of
statements, like loops, blocks and exceptions are not visited.
- More precisely, for set and call instructions: the writen l-values from
+ More precisely, for set and call instructions: the written l-values from
left-hand-side are not visited, but their inner l-values are visited; any
l-value from the right-hand-side of the instruction is also visited.
*)
@@ -50,14 +50,13 @@ val emitter : Emitter.t
(**
Creates a visitor that can be used to generate new annotations for all
visited instructions. The generated assertions are associated with the local
- {!generated} emitter. They are all assigned a valid status by
- {!Analysis.emitter}.
+ {!emitter}. They are all assigned a valid status by {!Analysis.emitter}.
*)
val generator : unit -> Visitor.frama_c_inplace
(**
Creates a visitor that can be used to remove all generated annotations from
- {!generated} emitter. This will also remove their associated status.
+ {!emitter}. This will also remove their associated status.
*)
val cleaner : unit -> Visitor.frama_c_inplace
--
GitLab