summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSidney Congard2022-06-23 15:43:49 +0200
committerSidney Congard2022-06-23 15:43:49 +0200
commitda118da3e590fbea4e880121837da2ee938837f6 (patch)
tree8a02fe42c66363a8761eced685504a42a357aa94 /tests
parent7703c4ca86a390303d0a120f8811c8fd704c5168 (diff)
adapt to new LLBC (without OperandConstantValue)
Diffstat (limited to 'tests')
-rw-r--r--tests/misc/Constants.fst19
1 files changed, 19 insertions, 0 deletions
diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst
index 9611c778..28a9ace7 100644
--- a/tests/misc/Constants.fst
+++ b/tests/misc/Constants.fst
@@ -117,3 +117,22 @@ let get_z2_fwd : result i32 =
end
end
+(** [constants::S1] *)
+let s1_fwd : result u32 = Return 6
+
+(** [constants::S2] *)
+let s2_fwd : result u32 =
+ begin match s1_fwd with
+ | Fail -> Fail
+ | Return i ->
+ begin match incr_fwd i with | Fail -> Fail | Return i0 -> Return i0 end
+ end
+
+(** [constants::S3] *)
+let s3_fwd : result (pair_t u32 u32) =
+ begin match p3_fwd with | Fail -> Fail | Return p -> Return p end
+
+(** [constants::S4] *)
+let s4_fwd : result (pair_t u32 u32) =
+ begin match mk_pair1_fwd 7 8 with | Fail -> Fail | Return p -> Return p end
+