--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on February 2014 ---
Hi, In my project, I have numerous enum types. One think we are checking is that all enum types are properly initialized/modified to valid instances during the life of a program. For example, this code, which I created for demo purpose, shows an invalid assignment. typedef enum {RED=0, BLUE=1} COLOR; typedef enum {SUN=0, MON=1, TUE=2} DAYS; COLOR color; int main() { color = TUE; /* This is invalid - COLOR should be RED or BLUE*/ } I wonder whether there is way for RTE and WP to automatically annotate and check such invalid usages. Currently, I'm doing it manually by searching through all enum types and explicitly creating ensures for each instance, and then using WP to prove all ensures automatically. This workaround was somewhat laborious and kind of error-prone. It will be good if the framework automatically handles such checkers without much user annotation. One more clarification: In the system I am analysing, BOOL is a typedef to unsigned char. Several thousand bool variables are used. We are checking whether all bool values are either 0 or 1. Currently, I'm searching the code base for all bool types and semi-automatically generate ensures such as 0 == bFlag || 1 == bFlag. I was wondering whether there is any feature within Frama-c that performs automated analysis of type constraints like this one. Thanks a lot. Dharma Thanks, Dharma