added regtest

Author: DrMichaelPetter

src/analyses/apron/apronAnalysis.apron.ml

@@ -15,7 +15,8 @@ let spec_module: (module MCPSpec) Lazy.t =
       let name () = "apron"
     end
     in
-    let narrowing_gas = GobConfig.get_int "ana.apron.narrowing_gas" in
+    let narrowing_gas = GobConfig.get_int "ana.apron.narrowing_gas"
+    in
     if (narrowing_gas > 0) then
       let module Narrowed =
       struct
@@ -27,7 +28,7 @@ let spec_module: (module MCPSpec) Lazy.t =
         include NarrowingGas.DLifter (Spec) (PolyhedraChainParams)
         module A = Spec.A
         let access = Spec.access
-        let name () = "apron"
+        let name = Spec.name
       end
       in
       (module Narrowed)

src/lifters/narrowingGas.ml

@@ -40,7 +40,7 @@ struct
   let widen (b1, i1) (b2, i2) = (Base.widen b1 b2, max i1 i2) 
   let narrow (b1, i1) (b2, i2) = 
     let i' = max i1 i2 in
-    if i' <= ChainParams.n () then
+    if i' < ChainParams.n () then
       (Base.meet b1 b2, i' + 1)  (* Stop narrowing when counter exceeds limit. *)
     else
       (Base.narrow b1 b2, i')

tests/regression/89-apron3/04-polyhedra-narrowing1.c

@@ -0,0 +1,28 @@
+// SKIP TODO TERM PARAM: --set ana.apron.narrowing_gas 1 --set ana.activated[+] apron --set ana.apron.domain polyhedra
+// Apron is not precise enough for some nested loops
+#include <goblint.h>
+#include <stdio.h>
+
+int loops0(){
+  int i, j, k;
+  int a = 0;
+  for (i = 500; i >= 1; i--)
+  {
+    a++;
+    __goblint_check(a + i - 501 == 0); // needs 1x narrowing or octagons
+    int b = 0;
+    for (j = i; j >= 1; j--)
+    {
+        __goblint_check(a + b + j == 501); // needs 1x narrowing, octagons insufficient
+        b++;
+    }
+  }
+  return 0;
+}
+
+int main()
+{
+  loops0();
+ 
+  return 0;
+}