From 3f4d866dccd81db96ee34348588426b48ff7c89c Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Thu, 28 Sep 2023 10:52:37 +0200
Subject: [PATCH] Rename Ast_info function to be less misleading
---
src/kernel_internals/runtime/special_hooks.ml | 2 +-
src/kernel_internals/typing/ghost_accesses.ml | 2 +-
src/kernel_services/ast_queries/ast_info.ml | 32 +++++++--------
src/kernel_services/ast_queries/ast_info.mli | 40 ++++++++++++++++---
src/kernel_services/ast_queries/filecheck.ml | 2 +-
src/plugins/eva/engine/function_calls.ml | 2 +-
src/plugins/eva/engine/transfer_stmt.ml | 12 +++---
.../eva/partitioning/auto_loop_unroll.ml | 2 +-
src/plugins/from/from_compute.ml | 2 +-
src/plugins/gui/property_navigator.ml | 2 +-
src/plugins/metrics/metrics_base.ml | 2 +-
src/plugins/report/scan.ml | 2 +-
src/plugins/rte/visit.ml | 2 +-
src/plugins/server/kernel_ast.ml | 2 +-
src/plugins/server/kernel_properties.ml | 2 +-
src/plugins/variadic/classify.ml | 2 +-
16 files changed, 69 insertions(+), 41 deletions(-)
diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index 96deb0afdae..9c4ebad6173 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -277,7 +277,7 @@ let warn_if_another_compiler_builtin name =
depends on Ast_info *)
let on_call_to_undeclared_function vi =
let name = vi.Cil_types.vname in
- if not (Ast_info.is_frama_c_builtin name) then begin
+ if not (Ast_info.start_with_frama_c_builtin name) then begin
if not (warn_if_another_compiler_builtin name) then
Kernel.warning ~wkey:Kernel.wkey_implicit_function_declaration
~current:true ~once:true
diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index aba019286b2..6f159f16bb6 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -173,7 +173,7 @@ class visitor = object(self)
Error.assigns_non_ghost_lvalue ~current:true lv
in
let is_builtin vi =
- Ast_info.is_frama_c_builtin vi.vname ||
+ Ast_info.start_with_frama_c_builtin vi.vname ||
Cil_builtins.is_builtin vi
in
let failed = match i with
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index 5030a6d76bd..5c49b7a5470 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -465,33 +465,33 @@ let pointed_type ty =
(** {2 Predefined} *)
(* ************************************************************************** *)
-let can_be_cea_function name =
- String.starts_with ~prefix:"Frama_" name
+let start_with_frama_c name =
+ String.starts_with ~prefix:"Frama_C_" name
-let is_cea_function name =
+let is_show_each_builtin name =
String.starts_with ~prefix:"Frama_C_show_each" name
-let is_cea_domain_function name =
+let is_domain_show_each_builtin name =
String.starts_with ~prefix:"Frama_C_domain_show_each" name
-let is_cea_dump_function name =
+let is_dump_each_builtin name =
String.starts_with ~prefix:"Frama_C_dump_each" name
-let is_cea_dump_file_function name =
+let is_dump_file_builtin name =
String.starts_with ~prefix:"Frama_C_dump_each_file" name
-let is_cea_builtin name =
- String.starts_with ~prefix:"Frama_C_builtin" name
+let is_split_builtin name =
+ String.starts_with ~prefix:"Frama_C_builtin_split" name
-let is_frama_c_builtin n =
- can_be_cea_function n &&
- (is_cea_dump_function n ||
- is_cea_function n ||
- is_cea_builtin n ||
- is_cea_domain_function n ||
- is_cea_dump_file_function n)
+let start_with_frama_c_builtin n =
+ start_with_frama_c n &&
+ (is_dump_each_builtin n ||
+ is_show_each_builtin n ||
+ is_split_builtin n ||
+ is_domain_show_each_builtin n ||
+ is_dump_file_builtin n)
-let () = Cil_builtins.add_special_builtin_family is_frama_c_builtin
+let () = Cil_builtins.add_special_builtin_family start_with_frama_c_builtin
(*
Local Variables:
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index b068cb7fac8..f1284573e29 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -240,12 +240,40 @@ end
(** {2 Predefined} *)
(* ************************************************************************** *)
-val can_be_cea_function : string -> bool
-val is_cea_function : string -> bool
-val is_cea_domain_function : string -> bool
-val is_cea_dump_function : string -> bool
-val is_cea_dump_file_function : string -> bool
-val is_frama_c_builtin : string -> bool
+val start_with_frama_c: string -> bool
+(** @return true if the given string starts with ["Frama_C_"].
+ @since Frama-C+dev
+*)
+
+val is_show_each_builtin: string -> bool
+(** @return true if the given string starts with ["Frama_C_show_each"].
+ @since Frama-C+dev
+*)
+
+val is_domain_show_each_builtin: string -> bool
+(** @return true if the given string starts with ["Frama_C_domain_show_each"].
+ @since Frama-C+dev
+*)
+
+val is_dump_each_builtin: string -> bool
+(** @return true if the given string starts with ["Frama_C_dump_each"].
+ @since Frama-C+dev
+*)
+
+val is_dump_file_builtin: string -> bool
+(** @return true if the given string starts with ["Frama_C_dump_each_file"].
+ @since Frama-C+dev
+*)
+
+val is_split_builtin: string -> bool
+(** @return true if the given string starts with ["Frama_C_builtin_split"].
+ @since Frama-C+dev
+*)
+
+val start_with_frama_c_builtin: string -> bool
+(** @return true if the given string starts with ["Frama_C_"].
+ @since Frama-C+dev
+*)
(*
Local Variables:
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 262a40268e8..891a2394b19 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -177,7 +177,7 @@ module Base_checker = struct
let unknown () =
check_abort "variable %s(%d) is not declared" v.vname v.vid
in
- if not v.vglob || not (Ast_info.is_frama_c_builtin v.vname) then
+ if not v.vglob || not (Ast_info.start_with_frama_c_builtin v.vname) then
(try
if Varinfo.Hashtbl.find known_vars v != v then not_shared ()
with Not_found -> unknown ()
diff --git a/src/plugins/eva/engine/function_calls.ml b/src/plugins/eva/engine/function_calls.ml
index ee88bbdc585..5b8cd029a76 100644
--- a/src/plugins/eva/engine/function_calls.ml
+++ b/src/plugins/eva/engine/function_calls.ml
@@ -146,7 +146,7 @@ let analysis_status kf =
(* Must be consistent with the choice made by [analysis_target] below. *)
let use_spec_instead_of_definition ?(recursion_depth = -1) kf =
- Ast_info.is_frama_c_builtin (Kernel_function.get_name kf) ||
+ Ast_info.start_with_frama_c_builtin (Kernel_function.get_name kf) ||
Builtins.is_builtin_overridden kf ||
recursion_depth >= Parameters.RecursiveUnroll.get () ||
not (Kernel_function.is_definition kf) ||
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 1bb0994dc6e..34a7b67ef1f 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -85,7 +85,7 @@ let do_copy_at = function
let is_determinate kf =
let name = Kernel_function.get_name kf in
(warn_indeterminate kf || Function_calls.use_spec_instead_of_definition kf)
- && not (Ast_info.is_frama_c_builtin name)
+ && not (Ast_info.start_with_frama_c_builtin name)
let subdivide_stmt = Eva_utils.get_subdivision
@@ -708,15 +708,15 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(** Applies the show_each or dump_each directives. *)
let apply_special_directives ~subdivnb kf arguments state =
let name = Kernel_function.get_name kf in
- if Ast_info.can_be_cea_function name
+ if Ast_info.start_with_frama_c name
then
- if Ast_info.is_cea_function name
+ if Ast_info.is_show_each_builtin name
then (show_each ~subdivnb name arguments state; true)
- else if Ast_info.is_cea_domain_function name
+ else if Ast_info.is_domain_show_each_builtin name
then (domain_show_each ~subdivnb name arguments state; true)
- else if Ast_info.is_cea_dump_file_function name
+ else if Ast_info.is_dump_file_builtin name
then (dump_state_file ~subdivnb name arguments state; true)
- else if Ast_info.is_cea_dump_function name
+ else if Ast_info.is_dump_each_builtin name
then (dump_state name state; true)
else false
else false
diff --git a/src/plugins/eva/partitioning/auto_loop_unroll.ml b/src/plugins/eva/partitioning/auto_loop_unroll.ml
index 58b52807752..fca0c44ebc0 100644
--- a/src/plugins/eva/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/eva/partitioning/auto_loop_unroll.ml
@@ -177,7 +177,7 @@ let add_written_var vi effect =
let is_frama_c_builtin exp =
match exp.enode with
- | Lval (Var vi, NoOffset) -> Ast_info.is_frama_c_builtin vi.vname
+ | Lval (Var vi, NoOffset) -> Ast_info.start_with_frama_c_builtin vi.vname
| _ -> false
let compute_instr_effect effect = function
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 4060d0d5183..4c662872580 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -346,7 +346,7 @@ struct
let states_with_formals = ref [] in
let do_on kf =
let called_vinfo = Kernel_function.get_vi kf in
- if Ast_info.is_frama_c_builtin called_vinfo.vname then
+ if Ast_info.start_with_frama_c_builtin called_vinfo.vname then
state
else
let froms_call = To_Use.get_from_call kf stmt in
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index 3f874465f59..a873fdbf6f8 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -43,7 +43,7 @@ let all_properties () =
match Property.get_kf ip with
| None -> globals := Property.Set.add ip !globals
| Some kf ->
- if not (Ast_info.is_frama_c_builtin (Kernel_function.get_name kf))
+ if not (Ast_info.start_with_frama_c_builtin (Kernel_function.get_name kf))
then try
let fips = Kernel_function.Map.find kf !functions in
fips := Property.Set.add ip !fips
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index b20821d6b8d..777bce0fd9b 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -367,7 +367,7 @@ let get_filename fdef =
let consider_function ~libc vinfo =
not (Eva.Builtins.is_builtin vinfo.vname
- || Ast_info.is_frama_c_builtin vinfo.vname
+ || Ast_info.start_with_frama_c_builtin vinfo.vname
|| Cil_builtins.is_unused_builtin vinfo
) && (libc || not (Cil.is_in_libc vinfo.vattr))
diff --git a/src/plugins/report/scan.ml b/src/plugins/report/scan.ml
index 522d3376ddd..e7c28026e6a 100644
--- a/src/plugins/report/scan.ml
+++ b/src/plugins/report/scan.ml
@@ -126,7 +126,7 @@ let iter (inspector:inspector) =
match Property.get_kf ip with
| None -> globals := Property.Set.add ip !globals
| Some kf ->
- if not (Ast_info.is_frama_c_builtin (Kernel_function.get_name kf))
+ if not (Ast_info.start_with_frama_c_builtin (Kernel_function.get_name kf))
then try
let fips = Kernel_function.Map.find kf !functions in
fips := Property.Set.add ip !fips
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 02f8d10d536..c92bf683b58 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -170,7 +170,7 @@ class annot_visitor kf flags on_alarm = object (self)
match funcexp.enode with
| Lval (Var vinfo, NoOffset) ->
let kf = Globals.Functions.get vinfo in
- let frama_b = Ast_info.is_frama_c_builtin (Kernel_function.get_name kf)
+ let frama_b = Ast_info.start_with_frama_c_builtin (Kernel_function.get_name kf)
in
let va_start = Kernel_function.get_name kf = "__builtin_va_start" in
(frama_b, va_start)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 46a17d9e142..0128d7e8bbe 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -618,7 +618,7 @@ struct
Globals.Functions.iter
(fun kf ->
let name = Kernel_function.get_name kf in
- if not (Ast_info.is_frama_c_builtin name) then f kf)
+ if not (Ast_info.start_with_frama_c_builtin name) then f kf)
let array : kernel_function States.array =
begin
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 57d3d0305f4..b7e821e4906 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -308,7 +308,7 @@ let is_relevant ip =
match Property.get_kf ip with
| None -> true
| Some kf ->
- not (Ast_info.is_frama_c_builtin (Kernel_function.get_name kf)
+ not (Ast_info.start_with_frama_c_builtin (Kernel_function.get_name kf)
|| Cil_builtins.is_unused_builtin (Kernel_function.get_vi kf))
let iter f =
diff --git a/src/plugins/variadic/classify.ml b/src/plugins/variadic/classify.ml
index 32d4c8c2c36..7717ee90837 100644
--- a/src/plugins/variadic/classify.ml
+++ b/src/plugins/variadic/classify.ml
@@ -111,7 +111,7 @@ let mk_format_fun vi f_kind f_buffer ~format_pos =
(* ************************************************************************ *)
let is_frama_c_builtin name =
- Ast_info.is_frama_c_builtin name ||
+ Ast_info.start_with_frama_c_builtin name ||
Cil_builtins.Builtin_functions.mem name ||
String.starts_with ~prefix:"__FRAMAC_" name (* Mthread prefixes *)
--
GitLab