CBMC
complexity_violation.h File Reference
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Enumerations

enum class  complexity_violationt { NONE , LOOP , BRANCH }
 What sort of symex-complexity violation has taken place. More...
 

Enumeration Type Documentation

◆ complexity_violationt

enum complexity_violationt
strong

What sort of symex-complexity violation has taken place.

Loop: If we've violated a loop complexity boundary, or are part of a blacklisted loop. Branch: If this particular branch has been deemed too complex.

Enumerator
NONE 
LOOP 
BRANCH 

Definition at line 17 of file complexity_violation.h.