diff --git a/tests/misc/custom_machdep.c b/tests/misc/custom_machdep.c index c51544e41f4e98bea09bda86ebeb580a1c6db8b8..b28d8660679fc128f7cc31daed65c2b62e2e5cb2 100644 --- a/tests/misc/custom_machdep.c +++ b/tests/misc/custom_machdep.c @@ -4,6 +4,9 @@ DEPS: @PTEST_NAME@/__fc_machdep_custom.h OPT: -cpp-extra-args="-I./@PTEST_NAME@ -D__FC_MACHDEP_CUSTOM" -machdep custom -print -then -print COMMENT: we need a -then to test double registering of a machdep + EXIT: 0 + DEPS: @PTEST_NAME@/__fc_machdep_custom.h + OPT: -cpp-extra-args="-I./@PTEST_NAME@ -D__FC_MACHDEP_CUSTOM" -machdep %{dep:@PTEST_DIR@/@PTEST_NAME@.json} -print */ #include "__fc_machdep_custom.h" // most of the following includes are not directly used, but they test if diff --git a/tests/misc/custom_machdep.json b/tests/misc/custom_machdep.json new file mode 100644 index 0000000000000000000000000000000000000000..0761e8060aefaa3ede539ff108e0ba32be392367 --- /dev/null +++ b/tests/misc/custom_machdep.json @@ -0,0 +1,32 @@ + { + "version": "foo", + "compiler": "bar", + "cpp_arch_flags" : [], + "sizeof_short" : 2, + "sizeof_int": 3, + "sizeof_long": 4, + "sizeof_longlong" : 8, + "sizeof_ptr" : 4, + "sizeof_float": 4, + "sizeof_double": 8, + "sizeof_longdouble": 12, + "sizeof_void": 1, + "sizeof_fun" : 1, + "size_t" : "unsigned long", + "wchar_t" : "int", + "ptrdiff_t": "int", + "alignof_short" : 2, + "alignof_int": 3, + "alignof_long": 4, + "alignof_longlong": 4, + "alignof_ptr" : 4, + "alignof_float": 4, + "alignof_double": 4, + "alignof_longdouble": 4, + "alignof_str": 1, + "alignof_fun": 1, + "alignof_aligned": 16, + "char_is_unsigned": false, + "little_endian": true, + "has__builtin_va_list": true + } diff --git a/tests/misc/custom_machdep.ml b/tests/misc/custom_machdep.ml index 503611ae1fec6f6b921e2d1cdeecfeae7fba075b..e7a740d59b40bc6b4f2b3a28c1a41998195bb0bb 100644 --- a/tests/misc/custom_machdep.ml +++ b/tests/misc/custom_machdep.ml @@ -30,9 +30,7 @@ let mach = alignof_fun = 1; alignof_aligned= 16; char_is_unsigned = false; - const_string_literals = true; little_endian = true; - underscore_name = false ; has__builtin_va_list = true; } diff --git a/tests/misc/oracle/custom_machdep.res.oracle b/tests/misc/oracle/custom_machdep.0.res.oracle similarity index 100% rename from tests/misc/oracle/custom_machdep.res.oracle rename to tests/misc/oracle/custom_machdep.0.res.oracle diff --git a/tests/misc/oracle/custom_machdep.1.res.oracle b/tests/misc/oracle/custom_machdep.1.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..10262698fca641f0558ec346f437476b0285b833 --- /dev/null +++ b/tests/misc/oracle/custom_machdep.1.res.oracle @@ -0,0 +1,26 @@ +[kernel] Registering machdep 'mach' as 'custom' +[kernel] Parsing custom_machdep.c (with preprocessing) +/* Generated by Frama-C */ +#include "ctype.h" +#include "errno.h" +#include "inttypes.h" +#include "locale.h" +#include "math.h" +#include "signal.h" +#include "stdarg.h" +#include "stddef.h" +#include "stdint.h" +#include "stdio.h" +#include "stdlib.h" +#include "string.h" +#include "strings.h" +#include "time.h" +#include "wchar.h" +int main(void) +{ + int __retres; + __retres = (int)2147483647; + return __retres; +} + +