diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 7c6a861097dd908090f4bb84631bababca4e97fa..5aef82eb76078dc339d8181e66e6b00258daed77 100644
--- a/src/kernel_internals/parsing/clexer.mll
+++ b/src/kernel_internals/parsing/clexer.mll
@@ -567,6 +567,16 @@ rule initial = parse
end
end
}
+| "\\ghost"
+ { if is_ghost_code () || is_oneline_ghost () then begin
+ GHOST (currentLoc())
+ end else begin
+ let start = Lexing.lexeme_start_p lexbuf in
+ let source = Cil_datatype.Position.of_lexing_pos start in
+ Kernel.abort ~source "Use of \\ghost out of ghost code"
+ end
+ }
+
| blank {initial lexbuf}
| '\n' { E.newline ();
if !pragmaLine then
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 294bcc29d272c0b36a71ebde7ebb80732cc66766..084eb5824356fed1965266ae9e5e5b895929c637 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -335,6 +335,7 @@ let in_ghost_block ?(battrs=[]) l =
%token<Cabs.cabsloc> SIGNED UNSIGNED LONG SHORT
%token<Cabs.cabsloc> VOLATILE EXTERN STATIC CONST RESTRICT AUTO REGISTER
%token<Cabs.cabsloc> THREAD
+%token<Cabs.cabsloc> GHOST
%token<Cabs.cabsloc> SIZEOF ALIGNOF
@@ -1463,8 +1464,17 @@ cvspec:
| CONST { SpecCV(CV_CONST), $1 }
| VOLATILE { SpecCV(CV_VOLATILE), $1 }
| RESTRICT { SpecCV(CV_RESTRICT), $1 }
- | ATTRIBUTE_ANNOT { let annot, loc = $1 in
- SpecCV(CV_ATTRIBUTE_ANNOT annot), loc }
+ | GHOST { SpecCV(CV_GHOST), $1 }
+ | ATTRIBUTE_ANNOT
+ {
+ let annot, loc = $1 in
+ if String.compare annot "\\ghost" = 0 then begin
+ let start = Parsing.symbol_start_pos () in
+ let source = Cil_datatype.Position.of_lexing_pos start in
+ Kernel.abort ~source "Use of \\ghost out of ghost code"
+ end else
+ SpecCV(CV_ATTRIBUTE_ANNOT annot), loc
+ }
;
/*** GCC attributes ***/
@@ -1507,6 +1517,7 @@ attribute:
| CONST { ("const", []), $1 }
| RESTRICT { ("restrict",[]), $1 }
| VOLATILE { ("volatile",[]), $1 }
+| GHOST { ("ghost",[]), $1 }
| ATTRIBUTE_ANNOT { let annot, loc = $1 in
("$annot:" ^ annot, []), loc }
;
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index e8e0f215dfae702cabb820957ec3f6f1402ec119..3f3d36715e0563dc0b212c9075ccb9fa584e22ed 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -4780,6 +4780,7 @@ and convertCVtoAttr (src: A.cvspec list) : A.attribute list =
| CV_VOLATILE :: tl -> ("volatile",[]) :: (convertCVtoAttr tl)
| CV_RESTRICT :: tl -> ("restrict",[]) :: (convertCVtoAttr tl)
| CV_ATTRIBUTE_ANNOT a :: tl -> (mkAttrAnnot a, []) :: convertCVtoAttr tl
+ | CV_GHOST :: tl -> ("ghost",[]) :: (convertCVtoAttr tl)
and makeVarInfoCabs
~(ghost:bool)
diff --git a/src/kernel_services/ast_printing/cabs_debug.ml b/src/kernel_services/ast_printing/cabs_debug.ml
index f7ea40bd18f2c9b3c9e3acf4a2369ae078021e2e..90a28b89a7125de34b7b761d84e88fc50bf62e6e 100644
--- a/src/kernel_services/ast_printing/cabs_debug.ml
+++ b/src/kernel_services/ast_printing/cabs_debug.ml
@@ -44,6 +44,7 @@ let pp_cvspec fmt = function
| CV_VOLATILE -> fprintf fmt "CV_VOLATILE"
| CV_RESTRICT -> fprintf fmt "CV_RESTRICT"
| CV_ATTRIBUTE_ANNOT s -> fprintf fmt "CV_ATTRIBUTE_ANNOT %s" s
+ | CV_GHOST -> fprintf fmt "CV_GHOST"
let pp_const fmt = function
| CONST_INT s -> fprintf fmt "CONST_INT %s" s
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 9643993773619485c7a2ec8b4e11b6e5c6f67acd..67cf0d4b22607ec80cd290b78298599e5361c196 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2003,6 +2003,7 @@ class cil_printer () = object (self)
| "aconst", [] when not (Cil.msvcMode ()) -> fprintf fmt "__const__"; true
| "thread", [] when not (Cil.msvcMode ()) -> fprintf fmt "__thread"; false
| "volatile", [] -> self#pp_keyword fmt "volatile"; false
+ | "ghost", [] -> self#pp_keyword fmt "\\ghost"; false
| "restrict", [] -> fprintf fmt "__restrict"; false
| "missingproto", [] ->
if self#display_comment () then fprintf fmt "/* missing proto */";
diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml
index 36b2a4797aae3cf09a6df313fa153a663d157dac..d083883d14b84fdfd3d9c87c67dddb6ec12d3389 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -193,6 +193,7 @@ let rec print_specifiers fmt (specs: spec_elem list) =
| SpecCV CV_VOLATILE -> fprintf fmt "volatile"
| SpecCV CV_RESTRICT -> fprintf fmt "restrict"
| SpecCV (CV_ATTRIBUTE_ANNOT a) -> fprintf fmt "/*@@ %s */" a
+ | SpecCV CV_GHOST -> fprintf fmt "\\ghost"
| SpecAttr al -> print_attribute fmt al
| SpecType bt -> print_type_spec fmt bt
| SpecPattern name -> fprintf fmt "@@specifier(%s)" name
diff --git a/src/kernel_services/parsetree/cabs.ml b/src/kernel_services/parsetree/cabs.ml
index 462f4edd55adad2feecc6fb1b61de3ddd09ed363..3db49d24d3d2dd9ef8516e864685491acf10eba8 100644
--- a/src/kernel_services/parsetree/cabs.ml
+++ b/src/kernel_services/parsetree/cabs.ml
@@ -82,7 +82,7 @@ and funspec =
and cvspec =
| CV_CONST | CV_VOLATILE | CV_RESTRICT
- | CV_ATTRIBUTE_ANNOT of string
+ | CV_ATTRIBUTE_ANNOT of string | CV_GHOST
(* Type specifier elements. These appear at the start of a declaration *)
(* Everywhere they appear in this file, they appear as a 'spec_elem list', *)
@@ -160,7 +160,7 @@ and enum_item = string * expression * cabsloc
** Declaration definition (at toplevel)
*)
and definition =
- FUNDEF of
+ FUNDEF of
(Logic_ptree.spec*cabsloc) option * single_name * block *
cabsloc * cabsloc
| DECDEF of (Logic_ptree.spec*cabsloc) option * init_name_group * cabsloc
@@ -196,7 +196,7 @@ and asm_details =
{ aoutputs: (string option * string * expression) list; (* optional name, constraints and expressions for outputs *)
ainputs: (string option * string * expression) list; (* optional name, constraints and expressions for inputs *)
aclobbers: string list; (* clobbered registers *)
- alabels: string list (* the labels for "asm goto" statements in gcc >= 4.6 *)
+ alabels: string list (* the labels for "asm goto" statements in gcc >= 4.6 *)
}
and raw_statement =
@@ -234,7 +234,7 @@ and raw_statement =
C parser, but can be used by external front-ends.
*)
| TRY_CATCH of statement * (single_name option * statement) list * cabsloc
- (** [TRY_CATCH(s,clauses,loc)] catches exceptions thrown by execution of
+ (** [TRY_CATCH(s,clauses,loc)] catches exceptions thrown by execution of
[s], according to [clauses]. An
exception [e] is caught by the first clause
[(spec,(name, decl, _, _)),body]
diff --git a/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle b/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle
index 50c3496685c56cc5f99c6deb4a4d4694218cd4e2..c9a4f54903239d12c44e6f4483016d28e1eda919 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.0.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing tests/syntax/ghost_cv_parsing_errors.c (with preprocessing)
[kernel] tests/syntax/ghost_cv_parsing_errors.c:13: User Error:
Use of \ghost out of ghost code
+[kernel] User Error: stopping on file "tests/syntax/ghost_cv_parsing_errors.c" that has errors.
+ Add '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle b/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle
index 462ee3a754f02ce6d87f010875c86e44d30c0137..e5d6e9f1545603d3084395f99831a23d76d37721 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.1.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing tests/syntax/ghost_cv_parsing_errors.c (with preprocessing)
[kernel] tests/syntax/ghost_cv_parsing_errors.c:19: User Error:
Use of \ghost out of ghost code
+[kernel] User Error: stopping on file "tests/syntax/ghost_cv_parsing_errors.c" that has errors.
+ Add '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle b/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
index 3c22db369c63563b4d65575069212ddd06a0e8d9..2cb2aecf5c426c0fb746d2375780ee122af350d9 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
@@ -1,4 +1,6 @@
[kernel] Parsing tests/syntax/ghost_cv_parsing_errors.c (with preprocessing)
[kernel] tests/syntax/ghost_cv_parsing_errors.c:25: User Error:
Use of \ghost out of ghost code
+[kernel] User Error: stopping on file "tests/syntax/ghost_cv_parsing_errors.c" that has errors.
+ Add '-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.