From 9c195bf5d86d67ea5eb419ccf6e48dc153e57c68 Mon Sep 17 00:00:00 2001 From: Tristan Gingold Date: Tue, 4 Nov 2014 20:14:19 +0100 Subject: Move sources to src/ subdirectory. --- src/psl/psl-subsets.adb | 177 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 177 insertions(+) create mode 100644 src/psl/psl-subsets.adb (limited to 'src/psl/psl-subsets.adb') diff --git a/src/psl/psl-subsets.adb b/src/psl/psl-subsets.adb new file mode 100644 index 000000000..f322eafda --- /dev/null +++ b/src/psl/psl-subsets.adb @@ -0,0 +1,177 @@ +with PSL.Errors; use PSL.Errors; +with Types; use Types; + +package body PSL.Subsets is + procedure Check_Simple (N : Node) + is + begin + case Get_Kind (N) is + when N_Not_Bool => + if Get_Psl_Type (Get_Boolean (N)) /= Type_Boolean then + Error_Msg_Sem + ("operand of a negation operator must be a boolean", N); + end if; + when N_Never => + case Get_Psl_Type (Get_Property (N)) is + when Type_Sequence | Type_Boolean => + null; + when others => + Error_Msg_Sem ("operand of a 'never' operator must be " + & "a boolean or a sequence", N); + end case; + when N_Eventually => + case Get_Psl_Type (Get_Property (N)) is + when Type_Sequence | Type_Boolean => + null; + when others => + Error_Msg_Sem ("operand of an 'eventually!' operator must be" + & " a boolean or a sequence", N); + end case; + when N_And_Bool => + if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then + Error_Msg_Sem ("left-hand side operand of logical 'and' must be" + & " a boolean", N); + end if; + when N_Or_Bool => + if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then + Error_Msg_Sem ("left-hand side operand of logical 'or' must be" + & " a boolean", N); + end if; + when N_Log_Imp_Prop => + if Get_Psl_Type (Get_Left (N)) /= Type_Boolean then + Error_Msg_Sem ("left-hand side operand of logical '->' must be" + & " a boolean", N); + end if; + -- FIXME: <-> + when N_Until => + if not Get_Inclusive_Flag (N) then + if Get_Psl_Type (Get_Right (N)) /= Type_Boolean then + Error_Msg_Sem ("right-hand side of a non-overlapping " + & "'until*' operator must be a boolean", N); + end if; + else + if Get_Psl_Type (Get_Right (N)) /= Type_Boolean + or else Get_Psl_Type (Get_Left (N)) /= Type_Boolean + then + Error_Msg_Sem ("both operands of an overlapping 'until*'" + & " operator are boolean", N); + end if; + end if; + when N_Before => + if Get_Psl_Type (Get_Right (N)) /= Type_Boolean + or else Get_Psl_Type (Get_Left (N)) /= Type_Boolean + then + Error_Msg_Sem ("both operands of a 'before*'" + & " operator are boolean", N); + end if; + when others => + null; + end case; + + -- Recursion. + case Get_Kind (N) is + when N_Error => + null; + when N_Hdl_Mod_Name => + null; + when N_Vunit + | N_Vmode + | N_Vprop => + declare + Item : Node; + begin + Item := Get_Item_Chain (N); + while Item /= Null_Node loop + Check_Simple (Item); + Item := Get_Chain (Item); + end loop; + end; + when N_Name_Decl => + null; + when N_Assert_Directive + | N_Property_Declaration => + Check_Simple (Get_Property (N)); + when N_Endpoint_Declaration + | N_Sequence_Declaration => + Check_Simple (Get_Sequence (N)); + when N_Clock_Event => + Check_Simple (Get_Property (N)); + Check_Simple (Get_Boolean (N)); + when N_Always + | N_Never + | N_Eventually + | N_Strong => + Check_Simple (Get_Property (N)); + when N_Braced_SERE => + Check_Simple (Get_SERE (N)); + when N_Concat_SERE + | N_Fusion_SERE + | N_Within_SERE => + Check_Simple (Get_Left (N)); + Check_Simple (Get_Right (N)); + when N_Name => + null; + when N_Star_Repeat_Seq + | N_Goto_Repeat_Seq + | N_Equal_Repeat_Seq => + declare + N2 : constant Node := Get_Sequence (N); + begin + if N2 /= Null_Node then + Check_Simple (N2); + end if; + end; + when N_Plus_Repeat_Seq => + Check_Simple (Get_Sequence (N)); + when N_Match_And_Seq + | N_And_Seq + | N_Or_Seq => + Check_Simple (Get_Left (N)); + Check_Simple (Get_Right (N)); + when N_Imp_Seq + | N_Overlap_Imp_Seq => + Check_Simple (Get_Sequence (N)); + Check_Simple (Get_Property (N)); + when N_Log_Imp_Prop + | N_Until + | N_Before + | N_Or_Prop + | N_And_Prop + | N_And_Bool + | N_Or_Bool + | N_Imp_Bool => + Check_Simple (Get_Left (N)); + Check_Simple (Get_Right (N)); + when N_Next + | N_Next_A + | N_Next_E => + Check_Simple (Get_Property (N)); + when N_Next_Event + | N_Next_Event_A + | N_Next_Event_E + | N_Abort => + Check_Simple (Get_Boolean (N)); + Check_Simple (Get_Property (N)); + when N_Not_Bool => + Check_Simple (Get_Boolean (N)); + when N_Const_Parameter + | N_Sequence_Parameter + | N_Boolean_Parameter + | N_Property_Parameter => + null; + when N_Actual => + null; + when N_Sequence_Instance + | N_Endpoint_Instance + | N_Property_Instance => + null; + when N_True + | N_False + | N_Number + | N_EOS + | N_HDL_Expr => + null; + end case; + end Check_Simple; +end PSL.Subsets; + -- cgit v1.2.3