From bfdbb20572ee1181e6b16fd86ccdb03c8c8e5bf5 Mon Sep 17 00:00:00 2001
From: Tristan Gingold <tgingold@free.fr>
Date: Wed, 16 Oct 2019 06:08:33 +0200
Subject: vhdl: check cover/restrict is followed by a sequence.
---
src/vhdl/vhdl-parse.adb | 4 ++--
src/vhdl/vhdl-parse_psl.adb | 56 ++++++++++++++++++++++++++++++++++++++-------
src/vhdl/vhdl-parse_psl.ads | 2 +-
src/vhdl/vhdl-sem_psl.adb | 14 ++++++++++++
4 files changed, 65 insertions(+), 11 deletions(-)
diff --git a/src/vhdl/vhdl-parse.adb b/src/vhdl/vhdl-parse.adb
index 1b498fbf1..3b5862922 100644
--- a/src/vhdl/vhdl-parse.adb
+++ b/src/vhdl/vhdl-parse.adb
@@ -8660,7 +8660,7 @@ package body Vhdl.Parse is
-- Skip 'cover'
Scan;
- Set_Psl_Sequence (Res, Parse_Psl.Parse_Psl_Sequence (True));
+ Set_Psl_Sequence (Res, Parse_Psl.Parse_Psl_Sequence);
Parse_Psl_Assert_Report_Severity (Res, Flag_Psl);
@@ -8679,7 +8679,7 @@ package body Vhdl.Parse is
-- Skip 'restrict'
Scan;
- Set_Psl_Sequence (Res, Parse_Psl.Parse_Psl_Sequence (True));
+ Set_Psl_Sequence (Res, Parse_Psl.Parse_Psl_Sequence);
-- No more PSL tokens after the sequence.
Vhdl.Scanner.Flag_Psl := Flag_Psl;
diff --git a/src/vhdl/vhdl-parse_psl.adb b/src/vhdl/vhdl-parse_psl.adb
index 956414e0f..004a4251d 100644
--- a/src/vhdl/vhdl-parse_psl.adb
+++ b/src/vhdl/vhdl-parse_psl.adb
@@ -127,6 +127,7 @@ package body Vhdl.Parse_Psl is
return Res;
end Vhdl_To_Psl;
+ function Parse_Psl_Sequence_Or_SERE (Full_Hdl_Expr : Boolean) return Node;
function Parse_FL_Property (Prio : Priority) return Node;
function Parse_Parenthesis_Boolean return Node;
function Parse_Boolean (Parent_Prio : Priority) return Node;
@@ -238,7 +239,7 @@ package body Vhdl.Parse_Psl is
Kind : Nkind;
Op_Prio : Priority;
begin
- Left := Parse_Psl_Sequence (True);
+ Left := Parse_Psl_Sequence_Or_SERE (True);
loop
case Current_Token is
when Tok_Semi_Colon =>
@@ -303,7 +304,8 @@ package body Vhdl.Parse_Psl is
end Parse_Braced_SERE;
-- Parse [ Count ] ']'
- function Parse_Maybe_Count (Kind : Nkind; Seq : Node) return Node is
+ function Parse_Maybe_Count (Kind : Nkind; Seq : Node) return Node
+ is
N : Node;
begin
N := Create_Node_Loc (Kind);
@@ -341,7 +343,8 @@ package body Vhdl.Parse_Psl is
end if;
end Parse_Bracket_Range;
- function Parse_Bracket_Number return Node is
+ function Parse_Bracket_Number return Node
+ is
Res : Node;
begin
if Current_Token /= Tok_Left_Bracket then
@@ -359,7 +362,8 @@ package body Vhdl.Parse_Psl is
end if;
end Parse_Bracket_Number;
- function Parse_Psl_Sequence (Full_Hdl_Expr : Boolean) return Node is
+ function Parse_Psl_Sequence_Or_SERE (Full_Hdl_Expr : Boolean) return Node
+ is
Res, N : Node;
begin
case Current_Token is
@@ -431,9 +435,45 @@ package body Vhdl.Parse_Psl is
end if;
Res := N;
when others =>
- return Res;
+ exit;
end case;
end loop;
+
+ return Res;
+ end Parse_Psl_Sequence_Or_SERE;
+
+ -- IEEE1850 A.4.7 Sequences
+ -- Sequence ::=
+ -- Sequence_Instance
+ -- | Repeated_SERE
+ -- | Braced_SERE
+ -- | Clocked_SERE
+ function Parse_Psl_Sequence return Node
+ is
+ Res : Node;
+ begin
+ Res := Parse_Psl_Sequence_Or_SERE (True);
+
+ -- May not be a sequence!
+ -- This test is also performed in sem_psl in order to fully handle
+ -- sequence_instance.
+ case Get_Kind (Res) is
+ when N_Star_Repeat_Seq
+ | N_Goto_Repeat_Seq
+ | N_Plus_Repeat_Seq
+ | N_Equal_Repeat_Seq
+ | N_Braced_SERE
+ | N_Clocked_SERE =>
+ null;
+ when N_HDL_Expr =>
+ -- Need to be checked later: can be a sequence instance or a
+ -- boolean.
+ null;
+ when others =>
+ Error_Msg_Parse ("sequence expected here");
+ end case;
+
+ return Res;
end Parse_Psl_Sequence;
-- precond: '('
@@ -567,7 +607,7 @@ package body Vhdl.Parse_Psl is
when Tok_Left_Paren =>
return Parse_Parenthesis_FL_Property;
when Tok_Left_Curly =>
- Res := Parse_Psl_Sequence (True);
+ Res := Parse_Psl_Sequence_Or_SERE (True);
if Get_Kind (Res) = N_Braced_SERE
and then Current_Token = Tok_Left_Paren
then
@@ -579,7 +619,7 @@ package body Vhdl.Parse_Psl is
Res := Tmp;
end if;
when others =>
- Res := Parse_Psl_Sequence (False);
+ Res := Parse_Psl_Sequence_Or_SERE (False);
end case;
return Res;
end Parse_FL_Property_1;
@@ -927,7 +967,7 @@ package body Vhdl.Parse_Psl is
Set_Property (Res, Parse_Psl_Property);
when N_Sequence_Declaration
| N_Endpoint_Declaration =>
- Set_Sequence (Res, Parse_Psl_Sequence (True));
+ Set_Sequence (Res, Parse_Psl_Sequence);
when others =>
raise Internal_Error;
end case;
diff --git a/src/vhdl/vhdl-parse_psl.ads b/src/vhdl/vhdl-parse_psl.ads
index f7128ac40..10446a0e1 100644
--- a/src/vhdl/vhdl-parse_psl.ads
+++ b/src/vhdl/vhdl-parse_psl.ads
@@ -20,7 +20,7 @@ with PSL.Types; use PSL.Types;
with Vhdl.Tokens; use Vhdl.Tokens;
package Vhdl.Parse_Psl is
- function Parse_Psl_Sequence (Full_Hdl_Expr : Boolean) return PSL_Node;
+ function Parse_Psl_Sequence return PSL_Node;
function Parse_Psl_Property return PSL_Node;
function Parse_Psl_Boolean return PSL_Node;
function Parse_Psl_Declaration (Tok : Token_Type) return PSL_Node;
diff --git a/src/vhdl/vhdl-sem_psl.adb b/src/vhdl/vhdl-sem_psl.adb
index bd8f98b13..4cdc834dd 100644
--- a/src/vhdl/vhdl-sem_psl.adb
+++ b/src/vhdl/vhdl-sem_psl.adb
@@ -758,6 +758,20 @@ package body Vhdl.Sem_Psl is
Seq := Get_Psl_Sequence (Stmt);
Seq := Sem_Sequence (Seq);
+ -- Expect a pure sequence.
+ case Get_Kind (Seq) is
+ when N_Sequence_Instance
+ | N_Star_Repeat_Seq
+ | N_Goto_Repeat_Seq
+ | N_Plus_Repeat_Seq
+ | N_Equal_Repeat_Seq
+ | N_Braced_SERE
+ | N_Clocked_SERE =>
+ null;
+ when others =>
+ Error_Msg_Sem (+Seq, "sequence expected here");
+ end case;
+
-- Properties must be clocked.
Sem_Psl_Directive_Clock (Stmt, Seq);
Set_Psl_Sequence (Stmt, Seq);
--
cgit v1.2.3