From 198dc51e1d4d46cf05d191ae0ac2c2c043e428cc Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 1 Aug 2023 14:57:25 +0300
Subject: [PATCH] Add non-terminating hh-ex3

---
 src/cdomains/apron/apronDomain.apron.ml       |  6 ++--
 src/goblint.ml                                |  2 +-
 tests/regression/56-witness/63-hh-ex3-term.c  | 33 +++++++++++++++++++
 .../regression/56-witness/63-hh-ex3-term.yml  | 25 ++++++++++++++
 4 files changed, 62 insertions(+), 4 deletions(-)
 create mode 100644 tests/regression/56-witness/63-hh-ex3-term.c
 create mode 100644 tests/regression/56-witness/63-hh-ex3-term.yml

diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index d9928df597..7dffafe967 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -693,16 +693,16 @@ struct
 
   let join x y =
     (* just to optimize joining folds, which start with bot *)
-    if is_bot x then
+    if is_bot x then (* TODO: also for non-empty env *)
       y
-    else if is_bot y then
+    else if is_bot y then (* TODO: also for non-empty env *)
       x
     else (
       if M.tracing then M.traceli "apron" "join %a %a\n" pretty x pretty y;
       let j = join x y in
       if M.tracing then M.trace "apron" "j = %a\n" pretty j;
       let j =
-        if strengthening_enabled then
+        if strengthening_enabled then (* TODO: skip if same envs? *)
           strengthening j x y
         else
           j
diff --git a/src/goblint.ml b/src/goblint.ml
index a73d0a9fad..4ea3a3d242 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -73,7 +73,7 @@ let main () =
     exit 1
   | Sys.Break -> (* raised on Ctrl-C if `Sys.catch_break true` *)
     do_stats ();
-    (* Printexc.print_backtrace BatInnerIO.stderr *)
+    Printexc.print_backtrace stderr;
     eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted by SIGINT (Ctrl-C)!"));
     Goblint_timing.teardown_tef ();
     exit 131 (* same exit code as without `Sys.catch_break true`, otherwise 0 *)
diff --git a/tests/regression/56-witness/63-hh-ex3-term.c b/tests/regression/56-witness/63-hh-ex3-term.c
new file mode 100644
index 0000000000..0d90e8753f
--- /dev/null
+++ b/tests/regression/56-witness/63-hh-ex3-term.c
@@ -0,0 +1,33 @@
+// SKIP PARAM: --enable ana.int.interval --set ana.activated[+] apron --set ana.apron.domain polyhedra --enable ana.apron.strengthening --set ana.activated[+] unassume --set witness.yaml.unassume 63-hh-ex3-term.yml --enable ana.widen.tokens --disable witness.invariant.other --enable exp.arg
+extern void __assert_fail (const char *__assertion, const char *__file,
+      unsigned int __line, const char *__function)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+extern void __assert_perror_fail (int __errnum, const char *__file,
+      unsigned int __line, const char *__function)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+extern void __assert (const char *__assertion, const char *__file, int __line)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+
+extern void abort(void);
+void reach_error() { ((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "hh-ex3.c", 3, __extension__ __PRETTY_FUNCTION__); })); }
+void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } }
+int main() {
+  int i = 0;
+  while (i < 4) {
+    int j = 0;
+    while (j < 4) {
+      i++;
+      j++;
+      __VERIFIER_assert(0 <= j);
+      __VERIFIER_assert(j <= i);
+      __VERIFIER_assert(i <= j + 3);
+      __VERIFIER_assert(j <= 4);
+    }
+    __VERIFIER_assert(0 <= j);
+    __VERIFIER_assert(j <= i);
+    __VERIFIER_assert(i <= j + 3);
+    __VERIFIER_assert(j <= 4);
+    i = i - j + 1;
+  }
+  return 0;
+}
diff --git a/tests/regression/56-witness/63-hh-ex3-term.yml b/tests/regression/56-witness/63-hh-ex3-term.yml
new file mode 100644
index 0000000000..e635e24014
--- /dev/null
+++ b/tests/regression/56-witness/63-hh-ex3-term.yml
@@ -0,0 +1,25 @@
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: d834761a-d0d7-4fea-bf42-2ff2b9a19143
+    creation_time: 2022-10-12T10:59:25Z
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - /home/vagrant/eval-prec/prec/hh-ex3.i
+      input_file_hashes:
+        /home/vagrant/eval-prec/prec/hh-ex3.i: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f
+      data_model: LP64
+      language: C
+  location:
+    file_name: 63-hh-ex3-term.c
+    file_hash: 9c984e89a790b595d2b37ca8a05e5967a15130592cb2567fac2fae4aff668a4f
+    line: 17
+    column: 4
+    function: main
+  location_invariant:
+    string: 0 <= i && i <= 3
+    type: assertion
+    format: C