From 4b98e87fe061e6d1e919e3f6cb9d7734cda5c62f Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 4 Jul 2024 14:34:15 +0200
Subject: [PATCH] [kernel] Generate terminates \false when noreturn attr
---
src/kernel_internals/typing/populate_spec.ml | 15 ++++++++++-----
src/kernel_services/ast_data/kernel_function.ml | 6 ++++++
src/kernel_services/ast_data/kernel_function.mli | 4 ++++
tests/spec/default_spec_mode.i | 6 ++++++
tests/spec/oracle/default_spec_mode.0.res.oracle | 12 ++++++++++++
tests/spec/oracle/default_spec_mode.1.res.oracle | 13 +++++++++++++
tests/spec/oracle/default_spec_mode.2.res.oracle | 13 +++++++++++++
tests/spec/oracle/default_spec_mode.3.res.oracle | 13 +++++++++++++
tests/spec/oracle/default_spec_mode.4.res.oracle | 12 ++++++++++++
9 files changed, 89 insertions(+), 5 deletions(-)
diff --git a/src/kernel_internals/typing/populate_spec.ml b/src/kernel_internals/typing/populate_spec.ml
index d44f3bb9ea5..ba758303dcf 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 cf77f043939..d2b9e4638a3 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 c7017e3421b..0fd0d34b471 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 87586463611..4863e6d481c 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 78fff7dc521..06e27d95b34 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 85761c8d8bb..28bd6a55879 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 1e6e902f935..a4e0f835c66 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 9dbaf0735f6..e1e0f73f927 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 ec63e420cac..b2591584562 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;
+}
+
--
GitLab