diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex index 5e81e4c5acbbe5a1a3b63694c770ce232b130838..770627e22ec1fc35553ea74e5755bdbd1fb2d24d 100644 --- a/doc/developer/advance.tex +++ b/doc/developer/advance.tex @@ -3206,9 +3206,9 @@ We present below a thorough description of each field. \item[\texttt{compiler}]: defines whether special compiler-specific extensions will be enabled. It should be one of the strings below: \begin{itemize} - \item[\texttt{msvc}]: enables \verb+Cil.msvcMode+, that is, + \item[\texttt{msvc}]: enables \verb+Machine.msvcMode+, that is, MSVC (Visual Studio)-specific extensions; - \item[\texttt{gcc}]: enables \verb+Cil.gccMode+, that is, + \item[\texttt{gcc}]: enables \verb+Machine.gccMode+, that is, GCC-specific extensions; \item[\texttt{generic}] (or any other string): no special compiler-specific extensions. diff --git a/src/kernel_services/ast_data/cil_types.ml b/src/kernel_services/ast_data/cil_types.ml index aaa0fa132b0164c4b0c67b13a15b1ff810c5e386..185a7fa68fe5f8f67c3219062965e23866e6e546 100644 --- a/src/kernel_services/ast_data/cil_types.ml +++ b/src/kernel_services/ast_data/cil_types.ml @@ -754,9 +754,9 @@ and exp_node = | Const of constant (** Constant *) | Lval of lval (** Lvalue *) | SizeOf of typ - (** sizeof(<type>). Has [unsigned int] type (ISO 6.5.3.4). This is not - turned into a constant because some transformations might want to change - types *) + (** sizeof(<type>). Has [size_t] type (ISO 6.5.3.4) which depends on machine + configuration (cf. {!Machine}). This is not turned into a constant + because some transformations might want to change types *) | SizeOfE of exp (** sizeof(<expression>) *) @@ -766,7 +766,8 @@ and exp_node = type pointer to character. *) | AlignOf of typ - (** This corresponds to the GCC __alignof_. Has [unsigned int] type *) + (** This corresponds to the GCC __alignof_. Has [size_t] type which depends on + machine configuration (cf. {!Machine}). *) | AlignOfE of exp