From 5b89aac94e4d10e1eb648ca0aac3731e01cb2ffd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 28 Jan 2022 12:58:26 +0100
Subject: [PATCH] [Eva] User manual: updates the default Frama-C machdep.
And fixes the example of misaligned read.
---
doc/value/examples/misa.c | 2 +-
doc/value/main.tex | 8 ++++----
2 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/doc/value/examples/misa.c b/doc/value/examples/misa.c
index 7c310b3662f..7ca812b5d32 100644
--- a/doc/value/examples/misa.c
+++ b/doc/value/examples/misa.c
@@ -3,5 +3,5 @@ int *t[2] = { &x, &y };
int main(void)
{
- return 1 + (int) * (int*) ((int) t + 2);
+ return * (int*) ((unsigned long) t + 6);
}
diff --git a/doc/value/main.tex b/doc/value/main.tex
index 06e5735b0a4..fe1e7decd6b 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -371,7 +371,7 @@ frama-c -eva main_1.c >log
\end{listing-nonumber}
Frama-C has its own model of the target platform (the default target is
-a little-endian 32-bit platform). It also uses the host system's preprocessor.
+a little-endian 64-bit platform). It also uses the host system's preprocessor.
If you want to do the analysis for a different platform than the host platform,
you need to provide Frama-C with a way to pre-process the files as they
would be during an actual compilation.
@@ -579,7 +579,7 @@ use variable \lstinline|ONE| to detect endianness.
Frama-C assumes a little-endian architecture
by default, so \Eva{} is only analyzing the
little-endian version of the library (Frama-C
-also assumes an IA-32 architecture, so we are only
+also assumes an IA-64 architecture, so we are only
analyzing the library as compiled and run on this architecture).
The big-endian version of the library could be analyzed
by reproducing the same steps we are taking here for
@@ -1349,14 +1349,14 @@ An example of a program leading to a misaligned read is the following:
\listinginput{1}{examples/misa.c}
The value returned by the function \lstinline|main| is\\
\lstinline|{{ garbled mix of &{ x; y } (origin: Misaligned { misa.c:6 }) }}|.\\
-The analyzer is by default configured for a 32-bit architecture,
+The analyzer is by default configured for a 64-bit architecture,
and that consequently the read memory access is not an out-of-bound access.
If it was, an alarm would be emitted, and the
analysis would go in a different direction.
With the default target platform, the read access remains
within the bounds of array \lstinline|t|,
-but due to the offset of two bytes,
+but due to the offset of six bytes,
the 32-bit word read is made of the last two bytes from \lstinline|t[0]|
and the first two bytes from \lstinline|t[1]|.
--
GitLab