Potentially undefined field not detected

[treiher]

The use of a potentially undefined field value is not detected in all cases. For example:

package Test is

   type T is mod 2**8;

   type M is
      message
         A : T
            then B
               if A = 1
            then C
               if A /= 1;
         B : T;
         C : T;
         D : Opaque
            with Size => B * 8;
      end message;

end Test;

The value of B cannot be used in the size aspect of D if A /= 1, as B is not present in this case: A -> C -> D.

[senier]

Looks like this class of issue is hitting us over and over again. @treiher Do you have an idea how to tackle this more systematically?

[treiher]

Looks like this class of issue is hitting us over and over again.

Is that really the case? In the last related issue that I can remember we had the opposite case: the checks were too strict (#492).

I cannot see a more systematic approach than the one we are already using: Each message path is separately analyzed using our type system. The current issue seems to be an implementation bug. The analysis of each of path is not that separate as it should be. The typing information for the expression B * 8 is kept from an analysis of another path which contains B.