Я использую компилятор MPLAB XC16 C для моего приложения. Если я использую machdep x86_16, Frama-C работает нормально. Например, я могу launche FRAMA-C таким образом:Ошибка синтаксиса в Frama-C из-за пользовательского machdep
$ 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.
После the instructions, я создал файл 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 должен определить ..."
#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_xc16.h и использовал -include machdep_xc16.h, но теперь у меня есть ошибка пользователя: .opam/4.02.3 + mingw64c/share/frama-c/libc/stdio.h: 101: [kernel] failure: невозможно разрешить переменную __FC_FOPEN_MAX [ядро] ошибка пользователя: остановка в файле «D: \\ project \\ get_data.c», что имеет ошибки. –
Я решил эту проблему, добавив #define __FC_FOPEN_MAX 0 –
Действительно, в вашем machdep были некоторые отсутствующие определения ('__FC_EOF',' __FC_FOPEN_MAX' и '__FC_RAND_MAX'), я добавил их к вашему вопросу, чтобы другие могли копировать/вставлять ваши пример. – anol