From de120f6dc46a8949cc5aa7b6f41b711c3764f8b2 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 5 Nov 2019 13:59:32 +0100
Subject: [PATCH] [ghost] Kernel now parses the \ghost keyword
---
src/kernel_internals/parsing/clexer.mll | 10 ++++++++++
src/kernel_internals/parsing/cparser.mly | 15 +++++++++++++--
src/kernel_internals/typing/cabs2cil.ml | 1 +
src/kernel_services/ast_printing/cabs_debug.ml | 1 +
src/kernel_services/ast_printing/cil_printer.ml | 1 +
src/kernel_services/ast_printing/cprint.ml | 1 +
src/kernel_services/parsetree/cabs.ml | 8 ++++----
.../oracle/ghost_cv_parsing_errors.0.res.oracle | 2 ++
.../oracle/ghost_cv_parsing_errors.1.res.oracle | 2 ++
.../oracle/ghost_cv_parsing_errors.2.res.oracle | 2 ++
10 files changed, 37 insertions(+), 6 deletions(-)
diff --git a/src/kernel_internals/parsing/clexer.mll b/src/kernel_internals/parsing/clexer.mll
index 7c6a861097d..5aef82eb760 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 294bcc29d27..084eb582435 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 e8e0f215dfa..3f3d36715e0 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 f7ea40bd18f..90a28b89a71 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 96439937736..67cf0d4b226 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 36b2a4797aa..d083883d14b 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 462f4edd55a..3db49d24d3d 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 50c3496685c..c9a4f549032 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 462ee3a754f..e5d6e9f1545 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 3c22db369c6..2cb2aecf5c4 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.
--
GitLab