diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index 8330edfe5e0c254f444498a1b506f6a860e161df..a123a753dd6b66055de9eabb656c8bd4ff07472c 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -202,7 +202,7 @@ class visitor = object(self)
error_if_incompatible lv (getReturnType fct.vtype) (evar fct)
| _ -> ()
end
- (* Note that we do not check "assigns" for a ghost function call has
+ (* Note that we do not check "assigns" for a ghost function call since
the method vglob_aux and vassigns requires ghost functions to have
either a contract or a definition.
Thus, if the casts in input are valid:
diff --git a/src/kernel_services/ast_data/kernel_function.ml b/src/kernel_services/ast_data/kernel_function.ml
index ec88837490f29c1a8de2b3d12c72e8bc50dad5e6..bc9017f7a08c6135c22fa01fbf9de0cc7ae2c2e7 100644
--- a/src/kernel_services/ast_data/kernel_function.ml
+++ b/src/kernel_services/ast_data/kernel_function.ml
@@ -76,6 +76,8 @@ let has_definition kf = match kf.fundec with
| Definition _ -> true
| Declaration _ -> false
+let is_ghost kf = (get_vi kf).vghost
+
(* ************************************************************************* *)
(** {2 Kernel functions are comparable} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/ast_data/kernel_function.mli b/src/kernel_services/ast_data/kernel_function.mli
index 0c954057a436afbac342fdb608cfb937cf405271..6c0f43f21885c29655969ce02d377623b53f4a70 100644
--- a/src/kernel_services/ast_data/kernel_function.mli
+++ b/src/kernel_services/ast_data/kernel_function.mli
@@ -213,9 +213,23 @@ val dummy: unit -> t
val get_vi : t -> varinfo
val get_id: t -> int
+(** @return the identifier of the function (which is the identifier of the
+ associated varinfo). *)
+
val get_name : t -> string
+
val get_type : t -> typ
+(** Be careful! The return type, as normalized by Cabs2Cil does not have any
+ qualifier at first level (e.g no ghost).
+ @return the type of the given kernel function
+*)
+
val get_return_type : t -> typ
+(** Be careful! The return type, as normalized by Cabs2Cil does not have any
+ qualifier at first level (e.g no ghost).
+ @return the return type of the function
+*)
+
val get_location: t -> Cil_types.location
val get_global : t -> global
(** For functions with a declaration and a definition, returns the definition.*)
@@ -236,6 +250,10 @@ val has_definition : t -> bool
(** @return [true] iff the given kernel function has a defintion.
@since 21.0-Scandium *)
+val is_ghost : t -> bool
+(** @return [true] iff the given kernel function is ghost
+ @since Frama-C+dev *)
+
(* ************************************************************************* *)
(** {2 Membership of variables} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 5e1397685e6239e0cca7c3a30ecf880ba7039462..2fdf4cdfb8459f70ffcc6da3f75418a8b6e4ac51 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1482,6 +1482,11 @@ val isWFGhostType : typ -> bool
@return true iff the type is well formed
@since 21.0-Scandium *)
+val typeAddGhost : typ -> typ
+(** Add the ghost attribute to a type (does nothing if the type is alreay ghost)
+ @return the ghost qualified original type
+ @since Frama-C+dev *)
+
(* ************************************************************************* *)
(** {2 The visitor} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 42996576ae75391881fca771af1ed42491192f57..8ce52066d869bc746224f636be65b84016dabd65 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -737,6 +737,10 @@ module Base_checker = struct
check_abort "\\result found outside of a function contract"
| Some kf ->
let t1 = Kernel_function.get_return_type kf in
+ let t1 =
+ if Kernel_function.is_ghost kf
+ then Cil.typeAddGhost t1 else t1
+ in
if Cil.isVoidType t1 then
check_abort
"\\result found in a contract for function %a that returns void"
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index ad5da768177477c5df00713c9a654c3231b3ddcf..4f9464ea5866754dfd36872f41ddda3775d91a19 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3765,7 +3765,10 @@ struct
let funspec old_behaviors vi formals typ s =
let env = append_pre_label (Lenv.funspec()) in
- let log_return_typ = Ctype (Cil.getReturnType typ) in
+ let typ = Cil.getReturnType typ in
+ (* Qualifiers are dropped on return type, recover ghost *)
+ let typ = if vi.vghost then Cil.typeAddGhost typ else typ in
+ let log_return_typ = Ctype typ in
let env =
match formals with
| None -> (* This is the spec of a function declaration *)
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 93c470161d88005c3f0c528537f4cc785ed273a4..edca90509034d05821aead93ad9e4f2114d195e5 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -495,11 +495,12 @@ let get_bhv_aux_fct kf bhv =
let assumes = Visitor.visitFramacPredicates vis bhv.b_assumes in
let assumes = List.map Logic_const.refresh_predicate assumes in
let assigns = Writes [] in
+ let ret_typ = Cil.typeAddGhost Cil.intType in
let post_cond =
[Normal,
Logic_const.(
new_predicate
- (prel (Req,tlogic_coerce (tresult Cil.intType) Linteger,lone())))]
+ (prel (Req,tlogic_coerce (tresult ret_typ) Linteger,lone())))]
in
let bhv_in =
Cil.mk_behavior ~name:bhv.b_name ~assumes ~assigns ~post_cond ()
@@ -515,7 +516,7 @@ let get_bhv_aux_fct kf bhv =
Logic_const.(
new_predicate
(prel
- (Req, tlogic_coerce (tresult Cil.intType) Linteger, lzero())))]
+ (Req, tlogic_coerce (tresult ret_typ) Linteger, lzero())))]
in
let bhv_out = Cil.mk_behavior ~name ~assumes ~assigns ~post_cond () in
Globals.Functions.replace_by_declaration (Cil.empty_funspec()) vi loc;
diff --git a/tests/spec/ghost_result_type.i b/tests/spec/ghost_result_type.i
new file mode 100644
index 0000000000000000000000000000000000000000..84ce3ad190cf5ffe9aa476f1c1002353e38ad02a
--- /dev/null
+++ b/tests/spec/ghost_result_type.i
@@ -0,0 +1,14 @@
+/*@ ghost
+ /@ assigns \result \from \nothing; @/
+ int *f(void);
+*/
+
+/*@ ghost
+ /@ assigns \result,*\result \from \nothing; @/
+ int \ghost * g(void);
+*/
+
+int main(void){
+ //@ ghost int* p = f() ;
+ //@ ghost int \ghost* q = g() ;
+}
diff --git a/tests/spec/oracle/ghost_result_type.res.oracle b/tests/spec/oracle/ghost_result_type.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0bd50ab54f799958f03378835fd64024b4f7ec26
--- /dev/null
+++ b/tests/spec/oracle/ghost_result_type.res.oracle
@@ -0,0 +1,23 @@
+[kernel] Parsing ghost_result_type.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ ghost /@ assigns \result;
+ assigns \result \from \nothing; @/
+int *f(void); */
+
+/*@ ghost
+/@ assigns \result, *\result;
+ assigns \result \from \nothing;
+ assigns *\result \from \nothing;
+ @/
+int \ghost *g(void); */
+
+int main(void)
+{
+ int __retres;
+ /*@ ghost int *p = f(); */
+ /*@ ghost int \ghost *q = g(); */
+ __retres = 0;
+ return __retres;
+}
+
+