Почему этот простой пример аннотации не отклоняется в Статическом анализе кода?

Question

Я использую SAL, чтобы убедиться, что все пути кода, которые создают объект X должен позвонить X::work() прежде чем уничтожить его.

#include <sal.h>

class X {
    bool worked = false;
public:
    _Post_satisfies_(!worked)
    X() : worked(false) {}

    _Post_satisfies_(worked)
    void work() {
        worked = true;
    }

    _Pre_satisfies_(worked)
    ~X() {
    }
};

int main() {
    X x;
    X y; // Does not call work() but still passes the test anyway
    x.work();
}

Когда я удаляю x.work()затем возникает ошибка, как и предполагалось:

warning C28020: The expression 'this->worked' is not true at this call.

Но как только я добавлю work() за один объект x, другой y Также, кажется, пройти тест. Есть ли проблема в моей аннотации?