From 5ce7907b44158615ec54e3aec9af8f043e2cb9f2 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 3 May 2023 18:31:41 +0200
Subject: [PATCH] [kernel] pointer_comparable needs a logic label
As specified in ACSL following #1248
---
src/kernel_internals/typing/logic_builtin.ml | 17 +++++++++--------
src/kernel_services/ast_queries/logic_utils.ml | 4 ++--
src/kernel_services/ast_queries/logic_utils.mli | 9 ++++++---
3 files changed, 17 insertions(+), 13 deletions(-)
diff --git a/src/kernel_internals/typing/logic_builtin.ml b/src/kernel_internals/typing/logic_builtin.ml
index 629040d5995..03c45e5023e 100644
--- a/src/kernel_internals/typing/logic_builtin.ml
+++ b/src/kernel_internals/typing/logic_builtin.ml
@@ -118,6 +118,7 @@ let init =
(fun c -> Logic_env.add_builtin_logic_ctor c.ctor_name c) ctors ;
list.lt_def <- Some (LTsum ctors);
let _list_of_integer = Ltype (list, [Linteger]) in
+ let l_label = FormalLabel "L" in
(* predicates *)
List.iter
(fun (f,tparams,labels,params) ->
@@ -154,14 +155,14 @@ let init =
"\\no_overflow_double", [], [], ["m", rounding_mode; "x", Lreal] ;
"\\subset", [a_name], [], ["s1", set_of_a_type;
"s2", set_of_a_type];
- "\\pointer_comparable", [], [], [("p1", object_ptr);
- ("p2", object_ptr)];
- "\\pointer_comparable", [], [], [("p1", fun_ptr);
- ("p2", fun_ptr)];
- "\\pointer_comparable", [], [], [("p1", fun_ptr);
- ("p2", object_ptr)];
- "\\pointer_comparable", [], [], [("p1", object_ptr);
- ("p2", fun_ptr)];
+ "\\pointer_comparable", [], [l_label], [("p1", object_ptr);
+ ("p2", object_ptr)];
+ "\\pointer_comparable", [], [l_label], [("p1", fun_ptr);
+ ("p2", fun_ptr)];
+ "\\pointer_comparable", [], [l_label], [("p1", fun_ptr);
+ ("p2", object_ptr)];
+ "\\pointer_comparable", [], [l_label], [("p1", object_ptr);
+ ("p2", fun_ptr)];
];
(* functions *)
List.iter
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 0af75114af3..02ed9f21ad4 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -2362,7 +2362,7 @@ class complete_types =
let complete_types f = Cil.visitCilFile (new complete_types) f
-let pointer_comparable ?loc t1 t2 =
+let pointer_comparable ?loc ?(label=Logic_const.here_label) t1 t2 =
let preds = Logic_env.find_all_logic_functions "\\pointer_comparable" in
let cfct_ptr = TPtr (TFun(Cil.voidType,None,false,[]),[]) in
let fct_ptr = Ctype cfct_ptr in
@@ -2404,7 +2404,7 @@ let pointer_comparable ?loc t1 t2 =
with Not_found ->
Kernel.fatal "built-in predicate \\pointer_comparable not found"
in
- Logic_const.unamed ?loc (Papp (pi, [], [t1;t2]))
+ Logic_const.unamed ?loc (Papp (pi, [label], [t1;t2]))
let is_min_max_function name li =
li.l_var_info.lv_name = name &&
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index 1e94484c56d..25113344618 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -146,9 +146,12 @@ val numeric_coerce: logic_type -> term -> term
(** \valid_range *)
(* val mk_pvalid_range: ?loc:location -> term * term * term -> predicate *)
-val pointer_comparable: ?loc:location -> term -> term -> predicate
-(** \pointer_comparable
- @since Fluorine-20130401 *)
+val pointer_comparable:
+ ?loc:location -> ?label:logic_label -> term -> term -> predicate
+(** \pointer_comparable. [label] defaults to {!Logic_const.here_label}
+ @since Fluorine-20130401
+ @before Frama-C+dev no [label] argument, as the builtin did not take a label
+*)
(** {2 Conversion from exp to term} *)
--
GitLab