diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly index 0da0b7020349f1bf7f3646cddf230055b094af86..87325decb88c1c7056de3787504affb710d37af0 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 f56d457bb9e8f3cf0362593497797b9cd82a2cd3..46bb53acd1fbaa7a8ecb59e934f2cdd9fc5514ee 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 4266c87b9c45f08a81233adeb258e1d958a6f6ed..fc4ec789d44e7c0cc3a2cee5c86b8e4ecc7171a8 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 dc24b079c5afc72e0080121870b5691f42fe3523..6cb26bb591736597e7398bfe889099a4037ecbcd 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; + } + +*/ +