From 81c535acb5d7676421bb3cef41a6f3f2fafcdbd4 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 28 Sep 2023 11:06:51 +0200
Subject: [PATCH] Create Cil_builtins.is_builtin : checks for frama_c and
special builtins
---
src/kernel_services/ast_queries/cil_builtins.ml | 3 +++
src/kernel_services/ast_queries/cil_builtins.mli | 9 +++++++--
src/plugins/eva/utils/summary.ml | 4 +---
src/plugins/obfuscator/obfuscate.ml | 3 +--
4 files changed, 12 insertions(+), 7 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index dd19bebde39..c80b32e7484 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -68,6 +68,9 @@ let special_builtins = Queue.create ()
let is_special_builtin s =
Queue.fold (fun res f -> res || f s) false special_builtins
+let is_builtin v =
+ has_fc_builtin_attr v || is_special_builtin v.vname
+
let add_special_builtin_family f = Queue.add f special_builtins
let add_special_builtin s =
diff --git a/src/kernel_services/ast_queries/cil_builtins.mli b/src/kernel_services/ast_queries/cil_builtins.mli
index 270cfd97d9e..c37b7e41c86 100644
--- a/src/kernel_services/ast_queries/cil_builtins.mli
+++ b/src/kernel_services/ast_queries/cil_builtins.mli
@@ -56,10 +56,15 @@ open Cil_types
module Frama_c_builtins:
State_builder.Hashtbl with type key = string and type data = varinfo
-val is_frama_c_builtin: varinfo -> bool
-(** @return true if the given variable refers to a Frama-C builtin.
+val is_builtin: varinfo -> bool
+(** @return true if {!has_fc_builtin_attr} or {!is_special_builtin} are true.
+ @before Frama-C+dev Only check for {!has_fc_builtin_attr}.
@since Fluorine-20130401 *)
+val has_fc_builtin_attr: varinfo -> bool
+(** @return true if the given variable refers to a Frama-C builtin.
+ @since Frama-C+dev *)
+
val is_unused_builtin: varinfo -> bool
(** @return true if the given variable refers to a Frama-C builtin that
is not used in the current program. Plugins may (and in fact should)
diff --git a/src/plugins/eva/utils/summary.ml b/src/plugins/eva/utils/summary.ml
index 84d99db49cb..6982ec1bfee 100644
--- a/src/plugins/eva/utils/summary.ml
+++ b/src/plugins/eva/utils/summary.ml
@@ -225,9 +225,7 @@ end
let consider_function vi =
vi.Cil_types.vdefined &&
- not (Cil_builtins.has_fc_builtin_attr vi
- || Cil_builtins.is_special_builtin vi.vname
- || Cil.is_in_libc vi.vattr)
+ not (Cil_builtins.is_builtin vi || Cil.is_in_libc vi.vattr)
let compute_events () =
let eva = Events.make () and kernel = Events.make () in
diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml
index e497fb82648..fba8a49e215 100644
--- a/src/plugins/obfuscator/obfuscate.ml
+++ b/src/plugins/obfuscator/obfuscate.ml
@@ -101,8 +101,7 @@ class visitor = object
else begin
if Cil.isFunctionType vi.vtype then begin
if vi.vname <> "main"
- && not (Cil_builtins.has_fc_builtin_attr vi)
- && not (Cil_builtins.is_special_builtin vi.vname)
+ && not (Cil_builtins.is_builtin vi)
&& not (Cil.is_in_libc vi.vattr) then
vi.vname <- Dictionary.fresh Obfuscator_kind.Function vi.vname
end
--
GitLab