Add non-terminating hh-ex3

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

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 *)

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;
+}

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