指定何时以及在何处应用批注

  • 项目

当批注有条件时，可能需要为分析器指定其他批注。 例如，如果函数具有的变量可能是同步的或异步的，则函数的行为如下所示：在同步情况下，始终会成功，但在异步情况下，如果无法立即成功，则报告错误。 同步调用函数时，检查结果值不会为代码分析器提供任何值，因为不会返回任何值。 但是，异步调用函数且未检查函数结果时，可能会出现严重错误。 此示例演示了可以使用 _When_ 批注（本文后面会介绍）来启用检查的情况。

结构化批注

若要控制应用批注的时间和位置，请使用以下结构批注。

注释 说明
_At_(expr, anno-list) expr 是生成左值的表达式。 anno-list 中的注释应用于命名为 expr 的对象。 对于 anno-list 中的每个批注，如果批注在先决条件中解释，则 expr 解释为先决条件，如果在后置条件中解释，则解释为后置条件。
_At_buffer_(expr, iter, elem-count, anno-list) expr 是生成左值的表达式。 anno-list 中的注释应用于命名为 expr 的对象。 对于 anno-list 中的每个批注，如果批注在先决条件中解释，则 expr 解释为先决条件，如果在后置条件中解释，则解释为后置条件。

iter 是作用域为批注（包括 anno-list）的变量的名称。 iter 具有隐式类型 long。 任何封闭范围内的同名变量都隐藏在计算中。

elem-count 是计算结果为一个整数的表达式。
_Group_(anno-list) anno-list 中的所有批注都视为具有应用于每个批注的组批注的任何限定符。
_When_(expr, anno-list) expr 是可转换为 bool 的表达式。 为非零值 (true) 时，anno-list 中所指定的批注是适用的。

默认情况下，对于 anno-list 中的每个批注，如果批注是先决条件，则将 expr 解释为使用输入值；如果批注是后置条件，则解释为使用输出值。 若要替代默认值，可以在评估后置条件时使用 _Old_ 内部函数来指示应使用输入值。 注意：如果涉及可变值（例如 *pLength），使用 _When_ 可能会导致启用不同的批注，因为先决条件下 expr 的计算结果可能与后置条件下的评估结果不同。

另请参阅