//@ axiomatic b4fc_bit { predicate BTest(integer v); }

//@ predicate Impl(int x,int y) = (BTest(x) ==> BTest(y));

struct BStr {
	int* addr;
	int bitpos;
};

/*@
	assigns s->bitpos;
	ensures Impl(s->addr[0],s->addr[1]);
*/
int Read(struct BStr* s);

void Bitstream_WriteThenRead(struct BStr* s,int v) {
	int r = Read(s);
	//@ assert left: Impl(r,v);
}