/**

* @name Inconsistent SAL annotation

* @description Annotations are different between declaration and definition.

* @kind problem

* @id cpp/inconsistent-sal

* @problem.severity warning

* @tags reliability

*/

import SAL

/** Holds if `e` has SAL annotation `name`. */

predicate hasAnnotation(DeclarationEntry e, string name) {

exists(SalAnnotation a |

a.getMacro().getName() = name and

a.getDeclarationEntry() = e

)

}

/** Holds if `e` is annotated to take its annotation from its declaration. */

predicate inheritsDeclAnnotations(DeclarationEntry e) {

// Is directly annotated

e.isDefinition() and

exists(SalAnnotation a | a.getMacro().getName() = "_Use_decl_annotations_" |

a.getDeclarationEntry() = e

)

or

// or is a parameter of a function with such an annotation

inheritsDeclAnnotations(e.(ParameterDeclarationEntry).getFunctionDeclarationEntry())

}

from DeclarationEntry e1, DeclarationEntry e2, string name

where

e1.getDeclaration() = e2.getDeclaration() and

hasAnnotation(e1, name) and

not hasAnnotation(e2, name) and

not name = "_Use_decl_annotations_" and

not inheritsDeclAnnotations(e2)

select e2,

"Missing SAL annotation " + name + " in " + e2.toString() + " although it is present on $@.", e1,

e1.toString()