Skip to content

Behavior Annex type conformance is disabled, so no type mismatch is reported 🤖 #3199

Description

@lwrage

Summary

AdaLikeDataTypeChecker.conformsTo returns true for every pair of types. Its whole body is commented out behind the
note "As type checking is not mature, we disable it", so no Behavior Annex check that compares two types can fail.

Observed: an external model that assigns a string to an integer-typed behavior variable, sends an integer on a
string-classified out event data port, adds a string to an integer, and compares an integer with a string is accepted
with zero diagnostics.

Inferred mechanism: every comparison routes through that method. Its own comment lists the affected checks, and each
one is reachable from AadlBaTypeChecker: assignment target against value, port send port against value, port dequeue
port against target, for/forall iterated values against the iterative variable, integer range bounds, and subprogram
call parameters. Two more are not in that list: getTopLevelType, which can therefore never return null, and the
operand-consistency guard at the top of checkDefinition.

Operator applicability is still checked, so this is not a total loss of type checking: and on a non-boolean, < on a
non-alphanumeric, and mod on a non-integer are still reported by checkDefinition after the disabled guard passes.
What is missing is agreement between the two types in every construct that pairs them.

Reproduction

package TypeMismatch
public
	with Base_Types;

	abstract mismatch
	features
		out_text: out event data port Base_Types::String;
	end mismatch;

	abstract implementation mismatch.i
	annex behavior_specification {**
		variables
			counter : Base_Types::Integer;
		states
			start : initial state;
			done : final state;
		transitions
			assign_wrong_type : start -[ ]-> done { counter := "text" };
			send_wrong_type : start -[ ]-> done { out_text!(42) };
			mixed_operands : start -[ ]-> done { counter := 1 + "text" };
			mixed_relation : start -[ ]-> done { counter := 1; if (counter < "text") counter := 2 end if };
	**};
	end mismatch.i;
end TypeMismatch;

Validated with the Behavior Annex validator registered (BehaviorAnnexInjectorProvider, as Issue3174Test and
CoveringSemanticTest do). The model has no AADL or Behavior Annex syntax errors and the resolver builds a complete
strict model; the issue count is 0.

Expected behavior

Each of the four transitions reports exactly one error naming the two types that disagree. AS5506/3 Rev A D.6 states the
assignment rule directly — "In an assignment action, the type of the value expression must match the type of the target"
— and D.7 requires operand consistency for the arithmetic and relational operators. assign_wrong_type and
mixed_operands are D.6/D.7 legality failures, send_wrong_type fails the D.5 port send obligation, and
mixed_relation fails D.7.

The substance of the work is not the one-line re-enable: turning conformsTo back on will surface diagnostics across the
checked-in corpus, including models/covering_semantic, models/covering_syntax, and the standard examples under
org.osate.ba/examples. Every model that starts reporting has to be triaged into "the model is wrong and the fixture
must change", "the rule is right but the message or location is wrong", and "the commented-out rule itself is wrong for
Rev A" — the last is likely for the fixed-point/universal-real and dimension clauses in the disabled body. The
characterization goldens under ba/org.osate.ba.tests/expected/diagnostics make that triage measurable.

Relevant code

  • ba/org.osate.ba/src/org/osate/ba/analyzers/AdaLikeDataTypeChecker.javaconformsTo (line 71, returns true with
    the body commented out), getTopLevelType (line 127), and the guard in checkDefinition (line 143).
  • ba/org.osate.ba/src/org/osate/ba/analyzers/AadlBaTypeChecker.java — the callers: checkAssignment (line 216),
    checkPortSend (line 240), checkInternalPortSend (line 260), checkPortDequeue (line 282), checkElementValues
    (line 329).
  • ba/org.osate.ba.tests/models/issue3174/InternalPortTypes.aadl and
    Issue3174Test.internalEventWithoutDataCarriesNoValue already record the same dormancy for internal ports: that test
    asserts the two data-less-internal-event diagnostics and documents why the two wrong-typed transitions in the same
    model produce nothing.
  • ba/doc/conformance.md overstates the current state in its D.6 row ("Type checks, conflicting assignments in action
    sets, and static minimum/maximum computation-time checks exist"), which is why none of the G or V findings covers this.

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

    Type

    Projects

    No projects

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions