From f6451e539e5205105d2356c30a638e29305a493e Mon Sep 17 00:00:00 2001
From: Tristan Gingold <tgingold@free.fr>
Date: Sun, 29 Aug 2021 07:29:25 +0200
Subject: vhdl-canon: detect PSL assertion that cannot fail.  For #1832

---
 src/vhdl/vhdl-canon.adb | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'src/vhdl')

diff --git a/src/vhdl/vhdl-canon.adb b/src/vhdl/vhdl-canon.adb
index 97901145c..f93d66d52 100644
--- a/src/vhdl/vhdl-canon.adb
+++ b/src/vhdl/vhdl-canon.adb
@@ -14,11 +14,13 @@
 --  You should have received a copy of the GNU General Public License
 --  along with this program.  If not, see <gnu.org/licenses>.
 
-with Vhdl.Errors; use Vhdl.Errors;
-with Vhdl.Utils; use Vhdl.Utils;
 with Types; use Types;
 with Flags; use Flags;
 with Name_Table;
+with Errorout; use Errorout;
+
+with Vhdl.Errors; use Vhdl.Errors;
+with Vhdl.Utils; use Vhdl.Utils;
 with Vhdl.Sem;
 with Vhdl.Sem_Inst;
 with Vhdl.Sem_Specs;
@@ -1728,9 +1730,12 @@ package body Vhdl.Canon is
 
    procedure Canon_Psl_Property_Directive (Stmt : Iir)
    is
+      use PSL.NFAs;
       Prop : PSL_Node;
       Fa : PSL_NFA;
+      Final : NFA_State;
    begin
+      --  Rewrite (simplify) the property.
       Prop := Get_Psl_Property (Stmt);
       Prop := PSL.Rewrites.Rewrite_Property (Prop);
       Set_Psl_Property (Stmt, Prop);
@@ -1739,6 +1744,11 @@ package body Vhdl.Canon is
       Fa := PSL.Build.Build_FA (Prop);
       Set_PSL_NFA (Stmt, Fa);
 
+      Final := Get_Final_State (Fa);
+      if Get_First_Dest_Edge (Final) = No_Edge then
+         Warning_Msg_Sem (Warnid_Useless, +Stmt, "property cannot fail");
+      end if;
+
       Canon_Psl_Clocked_NFA (Stmt);
       if Canon_Flag_Expressions then
          Canon_PSL_Expression (Get_PSL_Clock (Stmt));
-- 
cgit v1.2.3