From c644ef14b02c0d20f42c468537b572969056a5ac Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jos=C3=A9=20Manuel=20Calder=C3=B3n=20Trilla?=
 <jmct@galois.com>
Date: Tue, 1 Oct 2019 10:35:59 -0400
Subject: [PATCH] Add ./configure option to suppress overflow warnings

This addresses part of the concerns in issue #39. If we know
the overflow is sound, then we can choose to skip printing
to `stderr` when the sound overflow occurs.

The implementation is straightforward:

* We added an option to `./configure`: `-no-warn-overflow`

* When enabled, this adds `-DNO_WARN_OVERFLOW` to `extra_elina_options`

* The printing to `stderr` in `elina_poly/opt_pk/vector.c:570` is now under
  a CPP macro that checks whether `-DNO_WARN_OVERFLOW` is defined.
---
 configure                  |  6 +++++-
 elina_poly/opt_pk_vector.c | 10 ++++++----
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/configure b/configure
index 1f908e5a..655c71f1 100755
--- a/configure
+++ b/configure
@@ -27,6 +27,7 @@ where options include:
   -use-ocamlfind       enable OCamlfind support
   -use-java            enable Java support (only available with APRON)
   -use-opam            use opam to install ELINA
+  -no-warn-overflow    Silence all output relating to sound overflow
 
 Environment variables that affect configuration:
   CC                   C compiler to use (default: gcc)
@@ -55,6 +56,7 @@ has_java=0
 use_opam=0
 has_apron=0
 has_vector=0
+extra_elina_options=""
 force_absolute_dylib_install_names=0;
 while : ; do
     case "$1" in
@@ -78,6 +80,8 @@ while : ; do
         -java-prefix|--java-prefix)
             java_prefix="$2"
             shift;;
+        -no-warn-overflow|--no-warn-overflow)
+            extra_elina_options+="-DNO_WARN_OVERFLOW";;
         -use-ocaml|--use-ocaml)
             has_ocaml=1;;
         -use-ocamlfind|--use-ocamlfind)
@@ -287,7 +291,7 @@ done
 if test "$cc" = "none"; then echo "no C compiler found"; exit 1; fi
 
 acc=""
-for i in $c_cxx_flags -Werror-implicit-function-declaration -Wbad-function-cast -Wstrict-prototypes -Wno-strict-overflow -std=c99 $CFLAGS $LDFLAGS
+for i in $c_cxx_flags -Werror-implicit-function-declaration -Wbad-function-cast -Wstrict-prototypes -Wno-strict-overflow -std=c99 $CFLAGS $LDFLAGS $extra_elina_options
 do
     checkcomp "$cc" "$i"
 done
diff --git a/elina_poly/opt_pk_vector.c b/elina_poly/opt_pk_vector.c
index 97e3e406..a8543641 100644
--- a/elina_poly/opt_pk_vector.c
+++ b/elina_poly/opt_pk_vector.c
@@ -566,10 +566,12 @@ void opt_vector_combine(opt_pk_internal_t* opk,
 
     ov3[k] = 0;
     if(flag){
-      fprintf(stderr, "exception \n");
-      fflush(stderr);
-      opk->exn = ELINA_EXC_OVERFLOW;
-      return;
+#ifndef NO_WARN_OVERFLOW
+             fprintf(stderr,"overflow exception \n");
+             fflush(stderr);
+#endif /* NO_WARN_OVERFLOW */
+             opk->exn = ELINA_EXC_OVERFLOW;
+             return ;
     }
     /*for (j=0; j<size; j++){
         if (opt_numint_abs(ov3[j]) > (ELINA_INT_MAX/2)){