Il faut donc garder le pattern CEI à l'échelle d'une fonction, et tester les "invariants" de tout le protocole en plus.
Le plus difficile étant d'identifier les invariants de votre contrat. Pour certains contrats, il est possible de ne pas en avoir.