diff --git a/Makefile b/Makefile
index 92ccb6f36b481cf0198b9f721cc00d5c4b3864f2..9d94325ae423e998f608e5d2d06ac95347178f4e 100644
--- a/Makefile
+++ b/Makefile
@@ -125,11 +125,13 @@ FRAMAC_PTESTS:=$(FRAMAC_PTESTS_SRC)/ptests.exe
# WTESTS is internal
FRAMAC_WTESTS:=$(FRAMAC_PTESTS_SRC)/wtests.exe
-# Frama-C also have ptest directories in plugins, so we do not use default
-PTEST_ALL_DIRS:=tests $(wildcard src/plugins/*/tests)
+# Frama-C also has ptest directories in plugins, so we do not use default
+PTEST_ALL_DIRS:=tests $(wildcard src/plugins/*/tests) \
+ src/kernel_internals/parsing/tests
# Test aliasing definition allowing ./configure --disable-<plugin>
-PTEST_ALIASES:=@tests/ptests @src/plugins/ptests
+PTEST_ALIASES:=@tests/ptests @src/plugins/ptests \
+ @src/kernel_internals/parsing/tests/ptests
# WP tests need WP cache
PTEST_USE_WP_CACHE:=yes
diff --git a/bin/test.sh b/bin/test.sh
index c6da0cac0fc4aca2b94f1a61a25a109579eb789b..2e9558da3943989b9fb0281c5226ec96da649254 100755
--- a/bin/test.sh
+++ b/bin/test.sh
@@ -35,7 +35,7 @@ DUNE_LOG=./.test-errors.log
CACHEDIR=$(pwd -P)/.wp-cache
FRAMAC_WP_CACHE_GIT=git@git.frama-c.com:frama-c/wp-cache.git
-TEST_DIRS="tests/* src/plugins/*/tests/*"
+TEST_DIRS="tests/* src/plugins/*/tests/* src/kernel_internals/parsing/tests"
# --------------------------------------------------------------------------
# --- Help Message
diff --git a/dune b/dune
index a9457494dad99f7ab49c7bdacfb046af3e4955fd..82fbcdc86de6cb46540b47b9919e8171a30c3959 100644
--- a/dune
+++ b/dune
@@ -20,6 +20,9 @@
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(env
+ (trace-menhir (menhir_flags --trace)))
+
(alias (name default) (deps (alias install)))
(dirs bin headers man share src tools tests)
diff --git a/src/kernel_internals/parsing/dune b/src/kernel_internals/parsing/dune
index 9e358da57e09828bd2f73d9a4b618d62e32f9607..bfa9e3a404a65b96ae8d8df4010c44a4dd05d998 100644
--- a/src/kernel_internals/parsing/dune
+++ b/src/kernel_internals/parsing/dune
@@ -24,7 +24,11 @@
(ocamllex logic_preprocess)
(ocamllex logic_lexer)
-(ocamlyacc logic_parser)
+(menhir
+ (modules logic_parser)
+ ; "--fixed-exception" fixes compatibility with ocamlyacc Parsing.Parse_error
+ (flags :standard --fixed-exception --explain --dump --comment)
+)
(menhir
(modules cparser)
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index 5177559a48298019210e3bcaf5bc700e4aaebc41..876f7d98eb124a74204704059a26eb1561ba2225 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -103,127 +103,113 @@
let identifier, is_acsl_keyword =
let all_kw = Hashtbl.create 37 in
- let c_kw = Hashtbl.create 37 in
let type_kw = Hashtbl.create 3 in
List.iter
- (fun (i,t,flag) ->
- Hashtbl.add all_kw i t;
- if flag then Hashtbl.add c_kw i t
- )
+ (fun (i,t) -> Hashtbl.add all_kw i t;)
[
- "admit", (fun _ -> ADMIT), false;
- "allocates", (fun _ -> ALLOCATES), false;
- "assert", (fun _ -> ASSERT), false;
- "assigns", (fun _ -> ASSIGNS), false;
- "assumes", (fun _ -> ASSUMES), false;
- "at", (fun _ -> EXT_AT), false;
+ "admit", (fun _ -> ADMIT);
+ "allocates", (fun _ -> ALLOCATES);
+ "assert", (fun _ -> ASSERT);
+ "assigns", (fun _ -> ASSIGNS);
+ "assumes", (fun _ -> ASSUMES);
+ "at", (fun _ -> EXT_AT);
(* ACSL extension for external spec file *)
- "axiom", (fun _ -> AXIOM), false;
- "axiomatic", (fun _ -> AXIOMATIC), false;
- "behavior", (fun _ -> BEHAVIOR), false;
- "behaviors", (fun _ -> BEHAVIORS), false;
- "_Bool", (fun _ -> BOOL), true;
- "breaks", (fun _ -> BREAKS), false;
- "case", (fun _ -> CASE), true;
- "char", (fun _ -> CHAR), true;
- "check", (fun _ -> CHECK), false;
- "complete", (fun _ -> COMPLETE), false;
- "const", (fun _ -> CONST), true;
- "continues", (fun _ -> CONTINUES), false;
- "contract", (fun _ -> CONTRACT), false;
+ "axiom", (fun _ -> AXIOM);
+ "axiomatic", (fun _ -> AXIOMATIC);
+ "behavior", (fun _ -> BEHAVIOR);
+ "behaviors", (fun _ -> BEHAVIORS);
+ "_Bool", (fun _ -> BOOL);
+ "breaks", (fun _ -> BREAKS);
+ "case", (fun _ -> CASE);
+ "char", (fun _ -> CHAR);
+ "check", (fun _ -> CHECK);
+ "complete", (fun _ -> COMPLETE);
+ "const", (fun _ -> CONST);
+ "continues", (fun _ -> CONTINUES);
+ "contract", (fun _ -> CONTRACT);
(* ACSL extension for external spec file *)
- "decreases", (fun _ -> DECREASES), false;
- "disjoint", (fun _ -> DISJOINT), false;
- "double", (fun _ -> DOUBLE), true;
- "else", (fun _ -> ELSE), true;
- "ensures", (fun _ -> ENSURES), false ;
- "enum", (fun _ -> ENUM), true;
- "exits", (fun _ -> EXITS), false;
- "frees", (fun _ -> FREES), false;
- "function", (fun _ -> FUNCTION), false;
+ "decreases", (fun _ -> DECREASES);
+ "disjoint", (fun _ -> DISJOINT);
+ "double", (fun _ -> DOUBLE);
+ "else", (fun _ -> ELSE);
+ "ensures", (fun _ -> ENSURES);
+ "enum", (fun _ -> ENUM);
+ "exits", (fun _ -> EXITS);
+ "frees", (fun _ -> FREES);
+ "function", (fun _ -> FUNCTION);
(* ACSL extension for external spec file *)
- "float", (fun _ -> FLOAT), true;
- "for", (fun _ -> FOR), true;
- "global", (fun _ -> GLOBAL), false;
- "if", (fun _ -> IF), true;
- "impact", (fun _ -> IMPACT), false;
- "inductive", (fun _ -> INDUCTIVE), false;
- "include", (fun _ -> INCLUDE), false;
+ "float", (fun _ -> FLOAT);
+ "for", (fun _ -> FOR);
+ "global", (fun _ -> GLOBAL);
+ "if", (fun _ -> IF);
+ "impact", (fun _ -> IMPACT);
+ "inductive", (fun _ -> INDUCTIVE);
+ "include", (fun _ -> INCLUDE);
(* ACSL extension for external spec file *)
- "int", (fun _ -> INT), true;
- "invariant", (fun _ -> INVARIANT), false;
- "label", (fun _ -> LABEL), false;
- "lemma", (fun _ -> LEMMA), false;
- "let", (fun _ -> EXT_LET), false;
+ "int", (fun _ -> INT);
+ "invariant", (fun _ -> INVARIANT);
+ "label", (fun _ -> LABEL);
+ "lemma", (fun _ -> LEMMA);
+ "let", (fun _ -> EXT_LET);
(* ACSL extension for external spec file *)
- "logic", (fun _ -> LOGIC), false;
- "long", (fun _ -> LONG), true;
- "loop", (fun _ -> LOOP), false;
- "model", (fun _ -> MODEL), false;
+ "logic", (fun _ -> LOGIC);
+ "long", (fun _ -> LONG);
+ "loop", (fun _ -> LOOP);
+ "model", (fun _ -> MODEL);
(* ACSL extension for model fields *)
- "module", (fun _ -> MODULE), false;
+ "module", (fun _ -> MODULE);
(* ACSL extension for external spec file *)
- "pragma", (fun _ -> PRAGMA), false;
- "predicate", (fun _ -> PREDICATE), false;
- "reads", (fun _ -> READS), true;
- (* treated specifically in the parser to
- avoid issue in volatile clause. *)
- "requires", (fun _ -> REQUIRES), false;
- "returns", (fun _ -> RETURNS), false;
- "short", (fun _ -> SHORT), true;
- "signed", (fun _ -> SIGNED), true;
- "sizeof", (fun _ -> SIZEOF), true;
- "slice", (fun _ -> SLICE), false;
- "struct", (fun _ -> STRUCT), true;
- "terminates", (fun _ -> TERMINATES), false;
- "type", (fun _ -> TYPE), false;
- "union", (fun _ -> UNION), true;
- "unsigned", (fun _ -> UNSIGNED), true;
- "variant", (fun _ -> VARIANT), false;
- "void", (fun _ -> VOID), true;
- "volatile", (fun _ -> VOLATILE), true;
- "writes", (fun _ -> WRITES), true;
- (* treated specifically in the parser to
- avoid issue in volatile clause. *)
+ "pragma", (fun _ -> PRAGMA);
+ "predicate", (fun _ -> PREDICATE);
+ "reads", (fun _ -> READS);
+ "requires", (fun _ -> REQUIRES);
+ "returns", (fun _ -> RETURNS);
+ "short", (fun _ -> SHORT);
+ "signed", (fun _ -> SIGNED);
+ "sizeof", (fun _ -> SIZEOF);
+ "slice", (fun _ -> SLICE);
+ "struct", (fun _ -> STRUCT);
+ "terminates", (fun _ -> TERMINATES);
+ "type", (fun _ -> TYPE);
+ "union", (fun _ -> UNION);
+ "unsigned", (fun _ -> UNSIGNED);
+ "variant", (fun _ -> VARIANT);
+ "void", (fun _ -> VOID);
+ "volatile", (fun _ -> VOLATILE);
+ "writes", (fun _ -> WRITES);
"__FC_FILENAME__",
(fun loc ->
let filename =
Filepath.(Normalized.to_pretty_string (fst loc).pos_path)
in
- STRING_LITERAL (false,filename)),
- true;
+ STRING_LITERAL (false,filename));
];
List.iter (fun (x, y) -> Hashtbl.add type_kw x y)
["integer", INTEGER; "real", REAL; "boolean", BOOLEAN; ];
(fun s loc ->
try
- (Hashtbl.find (if Logic_utils.is_kw_c_mode () then c_kw else all_kw) s)
+ (Hashtbl.find all_kw s)
loc
with Not_found ->
let res =
- if not (Logic_utils.is_kw_c_mode ()) then begin
- match Logic_env.extension_category s with
- | exception Not_found -> None
- | Cil_types.Ext_contract -> Some (EXT_CONTRACT s)
- | Cil_types.Ext_global ->
- begin
- match Logic_env.is_extension_block s with
- | false -> Some (EXT_GLOBAL s)
- | true -> Some (EXT_GLOBAL_BLOCK s)
- end
- | Cil_types.Ext_code_annot _ -> Some (EXT_CODE_ANNOT s)
- end
- else None
+ match Logic_env.extension_category s with
+ | exception Not_found -> None
+ | Cil_types.Ext_contract -> Some (EXT_CONTRACT s)
+ | Cil_types.Ext_global ->
+ begin
+ match Logic_env.is_extension_block s with
+ | false -> Some (EXT_GLOBAL s)
+ | true -> Some (EXT_GLOBAL_BLOCK s)
+ end
+ | Cil_types.Ext_code_annot _ -> Some (EXT_CODE_ANNOT s)
in
match res with
| None ->
- if Logic_env.typename_status s then TYPENAME s
- else
- (try
- Hashtbl.find type_kw s
- with Not_found ->
- if Logic_utils.is_rt_type_mode () then TYPENAME s
- else IDENTIFIER s)
+ if Logic_env.typename_status s then TYPENAME s
+ else
+ (try
+ Hashtbl.find type_kw s
+ with Not_found -> IDENTIFIER s)
| Some lex -> lex
),
(fun s -> Hashtbl.mem all_kw s || Hashtbl.mem type_kw s)
@@ -555,8 +541,7 @@ and comment = parse
dest_lexbuf.lex_abs_pos <- src_pos.pos_cnum
let parse_from_position f (pos, s : Filepath.position * string) =
- let finally _ = Logic_utils.exit_kw_c_mode () in
- let output = Kernel.logwith finally ~wkey:Kernel.wkey_annot_error
+ let output = Kernel.warning ~wkey:Kernel.wkey_annot_error
in
let lb = from_string s in
set_initial_position lb (Cil_datatype.Position.to_lexing_pos pos);
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index be05d3183e02f95e78977ecc0cb83e7af031ed6b..d10a972435e8ed7c85c1a17a24a7063cabb66a11 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -30,20 +30,19 @@
open Logic_ptree
open Logic_utils
- let loc () =
+ let loc (start_pos, end_pos) =
Cil_datatype.Location.of_lexing_loc
- (symbol_start_pos (), symbol_end_pos ())
- let lexeme_start nb =
- Cil_datatype.Position.of_lexing_pos (Parsing.rhs_start_pos nb)
- let lexeme_end nb =
- Cil_datatype.Position.of_lexing_pos (Parsing.rhs_end_pos nb)
- let lexeme_loc nb = (lexeme_start nb, lexeme_end nb)
-
- let info x = { lexpr_node = x; lexpr_loc = loc () }
- let loc_info loc x = { lexpr_node = x; lexpr_loc = loc }
+ (start_pos, end_pos)
+
+ let pos pos =
+ Cil_datatype.Position.of_lexing_pos pos
+
+ let loc_info lexpr_loc x = { lexpr_node = x; lexpr_loc }
let loc_start x = fst x.lexpr_loc
let loc_end x = snd x.lexpr_loc
+ let info start_end x = loc_info (loc start_end) x
+
(* Normalize p1 && (p2 && p3) into (p1 && p2) && p3 *)
let rec pland p1 p2 =
match p2.lexpr_node with
@@ -59,17 +58,17 @@
PLor(loc_info loc (plor p1 p3),p4)
| _ -> PLor(p1,p2)
- let clause_order i name1 name2 =
+ let clause_order start_end name1 name2 =
raise
(Not_well_formed
- (lexeme_loc i,
+ (loc start_end,
"wrong order of clause in contract: "
^ name1 ^ " after " ^ name2 ^ "."))
- let missing i token next_token =
+ let missing start_end token next_token =
raise
(Not_well_formed
- (lexeme_loc i,
+ (loc start_end,
Format.asprintf "expecting '%s' before %s" token next_token))
type sense_of_relation = Unknown | Disequal | Less | Greater
@@ -97,17 +96,9 @@
let l = Stack.pop type_variables_stack in
List.iter Logic_env.remove_typename l
- let rt_type = ref false
-
- let set_rt_type () = rt_type:= true
-
- let reset_rt_type () = rt_type:=false
+ let loc_decl start_end d = { decl_node = d; decl_loc = loc start_end }
- let is_rt_type () = !rt_type
-
- let loc_decl d = { decl_node = d; decl_loc = loc () }
-
- let loc_ext d = { extended_node = d; extended_loc = loc () }
+ let loc_ext start_end d = { extended_node = d; extended_loc = loc start_end }
let filter_from l = function
| FromAny ->
@@ -168,16 +159,16 @@
| FreeAlloc(f1,a1),FreeAlloc(f2,a2) -> FreeAlloc(f2@f1,a2@a1)
(* a1 represents the assigns _after_ the current clause a2. *)
- let concat_assigns a1 a2 =
+ let concat_assigns start_pos a1 a2 =
match a1,a2 with
WritesAny,a -> Writes (concat_froms [] a)
| Writes [], [] -> a1
| Writes [], _ | Writes _, [] ->
raise (
- Not_well_formed (loc(),"Mixing \\nothing and a real location"))
+ Not_well_formed (loc start_pos,"Mixing \\nothing and a real location"))
| Writes a1, a2 -> Writes (concat_froms (concat_froms [] a2) a1)
- let concat_loop_assigns_allocation annots bhvs2 a2 fa2=
+ let concat_loop_assigns_allocation start_pos annots bhvs2 a2 fa2=
(* NB: this is supposed to merge assigns related to named behaviors, in
case of annotation like
for a,b: assigns x,y;
@@ -203,7 +194,7 @@
(match both with
| [] -> bhvs2, ca::acc
| _ ->
- let common_annot = AAssigns(both,concat_assigns a1 a2) in
+ let common_annot = AAssigns(both,concat_assigns start_pos a1 a2) in
let annots =
match only1 with
| [] -> common_annot :: acc
@@ -339,24 +330,6 @@
%%
-enter_kw_c_mode:
-/* empty */ { enter_kw_c_mode () }
-
-exit_kw_c_mode:
-/* empty */ { exit_kw_c_mode () }
-
-enter_rt_type:
-/* empty */ { if is_rt_type () then enter_rt_type_mode () }
-
-exit_rt_type:
-/* empty */ { if is_rt_type () then exit_rt_type_mode () }
-
-begin_rt_type:
-/* empty */ { set_rt_type () }
-
-end_rt_type:
-/* empty */ { reset_rt_type () }
-
/*** predicates and terms ***/
lexpr_list:
@@ -370,7 +343,7 @@ ne_lexpr_list:
;
lexpr_eof:
-| full_lexpr EOF { $1 }
+| lexpr EOF { $1 }
;
lexpr_option:
@@ -380,30 +353,30 @@ lexpr_option:
lexpr:
/* predicates */
-| lexpr IMPLIES lexpr { info (PLimplies ($1, $3)) }
-| lexpr IFF lexpr { info (PLiff ($1, $3)) }
-| lexpr OR lexpr { info (plor $1 $3) }
-| lexpr AND lexpr { info (pland $1 $3) }
-| lexpr HATHAT lexpr { info (PLxor ($1, $3)) }
+| lexpr IMPLIES lexpr { info $sloc (PLimplies ($1, $3)) }
+| lexpr IFF lexpr { info $sloc (PLiff ($1, $3)) }
+| lexpr OR lexpr { info $sloc (plor $1 $3) }
+| lexpr AND lexpr { info $sloc (pland $1 $3) }
+| lexpr HATHAT lexpr { info $sloc (PLxor ($1, $3)) }
/* terms */
-| lexpr AMP lexpr { info (PLbinop ($1, Bbw_and, $3)) }
-| lexpr PIPE lexpr { info (PLbinop ($1, Bbw_or, $3)) }
-| lexpr HAT lexpr { info (PLbinop ($1, Bbw_xor, $3)) }
-| lexpr BIMPLIES lexpr { info (PLbinop (info (PLunop (Ubw_not, $1)), Bbw_or, $3)) }
-| lexpr BIFF lexpr { info (PLbinop (info (PLunop (Ubw_not, $1)), Bbw_xor, $3)) }
-| lexpr IN lexpr { info (PLapp ("\\subset", [], [info ((PLset [$1]));$3])) }
+| lexpr AMP lexpr { info $sloc (PLbinop ($1, Bbw_and, $3)) }
+| lexpr PIPE lexpr { info $sloc (PLbinop ($1, Bbw_or, $3)) }
+| lexpr HAT lexpr { info $sloc (PLbinop ($1, Bbw_xor, $3)) }
+| lexpr BIMPLIES lexpr { info $sloc (PLbinop (info $sloc (PLunop (Ubw_not, $1)), Bbw_or, $3)) }
+| lexpr BIFF lexpr { info $sloc (PLbinop (info $sloc (PLunop (Ubw_not, $1)), Bbw_xor, $3)) }
+| lexpr IN lexpr { info $sloc (PLapp ("\\subset", [], [info $sloc (PLset [$1]);$3])) }
| lexpr QUESTION lexpr COLON2 lexpr %prec prec_question
- { info (PLif ($1, $3, $5)) }
+ { info $sloc (PLif ($1, $3, $5)) }
/* both terms and predicates */
-| any_identifier COLON lexpr %prec prec_named { info (PLnamed ($1, $3)) }
+| any_identifier COLON lexpr %prec prec_named { info $sloc (PLnamed ($1, $3)) }
| string COLON lexpr %prec prec_named
{ let (iswide,str) = $1 in
if iswide then begin
- let l = loc () in
+ let l = loc $sloc in
raise (Not_well_formed(l, "Wide strings are not allowed as labels."))
end;
let str = escape str in
- info (PLnamed (str, $3))
+ info $sloc (PLnamed (str, $3))
}
| lexpr_rel { $1 }
;
@@ -416,24 +389,25 @@ lexpr_rel:
let relation = loc_info loc (PLrel($1,rel,rhs)) in
match oth_rel with
None -> relation
- | Some oth_relation -> info (pland relation oth_relation)
+ | Some oth_relation -> info $sloc (pland relation oth_relation)
}
;
lexpr_binder:
-| LET bounded_var EQUAL lexpr SEMICOLON lexpr %prec LET {info (PLlet($2,$4,$6))}
+| LET bounded_var EQUAL lexpr SEMICOLON lexpr %prec LET
+ { info $sloc (PLlet($2,$4,$6))}
| FORALL binders SEMICOLON lexpr %prec prec_forall
- { info (PLforall ($2, $4)) }
+ { info $sloc (PLforall ($2, $4)) }
| EXISTS binders SEMICOLON lexpr %prec prec_exists
- { info (PLexists ($2, $4)) }
+ { info $sloc (PLexists ($2, $4)) }
| LAMBDA binders SEMICOLON lexpr %prec prec_lambda
- { info (PLlambda ($2,$4)) }
+ { info $sloc (PLlambda ($2,$4)) }
;
lexpr_end_rel:
lexpr_inner { $1 }
| lexpr_binder { $1 }
-| NOT lexpr_binder { info (PLnot $2) }
+| NOT lexpr_binder { info $sloc (PLnot $2) }
;
rel_list:
@@ -455,7 +429,7 @@ rel_list:
in
$1,$2,sense,Some oth_rel
else begin
- let loc = lexeme_start 1, lexeme_end 3 in
+ let loc = loc $sloc in
raise (Not_well_formed(loc,"Inconsistent relation chain."));
end
}
@@ -470,7 +444,7 @@ relation:
| NE { Neq }
/* C. Marche: added to produce better error messages */
| EQUAL {
- let l = loc () in
+ let l = loc $sloc in
raise
(Not_well_formed(l,
"Assignment operators not allowed in annotations."))
@@ -485,119 +459,119 @@ lexpr_inner:
else
StringConstant content
in
- info (PLconstant cst)
+ info $sloc (PLconstant cst)
}
-| NOT lexpr_inner { info (PLnot $2) }
-| TRUE { info PLtrue }
-| FALSE { info PLfalse }
-| OBJECT_POINTER opt_label_1 LPAR lexpr RPAR { info (PLobject_pointer ($2,$4)) }
-| VALID opt_label_1 LPAR lexpr RPAR { info (PLvalid ($2,$4)) }
-| VALID_READ opt_label_1 LPAR lexpr RPAR { info (PLvalid_read ($2,$4)) }
-| VALID_FUNCTION LPAR lexpr RPAR { info (PLvalid_function $3) }
+| NOT lexpr_inner { info $sloc (PLnot $2) }
+| TRUE { info $sloc PLtrue }
+| FALSE { info $sloc PLfalse }
+| OBJECT_POINTER opt_label_1 LPAR lexpr RPAR { info $sloc (PLobject_pointer ($2,$4)) }
+| VALID opt_label_1 LPAR lexpr RPAR { info $sloc (PLvalid ($2,$4)) }
+| VALID_READ opt_label_1 LPAR lexpr RPAR { info $sloc (PLvalid_read ($2,$4)) }
+| VALID_FUNCTION LPAR lexpr RPAR { info $sloc (PLvalid_function $3) }
| VALID_INDEX opt_label_1 LPAR lexpr COMMA lexpr RPAR {
- let source = fst (loc ()) in
+ let source = pos $symbolstartpos in
obsolete ~source "\\valid_index(addr,idx)" ~now:"\\valid(addr+idx)";
- info (PLvalid ($2,info (PLbinop ($4, Badd, $6)))) }
+ info $sloc (PLvalid ($2,info $sloc (PLbinop ($4, Badd, $6)))) }
| VALID_RANGE opt_label_1 LPAR lexpr COMMA lexpr COMMA lexpr RPAR {
- let source = fst (loc ()) in
+ let source = pos $symbolstartpos in
obsolete "\\valid_range(addr,min,max)"
~source ~now:"\\valid(addr+(min..max))";
- info (PLvalid
- ($2,info (PLbinop ($4, Badd, (info (PLrange((Some $6),Some $8)))))))
+ info $sloc (PLvalid
+ ($2,info $sloc (PLbinop ($4, Badd, (info $sloc (PLrange((Some $6),Some $8)))))))
}
-| INITIALIZED opt_label_1 LPAR lexpr RPAR { info (PLinitialized ($2,$4)) }
-| DANGLING opt_label_1 LPAR lexpr RPAR { info (PLdangling ($2,$4)) }
-| FRESH opt_label_2 LPAR lexpr COMMA lexpr RPAR { info (PLfresh ($2,$4, $6)) }
-| BASE_ADDR opt_label_1 LPAR lexpr RPAR { info (PLbase_addr ($2,$4)) }
-| BLOCK_LENGTH opt_label_1 LPAR lexpr RPAR { info (PLblock_length ($2,$4)) }
-| OFFSET opt_label_1 LPAR lexpr RPAR { info (PLoffset ($2,$4)) }
-| ALLOCABLE opt_label_1 LPAR lexpr RPAR { info (PLallocable ($2,$4)) }
-| FREEABLE opt_label_1 LPAR lexpr RPAR { info (PLfreeable ($2,$4)) }
+| INITIALIZED opt_label_1 LPAR lexpr RPAR { info $sloc (PLinitialized ($2,$4)) }
+| DANGLING opt_label_1 LPAR lexpr RPAR { info $sloc (PLdangling ($2,$4)) }
+| FRESH opt_label_2 LPAR lexpr COMMA lexpr RPAR { info $sloc (PLfresh ($2,$4, $6)) }
+| BASE_ADDR opt_label_1 LPAR lexpr RPAR { info $sloc (PLbase_addr ($2,$4)) }
+| BLOCK_LENGTH opt_label_1 LPAR lexpr RPAR { info $sloc (PLblock_length ($2,$4)) }
+| OFFSET opt_label_1 LPAR lexpr RPAR { info $sloc (PLoffset ($2,$4)) }
+| ALLOCABLE opt_label_1 LPAR lexpr RPAR { info $sloc (PLallocable ($2,$4)) }
+| FREEABLE opt_label_1 LPAR lexpr RPAR { info $sloc (PLfreeable ($2,$4)) }
| ALLOCATION opt_label_1 LPAR lexpr RPAR
- { let source = fst(loc()) in
+ { let source = pos $symbolstartpos in
Kernel.not_yet_implemented ~source "\\allocation" }
| AUTOMATIC {
- let source = fst(loc()) in
+ let source = pos $symbolstartpos in
Kernel.not_yet_implemented ~source "\\automatic" }
| DYNAMIC {
- let source = fst(loc()) in
+ let source = pos $symbolstartpos in
Kernel.not_yet_implemented ~source "\\dynamic" }
| REGISTER {
- let source = fst(loc()) in
+ let source = pos $symbolstartpos in
Kernel.not_yet_implemented ~source "\\register" }
| STATIC {
- let source = fst(loc()) in
+ let source = pos $symbolstartpos in
Kernel.not_yet_implemented ~source "\\static" }
| UNALLOCATED {
- let source = fst(loc()) in
+ let source = pos $symbolstartpos in
Kernel.not_yet_implemented ~source "\\unallocated" }
-| NULL { info PLnull }
-| constant { info (PLconstant $1) }
-| lexpr_inner PLUS lexpr_inner { info (PLbinop ($1, Badd, $3)) }
-| lexpr_inner MINUS lexpr_inner { info (PLbinop ($1, Bsub, $3)) }
-| lexpr_inner STAR lexpr_inner { info (PLbinop ($1, Bmul, $3)) }
-| lexpr_inner SLASH lexpr_inner { info (PLbinop ($1, Bdiv, $3)) }
-| lexpr_inner PERCENT lexpr_inner { info (PLbinop ($1, Bmod, $3)) }
-| lexpr_inner STARHAT lexpr_inner { info (PLrepeat ($1, $3)) }
-| lexpr_inner ARROW identifier_or_typename { info (PLarrow ($1, $3)) }
-| lexpr_inner DOT identifier_or_typename { info (PLdot ($1, $3)) }
-| lexpr_inner LSQUARE range RSQUARE { info (PLarrget ($1, $3)) }
-| lexpr_inner LSQUARE lexpr RSQUARE { info (PLarrget ($1, $3)) }
-| LSQUAREPIPE lexpr_list RSQUAREPIPE {info (PLlist $2) }
-| MINUS lexpr_inner %prec prec_unary_op { info (PLunop (Uminus, $2)) }
+| NULL { info $sloc PLnull }
+| constant { info $sloc (PLconstant $1) }
+| lexpr_inner PLUS lexpr_inner { info $sloc (PLbinop ($1, Badd, $3)) }
+| lexpr_inner MINUS lexpr_inner { info $sloc (PLbinop ($1, Bsub, $3)) }
+| lexpr_inner STAR lexpr_inner { info $sloc (PLbinop ($1, Bmul, $3)) }
+| lexpr_inner SLASH lexpr_inner { info $sloc (PLbinop ($1, Bdiv, $3)) }
+| lexpr_inner PERCENT lexpr_inner { info $sloc (PLbinop ($1, Bmod, $3)) }
+| lexpr_inner STARHAT lexpr_inner { info $sloc (PLrepeat ($1, $3)) }
+| lexpr_inner ARROW identifier_or_typename_full { info $sloc (PLarrow ($1, $3)) }
+| lexpr_inner DOT identifier_or_typename_full { info $sloc (PLdot ($1, $3)) }
+| lexpr_inner LSQUARE range RSQUARE { info $sloc (PLarrget ($1, $3)) }
+| lexpr_inner LSQUARE lexpr RSQUARE { info $sloc (PLarrget ($1, $3)) }
+| LSQUAREPIPE lexpr_list RSQUAREPIPE { info $sloc (PLlist $2) }
+| MINUS lexpr_inner %prec prec_unary_op { info $sloc (PLunop (Uminus, $2)) }
| PLUS lexpr_inner %prec prec_unary_op { $2 }
-| TILDE lexpr_inner { info (PLunop (Ubw_not, $2)) }
-| STAR lexpr_inner %prec prec_unary_op { info (PLunop (Ustar, $2)) }
-| AMP lexpr_inner %prec prec_unary_op { info (PLunop (Uamp, $2)) }
-| SIZEOF LPAR lexpr RPAR { info (PLsizeofE $3) }
-| SIZEOF LPAR cast_logic_type RPAR { info (PLsizeof $3) }
-| OLD LPAR lexpr RPAR { info (PLold $3) }
-| AT LPAR lexpr COMMA label_name RPAR { info (PLat ($3, $5)) }
-| RESULT { info PLresult }
+| TILDE lexpr_inner { info $sloc (PLunop (Ubw_not, $2)) }
+| STAR lexpr_inner %prec prec_unary_op { info $sloc (PLunop (Ustar, $2)) }
+| AMP lexpr_inner %prec prec_unary_op { info $sloc (PLunop (Uamp, $2)) }
+| SIZEOF LPAR lexpr RPAR { info $sloc (PLsizeofE $3) }
+| SIZEOF LPAR cast_logic_type RPAR { info $sloc (PLsizeof $3) }
+| OLD LPAR lexpr RPAR { info $sloc (PLold $3) }
+| AT LPAR lexpr COMMA label_name RPAR { info $sloc (PLat ($3, $5)) }
+| RESULT { info $sloc PLresult }
| SEPARATED LPAR ne_lexpr_list RPAR
- { info (PLseparated $3) }
-| identifier LPAR ne_lexpr_list RPAR
- { info (PLapp ($1, [], $3)) }
-| identifier LBRACE ne_label_args RBRACE LPAR ne_lexpr_list RPAR
- { info (PLapp ($1, $3, $6)) }
-| identifier LBRACE ne_label_args RBRACE
- { info (PLapp ($1, $3, [])) }
-| identifier { info (PLvar $1) }
-| PI { info (PLvar "\\pi") }
-| lexpr_inner GTGT lexpr_inner { info (PLbinop ($1, Brshift, $3))}
-| lexpr_inner LTLT lexpr_inner { info (PLbinop ($1, Blshift, $3))}
-| LPAR lexpr RPAR { info $2.lexpr_node }
-| LPAR range RPAR { info $2.lexpr_node }
+ { info $sloc (PLseparated $3) }
+| full_identifier LPAR ne_lexpr_list RPAR
+ { info $sloc (PLapp ($1, [], $3)) }
+| full_identifier LBRACE ne_label_args RBRACE LPAR ne_lexpr_list RPAR
+ { info $sloc (PLapp ($1, $3, $6)) }
+| full_identifier LBRACE ne_label_args RBRACE
+ { info $sloc (PLapp ($1, $3, [])) }
+| full_identifier { info $sloc (PLvar $1) }
+| PI { info $sloc (PLvar "\\pi") }
+| lexpr_inner GTGT lexpr_inner { info $sloc (PLbinop ($1, Brshift, $3))}
+| lexpr_inner LTLT lexpr_inner { info $sloc (PLbinop ($1, Blshift, $3))}
+| LPAR lexpr RPAR { info $sloc $2.lexpr_node }
+| LPAR range RPAR { info $sloc $2.lexpr_node }
| LPAR cast_logic_type RPAR lexpr_inner %prec prec_cast
- { info (PLcast ($2, $4)) }
-| TYPEOF LPAR lexpr RPAR { info (PLtypeof $3) }
-| BSTYPE LPAR type_spec RPAR { info (PLtype $3) }
-| BSTYPE LPAR type_spec stars RPAR { info (PLtype ($4 $3)) }
+ { info $sloc (PLcast ($2, $4)) }
+| TYPEOF LPAR lexpr RPAR { info $sloc (PLtypeof $3) }
+| BSTYPE LPAR type_spec(typename) RPAR { info $sloc (PLtype $3) }
+| BSTYPE LPAR type_spec(typename) stars RPAR { info $sloc (PLtype ($4 $3)) }
/* tsets */
-| EMPTY { info PLempty }
-| BSUNION LPAR lexpr_list RPAR { info (PLunion $3) }
-| INTER LPAR lexpr_list RPAR { info (PLinter $3) }
+| EMPTY { info $sloc PLempty }
+| BSUNION LPAR lexpr_list RPAR { info $sloc (PLunion $3) }
+| INTER LPAR lexpr_list RPAR { info $sloc (PLinter $3) }
| LBRACE lexpr_list RBRACE
- { info (PLset ($2)) }
+ { info $sloc (PLset ($2)) }
| LBRACE lexpr PIPE binders RBRACE
- {info (PLcomprehension ($2,$4,None)) }
+ { info $sloc (PLcomprehension ($2,$4,None)) }
| LBRACE lexpr PIPE binders SEMICOLON lexpr RBRACE
- { info (PLcomprehension ($2,$4,Some $6)) }
+ { info $sloc (PLcomprehension ($2,$4,Some $6)) }
/* Aggregated object initialization */
| LBRACE field_init RBRACE
- { info (PLinitField($2)) }
+ { info $sloc (PLinitField($2)) }
| LBRACE array_init RBRACE
- { info (PLinitIndex($2)) }
+ { info $sloc (PLinitIndex($2)) }
| LBRACE lexpr WITH update RBRACE
{ List.fold_left
- (fun a (path,upd_val) -> info (PLupdate(a,path,upd_val))) $2 $4 }
+ (fun a (path,upd_val) -> info $sloc (PLupdate(a,path,upd_val))) $2 $4 }
/*
-| LET bounded_var EQUAL lexpr SEMICOLON lexpr %prec LET {info (PLlet($2,$4,$6))}*/
+| LET bounded_var EQUAL lexpr SEMICOLON lexpr %prec LET { info $sloc (PLlet($2,$4,$6))}*/
;
ne_label_args:
-| identifier_or_typename { [ $1 ] }
-| identifier_or_typename COMMA ne_label_args { $1 :: $3 }
+| identifier_or_typename_full { [ $1 ] }
+| identifier_or_typename_full COMMA ne_label_args { $1 :: $3 }
string:
| STRING_LITERAL { $1 }
@@ -609,13 +583,13 @@ string:
;
range:
-| lexpr_option DOTDOT lexpr_option { info (PLrange($1,$3)) }
+| lexpr_option DOTDOT lexpr_option { info $sloc (PLrange($1,$3)) }
;
/*** Aggregated object initialization ***/
field_path_elt:
-| DOT identifier_or_typename { $2 }
+| DOT identifier_or_typename_full { $2 }
;
field_init_elt:
| field_path_elt EQUAL lexpr { ($1, $3) }
@@ -681,7 +655,7 @@ binders_reentrance:
;
decl_spec:
-| type_spec var_spec { ($1, let (modif, name) = $2 in (modif $1, name)) }
+| type_spec(typename) var_spec { ($1, let (modif, name) = $2 in (modif $1, name)) }
;
var_spec:
@@ -701,12 +675,12 @@ constant:
array_size:
| INT_CONSTANT { ASinteger $1 }
-| identifier { ASidentifier $1 }
+| full_identifier { ASidentifier $1 }
| /* empty */ { ASnone }
;
var_spec_bis:
-| identifier { ((fun x -> x),(fun x -> x), $1) }
+| full_identifier { ((fun x -> x),(fun x -> x), $1) }
| var_spec_bis LSQUARE array_size RSQUARE
{ let (outer, inner, name) = $1 in
(outer, (fun x -> inner (LTarray (x,$3))), name)
@@ -723,7 +697,7 @@ abs_param_type_list:
| /* empty */ { [ ] }
| abs_param_list { $1 }
| abs_param_list COMMA DOTDOTDOT {
- let source = fst(loc()) in
+ let source = pos $symbolstartpos in
Kernel.not_yet_implemented ~source "variadic C function types"
}
;
@@ -740,50 +714,50 @@ abs_param:
| logic_type { $1 }
;
-/*** restricted type expressions ***/
-
-id_as_typename:
-| identifier { LTnamed($1, []) }
-;
-
ne_parameters:
| parameter { [$1] }
| parameter COMMA ne_parameters { $1 :: $3 }
;
parameter:
-| type_spec var_spec { let (modif, name) = $2 in (modif $1, name)}
-| id_as_typename var_spec { let (modif, name) = $2 in (modif $1, name) }
+| type_spec(identifier_or_typename) var_spec
+ { let (modif, name) = $2 in (modif $1, name)}
;
/*** type expressions ***/
-logic_type:
-| type_spec abs_spec_option { $2 $1 }
+logic_type_gen(tname):
+| type_spec(tname) abs_spec_option { $2 $1 }
+;
+
+typename:
+| name = TYPENAME { name }
+/* TODO treat the case of an ACSL keyword that is also a typedef */
;
+logic_type: logic_type_gen(typename) { $1 }
+
cv:
CONST { cv_const }
| VOLATILE { cv_volatile }
| BSGHOST { cv_ghost }
;
-type_spec_cv:
- type_spec cv_after { $2 $1 }
-| cv type_spec_cv { LTattribute ($2, $1) }
+type_spec_cv(tname):
+ type_spec(tname) cv_after { $2 $1 }
+| cv type_spec_cv(tname) { LTattribute ($2, $1) }
cv_after:
/* empty */ { fun t -> t }
| cv cv_after { fun t -> $2 (LTattribute (t,$1)) }
cast_logic_type:
- | type_spec_cv abs_spec_cv_option { $2 $1 }
+ | type_spec_cv(TYPENAME) abs_spec_cv_option { $2 $1 }
;
logic_rt_type:
-| id_as_typename { $1 }
-| begin_rt_type logic_type end_rt_type { $2 }
+| logic_type_gen(identifier_or_typename) { $1 }
;
abs_spec_option:
@@ -849,7 +823,7 @@ tabs:
}
;
-type_spec:
+type_spec(tname):
| INTEGER { LTinteger }
| REAL { LTreal }
| BOOLEAN { LTnamed (Utf8_logic.boolean,[]) }
@@ -889,62 +863,62 @@ type_spec:
| FLOAT { LTfloat FFloat }
| DOUBLE { LTfloat FDouble }
| LONG DOUBLE { LTfloat FLongDouble }
-| STRUCT exit_rt_type identifier_or_typename { LTstruct $3 }
-| ENUM exit_rt_type identifier_or_typename { LTenum $3 }
-| UNION exit_rt_type identifier_or_typename { LTunion $3 }
-| TYPENAME { LTnamed ($1,[]) }
-| TYPENAME LT enter_rt_type ne_logic_type_list GT exit_rt_type
- { LTnamed($1,$4) }
+| STRUCT id = identifier_or_typename_full { LTstruct id }
+| ENUM id = identifier_or_typename_full { LTenum id }
+| UNION id = identifier_or_typename_full { LTunion id }
+| name = tname { LTnamed (name,[]) }
+| name = tname LT prms = ne_logic_type_list(tname) GT { LTnamed(name,prms) }
;
-ne_logic_type_list:
-| logic_type { [$1] }
-| logic_type COMMA enter_rt_type ne_logic_type_list { $1 :: $4 }
-;
-
-/*** from annotations ***/
-
-full_lexpr:
-| enter_kw_c_mode lexpr exit_kw_c_mode { $2 }
+ne_logic_type_list(tname):
+| l = separated_nonempty_list(COMMA,logic_type_gen(tname)) { l }
;
full_identifier:
-| enter_kw_c_mode identifier exit_kw_c_mode { $2 }
-;
-
-full_identifier_or_typename:
-| enter_kw_c_mode identifier_or_typename exit_kw_c_mode { $2 }
-;
-
-full_parameters:
-| enter_kw_c_mode ne_parameters exit_kw_c_mode { $2 }
-;
-
-full_parameter:
-| enter_kw_c_mode parameter exit_kw_c_mode { $2 }
-;
-
-full_zones:
-| enter_kw_c_mode zones exit_kw_c_mode { $2 }
-;
-
-full_ne_zones:
-| enter_kw_c_mode ne_zones exit_kw_c_mode { $2 }
-;
-
-full_ne_lexpr_list:
-enter_kw_c_mode ne_lexpr_list exit_kw_c_mode { $2 }
-;
-
-full_logic_type:
-| enter_kw_c_mode logic_type exit_kw_c_mode { $2 }
-;
-
-full_logic_rt_type:
-| enter_kw_c_mode logic_rt_type exit_kw_c_mode { $2 }
-
-full_assigns:
-| enter_kw_c_mode assigns exit_kw_c_mode { $2 }
+| id = identifier { id }
+| ADMIT { "admit" }
+| ALLOCATES { "allocates" }
+| ASSERT { "assert" }
+| ASSIGNS { "assigns" }
+| ASSUMES { "assumes" }
+| EXT_AT { "at" }
+| AXIOM { "axiom" }
+| AXIOMATIC { "axiomatic" }
+| BEHAVIOR { "behavior" }
+| BREAKS { "breaks" }
+| CHECK { "check" }
+| COMPLETE { "complete" }
+| CONTINUES { "continues" }
+| CONTRACT { "contract" }
+| DECREASES { "decreases" }
+| DISJOINT { "disjoint" }
+| ENSURES { "ensures" }
+| EXITS { "exits" }
+| FREES { "frees" }
+| FUNCTION { "function" }
+| GLOBAL { "global" }
+| IMPACT { "impact" }
+| INDUCTIVE { "inductive" }
+| INCLUDE { "include" }
+| INVARIANT { "invariant" }
+| LEMMA { "lemma" }
+| EXT_LET { "let" }
+| LOGIC { "logic" }
+| LOOP { "loop" }
+| MODEL { "model" }
+| MODULE { "module" }
+| PRAGMA { "pragma" }
+| PREDICATE { "predicate" }
+| REQUIRES { "requires" }
+| RETURNS { "returns" }
+| SLICE { "slice" }
+| TERMINATES { "terminates" }
+| TYPE { "type" }
+| VARIANT { "variant" }
+| id = EXT_CODE_ANNOT { id }
+| id = EXT_CONTRACT { id }
+| id = EXT_GLOBAL { id }
+| id = EXT_GLOBAL_BLOCK { id }
;
/*** ACSL extension for external spec file ***/
@@ -964,10 +938,10 @@ ext_global_clauses:
;
ext_global_clause:
-| decl { Ext_decl (loc_decl $1) }
-| EXT_LET any_identifier EQUAL full_lexpr SEMICOLON { Ext_macro (false, $2, $4) }
-| GLOBAL EXT_LET any_identifier EQUAL full_lexpr SEMICOLON { Ext_macro (true, $3, $5) }
-| INCLUDE string SEMICOLON { let b,s = $2 in Ext_include(b,s, loc()) }
+| decl { Ext_decl (loc_decl $sloc $1) }
+| EXT_LET any_identifier EQUAL lexpr SEMICOLON { Ext_macro (false, $2, $4) }
+| GLOBAL EXT_LET any_identifier EQUAL lexpr SEMICOLON { Ext_macro (true, $3, $5) }
+| INCLUDE string SEMICOLON { let b,s = $2 in Ext_include(b,s, loc $sloc) }
;
ext_global_specs_opt:
@@ -1026,7 +1000,7 @@ ext_fun_specs:
ext_fun_spec:
| ext_at_stmt_markup ext_stmt_loop_spec
- { Ext_stmt($1,$2,loc()) }
+ { Ext_stmt($1,$2,loc $sloc) }
| ext_contract_markup contract
{ let s,pos = $2 in Ext_spec (s,pos) }
;
@@ -1050,7 +1024,7 @@ ext_module_markup:
;
ext_function_markup:
-| FUNCTION ext_identifier COLON { $2, loc() }
+| FUNCTION ext_identifier COLON { $2, loc $sloc }
;
ext_contract_markup:
@@ -1094,54 +1068,54 @@ contract:
else if $2<>None || $3<>None ||
behaviors<>[] || completes<>[] ||disjoints<>[]
then behaviors
- else raise (Not_well_formed (loc(),"Empty annotation is not allowed"))
+ else raise (Not_well_formed (loc $sloc,"Empty annotation is not allowed"))
in
{ spec_terminates = $2;
spec_variant = $3;
spec_behavior = behaviors;
spec_complete_behaviors = completes;
spec_disjoint_behaviors = disjoints;
- }, loc()
+ }, loc $sloc
}
-| requires ne_terminates REQUIRES { clause_order 3 "requires" "terminates" }
+| requires ne_terminates REQUIRES { clause_order $loc($3) "requires" "terminates" }
| requires terminates ne_decreases REQUIRES
- { clause_order 4 "requires" "decreases" }
+ { clause_order $loc($4) "requires" "decreases" }
| requires terminates ne_decreases TERMINATES
- { clause_order 4 "terminates" "decreases" }
+ { clause_order $loc($4) "terminates" "decreases" }
| requires terminates decreases ne_simple_clauses REQUIRES
- { clause_order 5 "requires" "post-condition, assigns or allocates" }
+ { clause_order $loc($5) "requires" "post-condition, assigns or allocates" }
| requires terminates decreases ne_simple_clauses TERMINATES
- { clause_order 5 "terminates" "post-condition, assigns or allocates" }
+ { clause_order $loc($5) "terminates" "post-condition, assigns or allocates" }
| requires terminates decreases ne_simple_clauses DECREASES
- { clause_order 5 "decreases" "post-condition, assigns or allocates" }
+ { clause_order $loc($5) "decreases" "post-condition, assigns or allocates" }
| requires terminates decreases simple_clauses ne_behaviors TERMINATES
- { clause_order 6 "terminates" "behavior" }
+ { clause_order $loc($6) "terminates" "behavior" }
| requires terminates decreases simple_clauses ne_behaviors DECREASES
- { clause_order 6 "decreases" "behavior" }
+ { clause_order $loc($6) "decreases" "behavior" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
REQUIRES
- { clause_order 7 "requires" "complete or disjoint" }
+ { clause_order $loc($7) "requires" "complete or disjoint" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
TERMINATES
- { clause_order 7 "terminates" "complete or disjoint" }
+ { clause_order $loc($7) "terminates" "complete or disjoint" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
DECREASES
- { clause_order 7 "decreases" "complete or disjoint" }
+ { clause_order $loc($7) "decreases" "complete or disjoint" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
BEHAVIOR
- { clause_order 7 "behavior" "complete or disjoint" }
+ { clause_order $loc($7) "behavior" "complete or disjoint" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
ASSIGNS
- { clause_order 7 "assigns" "complete or disjoint" }
+ { clause_order $loc($7) "assigns" "complete or disjoint" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
ALLOCATES
- { clause_order 7 "allocates" "complete or disjoint" }
+ { clause_order $loc($7) "allocates" "complete or disjoint" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
FREES
- { clause_order 7 "frees" "complete or disjoint" }
+ { clause_order $loc($7) "frees" "complete or disjoint" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
post_cond_kind
- { clause_order 7 "post-condition" "complete or disjoint" }
+ { clause_order $loc($7) "post-condition" "complete or disjoint" }
;
// use that to detect potentially missing ';' at end of clause
@@ -1164,9 +1138,6 @@ clause_kw:
| FREES {"frees"}
| COMPLETE {"complete"}
| DISJOINT {"disjoint"}
-/* often, we'll be in c_kw_mode, where these keywords are
- recognized as identifiers... */
-| IDENTIFIER { $1 }
| EXT_CONTRACT { $1 }
| EOF { "end of annotation" }
;
@@ -1177,22 +1148,22 @@ requires:
;
ne_requires:
-| REQUIRES full_lexpr SEMICOLON requires { toplevel_pred Assert $2::$4 }
-| CHECK_REQUIRES full_lexpr SEMICOLON requires { toplevel_pred Check $2 :: $4 }
-| ADMIT_REQUIRES full_lexpr SEMICOLON requires { toplevel_pred Admit $2 :: $4 }
-| REQUIRES full_lexpr clause_kw { missing 2 ";" $3 }
-| CHECK_REQUIRES full_lexpr clause_kw { missing 2 ";" $3 }
-| ADMIT_REQUIRES full_lexpr clause_kw { missing 2 ";" $3 }
+| REQUIRES lexpr SEMICOLON requires { toplevel_pred Assert $2::$4 }
+| CHECK_REQUIRES lexpr SEMICOLON requires { toplevel_pred Check $2 :: $4 }
+| ADMIT_REQUIRES lexpr SEMICOLON requires { toplevel_pred Admit $2 :: $4 }
+| REQUIRES lexpr clause_kw { missing $loc($2) ";" $3 }
+| CHECK_REQUIRES lexpr clause_kw { missing $loc($2) ";" $3 }
+| ADMIT_REQUIRES lexpr clause_kw { missing $loc($2) ";" $3 }
;
terminates:
-| /* epsilon */ { None }
+| /* epsilon */ { None }
| ne_terminates { Some $1 }
;
ne_terminates:
-| TERMINATES full_lexpr SEMICOLON { $2 }
-| TERMINATES full_lexpr clause_kw { missing 2 ";" $3 }
+| TERMINATES lexpr SEMICOLON { $2 }
+| TERMINATES lexpr clause_kw { missing $loc($2) ";" $3 }
;
decreases:
@@ -1202,12 +1173,12 @@ decreases:
ne_decreases:
| DECREASES variant SEMICOLON { $2 }
-| DECREASES variant clause_kw { missing 2 ";" $3 }
+| DECREASES variant clause_kw { missing $loc($2) ";" $3 }
;
variant:
-| full_lexpr FOR any_identifier { ($1, Some $3) }
-| full_lexpr { ($1, None) }
+| lexpr FOR any_identifier { ($1, Some $3) }
+| lexpr { ($1, None) }
;
simple_clauses:
@@ -1216,11 +1187,11 @@ simple_clauses:
;
allocation:
-| ALLOCATES full_zones { FreeAlloc([],$2) }
-| FREES full_zones { FreeAlloc($2,[]) }
+| ALLOCATES zones { FreeAlloc([],$2) }
+| FREES zones { FreeAlloc($2,[]) }
ne_simple_clauses:
-| post_cond_kind full_lexpr SEMICOLON simple_clauses
+| post_cond_kind lexpr SEMICOLON simple_clauses
{ let tp_kind, kind = $1 in
let allocation,assigns,post_cond,extended = $4 in
allocation,assigns,
@@ -1230,31 +1201,27 @@ ne_simple_clauses:
let a = concat_allocation allocation $1 in
a,assigns,post_cond,extended
}
-| ASSIGNS full_assigns SEMICOLON simple_clauses
+| ASSIGNS assigns SEMICOLON simple_clauses
{ let allocation,assigns,post_cond,extended = $4 in
- let a = concat_assigns assigns $2
+ let a = concat_assigns $sloc assigns $2
in allocation,a,post_cond,extended
}
-| EXT_CONTRACT grammar_extension SEMICOLON simple_clauses
+| EXT_CONTRACT extension_content SEMICOLON simple_clauses
{ let allocation,assigns,post_cond,extended = $4 in
let processed = Logic_env.preprocess_extension $1 $2 in
allocation,assigns,post_cond,($1,processed)::extended
}
-| post_cond_kind full_lexpr clause_kw { missing 2 ";" $3 }
-| allocation clause_kw { missing 1 ";" $2 }
-| ASSIGNS full_assigns clause_kw { missing 2 ";" $3 }
-| EXT_CONTRACT ne_grammar_extension clause_kw { missing 1 ";" $3 }
+| post_cond_kind lexpr clause_kw { missing $loc($2) ";" $3 }
+| allocation clause_kw { missing $loc($1) ";" $2 }
+| ASSIGNS assigns clause_kw { missing $loc($2) ";" $3 }
+| EXT_CONTRACT ne_grammar_extension clause_kw { missing $loc($1) ";" $3 }
;
ne_grammar_extension:
-| full_zones { $1 }
+| zones { $1 }
;
/* possibly empty list of terms, for ACSL extensions registered by plugins. */
-grammar_extension:
-| enter_kw_c_mode extension_content exit_kw_c_mode { $2 }
-;
-
extension_content:
| /* epsilon */ { [] }
| zones { $1 }
@@ -1278,21 +1245,22 @@ ne_behaviors:
~assumes ~requires ~post_cond ~assigns ~allocation ~extended ()
in b::behaviors
}
+;
behavior_body:
| assumes requires simple_clauses { $1,$2,$3 }
| assumes ne_requires ASSUMES
- { clause_order 3 "assumes" "requires" }
+ { clause_order $loc($3) "assumes" "requires" }
| assumes requires ne_simple_clauses ASSUMES
- { clause_order 4 "assumes" "assigns or post-condition" }
+ { clause_order $loc($4) "assumes" "assigns or post-condition" }
| assumes requires ne_simple_clauses REQUIRES
- { clause_order 4 "requires" "assigns or post-condition" }
+ { clause_order $loc($4) "requires" "assigns or post-condition" }
;
assumes:
| /* epsilon */ { [] }
-| ASSUMES full_lexpr SEMICOLON assumes { $2::$4 }
-| ASSUMES full_lexpr clause_kw { missing 2 ";" $3 }
+| ASSUMES lexpr SEMICOLON assumes { $2::$4 }
+| ASSUMES lexpr clause_kw { missing $loc($2) ";" $3 }
;
complete_or_disjoint:
@@ -1309,8 +1277,8 @@ ne_complete_or_disjoint:
/* complete behaviors decreases; is valid (provided there's a behavior
named decreases)
*/
-| COMPLETE BEHAVIORS ne_behavior_name_list clause_kw { missing 3 ";" $4 }
-| DISJOINT BEHAVIORS ne_behavior_name_list clause_kw { missing 3 ";" $4 }
+| COMPLETE BEHAVIORS ne_behavior_name_list clause_kw { missing $loc($3) ";" $4 }
+| DISJOINT BEHAVIORS ne_behavior_name_list clause_kw { missing $loc($3) ";" $4 }
;
/*** assigns and tsets ***/
@@ -1342,23 +1310,23 @@ annotation:
{ let (b,v,p) = $1 in
(* TODO: do better, do not lose the structure ! *)
let l = b@v@p in
- Aloop_annot (loc (), l) }
+ Aloop_annot (loc $sloc, l) }
| FOR ne_behavior_name_list COLON contract_or_code_annotation
{ $4 $2 }
-| pragma_or_code_annotation { Acode_annot (loc(),$1) }
+| pragma_or_code_annotation { Acode_annot (loc $sloc,$1) }
| pragma_or_code_annotation beg_pragma_or_code_annotation
{ raise
- (Not_well_formed (loc(),
+ (Not_well_formed (loc $sloc,
"Only one code annotation is allowed per comment"))
}
-| full_identifier_or_typename { Aattribute_annot (loc (), $1) }
-| BSGHOST { Aattribute_annot(loc(),"\\ghost") }
+| identifier { Aattribute_annot (loc $sloc, $1) }
+| BSGHOST { Aattribute_annot(loc $sloc,"\\ghost") }
;
contract_or_code_annotation:
| contract
{ fun bhvs -> let s, pos = $1 in Acode_annot (pos, AStmtSpec (bhvs,s)) }
-| code_annotation { fun bhvs -> Acode_annot (loc(), ($1 bhvs)) }
+| code_annotation { fun bhvs -> Acode_annot (loc $sloc, ($1 bhvs)) }
;
/*** loop annotations ***/
@@ -1388,7 +1356,7 @@ loop_annot_stack:
| loop_invariant loop_annot_opt
{ let (i,fa,a,b,v,p,e) = $2 in ($1::i,fa,a,b,v,p,e) }
| loop_effects loop_annot_opt
- { let (i,fa,a,b,v,p,e) = $2 in (i,fa,concat_assigns a $1,b,v,p,e) }
+ { let (i,fa,a,b,v,p,e) = $2 in (i,fa,concat_assigns $sloc a $1,b,v,p,e) }
| loop_allocation loop_annot_opt
{ let (i,fa,a,b,v,p,e) = $2 in (i,concat_allocation fa $1,a,b,v,p,e) }
| FOR ne_behavior_name_list COLON loop_annot_stack
@@ -1396,7 +1364,7 @@ loop_annot_stack:
let behav = $2 in
let invs = List.map (fun i -> AInvariant(behav,true,i)) i in
let ext = List.map (fun x -> AExtended(behav,true,x)) e in
- let oth = concat_loop_assigns_allocation b behav a fa in
+ let oth = concat_loop_assigns_allocation $sloc b behav a fa in
([],FreeAllocAny,WritesAny,invs@ext@oth,v,p,[])
}
| loop_variant loop_annot_opt
@@ -1440,7 +1408,7 @@ loop_annot_opt:
;
loop_effects:
-| LOOP ASSIGNS full_assigns SEMICOLON { $3 }
+| LOOP ASSIGNS assigns SEMICOLON { $3 }
;
loop_allocation:
@@ -1448,18 +1416,18 @@ loop_allocation:
;
loop_invariant:
-| LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred Assert $3 }
-| CHECK_LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred Check $3 }
-| ADMIT_LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred Admit $3 }
+| LOOP INVARIANT lexpr SEMICOLON { toplevel_pred Assert $3 }
+| CHECK_LOOP INVARIANT lexpr SEMICOLON { toplevel_pred Check $3 }
+| ADMIT_LOOP INVARIANT lexpr SEMICOLON { toplevel_pred Admit $3 }
;
loop_variant:
-| LOOP VARIANT variant SEMICOLON { loc(),$3 }
+| LOOP VARIANT variant SEMICOLON { loc $sloc,$3 }
;
/* Grammar Extensibility for plugins */
loop_grammar_extension:
-| LOOP EXT_CODE_ANNOT grammar_extension SEMICOLON {
+| LOOP EXT_CODE_ANNOT extension_content SEMICOLON {
let open Cil_types in
let ext = $2 in
try
@@ -1470,17 +1438,17 @@ loop_grammar_extension:
| Ext_code_annot (Ext_here | Ext_next_stmt) ->
raise
(Not_well_formed
- (lexeme_loc 2, ext ^ " is not a loop annotation extension"))
+ (loc $loc($2), ext ^ " is not a loop annotation extension"))
| _ -> raise Not_found
end
with Not_found ->
- Kernel.fatal ~source:(lexeme_start 2)
+ Kernel.fatal ~source:(pos $startpos($2))
"%s is not a code annotation extension. Parser got wrong lexeme." ext
}
;
loop_pragma:
-| LOOP PRAGMA any_identifier full_ne_lexpr_list SEMICOLON
+| LOOP PRAGMA any_identifier ne_lexpr_list SEMICOLON
{ if $3 = "UNROLL_LOOP" || $3 = "UNROLL" then
(if $3 <> "UNROLL" then
Format.eprintf "Warning: use of deprecated keyword '%s'.\nShould use 'UNROLL' instead.@." $3;
@@ -1489,7 +1457,7 @@ loop_pragma:
Widen_variables $4
else if $3 = "WIDEN_HINTS" then
Widen_hints $4
- else raise (Not_well_formed (loc(),"Unknown loop pragma")) }
+ else raise (Not_well_formed (loc $sloc,"Unknown loop pragma")) }
;
/*** code annotations ***/
@@ -1516,19 +1484,19 @@ pragma_or_code_annotation:
;
code_annotation:
-| ASSERT full_lexpr SEMICOLON
+| ASSERT lexpr SEMICOLON
{ fun bhvs -> AAssert (bhvs,toplevel_pred Assert $2) }
-| CHECK full_lexpr SEMICOLON
+| CHECK lexpr SEMICOLON
{ fun bhvs -> AAssert (bhvs,toplevel_pred Check $2) }
-| ADMIT full_lexpr SEMICOLON
+| ADMIT lexpr SEMICOLON
{ fun bhvs -> AAssert (bhvs,toplevel_pred Admit $2) }
-| INVARIANT full_lexpr SEMICOLON
+| INVARIANT lexpr SEMICOLON
{ fun bhvs -> AInvariant (bhvs,false,toplevel_pred Assert $2) }
-| CHECK_INVARIANT full_lexpr SEMICOLON
+| CHECK_INVARIANT lexpr SEMICOLON
{ fun bhvs -> AInvariant (bhvs,false,toplevel_pred Check $2) }
-| ADMIT_INVARIANT full_lexpr SEMICOLON
+| ADMIT_INVARIANT lexpr SEMICOLON
{ fun bhvs -> AInvariant (bhvs,false,toplevel_pred Admit $2) }
-| EXT_CODE_ANNOT grammar_extension SEMICOLON
+| EXT_CODE_ANNOT extension_content SEMICOLON
{ fun bhvs ->
let open Cil_types in
let ext = $1 in
@@ -1540,46 +1508,47 @@ code_annotation:
| Ext_code_annot Ext_next_loop ->
raise
(Not_well_formed
- (lexeme_loc 1,
+ (loc $loc($1),
ext ^ " is not a loop annotation extension. It can't be used \
as plain code annotation extension"))
| _ -> raise Not_found
end
with Not_found ->
- Kernel.fatal ~source:(lexeme_start 1)
+ Kernel.fatal ~source:(pos $startpos($1))
"%s is not a code annotation extension. Parser got wrong lexeme" ext
}
;
slice_pragma:
-| SLICE PRAGMA any_identifier full_lexpr SEMICOLON
+| SLICE PRAGMA any_identifier lexpr SEMICOLON
{ if $3 = "expr" then SPexpr $4
- else raise (Not_well_formed (loc(), "Unknown slice pragma")) }
+ else raise (Not_well_formed (loc $sloc, "Unknown slice pragma")) }
| SLICE PRAGMA any_identifier SEMICOLON
{ if $3 = "ctrl" then SPctrl
else if $3 = "stmt" then SPstmt
- else raise (Not_well_formed (loc(), "Unknown slice pragma")) }
+ else raise (Not_well_formed (loc $sloc, "Unknown slice pragma")) }
;
impact_pragma:
-| IMPACT PRAGMA any_identifier full_lexpr SEMICOLON
+| IMPACT PRAGMA any_identifier lexpr SEMICOLON
{ if $3 = "expr" then IPexpr $4
- else raise (Not_well_formed (loc(), "Unknown impact pragma")) }
+ else raise (Not_well_formed (loc $sloc, "Unknown impact pragma")) }
| IMPACT PRAGMA any_identifier SEMICOLON
{ if $3 = "stmt" then IPstmt
- else raise (Not_well_formed (loc(), "Unknown impact pragma")) }
+ else raise (Not_well_formed (loc $sloc, "Unknown impact pragma")) }
;
/*** declarations and logical definitions ***/
decl_list:
-| decl { [loc_decl $1] }
-| decl decl_list { (loc_decl $1) :: $2 }
+| decl { [loc_decl $sloc $1] }
+| decl decl_list { (loc_decl $loc($1) $1) :: $2 }
+;
decl:
-| GLOBAL INVARIANT any_identifier COLON full_lexpr SEMICOLON
+| GLOBAL INVARIANT any_identifier COLON lexpr SEMICOLON
{ LDinvariant ($3, $5) }
-| VOLATILE full_ne_zones volatile_opt SEMICOLON { LDvolatile ($2, $3) }
+| VOLATILE ne_zones volatile_opt SEMICOLON { LDvolatile ($2, $3) }
| type_annot {LDtype_annot $1}
| model_annot {LDmodel_annot $1}
| logic_def { $1 }
@@ -1588,7 +1557,7 @@ decl:
;
ext_decl:
-| EXT_GLOBAL grammar_extension SEMICOLON {
+| EXT_GLOBAL extension_content SEMICOLON {
let processed = Logic_env.preprocess_extension $1 $2 in
Ext_lexpr($1, processed)
}
@@ -1608,7 +1577,7 @@ ext_decls:
;
ext_decl_loc:
-| ext_decl { loc_ext $1 }
+| ext_decl { loc_ext $sloc $1 }
;
volatile_opt:
@@ -1630,17 +1599,18 @@ volatile_opt:
;
type_annot:
-| TYPE INVARIANT any_identifier LPAR full_parameter RPAR EQUAL
- full_lexpr SEMICOLON
+| TYPE INVARIANT any_identifier LPAR parameter RPAR EQUAL
+ lexpr SEMICOLON
{ let typ,name = $5 in{ inv_name = $3; this_name = name; this_type = typ; inv = $8; } }
;
opt_semicolon:
| /* epsilon */ { }
| SEMICOLON { }
+;
model_annot:
-| MODEL type_spec LBRACE full_parameter opt_semicolon RBRACE SEMICOLON
+| MODEL type_spec(typename) LBRACE parameter opt_semicolon RBRACE SEMICOLON
{ let typ,name = $4 in
{ model_for_type = $2; model_name = name; model_type = typ; }
}
@@ -1674,17 +1644,17 @@ opt_parameters:
;
parameters:
-| LPAR full_parameters RPAR { $2 }
+| LPAR ne_parameters RPAR { $2 }
;
logic_def:
/* logic function definition */
-| LOGIC full_logic_rt_type poly_id opt_parameters EQUAL full_lexpr SEMICOLON
+| LOGIC logic_rt_type poly_id opt_parameters EQUAL lexpr SEMICOLON
{ let (id, labels, tvars) = $3 in
exit_type_variables_scope ();
LDlogic_def (id, labels, tvars, $2, $4, $6) }
/* predicate definition */
-| PREDICATE poly_id opt_parameters EQUAL full_lexpr SEMICOLON
+| PREDICATE poly_id opt_parameters EQUAL lexpr SEMICOLON
{ let (id,labels,tvars) = $2 in
exit_type_variables_scope ();
LDpredicate_def (id, labels, tvars, $3, $5) }
@@ -1693,15 +1663,15 @@ logic_def:
{ let (id,labels,tvars) = $2 in
exit_type_variables_scope ();
LDinductive_def(id, labels, tvars, $3, $5) }
-| LEMMA poly_id COLON full_lexpr SEMICOLON
+| LEMMA poly_id COLON lexpr SEMICOLON
{ let (id,labels,tvars) = $2 in
exit_type_variables_scope ();
LDlemma (id, labels, tvars, toplevel_pred Assert $4) }
-| CHECK_LEMMA poly_id COLON full_lexpr SEMICOLON
+| CHECK_LEMMA poly_id COLON lexpr SEMICOLON
{ let (id,labels,tvars) = $2 in
exit_type_variables_scope ();
LDlemma (id, labels, tvars, toplevel_pred Check $4) }
-| ADMIT_LEMMA poly_id COLON full_lexpr SEMICOLON
+| ADMIT_LEMMA poly_id COLON lexpr SEMICOLON
{ let (id,labels,tvars) = $2 in
exit_type_variables_scope ();
LDlemma (id, labels, tvars, toplevel_pred Admit $4) }
@@ -1716,9 +1686,9 @@ logic_def:
deprecated_logic_decl:
/* OBSOLETE: logic function declaration */
-| LOGIC full_logic_rt_type poly_id opt_parameters SEMICOLON
+| LOGIC logic_rt_type poly_id opt_parameters SEMICOLON
{ let (id, labels, tvars) = $3 in
- let source = fst (loc ()) in
+ let source = pos $symbolstartpos in
exit_type_variables_scope ();
obsolete "logic declaration" ~source ~now:"an axiomatic block";
LDlogic_reads (id, labels, tvars, $2, $4, None) }
@@ -1726,7 +1696,7 @@ deprecated_logic_decl:
| PREDICATE poly_id opt_parameters SEMICOLON
{ let (id,labels,tvars) = $2 in
exit_type_variables_scope ();
- let source = fst (loc ()) in
+ let source = pos $symbolstartpos in
obsolete "logic declaration" ~source ~now:"an axiomatic block";
LDpredicate_reads (id, labels, tvars, $3, None) }
/* OBSOLETE: type declaration */
@@ -1734,16 +1704,16 @@ deprecated_logic_decl:
{ let (id,tvars) = $2 in
Logic_env.add_typename id;
exit_type_variables_scope ();
- let source = fst (loc ()) in
+ let source = pos $symbolstartpos in
obsolete "logic type declaration" ~source ~now:"an axiomatic block";
LDtype(id,tvars,None)
}
/* OBSOLETE: axiom */
-| AXIOM poly_id COLON full_lexpr SEMICOLON
+| AXIOM poly_id COLON lexpr SEMICOLON
{ let (id,_,_) = $2 in
raise
(Not_well_formed
- (loc(),"Axiom " ^ id ^ " is declared outside of an axiomatic."))
+ (loc $sloc,"Axiom " ^ id ^ " is declared outside of an axiomatic."))
}
;
@@ -1758,7 +1728,7 @@ logic_decls:
logic_decl:
| logic_def { $1 }
/* logic function declaration */
-| LOGIC full_logic_rt_type poly_id opt_parameters reads_clause SEMICOLON
+| LOGIC logic_rt_type poly_id opt_parameters reads_clause SEMICOLON
{ let (id, labels, tvars) = $3 in
exit_type_variables_scope ();
LDlogic_reads (id, labels, tvars, $2, $4, $5) }
@@ -1774,25 +1744,25 @@ logic_decl:
exit_type_variables_scope ();
LDtype(id,tvars,None) }
/* axiom */
-| AXIOM poly_id COLON full_lexpr SEMICOLON
+| AXIOM poly_id COLON lexpr SEMICOLON
{ let (id,labels,tvars) = $2 in
exit_type_variables_scope ();
LDlemma (id, labels, tvars, toplevel_pred Admit $4) }
;
logic_decl_loc:
-| logic_decl { loc_decl $1 }
+| logic_decl { loc_decl $sloc $1 }
;
reads_clause:
| /* epsilon */ { None }
-| READS full_zones { Some $2 }
+| READS zones { Some $2 }
;
typedef:
| ne_datacons_list { TDsum $1 }
-| full_logic_type { TDsyn $1 }
+| logic_type { TDsyn $1 }
;
datacons_list:
@@ -1811,13 +1781,13 @@ datacons:
;
ne_type_list:
-| full_logic_type { [$1] }
-| full_logic_type COMMA ne_type_list { $1::$3 }
+| logic_type { [$1] }
+| logic_type COMMA ne_type_list { $1::$3 }
indcases:
| /* epsilon */
{ [] }
-| CASE poly_id COLON full_lexpr SEMICOLON indcases
+| CASE poly_id COLON lexpr SEMICOLON indcases
{ let (id,labels,tvars) = $2 in
exit_type_variables_scope ();
(id,labels,tvars,$4)::$6 }
@@ -1838,15 +1808,15 @@ opt_label_1:
| opt_label_list { match $1 with
| [] -> None
| l::[] -> Some l
- | _ -> raise (Not_well_formed (loc(),"Only one label is allowed")) }
+ | _ -> raise (Not_well_formed (loc $sloc,"Only one label is allowed")) }
;
opt_label_2:
| opt_label_list { match $1 with
| [] -> None
| l1::l2::[] -> Some (l1,l2)
- | _::[] -> raise (Not_well_formed (loc(),"One label is missing"))
- | _ -> raise (Not_well_formed (loc(),"Only two labels are allowed")) }
+ | _::[] -> raise (Not_well_formed (loc $sloc,"One label is missing"))
+ | _ -> raise (Not_well_formed (loc $sloc,"Only two labels are allowed")) }
;
opt_label_list:
@@ -1874,19 +1844,20 @@ behavior_name:
;
any_identifier:
-| identifier_or_typename { $1 }
+| identifier { $1 }
+| is_acsl_typename { $1 }
+| TYPENAME { $1 }
| keyword { $1 }
;
-identifier_or_typename: /* allowed as C field names */
+identifier_or_typename:
+| TYPENAME { $1 }
+| full_identifier { $1 }
+
+
+identifier_or_typename_full: /* allowed as C field names */
| is_acsl_typename { $1 }
-| TYPENAME { $1 } /* followed by the same list than 'identifier' */
-| IDENTIFIER { $1 }
-/* token list used inside acsl clauses: */
-| BEHAVIORS { "behaviors" }
-| LABEL { "label" }
-| READS { "reads" }
-| WRITES { "writes" }
+| identifier_or_typename { $1 }
;
identifier: /* part included into 'identifier_or_typename', but duplicated to avoid parsing conflicts */
@@ -1899,15 +1870,15 @@ identifier: /* part included into 'identifier_or_typename', but duplicated to av
;
bounded_var:
-| identifier { $1 }
+| full_identifier { $1 }
| is_acsl_typename /* Since TYPENAME cannot be accepted by lexpr rule */
{ raise
- (Not_well_formed(loc (),
+ (Not_well_formed(loc $sloc,
"Type names are not allowed as binding variable"))
}
| TYPENAME /* Since TYPENAME cannot be accepted by lexpr rule */
{ raise
- (Not_well_formed(loc (),
+ (Not_well_formed(loc $sloc,
"Type names are not allowed as binding variable"))
}
;
diff --git a/src/kernel_internals/parsing/tests/check_logic_parser.ml b/src/kernel_internals/parsing/tests/check_logic_parser.ml
index 7f6c9593da02981a51c698e0eaba009421b288d1..8435c5578611286dc8a5dd42015f84e1913f0fd7 100644
--- a/src/kernel_internals/parsing/tests/check_logic_parser.ml
+++ b/src/kernel_internals/parsing/tests/check_logic_parser.ml
@@ -73,12 +73,21 @@ let add_tokens s =
in add_token s
let wildcard_rules =
- [ "bs_keyword"; "wildcard"; "keyword"; "c_keyword";
- "non_logic_keyword"; "acsl_c_keyword"; "is_ext_spec";
+ [ "acsl_c_keyword";
+ "any_identifier";
+ "bs_keyword";
+ "c_keyword";
+ "identifier";
+ "identifier_or_typename";
+ "is_acsl_decl_or_code_annot";
+ "is_acsl_other";
+ "is_acsl_spec";
"is_acsl_typename";
- "is_acsl_spec"; "is_acsl_decl_or_code_annot";
- "is_acsl_other"; "post_cond";
- "identifier_or_typename"
+ "is_ext_spec";
+ "keyword";
+ "non_logic_keyword";
+ "post_cond";
+ "wildcard";
]
let find_rule_name s =
diff --git a/src/kernel_internals/parsing/tests/dune b/src/kernel_internals/parsing/tests/dune
index ba23e4861fb5a8289dc4e7fc5a1ae2af05299163..d77efd63c875dc4d3dd43be7f7f4ed3cb0997954 100644
--- a/src/kernel_internals/parsing/tests/dune
+++ b/src/kernel_internals/parsing/tests/dune
@@ -28,11 +28,11 @@
)
(rule
- (alias run-coding-tests)
+ (alias run-kernel-tests)
(deps ../logic_parser.mly)
(action (run %{dep:./check_logic_parser.exe})))
(alias
- (deps (alias run-coding-tests) )
+ (deps (alias run-kernel-tests) )
(name ptests)
)
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 06ea9e8192ac0a83de4cf26b18d79c885963b8ea..0af75114af3d582931d53b4b77dd12730b333c34 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -2362,38 +2362,6 @@ class complete_types =
let complete_types f = Cil.visitCilFile (new complete_types) f
-(* ************************************************************************* *)
-(** {2 Parsing utilities} *)
-(* ************************************************************************* *)
-
-(** Hack to allow typedefs whose names are ACSL keywords: the state of the
- lexer depends on the parser rule. See logic_lexer.mll and
- logic_parser.mly for more details. *)
-
-(**
- - false => keywords are all ACSL keywords
- - true => only C keywords are recognized as such.
- (other remains plain identifiers/typenames)
-*)
-let kw_c_mode = ref false
-
-let enter_kw_c_mode () = kw_c_mode := true
-
-let exit_kw_c_mode () = kw_c_mode := false
-
-let is_kw_c_mode () = !kw_c_mode
-
-let rt_type_mode = ref false
-
-(** enter a mode where any identifier is considered a type name. Needed for
- for return type of a logic function, as the list of admissible variables
- will be known afterwards. *)
-let enter_rt_type_mode () = rt_type_mode:=true
-
-let exit_rt_type_mode () = rt_type_mode:=false
-
-let is_rt_type_mode () = !rt_type_mode
-
let pointer_comparable ?loc t1 t2 =
let preds = Logic_env.find_all_logic_functions "\\pointer_comparable" in
let cfct_ptr = TPtr (TFun(Cil.voidType,None,false,[]),[]) in
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index c1df4b07514bb6cb767675155981b9a7fc376c74..1e94484c56da83f416155892b65fd691c73a0069 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -491,20 +491,6 @@ class simplify_const_lval: (varinfo -> init option) -> Cil.cilVisitor
@since Neon-20140301 *)
val complete_types: file -> unit
-(** {2 Parsing hackery} *)
-(** Values that control the various modes of the parser and lexer for logic.
- Use with care.
-*)
-
-val kw_c_mode : bool ref
-val enter_kw_c_mode : unit -> unit
-val exit_kw_c_mode : unit -> unit
-val is_kw_c_mode : unit -> bool
-val rt_type_mode : bool ref
-val enter_rt_type_mode : unit -> unit
-val exit_rt_type_mode : unit -> unit
-val is_rt_type_mode : unit -> bool
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/tests/spec/oracle/polymorph.res.oracle b/tests/spec/oracle/polymorph.res.oracle
index 0884261f3ea740425f4218ac742bc5fbef20b9df..983912ed0325cf0fb458343ef9e56fbf11e8df06 100644
--- a/tests/spec/oracle/polymorph.res.oracle
+++ b/tests/spec/oracle/polymorph.res.oracle
@@ -1,7 +1,8 @@
[kernel] Parsing polymorph.c (with preprocessing)
[kernel] polymorph.c:1: Warning:
parsing obsolete ACSL construct 'logic type declaration'. 'an axiomatic block' should be used instead.
-[kernel:annot-error] polymorph.c:4: Warning: unexpected token 'a'
+[kernel] polymorph.c:4: Warning:
+ parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[kernel] polymorph.c:6: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[kernel] polymorph.c:8: Warning:
@@ -10,6 +11,8 @@
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[kernel] polymorph.c:13: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
+[kernel:annot-error] polymorph.c:4: Warning:
+ no such type a. Ignoring global annotation
[kernel:annot-error] polymorph.c:13: Warning:
some type variable appears only in the return type. All type variables need to occur also in the parameters types.. Ignoring global annotation
[kernel:annot-error] polymorph.c:22: Warning: