From 029b5e43c3a82217e30a6104c854da226ea759f1 Mon Sep 17 00:00:00 2001 From: Snaipe Date: Thu, 3 Sep 2015 14:29:46 +0200 Subject: [PATCH] Added better theory sample --- samples/theories.c | 66 ++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 55 insertions(+), 11 deletions(-) diff --git a/samples/theories.c b/samples/theories.c index eb36d66..bd814de 100644 --- a/samples/theories.c +++ b/samples/theories.c @@ -1,19 +1,63 @@ #include +#include -TheoryDataPoints(theory, simple) = { - DataPoints(int, 1, 2, 3), - DataPoints(long, 314, 42) -}; +# define INT_DATAPOINTS DataPoints(int, 0, 1, 2, -1, -2, INT_MAX, INT_MIN) -Theory((int a, long b), theory, simple) { - cr_assume(a == 2); - printf("%d, %ld\n", a, b); +// Let's test the multiplicative properties of 32-bit integers: + +int bad_mul(int a, int b) { + return a * b; } -TheoryDataPoints(theory, float) = { - DataPoints(float, 3.14, 42), +int bad_div(int a, int b) { + return a / b; +} + +TheoryDataPoints(algebra, bad_divide_is_inverse_of_multiply) = { + INT_DATAPOINTS, + INT_DATAPOINTS, }; -Theory((float a), theory, float) { - printf("%f\n", (double) a); +Theory((int a, int b), algebra, bad_divide_is_inverse_of_multiply) { + cr_assume(b != 0); + cr_assert_eq(a, bad_div(bad_mul(a, b), b)); +} + +// The above implementation of mul & div fails the test because of overflows, +// let's try again: + +long long good_mul(long long a, long long b) { + return a * b; +} + +long long good_div(long long a, long long b) { + return a / b; +} + +TheoryDataPoints(algebra, good_divide_is_inverse_of_multiply) = { + INT_DATAPOINTS, + INT_DATAPOINTS, +}; + +Theory((int a, int b), algebra, good_divide_is_inverse_of_multiply) { + cr_assume(b != 0); + cr_assert_eq(a, good_div(good_mul(a, b), b)); +} + +// For triangulation + +Test(algebra, multiplication_by_integer) { + cr_assert_eq(10, good_mul(5, 2)); +} + +// Another property test + +TheoryDataPoints(algebra, zero_is_absorbing) = { + INT_DATAPOINTS, + INT_DATAPOINTS, +}; + +Theory((int a, int b), algebra, zero_is_absorbing) { + cr_assume(a == 0 || b == 0); + cr_assert_eq(0, good_mul(a, b)); }