Enforce Behavior Annex variable initialization 🤖

ba/doc/conformance.md

@@ -61,7 +61,7 @@ The review itself was a source and test-artifact audit. No Maven tests, simulato
 | D.4: thread dispatch | Dispatch conjunction/disjunction, `stop`, bare timeout, timeout with a duration, and an unparenthesized frozen-port list. Selected timeout/stop checks exist. | Partial. Required frozen-list parentheses were missing (G03) and timeout reset ports absent (G04), both since fixed. Full protocol/trigger compatibility and core-property consistency are not demonstrated. |
 | D.5: component interactions | Port send/dequeue/freeze, count/fresh/updated, shared-data lock/unlock syntax, and subprogram-call syntax/model classes. | Partial. `updated` was absent (G07), internal events were represented incorrectly (G10), and outgoing ports were accepted for the three input-freeze status values, all since fixed; call-signature and remaining communication direction/category checks need additional coverage. Input/output timing consistency is not established. |
 | D.6: action language | Assignment/`any`, sequences and sets, blocks, conditionals, loops with a written or an omitted iterator classifier, timed actions and processor bindings. Conflicting assignments in action sets and static minimum/maximum computation-time checks exist. | Partial. Type conformance is disabled outright, so no assignment, send, dequeue, range, or parameter type mismatch is reported (G18). Optional loop classifiers were missing (G09) and are now implemented; loop-variable assignment rejection was not enforced by the existing covering-test expectation (G16, since fixed, though the dequeue form is still open as [#3205](https://github.com/osate/osate2/issues/3205)); action-timeout catch and combination rules are now checked (V03), while resource-release and signature obligations remain incomplete or unverified. |
-| D.7: expressions | Boolean/numeric/string syntax, arithmetic/relational/logical operators, property references, indexing, and operator applicability checks per operand data representation. | Partial, with semantic preservation defects. Operand consistency between the two operands is not checked, only applicability of the operator to the first one (G18). Short-circuit logical operators, including in external conditions, and `updated` are now supported (#3166, #3169, and G07, since fixed), and value-expression precedence, association, admissible forms, and grouping now follow the document (G13, since fixed); numeric translation differs from the document, unary plus remains accepted as an extension but now produces a compatibility warning (G06), and initialization analysis is not demonstrated. |
+| D.7: expressions | Boolean/numeric/string syntax, arithmetic/relational/logical operators, property references, indexing, and operator applicability checks per operand data representation. | Partial, with semantic preservation defects. Operand consistency between the two operands is not checked, only applicability of the operator to the first one (G18). Short-circuit logical operators, including in external conditions, and `updated` are now supported (#3166, #3169, and G07, since fixed), and value-expression precedence, association, admissible forms, and grouping now follow the document (G13, since fixed); numeric translation differs from the document, unary plus remains accepted as an extension but now produces a compatibility warning (G06), and declarative initializer typing and definite initialization are now checked (#3190). Instance-dependent initialization from prefixed property values remains #3230. |
 | D.8: synchronization | `Behavior_Properties::Subprogram_Call_Protocol` declares HSER/LSER/ASER and defaults to HSER, matching the supplied document. A client/server example exists. | Property definition conforms. Enforcement of the two LSER/ASER legality rules and execution of the protocols are not established. |
 
 Useful positive evidence includes [CoveringSyntaxTest](../../ba/org.osate.ba.tests/src/org/osate/ba/tests/CoveringSyntaxTest.xtend), [CoveringSemanticTest](../../ba/org.osate.ba.tests/src/org/osate/ba/tests/CoveringSemanticTest.xtend), [GrammarHazards.aadl](../../ba/org.osate.ba.tests/models/characterization/GrammarHazards.aadl), [BehaviorAnnexIntegrationTest](../../ba/org.osate.xtext.aadl2.ba.tests/src/org/osate/xtext/aadl2/ba/tests/BehaviorAnnexIntegrationTest.java), and [Issue3153Test](../../ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3153Test.java), [Issue3154Test](../../ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3154Test.java), and [Issue3155Test](../../ba/org.osate.ba.tests/src/org/osate/ba/tests/Issue3155Test.java). The latter tests establish specific diagnostic behavior and source locations, rather than general standard coverage.
@@ -196,7 +196,7 @@ These are bounded findings from the inspected grammar/translator/checker path. E
 | V06 | D.4 protocol/trigger compatibility, legal trigger/frozen-port categories, and consistency with core dispatch/freeze properties. | The checker has dedicated timeout branches and a stop check, but no complete implementation of the document's protocol/trigger table was found. Dispatch references use generic `Reference` syntax. A rule implementing one timeout form is not evidence for all rows of the table. Test the matrix and invalid trigger direction/category through embedded source. |
 | V07 | D.5 C1/C2: BA freeze/send operations agree with `Input_Time`/`Output_Time`, or are absent where required. | No BA check referring to these properties was found in the active BA checker/translator/validator code. Core property validation alone does not establish agreement with BA actions. Use models that are individually legal on each side but inconsistent together. |
 | V08 | D.6: a complete state cannot be reached while shared data remains locked. | Lock/unlock syntax and holders exist; `Issue2372Test` checks resolved lock references. No path-sensitive lock-balance check was found. Cover a balanced path, an unreleased resource, alternative branches, loops, and wildcard lock/unlock. Parsing a lock operation does not establish this rule. |
-| V09 | D.7: right-hand-side variables/data must be initialized; declaration initialization overrides the Data Modeling `Initial_Value` property. | Variable initialization is copied, but `checkBehaviorVariable` does not check the initializer's value/type, and no definite-initialization flow analysis was found. Verify declaration precedence, read-before-write, and branch-dependent initialization separately from basic expression type compatibility. |
+| V09 | D.7: right-hand-side variables/data must be initialized; declaration initialization overrides the Data Modeling `Initial_Value` property. | Declaration initializer types and declarative definite initialization are checked by #3190. Explicit declaration initializers and unprefixed `Data_Model::Initial_Value` associations seed the analysis, with declaration initialization taking precedence. Instance-dependent initialization from prefixed property values is tracked by #3230 and blocked by #3229. |
 | V10 | D.7 property references are restricted to unitless properties or properties with time units. | Property reference machinery exists, but no explicit end-to-end check of this BA-specific restriction was identified. Add positive unitless/time cases and a property with another units type. Do not infer compliance merely because a property name resolves. |
 | V11 | D.8 LSER/ASER prohibits synchronous called-subprogram type and out/in-out parameters. | The [property set](../../ba/org.osate.ba.contrib/resources/properties/behavior_properties.aadl) matches the standard. Searches of BA and the core AADL validator found no checks consuming `Subprogram_Call_Protocol`; [ba_example_007.aadl](../../ba/org.osate.ba/examples/standard_examples/ba_example_007.aadl) describes the rules in comments but is not negative legality coverage. Add both prohibited combinations for both protocols. |
 

ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3190_DefiniteAssignment.txt

@@ -0,0 +1,4 @@
+error | semantic | 43 | 12 | 10 | Behavior variable 'guardValue' may be read before it is initialized
+error | semantic | 48 | 15 | 11 | Behavior variable 'branchValue' may be read before it is initialized
+error | semantic | 49 | 33 | 8 | Behavior variable 'setValue' may be read before it is initialized
+error | semantic | 54 | 33 | 9 | Behavior variable 'pathValue' may be read before it is initialized

ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba.tests_models_issue3190_InitializerType.txt

@@ -0,0 +1 @@
+error | semantic | 33 | 35 | 1 | type error for 'behavior variable initializer', 'Base_Types::Boolean' expected, found 'universal integer'.

ba/org.osate.ba.tests/expected/diagnostics-validated/org.osate.ba_examples_standard_examples_ba_example_007.txt

@@ -3,3 +3,5 @@ error | linking | 65 | 56 | 4 | Couldn't resolve reference to Property Constant,
 error | linking | 65 | 7 | 45 | Couldn't resolve reference to property definition 'Behavior_Properties::Subprogram_Call_Protocol'.
 error | linking | 67 | 56 | 4 | Couldn't resolve reference to Property Constant, Property Definition, Enumeration or Unit literal 'HSER'. For classifier references use classifier( <ref> ).
 error | linking | 67 | 7 | 45 | Couldn't resolve reference to property definition 'Behavior_Properties::Subprogram_Call_Protocol'.
+error | semantic | 54 | 12 | 1 | Behavior variable 'x' may be read before it is initialized
+error | semantic | 92 | 27 | 1 | Behavior variable 'v' may be read before it is initialized

ba/org.osate.ba.tests/expected/positions/org.osate.ba.tests_models_characterization_conformance_ShortCircuitOperators.txt

@@ -1,29 +1,30 @@
 annex[0] owner=ShortCircuitOperators::operation
-  (BehaviorAnnex, behavior_specification, 216, 246)
-  (BehaviorCondition, <null>, 368, 19)
-  (BehaviorCondition, <null>, 432, 18)
-  (BehaviorState, finish, 300, 6)
-  (BehaviorState, start, 275, 5)
-  (BehaviorStateGroup, <null>, 275, 21)
-  (BehaviorStateGroup, <null>, 300, 20)
-  (BehaviorTransition, and_then_transition, 338, 61)
-  (BehaviorTransition, or_else_transition, 403, 59)
+  (BehaviorAnnex, behavior_specification, 216, 255)
+  (BehaviorBooleanLiteral, <null>, 265, 5)
+  (BehaviorCondition, <null>, 377, 19)
+  (BehaviorCondition, <null>, 441, 18)
+  (BehaviorState, finish, 309, 6)
+  (BehaviorState, start, 284, 5)
+  (BehaviorStateGroup, <null>, 284, 21)
+  (BehaviorStateGroup, <null>, 309, 20)
+  (BehaviorTransition, and_then_transition, 347, 61)
+  (BehaviorTransition, or_else_transition, 412, 59)
   (BehaviorVariable, left, 229, 4)
   (BehaviorVariable, right, 235, 5)
-  (BehaviorVariableGroup, <null>, 229, 33)
-  (BinaryExpression, <null>, 368, 19)
-  (BinaryExpression, <null>, 432, 18)
-  (ExecuteCondition, <null>, 368, 19)
-  (ExecuteCondition, <null>, 432, 18)
-  (Reference, <null>, 368, 4)
-  (Reference, <null>, 382, 5)
-  (Reference, <null>, 432, 4)
-  (Reference, <null>, 445, 5)
-  (ReferenceExpression, <null>, 368, 4)
-  (ReferenceExpression, <null>, 382, 5)
-  (ReferenceExpression, <null>, 432, 4)
-  (ReferenceExpression, <null>, 445, 5)
-  (ReferenceSegment, left, 368, 4)
-  (ReferenceSegment, left, 432, 4)
-  (ReferenceSegment, right, 382, 5)
-  (ReferenceSegment, right, 445, 5)
+  (BehaviorVariableGroup, <null>, 229, 42)
+  (BinaryExpression, <null>, 377, 19)
+  (BinaryExpression, <null>, 441, 18)
+  (ExecuteCondition, <null>, 377, 19)
+  (ExecuteCondition, <null>, 441, 18)
+  (Reference, <null>, 377, 4)
+  (Reference, <null>, 391, 5)
+  (Reference, <null>, 441, 4)
+  (Reference, <null>, 454, 5)
+  (ReferenceExpression, <null>, 377, 4)
+  (ReferenceExpression, <null>, 391, 5)
+  (ReferenceExpression, <null>, 441, 4)
+  (ReferenceExpression, <null>, 454, 5)
+  (ReferenceSegment, left, 377, 4)
+  (ReferenceSegment, left, 441, 4)
+  (ReferenceSegment, right, 391, 5)
+  (ReferenceSegment, right, 454, 5)