add hook_INT_neg (#807)

* add hook_INT_neg * add unit test * fix unit test
runtimeverification · Jul 20, 2023 · dd4815e · dd4815e
1 parent 91bc226
commit dd4815e
Show file tree

Hide file tree

Showing 2 changed files with 29 additions and 0 deletions.
diff --git a/runtime/arithmetic/int.cpp b/runtime/arithmetic/int.cpp
@@ -80,6 +80,13 @@ SortInt hook_INT_sub(SortInt a, SortInt b) {
   return move_int(result);
 }
 
+SortInt hook_INT_neg(SortInt a) {
+  mpz_t result;
+  mpz_init(result);
+  mpz_neg(result, a);
+  return move_int(result);
+}
+
 SortInt hook_INT_tdiv(SortInt a, SortInt b) {
   mpz_t result;
   if (mpz_sgn(b) == 0) {

diff --git a/unittests/runtime-arithmetic/inttest.cpp b/unittests/runtime-arithmetic/inttest.cpp
@@ -16,6 +16,7 @@ mpz_ptr hook_INT_add(mpz_t, mpz_t);
 mpz_ptr hook_INT_and(mpz_t, mpz_t);
 mpz_ptr hook_INT_mul(mpz_t, mpz_t);
 mpz_ptr hook_INT_sub(mpz_t, mpz_t);
+mpz_ptr hook_INT_neg(mpz_t);
 mpz_ptr hook_INT_tdiv(mpz_t, mpz_t);
 mpz_ptr hook_INT_ediv(mpz_t, mpz_t);
 mpz_ptr hook_INT_shl(mpz_t, mpz_t);
@@ -196,6 +197,27 @@ BOOST_AUTO_TEST_CASE(sub) {
   mpz_clear(b);
 }
 
+BOOST_AUTO_TEST_CASE(neg) {
+  mpz_t a;
+  mpz_ptr result;
+  mpz_init_set_ui(a, 7);
+  result = hook_INT_neg(a);
+  BOOST_CHECK_EQUAL(mpz_cmp_si(result, -7), 0);
+  mpz_clear(result);
+  free(result);
+  mpz_set_si(a, -7);
+  result = hook_INT_neg(a);
+  BOOST_CHECK_EQUAL(mpz_cmp_ui(result, 7), 0);
+  mpz_clear(result);
+  free(result);
+  mpz_set_ui(a, 0);
+  result = hook_INT_neg(a);
+  BOOST_CHECK_EQUAL(mpz_cmp_ui(result, 0), 0);
+  mpz_clear(result);
+  free(result);
+  mpz_clear(a);
+}
+
 BOOST_AUTO_TEST_CASE(tdiv) {
   mpz_t a, b;
   mpz_ptr result;