Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] verification of enum safety

  • Subject: [Frama-c-discuss] verification of enum safety
  • From: dganesan at fc-md.umd.edu (Dharmalingam Ganesan)
  • Date: Wed, 12 Feb 2014 14:31:13 -0500
  • In-reply-to: <52F9EE09.2060600@cea.fr>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C7660449BC@Mail1.FCMD.local>, <52F9EE09.2060600@cea.fr>
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