Track state by value with fictitious functions…

brand.c

/* frama-c test.c -wp -then -report */

struct foo {
	unsigned int x;
	double y;
};

/*@ ghost int state_table[1UL << 30]; */
/*@ ghost unsigned long count; */

/*@ axiomatic hash {
  @  logic long hash(struct foo x);
  @  axiom range: ∀ struct foo x; 0 ≤ hash(x) < (1UL << 30);
  @  axiom biject: ∀ struct foo x, y; x ≡ y ⇔ hash(x) ≡ hash(y);
  @ }
  @*/

/*@ predicate hash_state(struct foo x, integer state) =
  @   state_table[hash(x)] ≡ (int)state;
  @*/

/*@ assigns state_table[hash(x)];
  @ ensures hash_state(x, state);
  @*/
extern void set_state(struct foo x, int state);

/*@ assigns state_table[hash(\result)], count;
  @ ensures \old(hash_state(\result, 0));
  @ ensures hash_state(\result, 1);
  @ ensures count ≡ \old(count) + 1;
  @*/
extern struct foo open(void);

/*@ requires hash_state(*foo, 1);
  @ assigns state_table[hash(*foo)];
  @ ensures hash_state(*foo, 2);
  @*/
extern void frob(const struct foo *foo);

/*@ requires hash_state(*foo, 2);
  @ assigns state_table[hash(*foo)];
  @ ensures hash_state(*foo, 1);
  @*/
extern void unfrob(const struct foo *foo);

/*@ requires hash_state(foo, 1);
  @ requires count > 0;
  @ assigns state_table[hash(foo)], count;
  @ ensures hash_state(foo, 0);
  @ ensures count ≡ \old(count) - 1;
  @*/
extern void close(struct foo foo);

/*@ ensures count ≡ \at(count, Pre);
  @*/
int
main()
{
	struct foo x;
	struct foo y;

	x = open();
	frob(&x);
	y = open();

	frob(&y);
	unfrob(&x);

	close(x);

	frob(&x);
	frob(&y);

	close(x);
	close(y);
	return 0;
}