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

当批注有条件时,可能需要为分析器指定其他批注。 例如,如果函数具有的变量可能是同步的或异步的,则函数的行为如下所示:在同步情况下,始终会成功,但在异步情况下,如果无法立即成功,则报告错误。 同步调用函数时,检查结果值不会为代码分析器提供任何值,因为不会返回任何值。 但是,异步调用函数且未检查函数结果时,可能会出现严重错误。 此示例演示了可以使用 _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 的计算结果可能与后置条件下的评估结果不同。

另请参阅