--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on October 2012 ---
Hello, I have a plugin that adds weak type invariants as pre- and postconditions of all functions that have a parameter of this type. For example, you can write typedef unsigned char admin_level; //@ type invariant admin_level_ti(admin_level al) = 0 <= al <= 2; Then, a function such as int foo(admin_level al) will have new pre- and postconditions. Or you can write typedef struct { unsigned char AES_key[32]; unsigned char validity; } key_t; typedef struct { key_t keys[2]; } keys_t; //@ type invariant keys_ti(keys_t *k) = (k->keys[0].validity == GOOD ==> k->keys[1].validity == BAD)&& (k->keys[1].validity == GOOD ==> k->keys[0].validity == BAD); Note that type invariants work on types, not on individual variables. So you can't uses them for the global variables in your examples. However, arrays are not fully supported. -- Best regards, Boris