diff --git a/tests/syntax/nullable.i b/tests/syntax/nullable.i new file mode 100644 index 0000000000000000000000000000000000000000..b63f6350fefb7fda3632ebd7668bb5e8a3066f48 --- /dev/null +++ b/tests/syntax/nullable.i @@ -0,0 +1,7 @@ +/* _Nullable is a macOS-specific qualifier. For now, we just ignore it. */ + +int * _Nullable test(void) { return (int*)0; } + +extern int (* _Nullable _fptr)(void); + +int f(int * _Nullable x) { if (x) return *x; else return 0; } diff --git a/tests/syntax/oracle/nullable.res.oracle b/tests/syntax/oracle/nullable.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..2e2dca9c504ea432c69fadc98fa7a6e105de0e4f --- /dev/null +++ b/tests/syntax/oracle/nullable.res.oracle @@ -0,0 +1,24 @@ +[kernel] Parsing nullable.i (no preprocessing) +/* Generated by Frama-C */ +int *test(void) +{ + int *__retres; + __retres = (int *)0; + return __retres; +} + +int f(int *x) +{ + int __retres; + if (x) { + __retres = *x; + goto return_label; + } + else { + __retres = 0; + goto return_label; + } + return_label: return __retres; +} + +