Sdílet prostřednictvím

Určení, kdy a kde se má poznámka použít

  • Článek

Pokud je poznámka podmíněná, může vyžadovat další poznámky, které se mají určit v analyzátoru. Pokud má například funkce proměnnou, která může být buď synchronní, nebo asynchronní, chová se takto: V synchronním případě vždy proběhne úspěšně, ale v asynchronním případě hlásí chybu, pokud nemůže být okamžitě úspěšná. Pokud je funkce volána synchronně, kontrola výsledné hodnoty neposkytuje analyzátoru kódu žádnou hodnotu, protože by se nevrátil. Pokud je však funkce volána asynchronně a výsledek funkce není kontrolován, může dojít k závažné chybě. Tento příklad ukazuje situaci, ve které můžete použít poznámku _When_ popsanou dále v tomto článku, abyste povolili kontrolu.

Strukturální poznámky

Pokud chcete určit, kdy a kde se poznámky používají, použijte následující strukturální poznámky.

Poznámka Popis
_At_(expr, anno-list) expr je výraz, který dává hodnotu lvalue. Poznámky jsou anno-list použity pro objekt, který je pojmenován .expr Pro každou anotaci je anno-listexpr interpretována v předmínce, pokud je poznámka interpretována v předmínce, a v post-condition, pokud je poznámka interpretována v post-condition.
_At_buffer_(expr, iter, elem-count, anno-list) expr je výraz, který dává hodnotu lvalue. Poznámky jsou anno-list použity pro objekt, který je pojmenován .expr Pro každou anotaci v anno-list, expr je interpretována v předmínce, pokud je poznámka interpretována v předběžné podmínky, a pokud je poznámka interpretována v post-condition.

iter je název proměnné, která je vymezena na poznámku (včetně anno-list). iter má implicitní typ long. Identické pojmenované proměnné v jakémkoli uzavřeném oboru jsou v vyhodnocení skryté.

elem-count je výraz, který se vyhodnotí jako celé číslo.
_Group_(anno-list) Všechny poznámky anno-list jsou považovány za kvalifikátor, který se vztahuje na poznámku skupiny použité u každé poznámky.
_When_(expr, anno-list) expr je výraz, který lze převést na bool. Pokud se jedná o nenulovou hodnotu (true), považují se za použitelné poznámky, které anno-list jsou zadány.

Ve výchozím nastavení je pro každou poznámku anno-listexpr interpretována jako použití vstupních hodnot, pokud je poznámka předběžnou podmínkou, a jako použití výstupních hodnot, pokud je poznámka po podmínce. Chcete-li přepsat výchozí hodnotu, můžete použít _Old_ vnitřní objekt při vyhodnocení po podmínce k označení, že se mají použít vstupní hodnoty. Poznámka: Různé poznámky mohou být povoleny v důsledku použití _When_ , pokud je například ztlumitelná hodnota *pLength, protože vyhodnocený výsledek expr předběžné podmínky se může lišit od vyhodnoceného výsledku po podmínce.

Viz také