From 923c1594a9207a5b0f406e6e469599956c59b05f Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 19 Mar 2020 09:18:59 +0100
Subject: [PATCH] [ghost] Clarifies a function in 'ghost_accesses'
---
src/kernel_internals/typing/ghost_accesses.ml | 13 ++++++++-----
1 file changed, 8 insertions(+), 5 deletions(-)
diff --git a/src/kernel_internals/typing/ghost_accesses.ml b/src/kernel_internals/typing/ghost_accesses.ml
index e2ab41966e4..ce796a384de 100644
--- a/src/kernel_internals/typing/ghost_accesses.ml
+++ b/src/kernel_internals/typing/ghost_accesses.ml
@@ -73,7 +73,7 @@ module Error = struct
"Call via a function pointer cannot be checked" ;
end
-let is_ret_var vi =
+let is_generated_ret_var vi =
String.equal vi.vorig_name "__retres"
let get_lvalue = function
@@ -81,7 +81,8 @@ let get_lvalue = function
| Local_init(vi, _, _) -> Some (Cil.var vi)
| _ -> None
-let rec ghost_term_type = function
+let rec ghost_term_type t =
+ match (Logic_utils.unroll_type t) with
| Ctype t -> isGhostType t
| t when Logic_const.is_set_type t ->
ghost_term_type (Logic_const.type_of_element t)
@@ -128,7 +129,8 @@ class visitor = object(self)
if vi.vghost && vi.vreferenced
&& not (Kernel_function.has_definition kf)
then begin
- let spec = try Annotations.funspec ~populate:false kf
+ let spec =
+ try Annotations.funspec ~populate:false kf
with _ -> empty_funspec ()
in
if is_empty_funspec spec then self#bad_ghost_function kf
@@ -137,11 +139,12 @@ class visitor = object(self)
| _ -> Cil.DoChildren
method! vvdec v =
- let current, source = match prefered_loc with
+ let current, source =
+ match prefered_loc with
| Some l -> false, l
| None -> true, (Log.get_current_source ())
in
- if not(is_ret_var v) && not (isWFGhostType v.vtype) then
+ if not(is_generated_ret_var v) && not (isWFGhostType v.vtype) then
Error.invalid_ghost_type_for_varinfo ~once:true ~current ~source v ;
if isFunctionType (unrollType v.vtype) then begin
let ftype = getReturnType (unrollType v.vtype) in
--
GitLab