--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on October 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Some information on invariant needs



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