Spécification du moment où une annotation est applicable et dans quel cas

  • Article

Lorsqu’une annotation est conditionnelle, il peut nécessiter d’autres annotations pour spécifier cela à l’analyseur. Par exemple, si une fonction a une variable qui peut être synchrone ou asynchrone, la fonction se comporte comme suit : Dans le cas synchrone, elle réussit toujours, mais dans le cas asynchrone, elle signale une erreur si elle ne peut pas réussir immédiatement. Lorsque la fonction est appelée de façon synchrone, case activée la valeur de résultat ne fournit aucune valeur à l’analyseur de code, car elle n’aurait pas retourné. Toutefois, lorsque la fonction est appelée de façon asynchrone et que le résultat de la fonction n’est pas case activée ed, une erreur grave peut se produire. Cet exemple illustre une situation dans laquelle vous pouvez utiliser l’annotation _When_ décrite plus loin dans cet article pour activer case activée ing.

Annotations structurelles

Pour contrôler quand et où les annotations s’appliquent, utilisez les annotations structurelles suivantes.

Annotation Description
_At_(expr, anno-list) expr est une expression qui génère une valeur lvalue. Les annotations contenues anno-list sont appliquées à l’objet nommé par expr. Pour chaque annotation dans anno-list, expr est interprétée en pré-condition si l’annotation est interprétée en pré-condition et en post-condition si l’annotation est interprétée dans la post-condition.
_At_buffer_(expr, iter, elem-count, anno-list) expr est une expression qui génère une valeur lvalue. Les annotations contenues anno-list sont appliquées à l’objet nommé par expr. Pour chaque annotation dans anno-list, expr est interprétée en pré-condition si l’annotation est interprétée en condition préalable et en post-condition si l’annotation est interprétée dans la post-condition.

iter est le nom d’une variable délimitée à l’annotation (inclusive de anno-list). iter a un type longimplicite . Les variables nommées de façon identique dans n’importe quelle étendue englobante sont masquées de l’évaluation.

elem-count est une expression qui prend la valeur d’un entier.
_Group_(anno-list) Les annotations contenues anno-list sont toutes considérées comme ayant un qualificateur qui s’applique à l’annotation de groupe appliquée à chaque annotation.
_When_(expr, anno-list) expr est une expression qui peut être convertie en bool. Lorsqu’il n’est pas égal à zéro (true), les annotations spécifiées anno-list sont considérées comme applicables.

Par défaut, pour chaque annotation dans anno-list, expr est interprétée comme l’utilisation des valeurs d’entrée si l’annotation est une condition préalable et comme l’utilisation des valeurs de sortie si l’annotation est une condition postérieure. Pour remplacer la valeur par défaut, vous pouvez utiliser l’intrinsèque _Old_ lorsque vous évaluez une condition post-condition pour indiquer que les valeurs d’entrée doivent être utilisées. Remarque : Différentes annotations peuvent être activées en conséquence de l’utilisation _When_ d’une valeur mutable( par exemple, *pLengthparce que le résultat évalué de expr la condition préalable peut différer de son résultat évalué après condition.

Voir aussi