diff options
Diffstat (limited to 'test/builtins/divmod.sail')
| -rw-r--r-- | test/builtins/divmod.sail | 92 |
1 files changed, 60 insertions, 32 deletions
diff --git a/test/builtins/divmod.sail b/test/builtins/divmod.sail index f9d7e7c5..458d8dfd 100644 --- a/test/builtins/divmod.sail +++ b/test/builtins/divmod.sail @@ -5,39 +5,67 @@ $include <arith.sail> $include <smt.sail> function main (() : unit) -> unit = { - assert(ediv_int( 7 , 5) == 1); - assert(ediv_int( 7 , -5) == -1); - assert(ediv_int(-7 , 5) == -2); - assert(ediv_int(-7 , -5) == 2); - assert(ediv_int( 12 , 3) == 4); - assert(ediv_int( 12 , -3) == -4); - assert(ediv_int(-12 , 3) == -4); - assert(ediv_int(-12 , -3) == 4); + assert(ediv_int(7, 5) == 1); + assert(ediv_int(7, -5) == -1); + assert(ediv_int(-7, 5) == -2); + assert(ediv_int(-7, -5) == 2); + assert(ediv_int(12, 3) == 4); + assert(ediv_int(12, -3) == -4); + assert(ediv_int(-12, 3) == -4); + assert(ediv_int(-12, -3) == 4); - assert(emod_int( 7 , 5) == 2); - assert(emod_int( 7 , -5) == 2); - assert(emod_int(-7 , 5) == 3); - assert(emod_int(-7 , -5) == 3); - assert(emod_int( 12 , 3) == 0); - assert(emod_int( 12 , -3) == 0); - assert(emod_int(-12 , 3) == 0); - assert(emod_int(-12 , -3) == 0); + assert(emod_int(7, 5) == 2); + assert(emod_int(7, -5) == 2); + assert(emod_int(-7, 5) == 3); + assert(emod_int(-7, -5) == 3); + assert(emod_int(12, 3) == 0); + assert(emod_int(12, -3) == 0); + assert(emod_int(-12, 3) == 0); + assert(emod_int(-12, -3) == 0); - assert(tdiv_int( 7 , 5) == 1); - assert(tdiv_int( 7 , -5) == -1); - assert(tdiv_int(-7 , 5) == -1); - assert(tdiv_int(-7 , -5) == 1); - assert(tdiv_int( 12 , 3) == 4); - assert(tdiv_int( 12 , -3) == -4); - assert(tdiv_int(-12 , 3) == -4); - assert(tdiv_int(-12 , -3) == 4); + assert(tdiv_int(7, 5) == 1); + assert(tdiv_int(7, -5) == -1); + assert(tdiv_int(-7, 5) == -1); + assert(tdiv_int(-7, -5) == 1); + assert(tdiv_int(12, 3) == 4); + assert(tdiv_int(12, -3) == -4); + assert(tdiv_int(-12, 3) == -4); + assert(tdiv_int(-12, -3) == 4); - assert(tmod_int( 7 , 5) == 2); - assert(tmod_int( 7 , -5) == 2); - assert(tmod_int(-7 , 5) == -2); - assert(tmod_int(-7 , -5) == -2); - assert(tmod_int( 12 , 3) == 0); - assert(tmod_int( 12 , -3) == 0); - assert(tmod_int(-12 , 3) == 0); - assert(tmod_int(-12 , -3) == 0); + assert(tmod_int(7, 5) == 2); + assert(tmod_int(7, -5) == 2); + assert(tmod_int(-7, 5) == -2); + assert(tmod_int(-7, -5) == -2); + assert(tmod_int(12, 3) == 0); + assert(tmod_int(12, -3) == 0); + assert(tmod_int(-12, 3) == 0); + assert(tmod_int(-12, -3) == 0); + + assert(fdiv_int(7, 5) == 1); + assert(fdiv_int(7, -5) == -2); + assert(fdiv_int(-7, 5) == -2); + assert(fdiv_int(-7, -5) == 1); + assert(fdiv_int(12, 3) == 4); + assert(fdiv_int(12, -3) == -4); + assert(fdiv_int(-12, 3) == -4); + assert(fdiv_int(-12, -3) == 4); + + assert(fmod_int(7, 5) == 2); + assert(fmod_int(7, -5) == -3); + assert(fmod_int(-7, 5) == 3); + assert(fmod_int(-7, -5) == -2); + assert(fmod_int(12, 3) == 0); + assert(fmod_int(12, -3) == 0); + assert(fmod_int(-12, 3) == 0); + assert(fmod_int(-12, -3) == 0); + + assert(fdiv_int(5, 2) == 2); + assert(fdiv_int(-5, -2) == 2); + assert(fdiv_int(5, -2) == -3); + assert(fdiv_int(-5, 2) == -3); + + assert(tdiv_int(5, 2) == 2); + assert(tdiv_int(-5, -2) == 2); + assert(tdiv_int(5, -2) == -2); + assert(tdiv_int(-5, 2) == -2); }
\ No newline at end of file |