------------------------------ -------------------------------------------------- -- -- -- OCARINA COMPONENTS -- -- -- -- O C A R I N A . A N A L Y Z E R . S E M A N T I C S -- -- -- -- B o d y -- -- -- -- Copyright (C) 2006-2007, GET-Telecom Paris. -- -- -- -- Ocarina is free software; you can redistribute it and/or modify -- -- it under terms of the GNU General Public License as published by the -- -- Free Software Foundation; either version 2, or (at your option) any -- -- later version. Ocarina is distributed in the hope that it will be -- -- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of -- -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General -- -- Public License for more details. You should have received a copy of the -- -- GNU General Public License distributed with Ocarina; see file COPYING. -- -- If not, write to the Free Software Foundation, 51 Franklin Street, Fifth -- -- Floor, Boston, MA 02111-1301, USA. -- -- -- -- As a special exception, if other files instantiate generics from this -- -- unit, or you link this unit with other files to produce an executable, -- -- this unit does not by itself cause the resulting executable to be -- -- covered by the GNU General Public License. This exception does not -- -- however invalidate any other reasons why the executable file might be -- -- covered by the GNU Public License. -- -- -- -- Ocarina is maintained by the Ocarina team -- -- (ocarina-users@listes.enst.fr) -- -- -- ------------------------------------------------------------------------------ with Utils; use Utils; with Ocarina.Nodes; with Ocarina.Nutils; with Ocarina.AADL_Values; with Ocarina.Analyzer.Messages; with Ocarina.Entities.Properties; with Ocarina.Entities.Components; with Ocarina.Entities.Components.Connections; with Ocarina.Analyzer.Queries; with Ocarina.Processor.Properties; package body Ocarina.Analyzer.Semantics is use Ocarina.Nodes; use Ocarina.Nutils; use Ocarina.AADL_Values; use Ocarina.Analyzer.Messages; use Ocarina.Entities; use Ocarina.Entities.Properties; use Ocarina.Entities.Components; use Ocarina.Entities.Components.Connections; use Ocarina.Analyzer.Queries; use Ocarina.Processor.Properties; function Check_Cycles_In_Component_Implementation (Node : node_id; Initial_Node : node_id := No_Node) return Boolean; function Check_Cycles_In_Port_Group_Or_Component_Type (Node : node_id; Initial_Node : node_id := No_Node) return Boolean; function Check_Cycles_In_Inversions_Of_Port_Groups (Node : node_id; Initial_Node : node_id := No_Node) return Boolean; function Check_For_A_Unique_Initial_Mode (Node : node_id) return Boolean; function Check_Cycles_In_Subcomponents (Node : node_id; Initial_Node : node_id := No_Node) return Boolean; function Check_Connections (Node : node_id) return Boolean; function Connection_End_Is_Local (Node : node_id) return Boolean; function Check_End_Types_Consistency (Node : node_id) return Boolean; -- Check that the end of the connection have compatible types function Check_Connection_Ends_Consistency (Node : node_id) return Boolean; -- Check if that the source is an in port, the destination is an -- out port, etc. function Check_Connection_End_Consistency (Connection_End : node_id; Connection_Category : connection_type) return Boolean; -- Check if the connection end (source or destination) is of a -- consistent type regarding the connection type. function Check_End_Directions_Consistency (Node : node_id) return Boolean; -- Check that the connected entities are consistent with the -- direction of the connection. function Check_Property_Associations (Properties : list_id; Container : node_id) return Boolean; -- Return True if the value type of the property association -- Property is consistent with the one specified in the property -- name declaration. Container is the entity declaration in which -- the property association is declared function Check_Applies_To (Property : node_id; Container : node_id) return Boolean; -- Return True if the property association can be applied to the -- container or to the entity designated by the 'applies to' -- statement, if any. function Check_Values_Of_Property_Association (Property_Association : node_id) return Boolean; -- Check wether the values of the property association are -- conformant with the type associated with the corresponding -- property name. function Check_Properties_Of_Component_Type (Component : node_id) return Boolean; function Check_Properties_Of_Component_Implementation (Component : node_id) return Boolean; function Check_Properties_Of_Port_Group_Type (Port_Group : node_id) return Boolean; function Check_Property_Type (Property_Type : node_id; Display_Error_Message : Boolean := True) return Boolean; -- Return True if the property type is consistent, else False function Compare_Numbers (Number_1 : node_id; Number_2 : node_id) return Integer; -- Return -1 if Number_1 > Number_2, 1 if Number_2 > Number_1, or -- 0 if Number_1 and Number_2 are equal. Return -2 if there is an -- error. If Number_1 and Number_2 are two unit number, the -- comparision is done with respect to the units (1sec is greater -- that 500ms). procedure Homogenize_Unit_Numbers (Number_1 : node_id; Number_2 : node_id; Literal_1 : out node_id; Literal_2 : out node_id); -- If Number_1 and Number_2 are to unit literals, convert them to -- the first common unit to be able to compare them. For example -- if Number_1 is 1sec and Number_2 is 500ms then Literal_1 is set -- to 1000 and Literal_2 is set to 500. function Convert_Single_Value_To_List (Property_Association : node_id) return Boolean; -- Edit the value of the property association in order to create a -- list with its single value function Test_Property_Type_Equivalence (Type_Of_Property_Name : Ocarina.Entities.Properties.property_type; Type_Of_Property_Association : Ocarina.Entities.Properties.property_type) return Boolean; function Test_Property_Value_Validity (Property_Type : node_id; Property_Value : node_id) return Boolean; ---------------------- -- Check_Applies_To -- ---------------------- function Check_Applies_To (Property : node_id; Container : node_id) return Boolean is pragma assert (Kind (Property) = k_property_association); pragma assert (Present (Container)); Entity_Of_Property : node_id; Success : Boolean; begin if Applies_To_Prop (Property) = No_List then Entity_Of_Property := Container; else Entity_Of_Property := Corresponding_Entity (Last_Node (Applies_To_Prop (Property))); end if; if Kind (Entity_Of_Property) = k_package_specification then Success := True; else Success := Property_Can_Apply_To_Entity (Property, Entity_Of_Property); end if; if Success then return True; else Display_Property_Not_Applicable (Property, Entity_Of_Property); return False; end if; end Check_Applies_To; ---------------------------------------------- -- Check_Cycles_In_Component_Implementation -- ---------------------------------------------- function Check_Cycles_In_Component_Implementation (Node : node_id; Initial_Node : node_id := No_Node) return Boolean is pragma assert (Kind (Node) = k_component_implementation); pragma assert (No (Initial_Node) or else Kind (Initial_Node) = k_component_implementation); First_Extension_Node : node_id; Success : Boolean := True; begin -- We note the first visited node in each component we -- scan. Thus, if we scan a component in which we find the same -- node_id, it means there is a cycle. if No (Initial_Node) then First_Extension_Node := Node; else First_Extension_Node := Initial_Node; end if; if First_Visited_Node (Node) = First_Extension_Node then Display_Cyclic_Extension (Node); Set_First_Visited_Node (Node, No_Node); return False; else Set_First_Visited_Node (Node, First_Extension_Node); end if; if Parent (Node) /= No_Node and then Get_Referenced_Entity (Parent (Node)) /= No_Node then Success := Check_Cycles_In_Component_Implementation (Get_Referenced_Entity (Parent (Node)), First_Extension_Node); else Success := Check_Cycles_In_Port_Group_Or_Component_Type (Corresponding_Entity (Component_Type_Identifier (Node))); end if; Set_First_Visited_Node (Node, No_Node); return Success; end Check_Cycles_In_Component_Implementation; ----------------------------------------------- -- Check_Cycles_In_Inversions_Of_Port_Groups -- ----------------------------------------------- function Check_Cycles_In_Inversions_Of_Port_Groups (Node : node_id; Initial_Node : node_id := No_Node) return Boolean is pragma assert (Kind (Node) = k_port_group_type); pragma assert (No (Initial_Node) or else Kind (Initial_Node) = k_port_group_type); First_Inversion_Node : node_id; Success : Boolean := True; begin -- We note the first visited node in each component we -- scan. Thus, if we scan a component in which we find the same -- node id, it means there is a cycle. if No (Initial_Node) then First_Inversion_Node := Node; else First_Inversion_Node := Initial_Node; end if; if First_Visited_Node (Node) = First_Inversion_Node then Display_Cyclic_Inversion (Node); Set_First_Visited_Node (Node, No_Node); return False; else Set_First_Visited_Node (Node, First_Inversion_Node); end if; if Inverse_Of (Node) /= No_Node and then Get_Referenced_Entity (Inverse_Of (Node)) /= No_Node then Success := Check_Cycles_In_Inversions_Of_Port_Groups (Get_Referenced_Entity (Inverse_Of (Node)), First_Inversion_Node); end if; Set_First_Visited_Node (Node, No_Node); return Success; end Check_Cycles_In_Inversions_Of_Port_Groups; -------------------------------------------------- -- Check_Cycles_In_Port_Group_Or_Component_Type -- -------------------------------------------------- function Check_Cycles_In_Port_Group_Or_Component_Type (Node : node_id; Initial_Node : node_id := No_Node) return Boolean is pragma assert (Kind (Node) = k_component_type or else Kind (Node) = k_port_group_type); pragma assert (No (Initial_Node) or else Kind (Initial_Node) = k_component_type or else Kind (Initial_Node) = k_port_group_type); First_Extension_Node : node_id; Success : Boolean := True; begin -- We note the first visited node in each component we -- scan. Thus, if we scan a component in which we find the same -- node id, it means there is a cycle. if No (Initial_Node) then First_Extension_Node := Node; else First_Extension_Node := Initial_Node; end if; if First_Visited_Node (Node) = First_Extension_Node then Display_Cyclic_Extension (Node); Set_First_Visited_Node (Node, No_Node); return False; else Set_First_Visited_Node (Node, First_Extension_Node); end if; if Parent (Node) /= No_Node and then Get_Referenced_Entity (Parent (Node)) /= No_Node then Success := Check_Cycles_In_Port_Group_Or_Component_Type (Get_Referenced_Entity (Parent (Node)), First_Extension_Node); end if; Set_First_Visited_Node (Node, No_Node); return Success; end Check_Cycles_In_Port_Group_Or_Component_Type; ----------------------------------- -- Check_Cycles_In_Subcomponents -- ----------------------------------- function Check_Cycles_In_Subcomponents (Node : node_id; Initial_Node : node_id := No_Node) return Boolean is pragma assert (Kind (Node) = k_component_implementation or else Kind (Node) = k_component_type); List_Node : node_id; First_Instance_Node : node_id; Success : Boolean := True; begin if Kind (Node) = k_component_implementation then if No (Initial_Node) then First_Instance_Node := Node; else First_Instance_Node := Initial_Node; end if; if First_Visited_Node (Node) = First_Instance_Node then Display_Cyclic_Subcomponents (Node); Set_First_Visited_Node (Node, No_Node); return False; else Set_First_Visited_Node (Node, First_Instance_Node); end if; if not Is_Empty (Subcomponents (Node)) then List_Node := First_Node (Subcomponents (Node)); while Present (List_Node) loop if Entity_Ref (List_Node) /= No_Node and then Get_Referenced_Entity (Entity_Ref (List_Node)) /= No_Node then Success := Success and then Check_Cycles_In_Subcomponents (Get_Referenced_Entity (Entity_Ref (List_Node)), First_Instance_Node); end if; List_Node := Next_Node (List_Node); end loop; end if; Set_First_Visited_Node (Node, No_Node); end if; return Success; end Check_Cycles_In_Subcomponents; ---------------------- -- Check_Connection -- ---------------------- function Check_Connection (Node : node_id) return Boolean is pragma assert (Kind (Node) = k_connection); Success : Boolean := True; begin if Is_Refinement (Node) then return True; end if; if not Check_Connection_End_Consistency (Connection_End => Get_Referenced_Entity (Destination (Node)), Connection_Category => connection_type'val (Category (Node))) then DAE (Node1 => Destination (Node), Message1 => " points to ", Node2 => Get_Referenced_Entity (Destination (Node)), Message2 => ", which is not of a proper type"); Success := False; end if; if not Check_Connection_End_Consistency (Connection_End => Get_Referenced_Entity (Source (Node)), Connection_Category => connection_type'val (Category (Node))) then DAE (Node1 => Source (Node), Message1 => " points to ", Node2 => Get_Referenced_Entity (Source (Node)), Message2 => ", which is not of a proper type"); Success := False; end if; if Success then Success := Check_End_Types_Consistency (Node) and then Check_Connection_Ends_Consistency (Node) and then Check_End_Directions_Consistency (Node); end if; return Success; end Check_Connection; --------------------------------------- -- Check_Connection_Ends_Consistency -- --------------------------------------- function Check_Connection_Ends_Consistency (Node : node_id) return Boolean is pragma assert (Kind (Node) = k_connection); Connection_Source : constant node_id := Get_Referenced_Entity (Source (Node)); Connection_Destination : constant node_id := Get_Referenced_Entity (Destination (Node)); Same_Kind : Boolean := False; Data_Port_And_Parameter : Boolean := False; Data_And_Require_Data_Access : Boolean := False; Provide_Data_Access_And_Data : Boolean := False; Provide_Bus_Access_And_Bus : Boolean := False; Bus_And_Require_Bus_Access : Boolean := False; Provide_Subprogram_Access_And_Subprogram : Boolean := False; Subprogram_And_Require_Subprogram_Access : Boolean := False; begin pragma assert (Kind (Connection_Source) = k_port_spec or else Kind (Connection_Source) = k_parameter or else Kind (Connection_Source) = k_port_group_spec or else Kind (Connection_Source) = k_subcomponent_access or else Kind (Connection_Source) = k_subcomponent or else Kind (Connection_Destination) = k_subprogram_call); pragma assert (Kind (Connection_Destination) = k_port_spec or else Kind (Connection_Destination) = k_parameter or else Kind (Connection_Destination) = k_port_group_spec or else Kind (Connection_Destination) = k_subcomponent_access or else Kind (Connection_Destination) = k_subcomponent or else Kind (Connection_Destination) = k_subprogram_call); Same_Kind := Kind (Connection_Source) = Kind (Connection_Destination); Data_Port_And_Parameter := (Kind (Connection_Source) = k_port_spec and then Is_Data (Connection_Source) and then Kind (Connection_Destination) = k_parameter) or else (Kind (Connection_Destination) = k_port_spec and then Is_Data (Connection_Destination) and then Kind (Connection_Source) = k_parameter); Data_And_Require_Data_Access := Kind (Connection_Source) = k_subcomponent and then component_category'val (Category (Connection_Source)) = cc_data and then Kind (Connection_Destination) = k_subcomponent_access and then component_category'val (Subcomponent_Category (Connection_Destination)) = cc_data; Provide_Data_Access_And_Data := (Kind (Connection_Destination) = k_subcomponent_access and then component_category'val (Subcomponent_Category (Connection_Destination)) = cc_data and then Is_Provided (Connection_Destination) and then Kind (Connection_Source) = k_subcomponent and then component_category'val (Category (Connection_Source)) = cc_data); Bus_And_Require_Bus_Access := Kind (Connection_Source) = k_subcomponent and then component_category'val (Category (Connection_Source)) = cc_bus and then Kind (Connection_Destination) = k_subcomponent_access and then component_category'val (Subcomponent_Category (Connection_Destination)) = cc_bus; Provide_Bus_Access_And_Bus := (Kind (Connection_Destination) = k_subcomponent_access and then component_category'val (Subcomponent_Category (Connection_Destination)) = cc_bus and then Is_Provided (Connection_Destination) and then Kind (Connection_Source) = k_subcomponent and then component_category'val (Category (Connection_Source)) = cc_bus); Subprogram_And_Require_Subprogram_Access := Kind (Connection_Source) = k_subcomponent and then component_category'val (Category (Connection_Source)) = cc_subprogram and then Kind (Connection_Destination) = k_subcomponent_access and then component_category'val (Subcomponent_Category (Connection_Destination)) = cc_subprogram; Provide_Subprogram_Access_And_Subprogram := (Kind (Connection_Destination) = k_subcomponent_access and then component_category'val (Subcomponent_Category (Connection_Destination)) = cc_subprogram and then Is_Provided (Connection_Destination) and then Kind (Connection_Source) = k_subcomponent and then component_category'val (Category (Connection_Source)) = cc_subprogram); -- We assume that the only possibility is to connect a -- subcomponent into a component requires. The contrary -- (connecting a component requires into a subcomponent) is -- forbidden. if not (Bus_And_Require_Bus_Access or else Provide_Bus_Access_And_Bus or else Provide_Data_Access_And_Data or else Data_And_Require_Data_Access or else Subprogram_And_Require_Subprogram_Access or else Provide_Subprogram_Access_And_Subprogram or else Data_Port_And_Parameter or else Same_Kind) then DAE (Loc => Ocarina.Nodes.Loc (Node), Node1 => Get_Referenced_Entity (Source (Node)), Message1 => " and ", Node2 => Get_Referenced_Entity (Destination (Node)), Message2 => " are not compatible"); return False; else return True; end if; end Check_Connection_Ends_Consistency; -------------------------------------- -- Check_Connection_End_Consistency -- -------------------------------------- function Check_Connection_End_Consistency (Connection_End : node_id; Connection_Category : connection_type) return Boolean is pragma assert (Kind (Connection_End) = k_port_spec or else Kind (Connection_End) = k_parameter or else Kind (Connection_End) = k_port_group_spec or else Kind (Connection_End) = k_subcomponent_access or else Kind (Connection_End) = k_subcomponent or else Kind (Connection_End) = k_subprogram_call); Success : Boolean := True; begin case Connection_Category is when ct_data | ct_data_delayed => Success := Kind (Connection_End) = k_port_spec and then Is_Data (Connection_End) and then not Is_Event (Connection_End); when ct_event => Success := Kind (Connection_End) = k_port_spec and then not Is_Data (Connection_End) and then Is_Event (Connection_End); when ct_event_data => Success := Kind (Connection_End) = k_port_spec and then Is_Data (Connection_End) and then Is_Event (Connection_End); when ct_port_group => Success := Kind (Connection_End) = k_port_group_spec; when ct_parameter => -- Parameter connections can connect (event) data ports -- to subprogram parameters, since parameter have the -- same semantic as (event) data ports. Success := Kind (Connection_End) = k_parameter or else (Kind (Connection_End) = k_port_spec and then Is_Data (Connection_End)); when ct_access_bus => Success := (Kind (Connection_End) = k_subcomponent_access and then component_category'val (Subcomponent_Category (Connection_End)) = cc_bus) or else (Kind (Connection_End) = k_subcomponent and then component_category'val (Category (Connection_End)) = cc_bus); when ct_access_data => Success := (Kind (Connection_End) = k_subcomponent_access and then component_category'val (Subcomponent_Category (Connection_End)) = cc_data) or else (Kind (Connection_End) = k_subcomponent and then component_category'val (Category (Connection_End)) = cc_data); when ct_access_subprogram => Success := (Kind (Connection_End) = k_subcomponent_access and then component_category'val (Subcomponent_Category (Connection_End)) = cc_subprogram) or else (Kind (Connection_End) = k_subcomponent and then component_category'val (Category (Connection_End)) = cc_subprogram); end case; return Success; end Check_Connection_End_Consistency; ----------------------- -- Check_Connections -- ----------------------- function Check_Connections (Node : node_id) return Boolean is pragma assert (Kind (Node) = k_component_implementation); List_Node : node_id; Success : Boolean := True; begin if not Is_Empty (Ocarina.Nodes.Connections (Node)) then List_Node := First_Node (Ocarina.Nodes.Connections (Node)); while Present (List_Node) loop Success := Check_Connection (List_Node) and then Success; List_Node := Next_Node (List_Node); end loop; end if; return Success; end Check_Connections; -------------------------------------- -- Check_End_Directions_Consistency -- -------------------------------------- function Check_End_Directions_Consistency (Node : node_id) return Boolean is pragma assert (Kind (Node) = k_connection); Connection_Source : constant node_id := Get_Referenced_Entity (Source (Node)); Source_Is_Local : constant Boolean := Connection_End_Is_Local (Source (Node)); Connection_Destination : constant node_id := Get_Referenced_Entity (Destination (Node)); Destination_Is_Local : constant Boolean := Connection_End_Is_Local (Destination (Node)); Directions : Boolean := False; begin pragma assert (Kind (Connection_Source) = k_port_spec or else Kind (Connection_Source) = k_parameter or else Kind (Connection_Source) = k_port_group_spec or else Kind (Connection_Source) = k_subcomponent_access or else Kind (Connection_Source) = k_subcomponent); pragma assert (Kind (Connection_Destination) = k_port_spec or else Kind (Connection_Destination) = k_parameter or else Kind (Connection_Destination) = k_port_group_spec or else Kind (Connection_Destination) = k_subcomponent_access or else Kind (Connection_Destination) = k_subcomponent); case Kind (Connection_Destination) is when k_port_spec | k_parameter => -- We do not check strict correspondence between port -- directions: an in port can be connected to an in/out -- port. This seems strange, but the examples provided -- with Osate accept this situation. After all, it can -- make sense: an in/out port could have two different -- connections. Directions := (not Source_Is_Local and then not Destination_Is_Local and then Is_Out (Connection_Source) and then Is_In (Connection_Destination)) or else (Source_Is_Local and then not Destination_Is_Local and then Is_In (Connection_Source) and then Is_In (Connection_Destination)) or else (not Source_Is_Local and then Destination_Is_Local and then Is_Out (Connection_Source) and then Is_Out (Connection_Destination)) or else (Source_Is_Local and then Destination_Is_Local and then Is_In (Connection_Source) and then Is_Out (Connection_Destination)) or else (Is_In (Connection_Source) and then Is_Out (Connection_Source) and then Is_Out (Connection_Destination) and then Is_In (Connection_Destination)); -- XXX The latest test may be redudant with the previous -- ones when k_port_group_spec => Directions := True; -- There is no direction for a port group when k_subcomponent_access => Directions := (not Source_Is_Local and then not Destination_Is_Local and then not Is_Provided (Connection_Destination) and then Kind (Connection_Source) = k_subcomponent_access and then Is_Provided (Connection_Source)) or else (Source_Is_Local and then not Destination_Is_Local and then not Is_Provided (Connection_Destination) and then ((Kind (Connection_Source) = k_subcomponent_access and then not Is_Provided (Connection_Source)) or else Kind (Connection_Source) = k_subcomponent)) or else (not Source_Is_Local and then Destination_Is_Local and then Is_Provided (Connection_Destination) and then Kind (Connection_Source) = k_subcomponent_access and then Is_Provided (Connection_Source)) or else (Source_Is_Local and then Destination_Is_Local and then Is_Provided (Connection_Destination) and then Kind (Connection_Source) = k_subcomponent); when k_subcomponent => Directions := False; when others => Directions := True; end case; if not Directions then DAE (Loc => Ocarina.Nodes.Loc (Node), Node1 => Get_Referenced_Entity (Source (Node)), Message1 => " and ", Node2 => Get_Referenced_Entity (Destination (Node)), Message2 => " do not have compatible directions"); Directions := False; end if; return Directions; end Check_End_Directions_Consistency; --------------------------------- -- Check_End_Types_Consistency -- --------------------------------- function Check_End_Types_Consistency (Node : node_id) return Boolean is pragma assert (Kind (Node) = k_connection); Source_Node : constant node_id := Get_Referenced_Entity (Source (Node)); Destination_Node : constant node_id := Get_Referenced_Entity (Destination (Node)); Source_Is_Local : constant Boolean := Connection_End_Is_Local (Source (Node)); Destination_Is_Local : constant Boolean := Connection_End_Is_Local (Destination (Node)); Source_Type : node_id; Destination_Type : node_id; Success : Boolean := True; No_Type : Boolean := True; begin -- For port and parameter connections, the consistency is -- ensured if the associated data are of the same type, or if -- one is an implementation of the other one. For subcomponent -- accesses, the provided subcomponent must be of the same type -- or be an implementation of the required one. Same thing for -- subprogram as features. Ends of a Port group connection must -- be the inverse one of the other. if Present (Entity_Ref (Source_Node)) then Source_Type := Get_Referenced_Entity (Entity_Ref (Source_Node)); else Source_Type := No_Node; end if; if Present (Entity_Ref (Destination_Node)) then Destination_Type := Get_Referenced_Entity (Entity_Ref (Destination_Node)); else Destination_Type := No_Node; end if; No_Type := No (Source_Type) or else No (Destination_Type); if No_Type then return True; -- If one of the two ends has no type, there is no use -- checking anything. end if; case connection_type'val (Category (Node)) is when ct_data | ct_data_delayed | ct_event_data | ct_parameter => if Source_Type = Destination_Type then Success := True; else DAE (Loc => Loc (Node), Node1 => Source (Node), Message1 => " and ", Node2 => Destination (Node), Message2 => " do not have compatible types"); Success := False; end if; when ct_event => Success := True; when ct_port_group => if Source_Is_Local = Destination_Is_Local then Success := (Present (Inverse_Of (Source_Type)) and then Get_Referenced_Entity (Inverse_Of (Source_Type)) = Destination_Type) or else (Present (Inverse_Of (Destination_Type)) and then Get_Referenced_Entity (Inverse_Of (Destination_Type)) = Source_Type); else Success := (Source_Type = Destination_Type); end if; if not Success then DAE (Loc => Loc (Node), Node1 => Source (Node), Message1 => " and ", Node2 => Destination (Node), Message2 => " do not have compatible types"); Success := False; end if; -- XXX This comparison is too basic. We should compare -- the content of the port groups instead when ct_access_bus | ct_access_data | ct_access_subprogram => if Source_Type = Destination_Type then Success := True; else DAE (Loc => Loc (Node), Node1 => Source (Node), Message1 => " and ", Node2 => Destination (Node), Message2 => " do not have compatible types"); Success := False; end if; end case; return Success; end Check_End_Types_Consistency; ------------------------------------- -- Check_For_A_Unique_Initial_Mode -- ------------------------------------- function Check_For_A_Unique_Initial_Mode (Node : node_id) return Boolean is pragma assert (Kind (Node) = k_component_implementation); First_Initial_Mode : node_id := No_Node; Number_Of_Modes : Integer := 0; Component : node_id := Node; Success : Boolean := True; List_Node : node_id; begin while Present (Component) loop if not Is_Empty (Modes (Component)) then List_Node := First_Node (Modes (Component)); while Present (List_Node) loop if Kind (List_Node) = k_mode then Number_Of_Modes := Number_Of_Modes + 1; if Is_Initial (List_Node) then if No (First_Initial_Mode) then First_Initial_Mode := List_Node; else Display_Conflicting_Initial_Modes (List_Node, First_Initial_Mode); Success := False; end if; end if; end if; List_Node := Next_Node (List_Node); end loop; end if; if Present (Parent (Component)) then Component := Get_Referenced_Entity (Parent (Component)); else Component := No_Node; end if; end loop; if No (First_Initial_Mode) and then Number_Of_Modes /= 0 then DAE (Node1 => Node, Message1 => " has no initial mode"); Success := False; end if; return Success; end Check_For_A_Unique_Initial_Mode; -------------------------------------------------- -- Check_Properties_Of_Component_Implementation -- -------------------------------------------------- function Check_Properties_Of_Component_Implementation (Component : node_id) return Boolean is pragma assert (Kind (Component) = k_component_implementation); Success : Boolean := True; List_Node : node_id; Call_List_Node : node_id; begin -- Type refinements if Refines_Type (Component) /= No_List then List_Node := First_Node (Refines_Type (Component)); while Present (List_Node) loop Success := Check_Property_Associations (Ocarina.Nodes.Properties (List_Node), List_Node) and then Success; List_Node := Next_Node (List_Node); end loop; end if; -- Subcomponents if Subcomponents (Component) /= No_List then List_Node := First_Node (Subcomponents (Component)); while Present (List_Node) loop Success := Check_Property_Associations (Ocarina.Nodes.Properties (List_Node), List_Node) and then Success; List_Node := Next_Node (List_Node); end loop; end if; -- Call sequences -- Some call sequences are anonymous if Calls (Component) /= No_List then List_Node := First_Node (Calls (Component)); while Present (List_Node) loop if Subprogram_Calls (List_Node) /= No_List then Call_List_Node := First_Node (Subprogram_Calls (List_Node)); while Present (Call_List_Node) loop Success := Check_Property_Associations (Ocarina.Nodes.Properties (Call_List_Node), Call_List_Node) and then Success; Call_List_Node := Next_Node (Call_List_Node); end loop; end if; List_Node := Next_Node (List_Node); end loop; end if; -- Connections -- Some connections are anonymous if Ocarina.Nodes.Connections (Component) /= No_List then List_Node := First_Node (Ocarina.Nodes.Connections (Component)); while Present (List_Node) loop Success := Check_Property_Associations (Ocarina.Nodes.Properties (List_Node), List_Node) and then Success; List_Node := Next_Node (List_Node); end loop; end if; -- Flows if Flows (Component) /= No_List then List_Node := First_Node (Flows (Component)); while Present (List_Node) loop Success := Check_Property_Associations (Ocarina.Nodes.Properties (List_Node), List_Node) and then Success; List_Node := Next_Node (List_Node); end loop; end if; -- Modes if Modes (Component) /= No_List then List_Node := First_Node (Modes (Component)); while Present (List_Node) loop if Kind (List_Node) = k_mode then Success := Check_Property_Associations (Ocarina.Nodes.Properties (List_Node), List_Node) and then Success; end if; List_Node := Next_Node (List_Node); end loop; end if; -- Properties Success := Check_Property_Associations (Ocarina.Nodes.Properties (Component), Component) and then Success; return Success; end Check_Properties_Of_Component_Implementation; ---------------------------------------- -- Check_Properties_Of_Component_Type -- ---------------------------------------- function Check_Properties_Of_Component_Type (Component : node_id) return Boolean is pragma assert (Kind (Component) = k_component_type); Success : Boolean := True; List_Node : node_id; begin -- Features if Features (Component) /= No_List then List_Node := First_Node (Features (Component)); while Present (List_Node) loop Success := Check_Property_Associations (Ocarina.Nodes.Properties (List_Node), List_Node) and then Success; List_Node := Next_Node (List_Node); end loop; end if; -- Flows if Flows (Component) /= No_List then List_Node := First_Node (Flows (Component)); while Present (List_Node) loop Success := Check_Property_Associations (Ocarina.Nodes.Properties (List_Node), List_Node) and then Success; List_Node := Next_Node (List_Node); end loop; end if; -- Properties Success := Check_Property_Associations (Ocarina.Nodes.Properties (Component), Component) and then Success; return Success; end Check_Properties_Of_Component_Type; ----------------------------------------- -- Check_Properties_Of_Port_Group_Type -- ----------------------------------------- function Check_Properties_Of_Port_Group_Type (Port_Group : node_id) return Boolean is pragma assert (Kind (Port_Group) = k_port_group_type); Success : Boolean := True; List_Node : node_id; begin -- Features if Features (Port_Group) /= No_List then List_Node := First_Node (Features (Port_Group)); while Present (List_Node) loop Success := Check_Property_Associations (Ocarina.Nodes.Properties (List_Node), List_Node) and then Success; List_Node := Next_Node (List_Node); end loop; end if; -- Properties Success := Check_Property_Associations (Ocarina.Nodes.Properties (Port_Group), Port_Group) and then Success; return Success; end Check_Properties_Of_Port_Group_Type; --------------------------------- -- Check_Property_Associations -- --------------------------------- function Check_Property_Associations (Properties : list_id; Container : node_id) return Boolean is pragma assert (Present (Container)); Success : Boolean := True; List_Node : node_id; begin if Properties /= No_List then List_Node := First_Node (Properties); while Present (List_Node) loop pragma assert (Kind (List_Node) = k_property_association); Success := Check_Applies_To (List_Node, Container) and then Check_Values_Of_Property_Association (List_Node) and then Success; List_Node := Next_Node (List_Node); end loop; end if; return Success; end Check_Property_Associations; ------------------------- -- Check_Property_Type -- ------------------------- function Check_Property_Type (Property_Type : node_id; Display_Error_Message : Boolean := True) return Boolean is pragma assert (Kind (Property_Type) = k_property_type_declaration or else Kind (Property_Type) = k_property_type or else Kind (Property_Type) = k_integer_type or else Kind (Property_Type) = k_real_type or else Kind (Property_Type) = k_enumeration_type or else Kind (Property_Type) = k_boolean_type or else Kind (Property_Type) = k_string_type or else Kind (Property_Type) = k_range_type or else Kind (Property_Type) = k_reference_type or else Kind (Property_Type) = k_classifier_type or else Kind (Property_Type) = k_unique_property_type_identifier); Type_Designator : node_id; Success : Boolean := True; begin case Kind (Property_Type) is when k_property_type_declaration => Type_Designator := Property_Type_Designator (Property_Type); when k_property_type => Type_Designator := Expanded_Type_Designator (Property_Type); when others => Type_Designator := Property_Type; end case; if Present (Type_Designator) then case Kind (Type_Designator) is when k_integer_type | k_real_type => if Present (Type_Range (Type_Designator)) and then Present (Lower_Bound (Type_Range (Type_Designator))) and then Kind (Lower_Bound (Type_Range (Type_Designator))) = k_literal and then Present (Upper_Bound (Type_Range (Type_Designator))) and then Kind (Upper_Bound (Type_Range (Type_Designator))) = k_literal then -- We only check the types that are completely -- defined. Typically, the types that have been -- expanded. Success := Compare_Numbers (Lower_Bound (Type_Range (Type_Designator)), Upper_Bound (Type_Range (Type_Designator))) >= 0; end if; when k_range_type => Success := Check_Property_Type (Number_Type (Type_Designator), False); when others => Success := True; end case; end if; if Display_Error_Message and then not Success then Display_Inconsistent_Property_Type (Property_Type); end if; return Success; end Check_Property_Type; ----------------------------------- -- Check_Semantics_In_Components -- ----------------------------------- function Check_Semantics_In_Components (Root : node_id) return Boolean is pragma assert (Kind (Root) = k_aadl_specification); Success : Boolean := True; List_Node : node_id; Package_List_Node : node_id; begin if not Is_Empty (Declarations (Root)) then List_Node := First_Node (Declarations (Root)); while Present (List_Node) loop case Kind (List_Node) is when k_component_implementation => Success := Check_For_A_Unique_Initial_Mode (List_Node) and then Check_Cycles_In_Subcomponents (List_Node) and then Check_Connections (List_Node) and then Success; when k_package_specification => if not Is_Empty (Declarations (List_Node)) then Package_List_Node := First_Node (Declarations (List_Node)); while Present (Package_List_Node) loop case Kind (Package_List_Node) is when k_component_implementation => Success := Check_For_A_Unique_Initial_Mode (Package_List_Node) and then Check_Cycles_In_Subcomponents (Package_List_Node) and then Check_Connections (Package_List_Node) and then Success; when others => null; end case; Package_List_Node := Next_Node (Package_List_Node); end loop; end if; when others => null; end case; List_Node := Next_Node (List_Node); end loop; end if; return Success; end Check_Semantics_In_Components; ----------------------------------- -- Check_Semantics_In_Namespaces -- ----------------------------------- function Check_Semantics_In_Namespaces (Root : node_id) return Boolean is pragma assert (Kind (Root) = k_aadl_specification); Success : Boolean := True; List_Node : node_id; Package_List_Node : node_id; begin if not Is_Empty (Declarations (Root)) then List_Node := First_Node (Declarations (Root)); while Present (List_Node) loop case Kind (List_Node) is when k_component_type => Success := Check_Cycles_In_Port_Group_Or_Component_Type (List_Node) and then Success; when k_component_implementation => Success := Check_Cycles_In_Component_Implementation (List_Node) and then Success; when k_port_group_type => Success := (Check_Cycles_In_Port_Group_Or_Component_Type (List_Node) and then Check_Cycles_In_Inversions_Of_Port_Groups (List_Node)) and then Success; when k_package_specification => if not Is_Empty (Declarations (List_Node)) then Package_List_Node := First_Node (Declarations (List_Node)); while Present (Package_List_Node) loop case Kind (Package_List_Node) is when k_component_type => Success := Check_Cycles_In_Port_Group_Or_Component_Type (Package_List_Node) and then Success; when k_component_implementation => Success := Check_Cycles_In_Component_Implementation (Package_List_Node) and then Success; when k_port_group_type => Success := (Check_Cycles_In_Port_Group_Or_Component_Type (Package_List_Node) and then Check_Cycles_In_Inversions_Of_Port_Groups (Package_List_Node)) and then Success; when others => null; end case; Package_List_Node := Next_Node (Package_List_Node); end loop; end if; when others => null; end case; List_Node := Next_Node (List_Node); end loop; end if; return Success; end Check_Semantics_In_Namespaces; ----------------------------------- -- Check_Semantics_Of_Properties -- ----------------------------------- function Check_Semantics_Of_Properties (Root : node_id) return Boolean is pragma assert (Kind (Root) = k_aadl_specification); Success : Boolean; List_Node : node_id; Package_List_Node : node_id; begin Success := Compute_Property_Values (Root); if Success and then Declarations (Root) /= No_List then List_Node := First_Node (Declarations (Root)); while Present (List_Node) loop case Kind (List_Node) is when k_component_implementation => Success := Check_Properties_Of_Component_Implementation (List_Node) and then Success; when k_component_type => Success := Check_Properties_Of_Component_Type (List_Node) and then Success; when k_port_group_type => Success := Check_Properties_Of_Port_Group_Type (List_Node) and then Success; when k_package_specification => Success := Check_Property_Associations (Ocarina.Nodes.Properties (List_Node), List_Node) and then Success; if Declarations (List_Node) /= No_List then Package_List_Node := First_Node (Declarations (List_Node)); while Present (Package_List_Node) loop case Kind (Package_List_Node) is when k_component_implementation => Success := Check_Properties_Of_Component_Implementation (Package_List_Node) and then Success; when k_component_type => Success := Check_Properties_Of_Component_Type (Package_List_Node) and then Success; when k_port_group_type => Success := Check_Properties_Of_Port_Group_Type (Package_List_Node) and then Success; when others => null; end case; Package_List_Node := Next_Node (Package_List_Node); end loop; end if; when k_property_set => if Declarations (List_Node) /= No_List then Package_List_Node := First_Node (Declarations (List_Node)); while Present (Package_List_Node) loop case Kind (Package_List_Node) is when k_property_type_declaration => Success := Check_Property_Type (Package_List_Node) and then Success; when others => null; end case; Package_List_Node := Next_Node (Package_List_Node); end loop; end if; when others => null; end case; List_Node := Next_Node (List_Node); end loop; end if; return Success; end Check_Semantics_Of_Properties; ------------------------------------------ -- Check_Values_Of_Property_Association -- ------------------------------------------ function Check_Values_Of_Property_Association (Property_Association : node_id) return Boolean is pragma assert (Kind (Property_Association) = k_property_association); Property_Name : constant node_id := Get_Referenced_Entity (Ocarina.Nodes.Property_Name (Property_Association)); Type_Of_Property_Name : constant property_type := Get_Type_Of_Property (Property_Name); List_Node : node_id; Success : Boolean := True; Types_Are_Compatible : Boolean := True; begin if Value_Of_Property_Association_Is_Undefined (Property_Association) then Success := True; else -- Extract from the AADL 1.0 standard (§10.3 page 158): -- "If the property declaration for the associated property -- name *does not* contain the reserved words *list of*, the -- property value must be a single property value. If the -- property declaration for the associated property name -- contains the reserved words *list of*, the property value -- *can be a single property value*, which is interpreted to -- be a list of one value." -- So list properties can take single values after '=>' and -- '+=>' -- However we convert these property to their right form -- (and keep the old form) to make easier further tree -- manipulations. if Is_Additive_Association (Property_Association) and then Present (Expanded_Single_Value (Property_Association_Value (Property_Association))) then -- Additive association allowed only for list properties if not Type_Of_Property_Is_A_List (Property_Name) then Success := Convert_Single_Value_To_List (Property_Association); -- Even if the conversion succeded, this is an -- error. This is a workaround to get the proper error -- message. Display_Property_List_Discrepancy (Property_Association => Property_Association, Property_Name => Property_Name); return False; else Success := Convert_Single_Value_To_List (Property_Association); -- We do not return since there are more tests to -- perform. end if; end if; -- To avoid endless recursion, we begin by testing list -- properties. if Expanded_Multi_Value (Property_Association_Value (Property_Association)) /= No_List then if Type_Of_Property_Is_A_List (Property_Name) then List_Node := First_Node (Expanded_Multi_Value (Property_Association_Value (Property_Association))); while Present (List_Node) loop Types_Are_Compatible := Test_Property_Type_Equivalence (Type_Of_Property_Name, Get_Type_Of_Property_Value (List_Node)) and then Test_Property_Value_Validity (Property_Name_Type (Property_Name), List_Node); if not Types_Are_Compatible then Display_Incompatible_Property_Types (Property_Association => Property_Association, Property_Value => List_Node, Property_Name => Property_Name); Success := False; end if; List_Node := Next_Node (List_Node); end loop; else -- Single value properties cannot have a list as -- value. Success := False; Display_Property_List_Discrepancy (Property_Association => Property_Association, Property_Name => Property_Name); end if; elsif Expanded_Single_Value (Property_Association_Value (Property_Association)) /= No_Node then if Type_Of_Property_Is_A_List (Property_Name) then -- If the value is a single element while we are -- expecting a list, we build a list from the single -- element, and display a warning. and keep the single -- element untouched. Display_Conversion_To_Property_List (Property_Association => Property_Association, Property_Name => Property_Name); Success := Convert_Single_Value_To_List (Property_Association) and then Check_Values_Of_Property_Association (Property_Association); else Success := Test_Property_Type_Equivalence (Type_Of_Property_Name, Get_Type_Of_Property_Value (Expanded_Single_Value (Property_Association_Value (Property_Association)))) and then Test_Property_Value_Validity (Property_Name_Type (Property_Name), Expanded_Single_Value (Property_Association_Value (Property_Association))); if not Success then Display_Incompatible_Property_Types (Property_Association => Property_Association, Property_Value => Expanded_Single_Value (Property_Association_Value (Property_Association)), Property_Name => Property_Name); end if; end if; else -- If the property association has no actual value Success := True; end if; end if; return Success; end Check_Values_Of_Property_Association; --------------------- -- Compare_Numbers -- --------------------- function Compare_Numbers (Number_1 : node_id; Number_2 : node_id) return Integer is pragma assert (Kind (Number_1) = k_literal or else Kind (Number_1) = k_signed_aadlnumber); pragma assert (Kind (Number_2) = k_literal or else Kind (Number_2) = k_signed_aadlnumber); Literal_1 : node_id; Literal_2 : node_id; Result : Integer; begin if Kind (Number_1) = k_literal and then Kind (Number_2) = k_literal then Literal_1 := Number_1; Literal_2 := Number_2; else Homogenize_Unit_Numbers (Number_1, Number_2, Literal_1, Literal_2); end if; -- Use the routines of the AADL_Values package to compare the -- values and wrapp them to intercept any comparison error. begin if Value (Value (Literal_1)) < Value (Value (Literal_2)) then Result := 1; elsif Value (Value (Literal_2)) < Value (Value (Literal_1)) then Result := -1; else Result := 0; end if; exception when Constraint_Error => Result := -2; end; return Result; end Compare_Numbers; ----------------------------- -- Connection_End_Is_Local -- ----------------------------- function Connection_End_Is_Local (Node : node_id) return Boolean is pragma assert (Kind (Node) = k_entity_reference); begin return Next_Node (First_Node (Path (Node))) = No_Node or else Kind (Corresponding_Entity (Item (First_Node (Path (Node))))) = k_port_group_spec; end Connection_End_Is_Local; ---------------------------------- -- Convert_Single_Value_To_List -- ---------------------------------- function Convert_Single_Value_To_List (Property_Association : node_id) return Boolean is pragma assert (Kind (Property_Association) = k_property_association); begin Set_Expanded_Multi_Value (Property_Association_Value (Property_Association), New_List (k_list_id, Loc (Expanded_Single_Value (Property_Association_Value (Property_Association))))); Append_Node_To_List (Expanded_Single_Value (Property_Association_Value (Property_Association)), Expanded_Multi_Value (Property_Association_Value (Property_Association))); Set_Multi_Value (Property_Association_Value (Property_Association), New_List (k_list_id, Loc (Single_Value (Property_Association_Value (Property_Association))))); Append_Node_To_List (Single_Value (Property_Association_Value (Property_Association)), Multi_Value (Property_Association_Value (Property_Association))); return True; end Convert_Single_Value_To_List; ----------------------------- -- Homogenize_Unit_Numbers -- ----------------------------- procedure Homogenize_Unit_Numbers (Number_1 : node_id; Number_2 : node_id; Literal_1 : out node_id; Literal_2 : out node_id) is function Convert_To_Base (L : node_id; U : node_id) return node_id; -- Converts the literal L associated to the unit U into a -- literal associated with the base dentifier of the units -- type. procedure Fetch (U : node_id; Fetched : out node_id; Base : out Boolean); -- Return the defining identifier corresponding to the -- multiplier U in the corresponding units type. Base is set to -- True if the fetched identifier is the base unit -- identifier. If the identifier is not found, return No_Node -- and False. --------------------- -- Convert_To_Base -- --------------------- function Convert_To_Base (L : node_id; U : node_id) return node_id is Fetched : node_id; N : node_id; Base : Boolean; Result : value_type; Count : Natural; Max_Iterations : Natural; Units_Type : node_id; begin Fetch (U, Fetched, Base); if not Base then -- To avoid infinite loops and detect bad formed units -- types. Units_Type := Corresponding_Entity (Unit_Identifier (Corresponding_Entity (Fetched))); Max_Iterations := Length (Unit_Definitions (Units_Type)); end if; Result := Value (Value (L)); Count := 0; while not Base loop Result := Result * Value (Value (Numeric_Literal (Corresponding_Entity (Fetched)))); Fetch (Unit_Identifier (Corresponding_Entity (Fetched)), Fetched, Base); Count := Count + 1; if Count > Max_Iterations + 1 then DAE (Message0 => "Units Type ", Node1 => Units_Type, Message1 => " Contains cycles is not correctly defined"); exit; end if; end loop; N := New_Node (k_literal, Loc (L)); Set_Value (N, New_Value (Result)); return N; end Convert_To_Base; ----------- -- Fetch -- ----------- procedure Fetch (U : node_id; Fetched : out node_id; Base : out Boolean) is Units_Type : node_id; Unit_Definition : node_id; begin if Kind (Corresponding_Entity (U)) = k_units_type then -- We have the base identifier Units_Type := Corresponding_Entity (U); else Units_Type := Corresponding_Entity (Unit_Identifier (Corresponding_Entity (U))); end if; -- This phase is neccessary because the Unit_Identifier of a -- Unit_definition is not linked directly to its -- corresponding unit definition. Fetched := Base_Identifier (Units_Type); if To_Lower (Name (Fetched)) = To_Lower (Name (U)) then Base := True; else Base := False; Unit_Definition := First_Node (Unit_Definitions (Units_Type)); while Present (Unit_Definition) loop Fetched := Identifier (Unit_Definition); exit when To_Lower (Name (Fetched)) = To_Lower (Name (U)); Fetched := No_Node; Unit_Definition := Next_Node (Unit_Definition); end loop; end if; end Fetch; Unit_1 : node_id; Unit_2 : node_id; begin -- If one of the numbers is a literal (without a unit) this -- means that the corresponding unit type contains only one -- unit identifier an that the node linker did not detect an -- error. So we return the literal without modifying them. if Kind (Number_1) = k_literal then Literal_1 := Number_1; -- Number_2 is necessarily a K_Signed_AADLNumber Literal_2 := Number_Value (Number_2); -- Nothing else to do return; end if; if Kind (Number_2) = k_literal then Literal_2 := Number_2; -- Number_1 is necessarily a K_Signed_AADLNumber Literal_1 := Number_Value (Number_1); -- Nothing more to do return; end if; -- At this stage, both numbers are K_Signed_AADLNumber's. But -- they may have null Unit identifiers. if No (Unit_Identifier (Number_1)) or else No (Unit_Identifier (Number_2)) then Literal_1 := Number_Value (Number_1); Literal_2 := Number_Value (Number_2); -- Nothing more to do return; end if; -- At this stage, we have two K_Signed_AADLNumber's with non -- null unit identifiers. -- Get the corresponding unit identifiers. If the name linker -- failed to find the corresponding unit identifier, do not -- cause error cascade. Unit_1 := Corresponding_Entity (Unit_Identifier (Number_1)); Unit_2 := Corresponding_Entity (Unit_Identifier (Number_2)); -- Convert the literals if Present (Unit_1) then Literal_1 := Convert_To_Base (Number_Value (Number_1), Unit_1); else Literal_1 := Number_Value (Number_1); end if; if Present (Unit_2) then Literal_2 := Convert_To_Base (Number_Value (Number_2), Unit_2); else Literal_2 := Number_Value (Number_2); end if; end Homogenize_Unit_Numbers; ------------------------------------ -- Test_Property_Type_Equivalence -- ------------------------------------ function Test_Property_Type_Equivalence (Type_Of_Property_Name : Ocarina.Entities.Properties.property_type; Type_Of_Property_Association : Ocarina.Entities.Properties.property_type) return Boolean is Success : Boolean; begin case Type_Of_Property_Name is when pt_boolean => Success := Type_Of_Property_Association = pt_boolean_expression or else Type_Of_Property_Association = pt_boolean; when pt_integer => Success := Type_Of_Property_Association = pt_integer or else Type_Of_Property_Association = pt_unsigned_integer; when pt_float => Success := Type_Of_Property_Association = pt_float or else Type_Of_Property_Association = pt_unsigned_float or else Type_Of_Property_Association = pt_integer or else Type_Of_Property_Association = pt_unsigned_integer; when pt_list => Success := False; when others => Success := Type_Of_Property_Association = Type_Of_Property_Name; end case; return Success; end Test_Property_Type_Equivalence; ---------------------------------- -- Test_Property_Value_Validity -- ---------------------------------- function Test_Property_Value_Validity (Property_Type : node_id; Property_Value : node_id) return Boolean is pragma assert (Kind (Property_Type) = k_property_type); pragma assert (Kind (Property_Value) = k_component_classifier_term or else Kind (Property_Value) = k_reference_term or else Kind (Property_Value) = k_number_range_term or else Kind (Property_Value) = k_literal or else Kind (Property_Value) = k_signed_aadlnumber); List_Node : node_id; Temp_Node : node_id; Type_Designator : node_id; Is_Integer : Boolean; Actual_Literal : node_id; Success : Boolean := True; begin Type_Designator := Expanded_Type_Designator (Property_Type); Success := Check_Property_Type (Type_Designator); if Success then case Kind (Type_Designator) is when k_classifier_type => List_Node := First_Node (list_id (Type_Designator)); Success := False; if Kind (Property_Value) = k_component_classifier_term then Temp_Node := Get_Referenced_Entity (Property_Value); if Present (Temp_Node) then while Present (List_Node) loop if Get_Category_Of_Component (Temp_Node) = component_category'val (Category (List_Node)) then Success := True; end if; List_Node := Next_Node (List_Node); end loop; end if; end if; when k_reference_type => List_Node := First_Node (list_id (Type_Designator)); if Present (List_Node) then Success := False; else Success := True; -- If no type is indicated, then any reference is -- correct. end if; if Kind (Property_Value) = k_reference_term then Temp_Node := Get_Referenced_Entity (Property_Value); if Present (Temp_Node) then while Present (List_Node) loop case (referable_element_category'val (Category (List_Node))) is when rec_component_category => if Get_Entity_Category (Temp_Node) = ec_subcomponent then -- If the subcomponent specification -- is incmplete (see AADL 1.0 -- standard §4.5 section -- `semantics'), then there is -- nothing else to analyze. if No (Entity_Ref (Temp_Node)) then Success := True; elsif Get_Category_Of_Component (Get_Referenced_Entity (Entity_Ref (Temp_Node))) = component_category'val (Component_Cat (List_Node)) then Success := True; end if; end if; when rec_connections => if Get_Entity_Category (Temp_Node) = ec_connection then Success := True; end if; when rec_server_subprogram => if Get_Entity_Category (Temp_Node) = ec_feature then -- XXX This is incomplete Success := True; end if; end case; List_Node := Next_Node (List_Node); end loop; end if; else Success := False; end if; when k_real_type => if Kind (Property_Value) = k_literal or else Kind (Property_Value) = k_signed_aadlnumber then Actual_Literal := Property_Value; else Actual_Literal := No_Node; end if; if Present (Actual_Literal) then if No (Type_Range (Type_Designator)) then Success := True; else Success := (Compare_Numbers (Lower_Bound (Type_Range (Type_Designator)), Actual_Literal) >= 0) and then (Compare_Numbers (Actual_Literal, Upper_Bound (Type_Range (Type_Designator))) >= 0); end if; else Success := False; end if; when k_integer_type => if Kind (Property_Value) = k_literal then Actual_Literal := Property_Value; Is_Integer := Value (Value (Actual_Literal)).T = lt_integer; elsif Kind (Property_Value) = k_signed_aadlnumber then Actual_Literal := Property_Value; Is_Integer := Value (Value (Number_Value (Actual_Literal))).T = lt_integer; else Actual_Literal := No_Node; Is_Integer := False; end if; if Is_Integer then if Type_Range (Type_Designator) = No_Node then Success := True; else Success := Present (Lower_Bound (Type_Range (Type_Designator))) and then (Compare_Numbers (Lower_Bound (Type_Range (Type_Designator)), Actual_Literal) >= 0) and then Present (Upper_Bound (Type_Range (Type_Designator))) and then (Compare_Numbers (Actual_Literal, Upper_Bound (Type_Range (Type_Designator))) >= 0); end if; else Success := False; end if; when k_range_type => Success := True; when k_boolean_type => Success := Kind (Property_Value) = k_literal and then Value (Value (Property_Value)).T = lt_boolean; when k_string_type => Success := Kind (Property_Value) = k_literal and then Value (Value (Property_Value)).T = lt_string; when k_enumeration_type => Success := Kind (Property_Value) = k_literal and then Value (Value (Property_Value)).T = lt_enumeration; if Success then Success := False; List_Node := First_Node (Identifiers (Type_Designator)); while Present (List_Node) loop Success := Success or else Name (List_Node) = Value (Value (Property_Value)).EVal; List_Node := Next_Node (List_Node); end loop; end if; when others => Success := False; end case; end if; return Success; end Test_Property_Value_Validity; end Ocarina.Analyzer.Semantics;