Skip to content
Snippets Groups Projects
Commit bcfd86c8 authored by Virgile Prevosto's avatar Virgile Prevosto Committed by Andre Maroneze
Browse files

[tests] update custom machdep test and test json loading

parent 08382f9f
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
{
"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
}
......@@ -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;
}
......
[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;
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment