vhdl-canon: detect PSL assertion that cannot fail. For #1832

2 files changed, 17 insertions, 3 deletions

diff --git a/src/errorout.ads b/src/errorout.ads
index 0bdd8fb5d..f6735c8b5 100644
--- a/src/errorout.ads
+++ b/src/errorout.ads
@@ -118,6 +118,10 @@ package Errorout is
       --  Incorrect use of attributes (like non-object prefix).
       Warnid_Attribute,
 
+      --  Useless code (condition is always false or true), assertion cannot
+      --  be triggered.
+      Warnid_Useless,
+
       --  Violation of staticness rules
       Warnid_Static,
 
@@ -313,7 +317,7 @@ private
         | Warnid_Runtime_Error | Warnid_Pure | Warnid_Specs | Warnid_Hide
         | Warnid_Pragma | Warnid_Analyze_Assert | Warnid_Attribute
         | Warnid_Deprecated_Option | Warnid_Unexpected_Option
-        | Warnid_No_Wait
+        | Warnid_No_Wait | Warnid_Useless
         | Msgid_Warning  => (Enabled => True, Error => False),
       Warnid_Delta_Cycle | Warnid_Body | Warnid_Static | Warnid_Nested_Comment
         | Warnid_Universal | Warnid_Port_Bounds
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));