Is simplifyCallTree is wrong on Choice Nop t ?

[lambdageek]

simplifyCallTree (Choice a b) = case (simplifyCallTree a, simplifyCallTree b) of
  (a', Nop) -> a'
  (Nop, b') -> b'
  (a', b') -> Choice a' b'

This seems wrong to me. That's saying that fnA and fnB below are equivalent. Is that really what we want?

void f1 (void);
void f2 (void);

void fnA (int i) {
  if (i)
    f1 ();
  f2 ();
}

void fnB (int i) {
  f1 ();
  f2 ();
}

conditionally granting or revoking or needing or using a permissions shouldn't be the same as always having it, should it?

[evincarofautumn]

I think it should be the same? grant(a) | 0 checks both branches and unifies them, resulting in lacks(a) → has(a), the same as just grant(a). We don’t know which branch will be taken until runtime, so we assume both effects happen.

[lambdageek]

So never taking a lock and possibly-always taking a lock are the same? What class of bugs will this detect?

I think the join point at the end of the if should have a conflict: not every path results in a has(a) (ie: if f1 is mutex_lock() then at the end of the if we have a conflict: one branch has(locked) and the other one doesn't.) So we shouldn't even begin to consider f2