diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/misc/Constants.v | 4 | ||||
| -rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 43 | ||||
| -rw-r--r-- | tests/coq/misc/_CoqProject | 6 |
3 files changed, 19 insertions, 34 deletions
diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v index c9ec0daf..7d3e5a34 100644 --- a/tests/coq/misc/Constants.v +++ b/tests/coq/misc/Constants.v @@ -86,9 +86,7 @@ Definition y_body : result (Wrap_t i32) := Definition y_c : Wrap_t i32 := y_body%global. (** [constants::unwrap_y] *) -Definition unwrap_y_fwd : result i32 := - match y_c with | mkWrap_t i => Return i end -. +Definition unwrap_y_fwd : result i32 := Return y_c.(Wrap_val). (** [constants::YVAL] *) Definition yval_body : result i32 := i <- unwrap_y_fwd; Return i. diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index 7c5212b2..a5f6126b 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -460,37 +460,24 @@ Definition new_pair1_fwd : result (Struct_with_pair_t u32 u32) := (** [no_nested_borrows::test_constants] *) Definition test_constants_fwd : result unit := swt <- new_tuple1_fwd; - match swt with - | mkStruct_with_tuple_t p => - let (i, _) := p in - if negb (i s= 1%u32) + let (i, _) := swt.(Struct_with_tuple_p) in + if negb (i s= 1%u32) + then Fail_ Failure + else ( + swt0 <- new_tuple2_fwd; + let (i0, _) := swt0.(Struct_with_tuple_p) in + if negb (i0 s= 1%i16) then Fail_ Failure else ( - swt0 <- new_tuple2_fwd; - match swt0 with - | mkStruct_with_tuple_t p0 => - let (i0, _) := p0 in - if negb (i0 s= 1%i16) + swt1 <- new_tuple3_fwd; + let (i1, _) := swt1.(Struct_with_tuple_p) in + if negb (i1 s= 1%u64) + then Fail_ Failure + else ( + swp <- new_pair1_fwd; + if negb (swp.(Struct_with_pair_p).(Pair_x) s= 1%u32) then Fail_ Failure - else ( - swt1 <- new_tuple3_fwd; - match swt1 with - | mkStruct_with_tuple_t p1 => - let (i1, _) := p1 in - if negb (i1 s= 1%u64) - then Fail_ Failure - else ( - swp <- new_pair1_fwd; - match swp with - | mkStruct_with_pair_t p2 => - match p2 with - | mkPair_t i2 i3 => - if negb (i2 s= 1%u32) then Fail_ Failure else Return tt - end - end) - end) - end) - end + else Return tt))) . (** Unit test for [no_nested_borrows::test_constants] *) diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject index 16fcaf44..b8590272 100644 --- a/tests/coq/misc/_CoqProject +++ b/tests/coq/misc/_CoqProject @@ -5,9 +5,9 @@ Primitives.v Constants.v -External__Funs.v -External__Opaque.v -External__Types.v +External_Funs.v +External_Opaque.v +External_Types.v NoNestedBorrows.v Paper.v PoloniusList.v
\ No newline at end of file |