I'm using VST v1.7.
Has anyone ever proved that an int is equal as an array of characters? Something along those lines:
Definition int2uchars (i : int) : list Z :=
[
Int.unsigned (Int.and (Int.shru i (Int.repr 24)) (Int.repr 255));
Int.unsigned (Int.and (Int.shru i (Int.repr 16)) (Int.repr 255));
Int.unsigned (Int.and (Int.shru i (Int.repr 8)) (Int.repr 255));
Int.unsigned (Int.and (Int.shru i (Int.repr 0)) (Int.repr 255))
].
Lemma int2chararray :
forall (i : int) (v : val),
field_at Tsh tuint [] (Vint i) v
= data_block Tsh (int2uchars i) v.
Is there another solution than breaking the field_at abstraction to prove that?
