From ad30bd5f2043cac0164b90937668d379be8a0069 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon, 8 Jul 2024 14:40:24 +0200
Subject: [PATCH] [tests] Add funptr_noreturn test + Update oracles
---
.../e-acsl/tests/builtin/oracle/gen_strcat.c | 4 +-
.../e-acsl/tests/builtin/oracle/gen_strcmp.c | 8 +--
.../e-acsl/tests/builtin/oracle/gen_strcpy.c | 4 +-
.../e-acsl/tests/builtin/oracle/gen_strlen.c | 8 +--
.../concurrency/oracle/gen_parallel_threads.c | 4 +-
.../concurrency/oracle/gen_threads_debug.c | 4 +-
.../e-acsl/tests/format/oracle/gen_fprintf.c | 4 +-
.../e-acsl/tests/format/oracle/gen_printf.c | 8 +--
tests/libc/oracle/fc_libc.1.res.oracle | 2 +-
tests/pretty_printing/funptr_noreturn.c | 24 +++++++
.../oracle/funptr_noreturn.res.oracle | 71 +++++++++++++++++++
.../oracle/default_spec_mode.0.res.oracle | 3 +-
.../oracle/default_spec_mode.1.res.oracle | 3 +-
.../oracle/default_spec_mode.2.res.oracle | 3 +-
.../oracle/default_spec_mode.3.res.oracle | 3 +-
.../oracle/default_spec_mode.4.res.oracle | 3 +-
tests/syntax/oracle/built.res.oracle | 4 +-
17 files changed, 125 insertions(+), 35 deletions(-)
create mode 100644 tests/pretty_printing/funptr_noreturn.c
create mode 100644 tests/pretty_printing/oracle/funptr_noreturn.res.oracle
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
index f3b8d9158f2..a235f02b21d 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
@@ -51,7 +51,7 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == -1 || \result >= 0;
ensures
@@ -784,7 +784,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
exit(status);
{
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
index 58862fef589..22861bb8b86 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
@@ -53,7 +53,7 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
assigns \exit_status \from \nothing;
*/
-void __gen_e_acsl_abort(void);
+ __attribute__((__noreturn__)) void __gen_e_acsl_abort(void);
/*@ terminates \false;
exits status: \exit_status == \old(status);
@@ -61,7 +61,7 @@ void __gen_e_acsl_abort(void);
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == -1 || \result >= 0;
ensures
@@ -352,7 +352,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
exit(status);
{
@@ -375,7 +375,7 @@ void __gen_e_acsl_exit(int status)
assigns \exit_status \from \nothing;
*/
-void __gen_e_acsl_abort(void)
+ __attribute__((__noreturn__)) void __gen_e_acsl_abort(void)
{
abort();
{
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
index 72d8735dd4a..9c38744e026 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
@@ -45,7 +45,7 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == -1 || \result >= 0;
ensures
@@ -765,7 +765,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
exit(status);
{
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
index 4aefe12825d..fbde72d4e6b 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
+++ b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
@@ -36,7 +36,7 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
assigns \exit_status \from \nothing;
*/
-void __gen_e_acsl_abort(void);
+ __attribute__((__noreturn__)) void __gen_e_acsl_abort(void);
/*@ terminates \false;
exits status: \exit_status == \old(status);
@@ -44,7 +44,7 @@ void __gen_e_acsl_abort(void);
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == -1 || \result >= 0;
ensures
@@ -326,7 +326,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
exit(status);
{
@@ -349,7 +349,7 @@ void __gen_e_acsl_exit(int status)
assigns \exit_status \from \nothing;
*/
-void __gen_e_acsl_abort(void)
+ __attribute__((__noreturn__)) void __gen_e_acsl_abort(void)
{
abort();
{
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
index a73f89d3e51..b6071854f7c 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_parallel_threads.c
@@ -133,7 +133,7 @@ void __gen_e_acsl_perror(char const *s);
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == 0 || \result == -1;
assigns \result, Frama_C_entropy_source;
@@ -768,7 +768,7 @@ int __gen_e_acsl_usleep(useconds_t usec)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
__e_acsl_store_block((void *)(& status),4UL);
exit(status);
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
index 7583e2dc85f..2a778a1f8cc 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/gen_threads_debug.c
@@ -133,7 +133,7 @@ void __gen_e_acsl_perror(char const *s);
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == 0 || \result == -1;
assigns \result, Frama_C_entropy_source;
@@ -450,7 +450,7 @@ int __gen_e_acsl_usleep(useconds_t usec)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
__e_acsl_store_block((void *)(& status),4UL);
exit(status);
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
index 8aa685ba92e..ed7d5351a40 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
@@ -66,7 +66,7 @@ int __gen_e_acsl_fclose(FILE *stream);
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == -1 || \result >= 0;
ensures
@@ -262,7 +262,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
exit(status);
{
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
index fed7aed3b60..0fd82086aff 100644
--- a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
+++ b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c
@@ -478,7 +478,7 @@ extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
assigns \exit_status \from \nothing;
*/
-void __gen_e_acsl_abort(void);
+ __attribute__((__noreturn__)) void __gen_e_acsl_abort(void);
/*@ terminates \false;
exits status: \exit_status == \old(status);
@@ -486,7 +486,7 @@ void __gen_e_acsl_abort(void);
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status);
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status);
/*@ ensures result_ok_or_error: \result == -1 || \result >= 0;
ensures
@@ -1119,7 +1119,7 @@ pid_t __gen_e_acsl_waitpid(pid_t pid, int *stat_loc, int options)
assigns \exit_status \from status;
*/
-void __gen_e_acsl_exit(int status)
+ __attribute__((__noreturn__)) void __gen_e_acsl_exit(int status)
{
exit(status);
{
@@ -1142,7 +1142,7 @@ void __gen_e_acsl_exit(int status)
assigns \exit_status \from \nothing;
*/
-void __gen_e_acsl_abort(void)
+ __attribute__((__noreturn__)) void __gen_e_acsl_abort(void)
{
abort();
{
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 88b5d0e3123..67ee1541e1c 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -907,7 +907,7 @@ extern __attribute__((__noreturn__)) void __builtin_abort(void);
ensures never_terminates: \false;
assigns \nothing; */
__attribute__((__noreturn__, __FC_BUILTIN__)) void Frama_C_abort(void);
-void Frama_C_abort(void)
+ __attribute__((__noreturn__)) void Frama_C_abort(void)
{
__builtin_abort();
return;
diff --git a/tests/pretty_printing/funptr_noreturn.c b/tests/pretty_printing/funptr_noreturn.c
new file mode 100644
index 00000000000..d1e5b586f5f
--- /dev/null
+++ b/tests/pretty_printing/funptr_noreturn.c
@@ -0,0 +1,24 @@
+/* run.config
+ STDOPT:
+*/
+
+#include <stdlib.h>
+
+__attribute__((__noreturn__)) void f1() {
+ exit(0);
+}
+
+__attribute__((__noreturn__)) void f2(){
+ __attribute__((__noreturn__)) void (*funptr)(void) = &f1;
+ (*funptr)();
+}
+
+_Noreturn void g1() {
+ exit(0);
+}
+
+_Noreturn void g2(){
+ _Noreturn void (*funptr)(void) = &g1;
+ (*funptr)();
+}
+
diff --git a/tests/pretty_printing/oracle/funptr_noreturn.res.oracle b/tests/pretty_printing/oracle/funptr_noreturn.res.oracle
new file mode 100644
index 00000000000..365d5165e0a
--- /dev/null
+++ b/tests/pretty_printing/oracle/funptr_noreturn.res.oracle
@@ -0,0 +1,71 @@
+[kernel] Parsing funptr_noreturn.c (with preprocessing)
+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdlib.h"
+ __attribute__((__noreturn__)) void f1(void)
+{
+ exit(0);
+ return;
+}
+
+ __attribute__((__noreturn__)) void f2(void)
+{
+ void ( __attribute__((__noreturn__)) (*funptr))(void) = & f1;
+ (*funptr)();
+ return;
+}
+
+ __attribute__((__noreturn__)) void g1(void)
+{
+ exit(0);
+ return;
+}
+
+ __attribute__((__noreturn__)) void g2(void)
+{
+ void ( __attribute__((__noreturn__)) (*funptr))(void) = & g1;
+ (*funptr)();
+ return;
+}
+
+
+[kernel] Parsing ocode_funptr_noreturn.c (with preprocessing)
+[kernel] Parsing funptr_noreturn.c (with preprocessing)
+[kernel] funptr_noreturn.c:7: Warning:
+ def'n of func f1 at funptr_noreturn.c:7 (sum 887) conflicts with the one at ocode_funptr_noreturn.c:4 (sum 1081); keeping the one at ocode_funptr_noreturn.c:4.
+[kernel] funptr_noreturn.c:11: Warning:
+ def'n of func f2 at funptr_noreturn.c:11 (sum 1774) conflicts with the one at ocode_funptr_noreturn.c:10 (sum 1968); keeping the one at ocode_funptr_noreturn.c:10.
+[kernel] funptr_noreturn.c:16: Warning:
+ def'n of func g1 at funptr_noreturn.c:16 (sum 887) conflicts with the one at ocode_funptr_noreturn.c:17 (sum 1081); keeping the one at ocode_funptr_noreturn.c:17.
+[kernel] funptr_noreturn.c:20: Warning:
+ def'n of func g2 at funptr_noreturn.c:20 (sum 1774) conflicts with the one at ocode_funptr_noreturn.c:23 (sum 1968); keeping the one at ocode_funptr_noreturn.c:23.
+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdlib.h"
+ __attribute__((__noreturn__)) void f1(void)
+{
+ exit(0);
+ return;
+}
+
+ __attribute__((__noreturn__)) void f2(void)
+{
+ void ( __attribute__((__noreturn__)) (*funptr))(void) = & f1;
+ (*funptr)();
+ return;
+}
+
+ __attribute__((__noreturn__)) void g1(void)
+{
+ exit(0);
+ return;
+}
+
+ __attribute__((__noreturn__)) void g2(void)
+{
+ void ( __attribute__((__noreturn__)) (*funptr))(void) = & g1;
+ (*funptr)();
+ return;
+}
+
+
diff --git a/tests/spec/oracle/default_spec_mode.0.res.oracle b/tests/spec/oracle/default_spec_mode.0.res.oracle
index 06e27d95b34..b3e13b9e5d8 100644
--- a/tests/spec/oracle/default_spec_mode.0.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.0.res.oracle
@@ -56,8 +56,7 @@ int f4(int *b)
/*@ terminates \false;
exits \false;
allocates \nothing; */
- __attribute__((__noreturn__)) void f5(void);
-void f5(void)
+ __attribute__((__noreturn__)) void f5(void)
{
while (1) ;
return;
diff --git a/tests/spec/oracle/default_spec_mode.1.res.oracle b/tests/spec/oracle/default_spec_mode.1.res.oracle
index 28bd6a55879..7668bbc5033 100644
--- a/tests/spec/oracle/default_spec_mode.1.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.1.res.oracle
@@ -46,8 +46,7 @@ int f4(int *b)
exits \false;
assigns \nothing;
allocates \nothing; */
- __attribute__((__noreturn__)) void f5(void);
-void f5(void)
+ __attribute__((__noreturn__)) void f5(void)
{
while (1) ;
return;
diff --git a/tests/spec/oracle/default_spec_mode.2.res.oracle b/tests/spec/oracle/default_spec_mode.2.res.oracle
index a4e0f835c66..b403960922c 100644
--- a/tests/spec/oracle/default_spec_mode.2.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.2.res.oracle
@@ -69,8 +69,7 @@ int f4(int *b)
exits \false;
assigns \nothing;
allocates \nothing; */
- __attribute__((__noreturn__)) void f5(void);
-void f5(void)
+ __attribute__((__noreturn__)) void f5(void)
{
while (1) ;
return;
diff --git a/tests/spec/oracle/default_spec_mode.3.res.oracle b/tests/spec/oracle/default_spec_mode.3.res.oracle
index e1e0f73f927..b6067af62b3 100644
--- a/tests/spec/oracle/default_spec_mode.3.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.3.res.oracle
@@ -71,8 +71,7 @@ int f4(int *b)
exits \false;
assigns \nothing;
allocates \nothing; */
- __attribute__((__noreturn__)) void f5(void);
-void f5(void)
+ __attribute__((__noreturn__)) void f5(void)
{
while (1) ;
return;
diff --git a/tests/spec/oracle/default_spec_mode.4.res.oracle b/tests/spec/oracle/default_spec_mode.4.res.oracle
index b2591584562..0822b20709a 100644
--- a/tests/spec/oracle/default_spec_mode.4.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.4.res.oracle
@@ -53,8 +53,7 @@ int f4(int *b)
/*@ terminates \false;
assigns \nothing;
allocates \nothing; */
- __attribute__((__noreturn__)) void f5(void);
-void f5(void)
+ __attribute__((__noreturn__)) void f5(void)
{
while (1) ;
return;
diff --git a/tests/syntax/oracle/built.res.oracle b/tests/syntax/oracle/built.res.oracle
index c763be7e968..5b247f48b47 100644
--- a/tests/syntax/oracle/built.res.oracle
+++ b/tests/syntax/oracle/built.res.oracle
@@ -2,8 +2,8 @@
[kernel] built.i:21:
Case label -1 exceeds range of unsigned int for switch expression. Nothing to worry.
/* Generated by Frama-C */
-__inline static _Noreturn int dummy_f__fc_inline(void);
-__inline static int dummy_f__fc_inline(void)
+__inline static __attribute__((__noreturn__)) int dummy_f__fc_inline
+(void)
{
int __retres;
while (1) ;
--
GitLab