Skip to content

Validate prefixed BA initialization per component instance 🤖 #3230

Description

@lwrage

Summary

Behavior Annex definite-initialization validation cannot decide whether a prefixed data-component reference is initialized from Data_Model::Initial_Value while validating the shared declarative classifier. Contained property associations can give different effective values to different instances of that classifier.

This is the instance-dependent portion split from #3190. It is blocked by #3229 because BA currently has no annex instantiation model or instance-side validation hook.

Reproduction

Define one component implementation with a data subcomponent that is read by its Behavior Annex. Instantiate that component twice, and apply Data_Model::Initial_Value through a contained property association to the data subcomponent of only one instance.

Declarative BA validation sees the same annex and data-subcomponent declaration for both instances, so it cannot distinguish the initialized instance from the uninitialized one.

Expected behavior

After #3229 provides an instance-side BA integration point, evaluate prefixed initialization separately for each component instance. Resolve the referenced data component to its corresponding instance object and use that object's effective Data_Model::Initial_Value. Report an uninitialized read only for instances where neither an effective initial value nor a dominating Behavior Annex assignment exists.

Unprefixed initialization of a local behavior variable remains declarative and is covered by #3190.

Blocked by #3229.

Relevant code

  • ba/org.osate.xtext.aadl2.ba/src/org/osate/xtext/aadl2/ba/validation/BehaviorAnnexValidator.java — classifier-scoped declarative validation.
  • ba/org.osate.xtext.aadl2.ba/src/org/osate/xtext/aadl2/ba/translation/DeclarativeToStrictTranslator.java — preservation and resolution of Behavior Annex references.
  • ba/org.osate.ba/src/org/osate/ba/analyzers/ — definite-initialization analysis introduced for Enforce Behavior Annex variable initialization rules 🤖 #3190.
  • core/org.osate.aadl2.instantiation/src/org/osate/aadl2/instantiation/AnnexInstantiationController.java — invokes registered annex instantiators after instance property caching.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions