From a52e5e6111301430ded01f94fc1f85b655045598 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 20 Feb 2024 17:08:35 +0000
Subject: [PATCH] [doc] Minor corrections in user manual and fix typos
---
doc/userman/user-acsl.tex | 9 +++++----
tests/libc/stdlib_c.c | 2 +-
tests/libc/string_c.c | 2 +-
3 files changed, 7 insertions(+), 6 deletions(-)
diff --git a/doc/userman/user-acsl.tex b/doc/userman/user-acsl.tex
index 53e00589c68..9da27d2c8d4 100644
--- a/doc/userman/user-acsl.tex
+++ b/doc/userman/user-acsl.tex
@@ -6,14 +6,15 @@
When a plug-in registers an extension, it can be used in \acsl annotations
with 2 different syntaxes. As an example, with an extension \lstinline|bar|
registered by the plug-in \lstinline|foo|, we can use the short syntax
-\lstinline|bar _| and the complete syntax \lstinline|\foo::bar _|.
+\lstinline|bar _| or the complete syntax \lstinline|\foo::bar _|.
-The complete syntax is usefull to print better warning/error messages, and to
+The complete syntax is useful to print better warning/error messages, and to
better understand which plug-in introduced the extension. Additionnaly, all
extensions coming from an unloaded plug-in can be ignored this way. For
example, if \Eva is not loaded, \lstinline|\eva::unroll _| annotations will be
-ignored with a warning, unlike \lstinline|unroll _| which by default will be
-treated as a user error.
+ignored with a warning, whereas \lstinline|unroll _| cannot be identified as
+being supported by Eva, which means that it can only be treated as a user
+error.
\section{Handling indirect calls with \texttt{calls}}
\label{acsl:calls}
diff --git a/tests/libc/stdlib_c.c b/tests/libc/stdlib_c.c
index 748849d1d76..16d93d84415 100644
--- a/tests/libc/stdlib_c.c
+++ b/tests/libc/stdlib_c.c
@@ -2,7 +2,7 @@
STDOPT: #"-eva-no-builtins-auto -eva-slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-msg-key malloc"
STDOPT: #"-eva-no-builtins-auto -eva-slevel 10 -eva-builtin calloc:Frama_C_calloc -eva-alloc-builtin by_stack -eva-no-alloc-returns-null -eva-msg-key malloc"
STDOPT: #"-eva-no-builtins-auto"
-*/ // \eva::slevel is used to \eva::unroll loops
+*/ // \eva::slevel is used to unroll loops
#define malloc(n) Frama_C_malloc(n)
#include "stdlib.c"
diff --git a/tests/libc/string_c.c b/tests/libc/string_c.c
index eeb65f0a999..3fb1d5a8056 100644
--- a/tests/libc/string_c.c
+++ b/tests/libc/string_c.c
@@ -1,6 +1,6 @@
/* run.config
STDOPT: #"-eva-no-builtins-auto -eva-slevel 1000 -eva-no-skip-stdlib-specs"
-*/ // \eva::slevel is used to \eva::unroll loops
+*/ // \eva::slevel is used to unroll loops
#include "string.c"
volatile int v;
--
GitLab