Opened 2 years ago

#134 new enhancement

Unification is not the right logic for assertion resolution

Reported by: Thierry Delisle Owned by:
Priority: major Component: cfa-cc
Version: 1.0 Keywords:
Cc:

Description

Currently assertion resolution uses unification. This means that to check if a function can satisfy an assertion we use the same rules as to obtain the type of ternary if expression.

The leads to problems where an expression that would resolve normally doesn't necessarily resolve assertions.
For example:

forall( dtype T | sized(T) | { void ^?{}( T & ); } ) void delete( T * ptr );

monitor a {};
void ^?{}( T mutex & this );

int main() {
    a * p = ...;
    delete(a); // destructor does not unify because of mutex
}

To fix this we need to use check assertion satisfaction using resolution rather than unification.

Change History (0)

Note: See TracTickets for help on using tickets.