From 45096eb38f75203a910f65f979c1e7020d0634cb Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 18 Dec 2019 09:53:34 +0100
Subject: [PATCH] Fix/acsl/typing functions sets
---
src/kernel_services/ast_queries/logic_typing.ml | 8 +++++++-
tests/spec/logic_functions_sets.i | 11 +++++++++++
tests/spec/logic_functions_sets.ml | 16 ++++++++++++++++
.../spec/oracle/logic_functions_sets.res.oracle | 1 +
4 files changed, 35 insertions(+), 1 deletion(-)
create mode 100644 tests/spec/logic_functions_sets.i
create mode 100644 tests/spec/logic_functions_sets.ml
create mode 100644 tests/spec/oracle/logic_functions_sets.res.oracle
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 9a4e7782568..8a4be465d70 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1447,7 +1447,13 @@ struct
Ltype(t1,l),oterm
| t1, Ltype ({lt_name = "set"},[t2]) ->
let typ, term = implicit_conversion ~overloaded loc oterm t1 t2 in
- make_set_type typ, term
+ let stype = make_set_type typ in
+ let term =
+ if not (Logic_const.is_set_type term.term_type) then
+ Logic_const.tlogic_coerce ~loc:term.term_loc term stype
+ else term
+ in
+ stype, term
| Linteger, Linteger | Lreal, Lreal -> ot, oterm
| Lvar s1, Lvar s2 when s1 = s2 -> ot, oterm
| Larrow(args1,rt1), Larrow(args2,rt2)
diff --git a/tests/spec/logic_functions_sets.i b/tests/spec/logic_functions_sets.i
new file mode 100644
index 00000000000..60190e8cc24
--- /dev/null
+++ b/tests/spec/logic_functions_sets.i
@@ -0,0 +1,11 @@
+/* run.config
+ MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -no-autoload-plugins
+*/
+
+/*@
+ logic set<integer> constant_1(integer n) = 1 ;
+ logic set<integer> constant_2(integer n) = { 1 } ;
+ logic set<integer> with_sub_1(integer n) = (n < 0) ? 1 : 2 ;
+ logic set<integer> with_sub_2(integer n) = (n < 0) ? 1 : { 2 } ;
+*/
diff --git a/tests/spec/logic_functions_sets.ml b/tests/spec/logic_functions_sets.ml
new file mode 100644
index 00000000000..0eb5f933fd7
--- /dev/null
+++ b/tests/spec/logic_functions_sets.ml
@@ -0,0 +1,16 @@
+open Cil_types
+
+let check = function
+ | Dfun_or_pred (li, _) ->
+ let decl_type = Extlib.the li.l_type in
+ let body_type = match li.l_body with
+ | LBterm t -> t.term_type
+ | _ -> assert false
+ in
+ if 0 <> Cil_datatype.Logic_type.compare decl_type body_type then begin
+ Kernel.failure "Bad type for: %a" Cil_datatype.Logic_info.pretty li
+ end
+ | _ -> ()
+
+let () =
+ Db.Main.extend (fun () -> Annotations.iter_global (fun _ g -> check g))
\ No newline at end of file
diff --git a/tests/spec/oracle/logic_functions_sets.res.oracle b/tests/spec/oracle/logic_functions_sets.res.oracle
new file mode 100644
index 00000000000..d15532848e8
--- /dev/null
+++ b/tests/spec/oracle/logic_functions_sets.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/spec/logic_functions_sets.i (no preprocessing)
--
GitLab