I wonder how it stacks up against Microsoft's SAL annotations. So far I've only used SAL annotation, with the compiler's /Analyze flag, but the amount of checki

I wonder how it stacks up against Microsoft's SAL annotations. So far I've only used SAL annotation, with the compiler's /Analyze flag, but the amount of checking done is limited, and the system itself is far from perfect, sometimes pointing to logical errors that are clearly not there. However it is still very useful. Maybe Frama-C is better?