diff options
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/misc/Constants.fst | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/tests/misc/Constants.fst b/tests/misc/Constants.fst index e1a942a0..f5bd41cb 100644 --- a/tests/misc/Constants.fst +++ b/tests/misc/Constants.fst @@ -4,3 +4,13 @@ module Constants open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** [constants::X0] *) +let x0_body : result u32 = Return 0 +let x0_c : u32 = eval_global x0_body + +(** [core::num::u32::{8}::MAX] *) +let core_num_u32_max_body : result u32 = Return 4294967295 +let core_num_u32_max_c : u32 = eval_global core_num_u32_max_body + +(** [constants::X1] *)
\ No newline at end of file |