From 828b1cd17d252c29e5962ec4beddec040952a84d Mon Sep 17 00:00:00 2001 From: Virgile Prevosto <virgile.prevosto@m4x.org> Date: Thu, 31 Aug 2023 18:37:58 +0200 Subject: [PATCH] add test for _Nullable handling --- tests/syntax/nullable.i | 7 +++++++ tests/syntax/oracle/nullable.res.oracle | 24 ++++++++++++++++++++++++ 2 files changed, 31 insertions(+) create mode 100644 tests/syntax/nullable.i create mode 100644 tests/syntax/oracle/nullable.res.oracle diff --git a/tests/syntax/nullable.i b/tests/syntax/nullable.i new file mode 100644 index 00000000000..b63f6350fef --- /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 00000000000..2e2dca9c504 --- /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; +} + + -- GitLab