C ISO 99 standard supports so-called "type punning". Here is a small example:
char *f(const char *x) {
union {
const char *x;
char *y;
} t;
t.x = x;
return t.y;
}
As you can see, here we're using union type to get rid of const modifier by accessing second field with the same type but without const.
VST:
Require Import VST.floyd.proofauto.
Require Import example.
Definition Vprog : varspecs. mk_varspecs prog. Defined.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Open Scope Z.
Definition f_spec : ident * funspec :=
DECLARE _f
WITH x : val
PRE [tptr tschar]
PROP ()
PARAMS (x)
GLOBALS ()
SEP (data_at_ Tsh (tptr tschar) x)
POST [tptr tschar]
PROP ()
LOCAL ()
SEP ().
Definition Gprog := ltac:(with_library prog [f_spec]).
Theorem test : semax_body Vprog Gprog f_f f_spec.
Proof.
start_function.
forward.
forward.
(* if you run entailer! here, you'll get False, which is unprovable *)
entailer!.
Admitted.
If you run this coq code, you'll get to unprovable goal(mentioned in the comment) where VST checks whether we're trying to get initialized field from union. It looks as follows:
ENTAIL Delta,
PROP ( )
LOCAL (lvar _t (Tunion __136 noattr) v_t; temp _x x)
SEP (data_at Tsh (Tunion __136 noattr) (inl x) v_t; data_at_ Tsh (tptr tschar) x)
|-- local (liftx (tc_val (tptr tschar) Vundef))
which transforms into False by entailer! tactic.
So, the questions are: 1) Why VST represents unions as disjoint sum?
2) Is this feature(type punning) not supported by VST?
3) Are there any workarounds around this issue excluding editing C code?
