diff --git a/Changelog b/Changelog
index 06f046e141359e41c3acc9a45093fa00a680ac41..a173d8fbcd0128aa34a40dd0670640855bc8b018 100644
--- a/Changelog
+++ b/Changelog
@@ -72,8 +72,8 @@ o! Kernel [2021-01-15] Make cfields list optional. None means undefined,
removed cdefined field
-* RTE [2021-01-13] Remove spurious assert when comparing function
pointer to NULL (fixes #@940)
-- Kernel [2021-01-12] Set default machdep to x86_64; allow setting machdep
- via environment variable FRAMAC_MACHDEP.
+- Kernel [2021-01-12] Set default machdep to x86_64 (was x86_32);
+ allow setting machdep via environment variable FRAMAC_MACHDEP.
- Kernel [2021-01-08] Allow -add-symbolic-path to survive saves/loads and
invert argument order (path:name).
-* Eva [2020-12-05] Fixes a crash when subdividing the evaluation of
diff --git a/doc/value/main.tex b/doc/value/main.tex
index d689a9bb981ab7fb41726250b375f9bc4d547249..7bb3bdb724081a1d77fcbec1e60d12f4469883ad 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -378,13 +378,13 @@ would be during an actual compilation.
There are analyses where the influence of host platform parameters
is not noticeable. The analysis we are embarking on is not one of them.
-If you pre-process the Skein source code with a 64-bit compiler and
-then analyze it with Frama-C targeting its default 32-bit platform,
+If you pre-process the Skein source code with a 32-bit compiler and
+then analyze it with Frama-C targeting its default 64-bit platform,
the analysis will be meaningless and you won't be able to make sense of
this tutorial.
-If you are using a 64-bit compiler, simply match
+If you are using a 32-bit compiler, simply match
Frama-C's target platform with your host header files by systematically adding
-the option \verb|-machdep x86_64| to all commands in
+the option \verb|-machdep x86_32| to all commands in
this tutorial.
The ``\lstinline|>log|'' part of the command sends all
@@ -3246,7 +3246,7 @@ sets a number of parameters for the low-level description of the
target platform, including the
\emph{endianness} of the target and size of each C type.
The option \lstinline|-machdep help| provides a list of currently supported
-platforms. The default is \lstinline|x86_32|, an IA-32 processor with
+platforms. The default is \lstinline|x86_64|, an AMD64-compatible processor with
what are roughly the default compilation choices of gcc.
\subsubsection{Targeting a different platform}
diff --git a/man/frama-c.1 b/man/frama-c.1
index a0173eeecbf1c2ad09aa1805593b0d524aeb8571..969afd9eac24f67f59b967eef0e51b17082bed4c 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -1,6 +1,6 @@
-.\" Automatically generated by Pandoc 2.11.3
+.\" Automatically generated by Pandoc 2.14.0.2
.\"
-.TH "FRAMA-C" "1" "" "2021-02-16" ""
+.TH "FRAMA-C" "1" "" "2021-06-18" ""
.hy
.\"------------------------------------------------------------------------
.\"
@@ -390,7 +390,7 @@ uses \f[I]machine\f[R] as the current machine-dependent configuration
(size of the various integer types, endiandness, \&...).
The list of currently supported machines is available through option
\f[I]-machdep help\f[R].
-Default is \f[B]x86_32\f[R].
+Default is \f[B]x86_64\f[R].
.TP
-main \f[I]f\f[R]
sets \f[I]f\f[R] as the entry point of the analysis.
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index 5ed2c0f2b2385f7a93419eea37c5f19e106c9636..3d7aabda6cd921a3a8a6801f53049016bdd1671f 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -1,5 +1,5 @@
---
-title: 'FRAMA-C(1) 2021-02-16'
+title: 'FRAMA-C(1) 2021-06-18'
header-includes:
- |
```{=man}
@@ -332,7 +332,7 @@ Loading order is preserved and additional dependencies can be listed in
-machdep *machine*
: uses *machine* as the current machine-dependent configuration (size of the
various integer types, endiandness, ...). The list of currently supported
-machines is available through option *-machdep help*. Default is **x86_32**.
+machines is available through option *-machdep help*. Default is **x86_64**.
-main *f*
: sets *f* as the entry point of the analysis. Defaults to **main**.
diff --git a/share/analysis-scripts/template.mk b/share/analysis-scripts/template.mk
index caaee20f0d9aa3db2bad843121689acf99e3a48f..d054288c0ac1ee71f9a16a44a1c65f89ecf38fd1 100644
--- a/share/analysis-scripts/template.mk
+++ b/share/analysis-scripts/template.mk
@@ -12,7 +12,7 @@ include $(shell $(FRAMAC)-config -print-share-path)/analysis-scripts/prologue.mk
# Edit below as needed. Suggested flags are optional.
-MACHDEP = x86_32
+MACHDEP = x86_64
## Preprocessing flags (for -cpp-extra-args)
CPPFLAGS += \
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 23900b640933ece2d12960901d2e8f5bce7b1697..a1f3467b9489bfa294a67c5a0fa9dd8f7ffa53b9 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -125,11 +125,9 @@ type theMachine =
mutable kindOfSizeOf: ikind;
}
-let default_machdep = Machdeps.x86_32
-
let createMachine () = (* Contain dummy values *)
{ useLogicalOperators = false;
- theMachine = default_machdep;
+ theMachine = Machdeps.x86_64;
lowerConstants = false(*true*);
insertImplicitCasts = true;
underscore_name = true;
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 7e7117dfaf4f9e9893b1ec6d00c1a013ad33f1e7..e2c3f91b346641b981ddae8b3ea4ec07990ca0b4 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -310,7 +310,7 @@ let default_machdeps =
[ "x86_16", Machdeps.x86_16;
"x86_32", Machdeps.x86_32;
"x86_64", Machdeps.x86_64;
- "gcc_x86_16", Machdeps.x86_16;
+ "gcc_x86_16", Machdeps.gcc_x86_16;
"gcc_x86_32", Machdeps.gcc_x86_32;
"gcc_x86_64", Machdeps.gcc_x86_64;
"ppc_32", Machdeps.ppc_32;
@@ -367,7 +367,7 @@ let machdep_help () =
let m = Kernel.Machdep.get () in
if m = "help" then begin
Kernel.feedback
- "@[supported machines are%t@ (default is x86_32).@]"
+ "@[supported machines are%t@ (default is x86_64).@]"
pretty_machdeps;
raise Cmdline.Exit
end else