From 2cd042653e63c70a413b6774c720123e53017f77 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 11 Oct 2019 16:11:57 +0200
Subject: [PATCH] [typing] fixes parsing and typing of ghost functions
---
src/kernel_internals/parsing/cparser.mly | 36 +++++++++++--------
src/kernel_internals/typing/cabs2cil.ml | 2 +-
tests/syntax/ghost_local_capture.i | 3 ++
.../oracle/ghost_local_capture.res.oracle | 9 +++++
4 files changed, 34 insertions(+), 16 deletions(-)
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 0da0b702034..87325decb88 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -161,6 +161,18 @@ let doDeclaration logic_spec (loc: cabsloc) (specs: spec_elem list) (nl: init_na
DECDEF (logic_spec, (specs, nl), loc)
end
+let in_ghost =
+ let ghost_me = object
+ inherit Cabsvisit.nopCabsVisitor
+ method! vstmt s =
+ s.stmt_ghost <- true;
+ Cil.DoChildren
+ end
+ in
+ List.map
+ (fun s -> ignore (Cabsvisit.visitCabsStatement ghost_me s); s)
+
+let ghost_global = ref false
let doFunctionDef spec (loc: cabsloc)
(lend: cabsloc)
@@ -170,6 +182,7 @@ let doFunctionDef spec (loc: cabsloc)
let fname = (specs, n) in
let name = match n with (n,_,_,_) -> n in
Extlib.may (fun (spec, _) -> check_funspec_abrupt_clauses name spec) spec;
+ let b = if !ghost_global then { b with bstmts = in_ghost b.bstmts } else b in
FUNDEF (spec, fname, b, loc, lend)
let doOldParDecl (names: string list)
@@ -279,17 +292,6 @@ let no_ghost_stmt s = {stmt_ghost = false ; stmt_node = s}
let no_ghost = List.map no_ghost_stmt
-let in_ghost =
- let ghost_me = object
- inherit Cabsvisit.nopCabsVisitor
- method! vstmt s =
- s.stmt_ghost <- true;
- Cil.DoChildren
- end
- in
- List.map
- (fun s -> ignore (Cabsvisit.visitCabsStatement ghost_me s); s)
-
let in_block l =
match l with
[] -> no_ghost_stmt (NOP cabslu)
@@ -440,15 +442,19 @@ file: globals EOF {$1}
globals:
/* empty */ { [] }
| global globals { (false,$1) :: $2 }
-| LGHOST ghost_globals globals { $2 @ $3 }
+| ghost_glob_begin ghost_globals globals { $2 @ $3 }
| SEMICOLON globals { $2 }
;
+ghost_glob_begin:
+| LGHOST { ghost_global:=true }
+;
+
/* Rules for global ghosts: TODO keep the ghost status! */
ghost_globals:
-| declaration ghost_globals { (true,$1)::$2 }
-| function_def ghost_globals { (true,$1)::$2 }
-| RGHOST { [] }
+| declaration ghost_globals { (true,$1)::$2 }
+| function_def ghost_globals { (true,$1)::$2 }
+| RGHOST { ghost_global:=false; [] }
;
/*** Global Definition ***/
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index f56d457bb9e..46bb53acd1f 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -8979,7 +8979,7 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
(* Make the fundec right away, and we'll populate it later. We
* need this throughout the code to create temporaries. *)
currentFunctionFDEC :=
- { svar = makeGlobalVar ~temp:false n voidType;
+ { svar = makeGlobalVar ~temp:false ~ghost n voidType;
slocals = []; (* For now we'll put here both the locals and
* the formals. Then "endFunction" will
* separate them *)
diff --git a/tests/syntax/ghost_local_capture.i b/tests/syntax/ghost_local_capture.i
index 4266c87b9c4..fc4ec789d44 100644
--- a/tests/syntax/ghost_local_capture.i
+++ b/tests/syntax/ghost_local_capture.i
@@ -10,3 +10,6 @@ void titi() {
}
/*@ assert c == 2; */
}
+
+/*@ ghost int x; */
+/*@ ghost void f() { x++; } */
diff --git a/tests/syntax/oracle/ghost_local_capture.res.oracle b/tests/syntax/oracle/ghost_local_capture.res.oracle
index dc24b079c5a..6cb26bb5917 100644
--- a/tests/syntax/oracle/ghost_local_capture.res.oracle
+++ b/tests/syntax/oracle/ghost_local_capture.res.oracle
@@ -16,4 +16,13 @@ void titi(void)
return;
}
+/*@ ghost int x; */
+/*@ ghost void f(void)
+ {
+ x ++;
+ return;
+ }
+
+*/
+
--
GitLab