1-- PSL - Simple subset 2-- Copyright (C) 2002-2016 Tristan Gingold 3-- 4-- This program is free software: you can redistribute it and/or modify 5-- it under the terms of the GNU General Public License as published by 6-- the Free Software Foundation, either version 2 of the License, or 7-- (at your option) any later version. 8-- 9-- This program is distributed in the hope that it will be useful, 10-- but WITHOUT ANY WARRANTY; without even the implied warranty of 11-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 12-- GNU General Public License for more details. 13-- 14-- You should have received a copy of the GNU General Public License 15-- along with this program. If not, see <gnu.org/licenses>. 16 17with PSL.Types; use PSL.Types; 18with PSL.Errors; use PSL.Errors; 19 20package body PSL.Subsets is 21 procedure Check_Simple (N : Node) 22 is 23 begin 24 case Get_Kind (N) is 25 when N_Not_Bool => 26 if Get_Psl_Type (Get_Boolean (N)) /= Type_Boolean then 27 Error_Msg_Sem 28 ("operand of a negation operator must be a boolean", N); 29 end if; 30 when N_Never => 31 case Get_Psl_Type (Get_Property (N)) is 32 when Type_Sequence | Type_Boolean => 33 null; 34 when others => 35 Error_Msg_Sem ("operand of a 'never' operator must be " 36 & "a boolean or a sequence", N); 37 end case; 38 when N_Eventually => 39 case Get_Psl_Type (Get_Property (N)) is 40 when Type_Sequence | Type_Boolean => 41 null; 42 when others => 43 Error_Msg_Sem ("operand of an 'eventually!' operator must be" 44 & " a boolean or a sequence", N); 45 end case; 46 when N_And_Bool => 47 if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then 48 Error_Msg_Sem ("left-hand side operand of logical 'and' must be" 49 & " a boolean", N); 50 end if; 51 when N_Or_Bool => 52 if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then 53 Error_Msg_Sem ("left-hand side operand of logical 'or' must be" 54 & " a boolean", N); 55 end if; 56 when N_Log_Imp_Prop => 57 if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then 58 Error_Msg_Sem ("left-hand side operand of logical '->' must be" 59 & " a boolean", N); 60 end if; 61 -- FIXME: <-> 62 when N_Until => 63 if not Get_Inclusive_Flag (N) then 64 if Get_Psl_Type (Get_Right (N)) /= Type_Boolean then 65 Error_Msg_Sem ("right-hand side of a non-overlapping " 66 & "'until*' operator must be a boolean", N); 67 end if; 68 else 69 if Get_Psl_Type (Get_Right (N)) /= Type_Boolean 70 or else Get_Psl_Type (Get_Left (N)) /= Type_Boolean 71 then 72 Error_Msg_Sem ("both operands of an overlapping 'until*'" 73 & " operator are boolean", N); 74 end if; 75 end if; 76 when N_Before => 77 if Get_Psl_Type (Get_Right (N)) /= Type_Boolean 78 or else Get_Psl_Type (Get_Left (N)) /= Type_Boolean 79 then 80 Error_Msg_Sem ("both operands of a 'before*'" 81 & " operator are boolean", N); 82 end if; 83 when others => 84 null; 85 end case; 86 87 -- Recursion. 88 case Get_Kind (N) is 89 when N_Error => 90 null; 91 when N_Hdl_Mod_Name => 92 null; 93 when N_Vunit 94 | N_Vmode 95 | N_Vprop => 96 declare 97 Item : Node; 98 begin 99 Item := Get_Item_Chain (N); 100 while Item /= Null_Node loop 101 Check_Simple (Item); 102 Item := Get_Chain (Item); 103 end loop; 104 end; 105 when N_Name_Decl => 106 null; 107 when N_Assert_Directive 108 | N_Property_Declaration => 109 Check_Simple (Get_Property (N)); 110 when N_Endpoint_Declaration 111 | N_Sequence_Declaration => 112 Check_Simple (Get_Sequence (N)); 113 when N_Clock_Event => 114 Check_Simple (Get_Property (N)); 115 Check_Simple (Get_Boolean (N)); 116 when N_Always 117 | N_Never 118 | N_Eventually 119 | N_Strong => 120 Check_Simple (Get_Property (N)); 121 when N_Braced_SERE 122 | N_Clocked_SERE => 123 Check_Simple (Get_SERE (N)); 124 when N_Concat_SERE 125 | N_Fusion_SERE 126 | N_Within_SERE => 127 Check_Simple (Get_Left (N)); 128 Check_Simple (Get_Right (N)); 129 when N_Name => 130 null; 131 when N_Star_Repeat_Seq 132 | N_Goto_Repeat_Seq 133 | N_Equal_Repeat_Seq => 134 declare 135 N2 : constant Node := Get_Sequence (N); 136 begin 137 if N2 /= Null_Node then 138 Check_Simple (N2); 139 end if; 140 end; 141 when N_Plus_Repeat_Seq => 142 Check_Simple (Get_Sequence (N)); 143 when N_Match_And_Seq 144 | N_And_Seq 145 | N_Or_Seq => 146 Check_Simple (Get_Left (N)); 147 Check_Simple (Get_Right (N)); 148 when N_Imp_Seq 149 | N_Overlap_Imp_Seq => 150 Check_Simple (Get_Sequence (N)); 151 Check_Simple (Get_Property (N)); 152 when N_Log_Imp_Prop 153 | N_Log_Equiv_Prop 154 | N_Until 155 | N_Before 156 | N_Or_Prop 157 | N_And_Prop 158 | N_And_Bool 159 | N_Or_Bool 160 | N_Imp_Bool 161 | N_Equiv_Bool => 162 Check_Simple (Get_Left (N)); 163 Check_Simple (Get_Right (N)); 164 when N_Next 165 | N_Next_A 166 | N_Next_E 167 | N_Paren_Prop => 168 Check_Simple (Get_Property (N)); 169 when N_Next_Event 170 | N_Next_Event_A 171 | N_Next_Event_E 172 | N_Abort => 173 Check_Simple (Get_Boolean (N)); 174 Check_Simple (Get_Property (N)); 175 when N_Not_Bool 176 | N_Paren_Bool => 177 Check_Simple (Get_Boolean (N)); 178 when N_Const_Parameter 179 | N_Sequence_Parameter 180 | N_Boolean_Parameter 181 | N_Property_Parameter => 182 null; 183 when N_Actual => 184 null; 185 when N_Sequence_Instance 186 | N_Endpoint_Instance 187 | N_Property_Instance => 188 null; 189 when N_True 190 | N_False 191 | N_Number 192 | N_EOS 193 | N_HDL_Expr 194 | N_HDL_Bool => 195 null; 196 end case; 197 end Check_Simple; 198end PSL.Subsets; 199