diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index d44f3bb9ea54dbf0153727996a3a36205037c67f..ba758303dcf7e02f537d5216ac9a3a9fb09b0edf 100644
--- a/src/kernel_internals/typing/populate_spec.ml
+++ b/src/kernel_internals/typing/populate_spec.ml
@@ -653,6 +653,8 @@ end
 (* |-------|------|-------|------|-------|------|-------|------| *)
 (* | true  | true | ACSL  | ACSL | false | true |  ???  |  ??  | *)
 (* |-----------------------------------------------------------| *)
+(* Note: Terminates are set to false in ACSL, Frama-C and Safe   *)
+(* modes if the function has the attribute noreturn.             *)
 (* ***************************************************************)
 (* ****** Status emitted on prototypes ******)
 (* |--------------------------------------| *)
@@ -679,13 +681,16 @@ struct
 
   let get_clauses _spec _table = None
 
-  let acsl_default _kf =
-    Some(Logic_const.(new_predicate ptrue))
+  let acsl_default kf =
+    if Kernel_function.has_noreturn_attr kf then
+      Some(Logic_const.(new_predicate pfalse))
+    else
+      Some(Logic_const.(new_predicate ptrue))
 
   let safe_default kf =
-    if Kernel_function.has_definition kf
-    then Some(Logic_const.(new_predicate ptrue))
-    else Some(Logic_const.(new_predicate pfalse))
+    if Kernel_function.has_noreturn_attr kf || not (Kernel_function.has_definition kf) then
+      Some(Logic_const.(new_predicate pfalse))
+    else Some(Logic_const.(new_predicate ptrue))
 
   let frama_c_default kf =
     acsl_default kf
diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index cf77f0439392beb1154edd9001b49c8df132b91b..d2b9e4638a32384ee7e8242c2a69a219e930ebb8 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -567,6 +567,12 @@ let is_in_libc kf =
     | Declaration (_, { vattr }, _, _) -> vattr
   in Cil.is_in_libc attrs
 
+let has_noreturn_attr kf =
+  match kf.fundec with
+  | Definition ({ svar = { vattr } },_)
+  | Declaration (_, { vattr }, _, _) ->
+    Cil.hasAttribute "noreturn" vattr
+
 let is_first_stmt kf stmt =
   try
     let first = find_first_stmt kf in
diff --git a/src/kernel_services/ast_data/kernel_function.mli b/src/kernel_services/ast_data/kernel_function.mli
index c7017e3421b8ad57fea641653be18d3564220930..0fd0d34b4713721a2a06a6e642eba4b64e6abc28 100644
--- a/src/kernel_services/ast_data/kernel_function.mli
+++ b/src/kernel_services/ast_data/kernel_function.mli
@@ -182,6 +182,10 @@ val is_in_libc : t -> bool
 (** @return true iff the given function attributes contain libc indicators.
     @since 24.0-Chromium *)
 
+val has_noreturn_attr : t -> bool
+(** @return true iff the given function contain the noreturn attribute.
+    @since Frama-C+dev *)
+
 val is_not_called: t -> bool
 (** @return true if the given function is not called in the program.
     Warning, return false does not ensure that the function is called.
diff --git a/tests/spec/default_spec_mode.i b/tests/spec/default_spec_mode.i
index 87586463611990f2a8e6f6da4f623d4b8279f821..4863e6d481c15d23e3bfb244d4171b1be184821c 100644
--- a/tests/spec/default_spec_mode.i
+++ b/tests/spec/default_spec_mode.i
@@ -30,3 +30,9 @@ int f3(int* a);
 int f4(int* b){
   return f3(b);
 }
+
+__attribute__((__noreturn__)) void f5();
+
+void f5(){
+  while(1);
+}
diff --git a/tests/spec/oracle/default_spec_mode.0.res.oracle b/tests/spec/oracle/default_spec_mode.0.res.oracle
index 78fff7dc521e9b55b651f06401a9629fd669497d..06e27d95b3448c17ac6bd3e2344a9d49ee68897d 100644
--- a/tests/spec/oracle/default_spec_mode.0.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.0.res.oracle
@@ -51,4 +51,16 @@ int f4(int *b)
   return tmp;
 }
 
+ __attribute__((__noreturn__)) void f5(void);
+
+/*@ terminates \false;
+    exits \false;
+    allocates \nothing; */
+ __attribute__((__noreturn__)) void f5(void);
+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 85761c8d8bbbb1d2922643f3bd4b37af08e44c00..28bd6a55879c1d62314ef0f7a5f9abe749454cf6 100644
--- a/tests/spec/oracle/default_spec_mode.1.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.1.res.oracle
@@ -40,4 +40,17 @@ int f4(int *b)
   return tmp;
 }
 
+ __attribute__((__noreturn__)) void f5(void);
+
+/*@ terminates \false;
+    exits \false;
+    assigns \nothing;
+    allocates \nothing; */
+ __attribute__((__noreturn__)) void f5(void);
+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 1e6e902f9357867d48dcf93252318547e1d5b75f..a4e0f835c66729e68a1abcef6d843425dc2ec583 100644
--- a/tests/spec/oracle/default_spec_mode.2.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.2.res.oracle
@@ -63,4 +63,17 @@ int f4(int *b)
   return tmp;
 }
 
+ __attribute__((__noreturn__)) void f5(void);
+
+/*@ terminates \false;
+    exits \false;
+    assigns \nothing;
+    allocates \nothing; */
+ __attribute__((__noreturn__)) void f5(void);
+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 9dbaf0735f618c9a503619b4c408d748b3d08615..e1e0f73f9270034131131f5f7ae756e8efd2c9f7 100644
--- a/tests/spec/oracle/default_spec_mode.3.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.3.res.oracle
@@ -65,4 +65,17 @@ int f4(int *b)
   return tmp;
 }
 
+ __attribute__((__noreturn__)) void f5(void);
+
+/*@ terminates \false;
+    exits \false;
+    assigns \nothing;
+    allocates \nothing; */
+ __attribute__((__noreturn__)) void f5(void);
+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 ec63e420cacbf9b4253d6632a1e10ad991321f50..b2591584562925cd8465bd70b86352c20614a251 100644
--- a/tests/spec/oracle/default_spec_mode.4.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.4.res.oracle
@@ -48,4 +48,16 @@ int f4(int *b)
   return tmp;
 }
 
+ __attribute__((__noreturn__)) void f5(void);
+
+/*@ terminates \false;
+    assigns \nothing;
+    allocates \nothing; */
+ __attribute__((__noreturn__)) void f5(void);
+void f5(void)
+{
+  while (1) ;
+  return;
+}
+