diff --git a/doc/value/examples/misa.c b/doc/value/examples/misa.c index 7c310b3662fa3e05c5157dc740df66513340c24f..7ca812b5d323a9b52130b1037c6f091bd7453f1b 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 06e5735b0a4afc8a5df2a6fb238afc39aa8118cd..fe1e7decd6bbf224fbf55c7196514007a78798d5 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]|.