sal - 为什么静态代码分析中没有拒绝这个简单的注释示例？

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似乎也通过了测试。我的注释有问题吗？