Merge branch 'fix/acsl/typing-functions-sets' into 'master'

Fix/acsl/typing functions sets

See merge request frama-c/frama-c!2482

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)

tests/spec/logic_functions_sets.i

+/* 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 } ;
+*/

tests/spec/logic_functions_sets.ml

+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

tests/spec/oracle/logic_functions_sets.res.oracle

+[kernel] Parsing tests/spec/logic_functions_sets.i (no preprocessing)