diff --git a/examples/real/resources/all.aadl.out b/examples/real/resources/all.aadl.out index 48f00d1ccd9273b38998903fbea77939299dd8d8..84a881c8c745471cdd65d3667a9274e81d570687 100644 --- a/examples/real/resources/all.aadl.out +++ b/examples/real/resources/all.aadl.out @@ -14,7 +14,7 @@ requirement : mutexes theorem mutexes is: TRUE requirement : latency requirement : buses_rate -lib.real:12:33 Backends: warning : property "assert_properties::access_bandwidth" is not defined on element Bus_Set +lib.real:12:33 Backends: warning : property "assert_properties::access_bandwidth" is not defined on element 607 (shared.impl_a_bus) all.aadl:104:01Bus_Set lib.real:12:72 Backends: error : Property is false for instance 607 (shared.impl_a_bus) theorem buses_rate is: FALSE lib.real:85:01 Backends: fatal error : requirements are not fulfilled diff --git a/src/backends/ocarina-be_aadl-properties-values.adb b/src/backends/ocarina-be_aadl-properties-values.adb index 81e8bcc9a79c5d50499c8ec7e15fad5eafb29871..0aa349927a556c1169616088631fef6d994c7a6e 100644 --- a/src/backends/ocarina-be_aadl-properties-values.adb +++ b/src/backends/ocarina-be_aadl-properties-values.adb @@ -307,7 +307,7 @@ package body Ocarina.BE_AADL.Properties.Values is ----------------------- procedure Print_Record_Term (Node : Node_Id) is - pragma Assert (Kind (Node) = K_Record_Term_Element); + pragma Assert (Kind (Node) = K_Record_Term); List_Node : Node_Id; begin @@ -318,16 +318,11 @@ package body Ocarina.BE_AADL.Properties.Values is (Ocarina.ME_AADL.AADL_Tree.Nodes.List_Items (Node)); while Present (List_Node) loop - if List_Node /= - First_Node (Ocarina.ME_AADL.AADL_Tree.Nodes.List_Items (Node)) then - - Print_Token (T_Comma); - Write_Space; - end if; - case Kind (List_Node) is when K_Record_Term_Element => Print_Record_Term_Element (List_Node); + Print_Token (T_Semicolon); + Write_Space; when others => Node_Not_Handled (Node); end case; diff --git a/src/core/model/ocarina-analyzer-aadl-semantics.adb b/src/core/model/ocarina-analyzer-aadl-semantics.adb index b9209e4eac9f6d4ce6ef4d61b6d0c7a77e90f572..b3b161703426c854ff9affbd02aced472a0c6434 100644 --- a/src/core/model/ocarina-analyzer-aadl-semantics.adb +++ b/src/core/model/ocarina-analyzer-aadl-semantics.adb @@ -2145,7 +2145,7 @@ package body Ocarina.Analyzer.AADL.Semantics is DAE (Message0 => "Units Type ", Node1 => Units_Type, - Message1 => " contains cycles is not correctly defined"); + Message1 => " is ill-defined: it contains cycles"); exit; end if; diff --git a/src/core/model/ocarina-analyzer-messages.adb b/src/core/model/ocarina-analyzer-messages.adb index 5ab5f40613e96ec100df6022f4dac0f6142c26e0..803cd2980119f08a2742654f7e8d45f614c1779b 100644 --- a/src/core/model/ocarina-analyzer-messages.adb +++ b/src/core/model/ocarina-analyzer-messages.adb @@ -138,6 +138,9 @@ package body Ocarina.Analyzer.Messages is elsif Kind (Node2) = K_Entity_Reference then Write_Name (Get_Name_Of_Entity_Reference (Node2, Get_Display_Name => True)); + + elsif Kind (Node2) = K_Identifier then + Write_Name (Name (Node2)); end if; Write_Str (" (" & Image (Kind (Node2)) & ") "); diff --git a/src/core/model/ocarina-processor-properties.adb b/src/core/model/ocarina-processor-properties.adb index 4039502719f305d1036aebac2bfcd70315c7f4e2..01f714fd37947129270de5d379a1c581cf344c5b 100644 --- a/src/core/model/ocarina-processor-properties.adb +++ b/src/core/model/ocarina-processor-properties.adb @@ -563,12 +563,13 @@ package body Ocarina.Processor.Properties is or else Kind (Property_Value) = K_Parenthesis_Boolean_Term or else Kind (Property_Value) = K_Component_Classifier_Term or else Kind (Property_Value) = K_Unique_Property_Const_Identifier + or else Kind (Property_Value) = K_Record_Term or else Ocarina.ME_AADL.Aadl_Tree.Entities.DNKE (Property_Value)); pragma Assert (Reference_Property /= No_Node); - Evaluated_Value : Node_Id; - Ref_Term : Node_Id; + Evaluated_Value : Node_Id := No_Node; + Ref_Term : Node_Id := No_Node; begin if Property_Value = No_Node then Evaluated_Value := No_Node; @@ -1028,6 +1029,9 @@ package body Ocarina.Processor.Properties is Set_Component_Cat (Evaluated_Value, Component_Cat (Property_Value)); + when K_Record_Term => + null; -- XXX + when others => raise Program_Error; end case; diff --git a/src/frontends/aadl/ocarina-fe_aadl-parser-properties-values.adb b/src/frontends/aadl/ocarina-fe_aadl-parser-properties-values.adb index 5de2f549fdc225b4fb7ef7a0e264f9559ef2975b..8e15f05ae32768d619976b60b3134c753b67114a 100644 --- a/src/frontends/aadl/ocarina-fe_aadl-parser-properties-values.adb +++ b/src/frontends/aadl/ocarina-fe_aadl-parser-properties-values.adb @@ -1741,7 +1741,6 @@ package body Ocarina.FE_AADL.Parser.Properties.Values is Save_Lexer (Start_Loc); Scan_Token; if Token /= T_Right_Parenthesis then - Record_List := P_Items_List (P_Record_Type_Element'Access, No_Node, T_Semicolon, @@ -2407,7 +2406,6 @@ package body Ocarina.FE_AADL.Parser.Properties.Values is DPE (PC_Boolean_Or_Record_Term); return No_Node; end case; - end P_Boolean_Or_Record_Term; ---------------------- @@ -2548,8 +2546,15 @@ package body Ocarina.FE_AADL.Parser.Properties.Values is return No_Node; end if; - Items := P_Items_List (P_Record_Term_Element'Access, No_Node, - T_Semicolon, T_Right_Parenthesis, PC_Record_Term); + Save_Lexer (Start_Loc); + Scan_Token; + Items := P_Items_List (P_Record_Term_Element'Access, + No_Node, + T_Semicolon, + T_Right_Parenthesis, + PC_Record_Term, + True); + if No (Items) then Skip_Tokens (T_Semicolon); return No_Node; @@ -2559,12 +2564,11 @@ package body Ocarina.FE_AADL.Parser.Properties.Values is Item := First_Node (Items); while Present (Item) loop - Set_Corresponding_Entity (Item, Record_Term); + -- Set_Corresponding_Entity (Item, Record_Term); Item := Next_Node (Item); end loop; return Record_Term; - end P_Record_Term; --------------------------- @@ -2576,7 +2580,8 @@ package body Ocarina.FE_AADL.Parser.Properties.Values is function P_Record_Term_Element (Container : Node_Id) - return Node_Id is + return Node_Id + is use Ocarina.ME_AADL.AADL_Tree.Nodes; use Ocarina.ME_AADL.AADL_Tree.Nutils; use Lexer; @@ -2592,10 +2597,10 @@ package body Ocarina.FE_AADL.Parser.Properties.Values is begin Save_Lexer (Loc); - Scan_Token; if Token /= T_Identifier then DPE (PC_Record_Term_Element, T_Identifier); + Restore_Lexer (Loc); return No_Node; end if; @@ -2603,12 +2608,13 @@ package body Ocarina.FE_AADL.Parser.Properties.Values is Identifier := Make_Current_Identifier (Record_Term_Element); Set_Identifier (Record_Term_Element, Identifier); + Save_Lexer (Loc); Scan_Token; + if Token = T_Association then Property_Expression := P_Property_Expression (No_Node); if No (Property_Expression) then - -- error when parsing Property_Expression, quit return No_Node; end if; else @@ -2617,8 +2623,7 @@ package body Ocarina.FE_AADL.Parser.Properties.Values is return No_Node; end if; - Set_Property_Expression (Property_Expression, Record_Term_Element); - + Set_Property_Expression (Record_Term_Element, Property_Expression); return Record_Term_Element; end P_Record_Term_Element; diff --git a/src/frontends/aadl/ocarina-fe_aadl-parser-properties.adb b/src/frontends/aadl/ocarina-fe_aadl-parser-properties.adb index f4f5be9c41b40005d3b2059dbf580b1c7de25d78..c8fcb16b0cf992e212794d8f23c19f5725ad0499 100644 --- a/src/frontends/aadl/ocarina-fe_aadl-parser-properties.adb +++ b/src/frontends/aadl/ocarina-fe_aadl-parser-properties.adb @@ -208,6 +208,8 @@ package body Ocarina.FE_AADL.Parser.Properties is Loc : Location; Property_Loc : Location; Item : Node_Id; + + Parse_List_Of_Properties : Boolean := True; begin Save_Lexer (Loc); Scan_Token; @@ -302,7 +304,30 @@ package body Ocarina.FE_AADL.Parser.Properties is Save_Lexer (Loc); Scan_Token; - if Token = T_Left_Parenthesis then + -- The AADLv2 BNF is ambiguous, a string starting with a '(' + -- can either be a list of property expressions e.g. "(foo, + -- bard);"_or_ a single_expression containing a record term, + -- e.g. "(foo => 1; bar =>2;)". This look ahead loop scans + -- token to see which case we are currently processing. + + declare + Loc2 : Location; + begin + Save_Lexer (Loc2); + if Token = T_Left_Parenthesis then + while Token /= T_Right_Parenthesis loop + Scan_Token; + if Token = T_Semicolon then + Parse_List_Of_Properties := False; + end if; + end loop; + else + Parse_List_Of_Properties := False; + end if; + Restore_Lexer (Loc2); + end; + + if Parse_List_Of_Properties then Save_Lexer (Loc); Scan_Token; diff --git a/tests/SAE-standard-examples-01192009/example_023.aadl.out b/tests/SAE-standard-examples-01192009/example_023.aadl.out index eea407505814c5a254f69a134c315c359026a9a4..e7baea3f786c2a0c6db34c51e9826f0f68f9c116 100644 --- a/tests/SAE-standard-examples-01192009/example_023.aadl.out +++ b/tests/SAE-standard-examples-01192009/example_023.aadl.out @@ -1,3 +1,3 @@ -example_023.aadl:22:26: parsing Record_Term_Element, token '=>' is expected, found token ',' +example_023.aadl:22:27: parsing Record_Term_Element, token '=>' is expected, found token ',' example_023.aadl:20:01: parsing Connections, list is empty -Cannot parse AADL specifications \ No newline at end of file +Cannot parse AADL specifications diff --git a/tests/real-annexes-execution-environment/test_real_exec_env_01.aadl.out b/tests/real-annexes-execution-environment/test_real_exec_env_01.aadl.out index 43e7ae2bd858a70695bc8839d3bfb4a6af65e081..f0765f5d728d7571688124c7184600dfd84a2acc 100644 --- a/tests/real-annexes-execution-environment/test_real_exec_env_01.aadl.out +++ b/tests/real-annexes-execution-environment/test_real_exec_env_01.aadl.out @@ -34,3 +34,4 @@ test_env_subtheorem_call_with_empty_domain execution lib.real:38:01 Backends: warning : Empty range set, returned value is 0.0 value for x after evaluating sub_theorem_6 is 0.00000E+00 theorem test_env_subtheorem_call_with_empty_domain is: TRUE + diff --git a/tests/real-annexes-execution/test_real_exec_05.aadl.out b/tests/real-annexes-execution/test_real_exec_05.aadl.out index 45fb7c34261fdf6163a11defb8659b3d112c24da..a54f93302f3c779e6c61a2341c2467a744899343 100644 --- a/tests/real-annexes-execution/test_real_exec_05.aadl.out +++ b/tests/real-annexes-execution/test_real_exec_05.aadl.out @@ -56,3 +56,4 @@ theorem test_head_and_queue is: TRUE test_reference_property execution theorem test_reference_property is: TRUE + diff --git a/tests/real-annexes-parsing/test_real_parse_01.aadl.out b/tests/real-annexes-parsing/test_real_parse_01.aadl.out index dd40fc4adf36749a069f99fde6455039da86aac7..abec09f8dd8f0e0e336b1a7dde600ba579bf128d 100644 --- a/tests/real-annexes-parsing/test_real_parse_01.aadl.out +++ b/tests/real-annexes-parsing/test_real_parse_01.aadl.out @@ -44,6 +44,22 @@ property set Deployment is Configuration : aadlstring applies to (device); + Config : aadlstring + applies to (device); + + ASN1_Module_Name : aadlstring + applies to ( all); + + Help : aadlstring + applies to ( all); + + Version : aadlstring + applies to ( all); + + Configuration_Type : classifier ( +data) + applies to ( all); + end Deployment; package RMAAadl diff --git a/tests/real-annexes-parsing/test_real_parse_02.aadl.out b/tests/real-annexes-parsing/test_real_parse_02.aadl.out index a6c176d312564acaa8cbda6ac02d64f3cf28c93d..b0a8713cdd76f6bc38aa95805b03e1bf0cede220 100644 --- a/tests/real-annexes-parsing/test_real_parse_02.aadl.out +++ b/tests/real-annexes-parsing/test_real_parse_02.aadl.out @@ -44,6 +44,22 @@ property set Deployment is Configuration : aadlstring applies to (device); + Config : aadlstring + applies to (device); + + ASN1_Module_Name : aadlstring + applies to ( all); + + Help : aadlstring + applies to ( all); + + Version : aadlstring + applies to ( all); + + Configuration_Type : classifier ( +data) + applies to ( all); + end Deployment; package RMAAadl diff --git a/tests/real-annexes-parsing/test_real_parse_03.aadl.out b/tests/real-annexes-parsing/test_real_parse_03.aadl.out index c72da929b6c64fb1a74afbd64ef39e5cbf372bd6..b2441a19afd25ce332c72f0dc6d3b3724a45d5c9 100644 --- a/tests/real-annexes-parsing/test_real_parse_03.aadl.out +++ b/tests/real-annexes-parsing/test_real_parse_03.aadl.out @@ -44,6 +44,22 @@ property set Deployment is Configuration : aadlstring applies to (device); + Config : aadlstring + applies to (device); + + ASN1_Module_Name : aadlstring + applies to ( all); + + Help : aadlstring + applies to ( all); + + Version : aadlstring + applies to ( all); + + Configuration_Type : classifier ( +data) + applies to ( all); + end Deployment; package RMAAadl diff --git a/tests/real-annexes-parsing/test_real_parse_04.aadl.out b/tests/real-annexes-parsing/test_real_parse_04.aadl.out index f336c21f314adbcbd8da32cb0f23039bd9a65509..c2e0ea319743d4dcbcf111a5dc10bf00d93d8834 100644 --- a/tests/real-annexes-parsing/test_real_parse_04.aadl.out +++ b/tests/real-annexes-parsing/test_real_parse_04.aadl.out @@ -44,6 +44,22 @@ property set Deployment is Configuration : aadlstring applies to (device); + Config : aadlstring + applies to (device); + + ASN1_Module_Name : aadlstring + applies to ( all); + + Help : aadlstring + applies to ( all); + + Version : aadlstring + applies to ( all); + + Configuration_Type : classifier ( +data) + applies to ( all); + end Deployment; package RMAAadl diff --git a/tests/real-annexes-parsing/test_real_parse_05.aadl.out b/tests/real-annexes-parsing/test_real_parse_05.aadl.out index ddbc76e2479fce3a1fea0c2d8aa7228f30818169..dd651991cb14255e9b7b4060990bbac720fa9432 100644 --- a/tests/real-annexes-parsing/test_real_parse_05.aadl.out +++ b/tests/real-annexes-parsing/test_real_parse_05.aadl.out @@ -44,6 +44,22 @@ property set Deployment is Configuration : aadlstring applies to (device); + Config : aadlstring + applies to (device); + + ASN1_Module_Name : aadlstring + applies to ( all); + + Help : aadlstring + applies to ( all); + + Version : aadlstring + applies to ( all); + + Configuration_Type : classifier ( +data) + applies to ( all); + end Deployment; package RMAAadl diff --git a/tests/test_ocarina_help/dummy.aadl.out b/tests/test_ocarina_help/dummy.aadl.out index 6686e626b251449a28d343f96d2e7f3c30ea4e09..7a57b044c89f22d8f01b644da2f2ce4bcca8abd5 100644 --- a/tests/test_ocarina_help/dummy.aadl.out +++ b/tests/test_ocarina_help/dummy.aadl.out @@ -50,6 +50,7 @@ Usage: carts asn1_deployment cheddar + connection_matrix aadl aadl_min aadl_annex