Określanie warunków pojawiania się adnotacji
Gdy adnotacja jest warunkowe, może wymagać innych adnotacji, aby określić, że do tego narzędzia.Na przykład, jeśli funkcja ma zmienna, która może być synchroniczna lub asynchroniczna, funkcja zachowuje się następująco: W przypadku synchroniczne zawsze po pewnym czasie skutku, ale w przypadku asynchronicznych to zgłasza błąd, jeśli nie można pomyślnie natychmiast.Gdy funkcja jest wywoływana synchronicznie, sprawdzanie wartość wyniku zapewnia żadna wartość, do analizatora kodu, ponieważ nie będzie mieć zwracane.Jednakże gdy funkcja jest wywoływana asynchronicznie i wynik funkcji nie jest zaznaczone, może wystąpić po poważnym błędzie.Ten przykład ilustruje sytuację, w której można użyć _When_ adnotacji — opisano w dalszej części niniejszego artykułu — Aby włączyć sprawdzanie.
Adnotacje strukturalne
Aby kontrolować, kiedy i gdzie stosuje się adnotacje, należy użyć następujących adnotacji strukturalnych.
Adnotacja |
Opis |
|---|---|
_At_(expr, anno-list) |
exprto wyrażenie, której wynikiem jest wartość lvalue.Adnotacje w anno-list są stosowane do obiektu, który ma taką samą nazwę expr.Dla każdego wpisu anno-list, expr jest interpretowana w warunkiem wstępnym, jeżeli adnotacja jest interpretowana w warunek wstępny, a w post-condition, jeśli adnotacja jest interpretowana w post-condition. |
_At_buffer_(expr, iter, elem-count, anno-list) |
exprto wyrażenie, której wynikiem jest wartość lvalue.Adnotacje w anno-list są stosowane do obiektu, który ma taką samą nazwę expr.Dla każdego wpisu anno-list, expr jest interpretowana w warunkiem wstępnym, jeżeli adnotacja jest interpretowana w warunku wstępnego, a w post-condition, jeśli adnotacja jest interpretowana w post-condition. iterjest nazwą zmiennej, która obejmuje zasięgiem adnotacja (zawierający od anno-list).iter jest niejawnego typu long.Identycznie nazwane zmienne w dowolnym zamkniętym zakresie są ukryte przed oceną. elem-count to wyrażenie oceniane jako liczba całkowita. |
_Group_(anno-list) |
Adnotacje w anno-list wszystkie stwierdzenia, że wszelkie kwalifikator, którego dotyczy adnotacja grupy, która jest stosowana do każdej adnotacji. |
_When_(expr, anno-list) |
expr to wyrażenie, które można przekonwertować do wartości bool.Kiedy jest różna od zera (true), adnotacje, które są określone w anno-list są uznawane za mające zastosowanie. Domyślnie, w odniesieniu do każdego wpisu w anno-list, expr jest interpretowana jako przy użyciu wartości wejściowych, jeśli adnotacja jest warunkiem koniecznym, i jak za pomocą wartości wyjściowych, jeżeli adnotacja jest post-condition.Aby zastąpić ustawienia domyślne, można użyć _Old_ wewnętrzne, weryfikując post-condition, aby wskazać, że należy użyć wartości wejściowych. .gif "Uwaga") Uwaga
Adnotacje różnych może być włączona w związku z wykorzystaniem _When_ Jeśli wartość tych — na przykład, *pLength— jest zaangażowany, ponieważ obliczony wynik expr w warunku wstępnego może różnić się od jego obliczony wynik w post-condition.
|
Zobacz też
Informacje
Dodawanie adnotacji do parametrów funkcji i zwracanych wartości
Zachowanie funkcji dodawania adnotacji
Dodawanie adnotacji struktur i klas
Dodawanie adnotacji do zachowania blokującego
Najlepsze praktyki i przykłady (SAL)