diff options
| author | Guillaume Bertholon | 2018-07-16 13:30:37 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-11-01 10:20:15 +0100 |
| commit | 1b0bd3a9e3a913a4928b68546a134a1a4448f9e8 (patch) | |
| tree | 3cd5378c9810fcd546c5f12ca25673ffb4ec2421 /test-suite/primitive/uint63/addmuldiv.v | |
| parent | 5c24b95890f6b57e6f20b03ade543e1e9d1e8324 (diff) | |
Add tests for primitive floats
Add utility ldexp and frexp functions to prevent dealing with the shift of
ldshiftexp and frshiftexp everywhere.
Also move primitive integer tests to place all primitive tests in the
same directory.
Diffstat (limited to 'test-suite/primitive/uint63/addmuldiv.v')
| -rw-r--r-- | test-suite/primitive/uint63/addmuldiv.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/primitive/uint63/addmuldiv.v b/test-suite/primitive/uint63/addmuldiv.v new file mode 100644 index 0000000000..72b0164b49 --- /dev/null +++ b/test-suite/primitive/uint63/addmuldiv.v @@ -0,0 +1,12 @@ +Require Import Int63. + +Set Implicit Arguments. + +Open Scope int63_scope. + +Check (eq_refl : addmuldiv 32 3 5629499534213120 = 12887523328). +Check (eq_refl 12887523328 <: addmuldiv 32 3 5629499534213120 = 12887523328). +Check (eq_refl 12887523328 <<: addmuldiv 32 3 5629499534213120 = 12887523328). + +Definition compute2 := Eval compute in addmuldiv 32 3 5629499534213120. +Check (eq_refl compute2 : 12887523328 = 12887523328). |