Commits on Feb 3, 2021

1. Emit exhaustivity warning despite uninhabited types …

   An abstract sealed class with no subtypes is uninhabited (ignoring null
   for 1 second).  Previously the pattern matcher added an eq axiom of
   "False" in this case, which wipes out the whole formula as the axioms
   are AND-ed together and with the rest of the pure prop formula.
   
   Keeping the definitions of enumerateSubtypes and domain/domainSyms as
   they are, I believe it's correct to fix this locally to removeVarEq.
   The branch is dead (indeed it gets a reachability warning) but that
   shouldn't preclude the emission of exhaustivity warnings.
   
   However, we should continue to wipe out the formula when the domain is
   that of the scrutinee variable.  While I was at it I made the variable
   ordering insertion order, which makes it deterministic.
   
   One additional consideration is modelNull/NullConst.  When that is
   present then the domain symbols won't be empty as it will contain the
   symbol reflecting the proposition that the variable may be null.  In a
   such case it's right to continue to add it as an axiom, because even
   "uninhabited" types may be inhabited by "null" (sadly).

   

   dwijnand committed Feb 3, 2021
   Copy the full SHA

   335aae6 View commit details

   Browse the repository at this point in the history