From dd7e4c6ba5f67c04169ec196e9649307ff773315 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 28 Sep 2023 11:23:41 +0200
Subject: [PATCH] Add is_frama_c_builtin: checks FC attr and start_with_Frama_C
---
src/kernel_internals/typing/ghost_accesses.ml | 12 ++++--------
src/kernel_services/ast_queries/ast_info.ml | 3 +++
src/kernel_services/ast_queries/ast_info.mli | 6 ++++++
3 files changed, 13 insertions(+), 8 deletions(-)
diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index c125b5be59e..3d017490d7d 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -172,22 +172,18 @@ class visitor = object(self)
if not (isGhostType (typeOfLval lv)) then
Error.assigns_non_ghost_lvalue ~current:true lv
in
- let is_builtin vi =
- Ast_info.start_with_frama_c_builtin vi.vname ||
- Cil_builtins.has_fc_builtin_attr vi
- in
let failed = match i with
| Call(_, fexp, _, _) ->
begin match Kernel_function.(Option.map get_vi @@ get_called fexp) with
| Some fct
- when not (is_builtin fct) && not fct.vghost ->
+ when not (Ast_info.is_frama_c_builtin fct) && not fct.vghost ->
Error.non_ghost_function_call_in_ghost ~current:true () ; true
| None ->
Error.function_pointer_call ~current:true () ; true
| _ -> false
end
| Local_init(_, ConsInit(fct, _, _), _)
- when not (is_builtin fct) && not fct.vghost ->
+ when not (Ast_info.is_frama_c_builtin fct) && not fct.vghost ->
Error.non_ghost_function_call_in_ghost ~current:true () ; true
| _ -> false
in
@@ -200,10 +196,10 @@ class visitor = object(self)
| Call(_, fexp, _, _) ->
let vi =
Kernel_function.(get_vi @@ Option.get @@ get_called fexp) in
- if not (is_builtin vi) then
+ if not (Ast_info.is_frama_c_builtin vi) then
error_if_incompatible lv (getReturnType (typeOf fexp)) fexp
| Local_init(_, ConsInit(fct, _, _), _) ->
- if not (is_builtin fct) then
+ if not (Ast_info.is_frama_c_builtin fct) then
error_if_incompatible lv (getReturnType fct.vtype) (evar fct)
| _ -> ()
end
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index 5c49b7a5470..794763d3e27 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -491,6 +491,9 @@ let start_with_frama_c_builtin n =
is_domain_show_each_builtin n ||
is_dump_file_builtin n)
+let is_frama_c_builtin v =
+ Cil_builtins.has_fc_builtin_attr v || start_with_frama_c_builtin v.vname
+
let () = Cil_builtins.add_special_builtin_family start_with_frama_c_builtin
(*
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index f1284573e29..771f071232a 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -275,6 +275,12 @@ val start_with_frama_c_builtin: string -> bool
@since Frama-C+dev
*)
+val is_frama_c_builtin: varinfo -> bool
+(** @return true if {!start_with_frama_c_builtin} or
+ {!Cil_builtins.has_fc_builtin_attr} are true.
+ @before Frama-C+dev Behave like {!start_with_frama_c_builtin}.
+*)
+
(*
Local Variables:
compile-command: "make -C ../../.."
--
GitLab