由于自定义 machdep，Frama-C 中出现语法错误
Syntax error in Frama-C due to custom machdep
我正在为我的应用程序使用 MPLAB XC16 C 编译器。如果我使用 machdep x86_16，Frama-C 可以正常工作。例如，我可以这样启动 Frama-C：
$ frama-c-gui machdep x86_16 -cpp-command 'C:\"Program Files (x86)"\Microchip\xc16\v1.26\bin\xc16-gcc.exe -E' -no-cpp-gnu-like D:\project\*.c
但是 machdep x86_16 不完全符合 XC16。所以我想自定义machdep。
在 之后，我创建了文件 machdep_xc16.ml，其中包含：
open Cil_types
let xc16 =
{
version = "dsPIC33F";
compiler = "XC16"; (* Compiler being used. *)
sizeof_short = 2; (* Size of "short" *)
sizeof_int = 2; (* Size of "int" *)
sizeof_long = 4; (* Size of "long" *)
sizeof_longlong = 8; (* Size of "long long" *)
sizeof_ptr = 2; (* Size of pointers *)
sizeof_float = 4; (* Size of "float" *)
sizeof_double = 4; (* Size of "double" *)
sizeof_longdouble = 8; (* Size of "long double" *)
sizeof_void = 0; (* Size of "void" *)
sizeof_fun = 0; (* Size of function *)
size_t = "unsigned int"; (* Type of "sizeof(T)" *)
wchar_t = "unsigned short"; (* Type of "wchar_t" *)
ptrdiff_t = "int"; (* Type of "ptrdiff_t" *)
alignof_short = 2; (* Alignment of "short" *)
alignof_int = 2; (* Alignment of "int" *)
alignof_long = 2; (* Alignment of "long" *)
alignof_longlong = 2; (* Alignment of "long long" *)
alignof_ptr = 2; (* Alignment of pointers *)
alignof_float = 2; (* Alignment of "float" *)
alignof_double = 2; (* Alignment of "double" *)
alignof_longdouble = 2; (* Alignment of "long double" *)
alignof_str = 1; (* Alignment of strings *)
alignof_fun = 1; (* Alignment of function *)
alignof_aligned = 16; (* Alignment of a type with aligned attribute *)
char_is_unsigned = false; (* Whether "char" is unsigned *)
const_string_literals = true; (* Whether string literals have const chars *)
little_endian = true; (* whether the machine is little endian *)
underscore_name = true; (* If assembly names have leading underscore *)
has__builtin_va_list = false; (* Whether [__builtin_va_list] is a known type *)
__thread_is_keyword = false; (* Whether [__thread] is a keyword *)
}
let mach2 = { xc16 with compiler = "baz" }
let () =
let ran = ref false in
Cmdline.run_after_loading_stage
(fun () ->
Kernel.result "Registering machdep 'xc16' as 'XC16'";
File.new_machdep "XC16" xc16;
if !ran then begin
Kernel.result "Trying to register machdep 'mach2' as 'XC16'";
File.new_machdep "XC16" mach2
end
else ran := true
)
我在文件 __fc_machdep.h 行“#error Must define ...”之前插入了以下几行
#ifdef __FC_MACHDEP_XC16
#define __FC_BYTE_ORDER __LITTLE_ENDIAN
/* min and max values as specified in limits.h */
#define __FC_SCHAR_MAX 0x7f
#define __FC_SCHAR_MIN (-__FC_SCHAR_MAX -1)
#define __FC_UCHAR_MAX 0xff
#define __FC_CHAR_MIN __FC_SCHAR_MIN
#define __FC_CHAR_MAX __FC_SCHAR_MAX
#define __FC_SHRT_MAX 0x7fff
#define __FC_SHRT_MIN (-__FC_SHRT_MAX -1)
#define __FC_USHRT_MAX 0xffff
#define __FC_INT_MAX __FC_SHRT_MAX
#define __FC_INT_MIN __FC_SHRT_MIN
#define __FC_UINT_MAX __FC_USHRT_MAX
#define __FC_LONG_MAX 0x7fffffff
#define __FC_LONG_MIN (-__FC_LONG_MAX -1)
#define __FC_ULONG_MAX 0xffffffffU
#define __FC_LLONG_MAX 0x7fffffffffffffffLL
#define __FC_LLONG_MIN (-__FC_LLONG_MAX -1)
#define __FC_ULLONG_MAX 0xffffffffffffffffUL
/* Required */
#undef __CHAR_UNSIGNED__
#define __WORDSIZE 16
#define __SIZEOF_SHORT 2
#define __SIZEOF_INT 2
#define __SIZEOF_LONG 4
#define __SIZEOF_LONGLONG 8
#define __CHAR_BIT 8
#define __PTRDIFF_T int
#define __SIZE_T unsigned int
#define __FC_SIZE_MAX __FC_INT_MAX
/* stdio.h */
#define __FC_EOF (-1)
#define __FC_FOPEN_MAX 8
#define __FC_RAND_MAX 32767
#define __FC_PATH_MAX 260
#define __WCHAR_T unsigned short
/* Optional */
#define __INT8_T signed char
#define __UINT8_T unsigned char
#define __INT16_T signed int
#define __UINT16_T unsigned int
#define __INTPTR_T signed int
#define __UINTPTR_T unsigned int
#define __INT32_T signed long
#define __UINT32_T unsigned long
#define __INT64_T signed long long
#define __UINT64_T unsigned long long
/* Required */
#define __INT_LEAST8_T signed char
#define __UINT_LEAST8_T unsigned char
#define __INT_LEAST16_T signed int
#define __UINT_LEAST16_T unsigned int
#define __INT_LEAST32_T signed long
#define __UINT_LEAST32_T unsigned long
#define __INT_LEAST64_T signed long long
#define __UINT_LEAST64_T unsigned long long
#define __INT_FAST8_T signed char
#define __UINT_FAST8_T unsigned char
#define __INT_FAST16_T signed int
#define __UINT_FAST16_T unsigned int
#define __INT_FAST32_T signed long
#define __UINT_FAST32_T unsigned long
#define __INT_FAST64_T signed long long
#define __UINT_FAST64_T unsigned long long
/* POSIX */
#define __SSIZE_T signed long
#define __FC_PTRDIFF_MIN __FC_INT_MIN
#define __FC_PTRDIFF_MAX __FC_INT_MAX
#define __FC_VA_LIST_T char*
/* Required */
#define __INT_MAX_T signed long long
#define __UINT_MAX_T unsigned long long
#else
现在，如果我以这种方式启动 Frama-C：
$ frama-c-gui -load-script machdep_xc16 -machdep XC16 -cpp-command 'C:\"Program Files (x86)"\Microchip\xc16\v1.26\bin\xc16-gcc.exe -E' -no-cpp-gnu-like D:\project\*.c
我得到这样的输出：
[kernel] Registering machdep 'xc16' as 'XC16'
[kernel] Parsing .opam/4.02.3+mingw64c/share/frama-c/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] warning: machdep XC16 has no registered macro. Using __FC_MACHDEP_XC16 for pre-processing
[kernel] Parsing D:/project/main.c (with preprocessing)
. . .
[kernel] Parsing D:/project/get_data.c (with preprocessing)
[kernel] syntax error at .opam/4.02.3+mingw64c/share/frama-c/libc/__fc_define_wchar_t.h:28:
26 #if !defined(__cplusplus)
27 /* wchar_t is a keyword in C++ and shall not be a typedef. */
28 typedef __WCHAR_T wchar_t;
^^^^^^^^^^^^^^^^^^^^^^^^^^
29 #else
30 typedef __WCHAR_T fc_wchar_t;
处理包含#include <stdio.h>的文件时出现语法错误。
我做错了什么？
有关如何添加新 machdep 的说明已在手册中进行了修订，并将在下一个 Frama-C 版本（Phosporus）中提供。
新 machdep 的主要问题是 machdep 有两个（看似多余的）部分：OCaml-level 定义，由 Frama-C 使用，以及 C-level 定义，在解析 Frama-C 标准库时由 C 预处理器使用。意识到两者都是必要的和互补的有助于理解为什么整个过程很麻烦（尽管将来会简化）。
以下是即将发布的说明的摘录：
A custom machine description may be implemented as follows:
let my_machine = {
version = "generic C compiler for my machine";
compiler = "generic"; (* may also be "gcc" or "msvc" *)
cpp_arch_flags = ["-m64"];
sizeof_short = 2;
sizeof_int = 4;
sizeof_long = 8;
(* ... *)
}
let () = File.new_machdep "my_machine" my_machine
请注意，您的 machdep_xc16.ml 可以简化：您使用的代码是尝试注册两次相同 machdep 的测试的一部分，只是为了确保它失败。但实际上，当你使用 -load-script 时，你可以像上面那样直接创建 machdep，直接调用 File.new_machdep。
After this code is loaded, Frama-C can be instructed to use the new machine
model using the -machdep command line option.
If you intend to use Frama-C's standard library headers, you must also do the following:
define constant __FC_MACHDEP_<CUSTOM>, replacing <CUSTOM>
with the name (in uppercase letters) of your created machdep;
this can be done via -cpp-extra-args="-D__FC_MACHDEP_<CUSTOM>";
provide a header file with macro definitions corresponding to your caml
definitions. For the most part, these are macros prefixed by __FC_,
corresponding to standard C macro definitions, e.g.,
__FC_UCHAR_MAX. These definitions are used by Frama-C's
<limits.h> and other headers to provide the standard C definitions.
The test file tests/misc/custom_machdep/__fc_machdep_custom.h
contains a complete example of the required definitions. Other examples can
be found in share/libc/__fc_machdep.h.
Make sure that your custom header defines the __FC_MACHDEP
include guard, and that the program you are analyzing includes this header
before all other headers. One way to ensure this without having to modify any
source files is to use an option such as -include in GCC.
An example of the complete command-line is presented below, for a custom
machdep called myarch, defined in file my_machdep.ml and
with stdlib constants defined in machdep_myarch.h:
frama-c -load-script my_machdep.ml -machdep myarch \
-cpp-extra-args="-D__FC_MACHDEP_MYARCH -include machdep_myarch.h"
请注意，Silicon 中的 __fc_machdep_custom.h 不完整，但您发布的版本似乎是完整的，因此请改用它：将它放在一个名为 e.g. 的文件中。 machdep_xc16.h，向其添加 #define __FC_MACHDEP，并将其包含在其他文件之前，例如使用 -include machdep_xc16.h 作为预处理器标志。这将确保使用您的 machdep 版本而不是 Frama-C 的版本，这样您就可以使用 Frama-C 的标准库以及根据您的架构定义的常量。
此外，因为您的命令行包含 -cpp-command 和 -no-cpp-gnu-like，您必须调整上面的 -cpp-extra-args，将 -D__FC_MACHDEP_MYARCH 和 -include machdep_myarch.h直接在您的 -cpp-command.
我正在为我的应用程序使用 MPLAB XC16 C 编译器。如果我使用 machdep x86_16，Frama-C 可以正常工作。例如，我可以这样启动 Frama-C：
$ frama-c-gui machdep x86_16 -cpp-command 'C:\"Program Files (x86)"\Microchip\xc16\v1.26\bin\xc16-gcc.exe -E' -no-cpp-gnu-like D:\project\*.c
但是 machdep x86_16 不完全符合 XC16。所以我想自定义machdep。
在
open Cil_types
let xc16 =
{
version = "dsPIC33F";
compiler = "XC16"; (* Compiler being used. *)
sizeof_short = 2; (* Size of "short" *)
sizeof_int = 2; (* Size of "int" *)
sizeof_long = 4; (* Size of "long" *)
sizeof_longlong = 8; (* Size of "long long" *)
sizeof_ptr = 2; (* Size of pointers *)
sizeof_float = 4; (* Size of "float" *)
sizeof_double = 4; (* Size of "double" *)
sizeof_longdouble = 8; (* Size of "long double" *)
sizeof_void = 0; (* Size of "void" *)
sizeof_fun = 0; (* Size of function *)
size_t = "unsigned int"; (* Type of "sizeof(T)" *)
wchar_t = "unsigned short"; (* Type of "wchar_t" *)
ptrdiff_t = "int"; (* Type of "ptrdiff_t" *)
alignof_short = 2; (* Alignment of "short" *)
alignof_int = 2; (* Alignment of "int" *)
alignof_long = 2; (* Alignment of "long" *)
alignof_longlong = 2; (* Alignment of "long long" *)
alignof_ptr = 2; (* Alignment of pointers *)
alignof_float = 2; (* Alignment of "float" *)
alignof_double = 2; (* Alignment of "double" *)
alignof_longdouble = 2; (* Alignment of "long double" *)
alignof_str = 1; (* Alignment of strings *)
alignof_fun = 1; (* Alignment of function *)
alignof_aligned = 16; (* Alignment of a type with aligned attribute *)
char_is_unsigned = false; (* Whether "char" is unsigned *)
const_string_literals = true; (* Whether string literals have const chars *)
little_endian = true; (* whether the machine is little endian *)
underscore_name = true; (* If assembly names have leading underscore *)
has__builtin_va_list = false; (* Whether [__builtin_va_list] is a known type *)
__thread_is_keyword = false; (* Whether [__thread] is a keyword *)
}
let mach2 = { xc16 with compiler = "baz" }
let () =
let ran = ref false in
Cmdline.run_after_loading_stage
(fun () ->
Kernel.result "Registering machdep 'xc16' as 'XC16'";
File.new_machdep "XC16" xc16;
if !ran then begin
Kernel.result "Trying to register machdep 'mach2' as 'XC16'";
File.new_machdep "XC16" mach2
end
else ran := true
)
我在文件 __fc_machdep.h 行“#error Must define ...”之前插入了以下几行
#ifdef __FC_MACHDEP_XC16
#define __FC_BYTE_ORDER __LITTLE_ENDIAN
/* min and max values as specified in limits.h */
#define __FC_SCHAR_MAX 0x7f
#define __FC_SCHAR_MIN (-__FC_SCHAR_MAX -1)
#define __FC_UCHAR_MAX 0xff
#define __FC_CHAR_MIN __FC_SCHAR_MIN
#define __FC_CHAR_MAX __FC_SCHAR_MAX
#define __FC_SHRT_MAX 0x7fff
#define __FC_SHRT_MIN (-__FC_SHRT_MAX -1)
#define __FC_USHRT_MAX 0xffff
#define __FC_INT_MAX __FC_SHRT_MAX
#define __FC_INT_MIN __FC_SHRT_MIN
#define __FC_UINT_MAX __FC_USHRT_MAX
#define __FC_LONG_MAX 0x7fffffff
#define __FC_LONG_MIN (-__FC_LONG_MAX -1)
#define __FC_ULONG_MAX 0xffffffffU
#define __FC_LLONG_MAX 0x7fffffffffffffffLL
#define __FC_LLONG_MIN (-__FC_LLONG_MAX -1)
#define __FC_ULLONG_MAX 0xffffffffffffffffUL
/* Required */
#undef __CHAR_UNSIGNED__
#define __WORDSIZE 16
#define __SIZEOF_SHORT 2
#define __SIZEOF_INT 2
#define __SIZEOF_LONG 4
#define __SIZEOF_LONGLONG 8
#define __CHAR_BIT 8
#define __PTRDIFF_T int
#define __SIZE_T unsigned int
#define __FC_SIZE_MAX __FC_INT_MAX
/* stdio.h */
#define __FC_EOF (-1)
#define __FC_FOPEN_MAX 8
#define __FC_RAND_MAX 32767
#define __FC_PATH_MAX 260
#define __WCHAR_T unsigned short
/* Optional */
#define __INT8_T signed char
#define __UINT8_T unsigned char
#define __INT16_T signed int
#define __UINT16_T unsigned int
#define __INTPTR_T signed int
#define __UINTPTR_T unsigned int
#define __INT32_T signed long
#define __UINT32_T unsigned long
#define __INT64_T signed long long
#define __UINT64_T unsigned long long
/* Required */
#define __INT_LEAST8_T signed char
#define __UINT_LEAST8_T unsigned char
#define __INT_LEAST16_T signed int
#define __UINT_LEAST16_T unsigned int
#define __INT_LEAST32_T signed long
#define __UINT_LEAST32_T unsigned long
#define __INT_LEAST64_T signed long long
#define __UINT_LEAST64_T unsigned long long
#define __INT_FAST8_T signed char
#define __UINT_FAST8_T unsigned char
#define __INT_FAST16_T signed int
#define __UINT_FAST16_T unsigned int
#define __INT_FAST32_T signed long
#define __UINT_FAST32_T unsigned long
#define __INT_FAST64_T signed long long
#define __UINT_FAST64_T unsigned long long
/* POSIX */
#define __SSIZE_T signed long
#define __FC_PTRDIFF_MIN __FC_INT_MIN
#define __FC_PTRDIFF_MAX __FC_INT_MAX
#define __FC_VA_LIST_T char*
/* Required */
#define __INT_MAX_T signed long long
#define __UINT_MAX_T unsigned long long
#else
现在，如果我以这种方式启动 Frama-C：
$ frama-c-gui -load-script machdep_xc16 -machdep XC16 -cpp-command 'C:\"Program Files (x86)"\Microchip\xc16\v1.26\bin\xc16-gcc.exe -E' -no-cpp-gnu-like D:\project\*.c
我得到这样的输出：
[kernel] Registering machdep 'xc16' as 'XC16'
[kernel] Parsing .opam/4.02.3+mingw64c/share/frama-c/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] warning: machdep XC16 has no registered macro. Using __FC_MACHDEP_XC16 for pre-processing
[kernel] Parsing D:/project/main.c (with preprocessing)
. . .
[kernel] Parsing D:/project/get_data.c (with preprocessing)
[kernel] syntax error at .opam/4.02.3+mingw64c/share/frama-c/libc/__fc_define_wchar_t.h:28:
26 #if !defined(__cplusplus)
27 /* wchar_t is a keyword in C++ and shall not be a typedef. */
28 typedef __WCHAR_T wchar_t;
^^^^^^^^^^^^^^^^^^^^^^^^^^
29 #else
30 typedef __WCHAR_T fc_wchar_t;
处理包含#include <stdio.h>的文件时出现语法错误。
我做错了什么？
有关如何添加新 machdep 的说明已在手册中进行了修订，并将在下一个 Frama-C 版本（Phosporus）中提供。
新 machdep 的主要问题是 machdep 有两个（看似多余的）部分：OCaml-level 定义，由 Frama-C 使用，以及 C-level 定义，在解析 Frama-C 标准库时由 C 预处理器使用。意识到两者都是必要的和互补的有助于理解为什么整个过程很麻烦（尽管将来会简化）。
以下是即将发布的说明的摘录：
A custom machine description may be implemented as follows:
let my_machine = {
version = "generic C compiler for my machine";
compiler = "generic"; (* may also be "gcc" or "msvc" *)
cpp_arch_flags = ["-m64"];
sizeof_short = 2;
sizeof_int = 4;
sizeof_long = 8;
(* ... *)
}
let () = File.new_machdep "my_machine" my_machine
请注意，您的 machdep_xc16.ml 可以简化：您使用的代码是尝试注册两次相同 machdep 的测试的一部分，只是为了确保它失败。但实际上，当你使用 -load-script 时，你可以像上面那样直接创建 machdep，直接调用 File.new_machdep。
After this code is loaded, Frama-C can be instructed to use the new machine model using the
-machdepcommand line option.If you intend to use Frama-C's standard library headers, you must also do the following:
define constant
__FC_MACHDEP_<CUSTOM>, replacing<CUSTOM>with the name (in uppercase letters) of your created machdep; this can be done via-cpp-extra-args="-D__FC_MACHDEP_<CUSTOM>";provide a header file with macro definitions corresponding to your caml definitions. For the most part, these are macros prefixed by
__FC_, corresponding to standard C macro definitions, e.g.,__FC_UCHAR_MAX. These definitions are used by Frama-C's<limits.h>and other headers to provide the standard C definitions. The test filetests/misc/custom_machdep/__fc_machdep_custom.hcontains a complete example of the required definitions. Other examples can be found inshare/libc/__fc_machdep.h.Make sure that your custom header defines the
__FC_MACHDEPinclude guard, and that the program you are analyzing includes this header before all other headers. One way to ensure this without having to modify any source files is to use an option such as-includein GCC.An example of the complete command-line is presented below, for a custom machdep called
myarch, defined in filemy_machdep.mland with stdlib constants defined inmachdep_myarch.h:
frama-c -load-script my_machdep.ml -machdep myarch \
-cpp-extra-args="-D__FC_MACHDEP_MYARCH -include machdep_myarch.h"
请注意，Silicon 中的 __fc_machdep_custom.h 不完整，但您发布的版本似乎是完整的，因此请改用它：将它放在一个名为 e.g. 的文件中。 machdep_xc16.h，向其添加 #define __FC_MACHDEP，并将其包含在其他文件之前，例如使用 -include machdep_xc16.h 作为预处理器标志。这将确保使用您的 machdep 版本而不是 Frama-C 的版本，这样您就可以使用 Frama-C 的标准库以及根据您的架构定义的常量。
此外，因为您的命令行包含 -cpp-command 和 -no-cpp-gnu-like，您必须调整上面的 -cpp-extra-args，将 -D__FC_MACHDEP_MYARCH 和 -include machdep_myarch.h直接在您的 -cpp-command.