also test UserUnion.union_field0

project-everest · Jul 12, 2023 · d617656 · d617656
1 parent 9292a30
commit d617656
Showing 1 changed file with 4 additions and 0 deletions.
diff --git 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 _