From d617656a46edfe5596180767c5b4bbafd8717a45 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Tue, 11 Jul 2023 21:45:52 -0700 Subject: [PATCH] also test UserUnion.union_field0 --- src/cbor/CBOR.SteelC.fst | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/cbor/CBOR.SteelC.fst b/src/cbor/CBOR.SteelC.fst index 24b245a99..a0927d871 100644 --- a/src/cbor/CBOR.SteelC.fst +++ b/src/cbor/CBOR.SteelC.fst @@ -376,6 +376,10 @@ let test (#s: Ghost.erased cbor_case) (p: C.ref cbor_case_td) C.write ps 1729uL; Cu.ununion_field p "cbor_case_int64" ps; drop (Cu.has_union_field p "cbor_case_int64" _); + let ps = Cu.union_field0 p "cbor_case_int64" (C.scalar U64.t) in + C.write ps 42uL; + Cu.ununion_field p "cbor_case_int64" ps; + drop (Cu.has_union_field p "cbor_case_int64" _); let s' = vpattern_replace (C.pts_to p) in Cu.full_union cbor_case_union_def (Ghost.reveal s') "cbor_case_int64"; // FIXME: find a better pattern for that lemma return _