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 f3b8d9158f23ce63b2b85f12d6f53703f6ddec79..a235f02b21d675b3f6fdc259092829b4b98cbcea 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 58862fef58937dbf5328350046f9e835f5142be9..22861bb8b860502478a963a058939debbb3fe233 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 72d8735dd4ac5ada3917fd9c83cc0d36d932e785..9c38744e026b52389077dae64f7fe875e17a8dd0 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 4aefe12825df4a78123395e03c8b5f25002e56eb..fbde72d4e6bb3694690b2025904cbcf9a5e49a5f 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 a73f89d3e51b69b8b0ed5a264d31391af19baff4..b6071854f7cf43a8065d7089c354f472a5c06b07 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 7583e2dc85f677bd3a25857ec814ec92e0d3f613..2a778a1f8cc1164a0cc0c7124dd2b8fc723976a8 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 8aa685ba92e18af0bf58a72afac4562571263bde..ed7d5351a40d9b0e83800814275cc156bb380ccf 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 fed7aed3b602e54e12c844e3bc599200bb7375d3..0fd82086aff53183bb5c5a2f320a2fb4a147469d 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 88b5d0e312385b2f4afe6fa2ea4222bb85bbd803..67ee1541e1c7d78632fa1889de24a777df5c24b3 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 0000000000000000000000000000000000000000..d1e5b586f5f39756c3a29da7168fb3703ff1c5ff
--- /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 0000000000000000000000000000000000000000..365d5165e0af77831dcea9c5551f89b912473fbe
--- /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 06e27d95b3448c17ac6bd3e2344a9d49ee68897d..b3e13b9e5d89582d933fd1ae0127ac058577f079 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 28bd6a55879c1d62314ef0f7a5f9abe749454cf6..7668bbc5033fcfc662d9bcde65198dcecf365055 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 a4e0f835c66729e68a1abcef6d843425dc2ec583..b403960922c45df81a872e0f22e4b016b6af6ae9 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 e1e0f73f9270034131131f5f7ae756e8efd2c9f7..b6067af62b3e8e49e5454106c88617e5f87cd37b 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 b2591584562925cd8465bd70b86352c20614a251..0822b20709abffb37eac518289366ce12b720f29 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 c763be7e968b1a58dd56d638d1819526083f6002..5b247f48b47141bf909d042d90b8c4f839d53a60 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) ;