From 44ca18f9fc47af81b4320ef9371e2d1b3da1fea2 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 12 May 2020 08:33:35 +0200
Subject: [PATCH] Typos in ACSL + Kernel
---
html/acsl.html | 8 ++++----
html/kernel.html | 14 +++++++-------
2 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/html/acsl.html b/html/acsl.html
index 4cccb832..a8b5ad80 100755
--- a/html/acsl.html
+++ b/html/acsl.html
@@ -33,7 +33,7 @@ ACSL is a <em>formal</em> language.</p>
assigns a[0..n-1];
- ensures<sidenote>As a formal language, ACSL enables a precise specification of function contracts. That makes the specification not only understandable by a human, but also manipulable by an analyzer. Furthermore, as a complete specification is not always useful, the contract can be partial, it depends on one wants to verify.</sidenote><point></point>
+ ensures<sidenote>As a formal language, ACSL enables a precise specification of function contracts. That makes the specification not only understandable by a human, but also manipulable by an analyzer. Furthermore, as a complete specification is not always useful, the contract can be partial, it depends on what one wants to verify.</sidenote><point></point>
\forall integer i;
0 <= i < n ==> a[i] == 0;
*/
@@ -58,13 +58,13 @@ void set_to_0(int* a, int n){
<a href="../fc-plugins/jessie.html">Jessie</a>
plug-ins use Hoare-style weakest precondition computations to
formally prove ACSL properties. The process can be quite automatic,
-thanks to external theorem provers such as Alt-Ergo, Z3 or CVC4
+thanks to external theorem provers such as Alt-Ergo, Z3 or CVC4,
or more interactive, with WP's built-in interactive prover
-or the use of the Coq proof-assistant. Other
+or the use of the Coq proof assistant. Other
plug-ins, such as the <a href="../fc-plugins/eva.html">Eva</a>
plug-in, may
also contribute to the verification of ACSL properties. They may
-also report static analysis results in terms of asserted new ACSL
+also report static analysis results in terms of new asserted ACSL
properties inside the source code.</p>
<h2>More information</h2>
diff --git a/html/kernel.html b/html/kernel.html
index ecb256a9..757b0770 100755
--- a/html/kernel.html
+++ b/html/kernel.html
@@ -5,10 +5,10 @@ title: Kernel & Plugins - Frama-C
active: 2
---
-<p>The Frama-C platform allows checking security, verifying requirement and
+<p>The Frama-C platform allows checking security, verifying requirements and
guaranteeing trust in C programs, thanks to a collection of collaborative
<a href="/html/kernel-plugin.html">plugins</a> that
- perform static analysis, deductive verification, and testing, for safety- and
+ perform static and dynamic analysis, for safety- and
security-critical software. Collaborative verification across cooperating
plug-ins is enabled by their integration on top of a shared kernel and
datastructures, and their compliance to
@@ -49,9 +49,9 @@ active: 2
notion of project. A project consistently stores a program with all its
required information, including results computed by analyzers and their
parameters. Several projects may coexist in memory at the same time. The
- projects are partitionned so that a modification on a particular projet does
- not impact the other ones. The project mechanism may also be used for example
- to perform different code transformation on the same original project, or to
+ projects are partitioned so that a modification on a particular projet does
+ not impact the others. The project mechanism may also be used for example
+ to perform different code transformations on the same original project, or to
execute a particular analysis on the same project but with different
parameters.
</p>
@@ -73,7 +73,7 @@ active: 2
the correctness of the entire verification process.
</p>
<p>The main correctness property of the Frama-C kernel can be stated as:
- “if the consolidated status of a property is computed as valid [resp. invalid]
+ "if the consolidated status of a property is computed as valid [resp. invalid]
by the kernel, then the property is valid [resp. invalid] with respect to ACSL
- semanticsâ€.
+ semantics".
</p>
--
GitLab