Fix variable counting with ana.apron.invariant.one-var

Author: sim642

src/analyses/apron/apronAnalysis.apron.ml

@@ -542,7 +542,7 @@ struct
     |> List.enum
     |> Enum.filter_map (fun (lincons1: Lincons1.t) ->
         (* filter one-vars *)
-        if one_var || Apron.Linexpr0.get_size lincons1.lincons0.linexpr0 >= 2 then
+        if one_var || Lincons1.num_vars lincons1 >= 2 then
           CilOfApron.cil_exp_of_lincons1 lincons1
           |> Option.map e_inv
           |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp) && InvariantCil.exp_is_in_scope scope exp)

src/cdomains/apron/apronDomain.apron.ml

@@ -158,6 +158,15 @@ struct
 
   let show = Format.asprintf "%a" print
   let compare x y = String.compare (show x) (show y) (* HACK *)
+
+  let num_vars x =
+    (* Apron.Linexpr0.get_size returns some internal nonsense, so we count ourselves. *)
+    let size = ref 0 in
+    Lincons1.iter (fun coeff var ->
+        if not (Apron.Coeff.is_zero coeff) then
+          incr size
+      ) x;
+    !size
 end
 
 module Lincons1Set =

tests/regression/36-apron/12-traces-min-rpb1.t

@@ -14,81 +14,14 @@
     write with [mhp:{tid=[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}, lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110) (12-traces-min-rpb1.c:15:3-15:8)
     read with [mhp:{tid=[main]; created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110) (12-traces-min-rpb1.c:27:3-27:26)
   [Info][Witness] witness generation summary:
-    total: 12
+    total: 3
   [Info][Race] Memory locations race summary:
     safe: 0
     vulnerable: 0
     unsafe: 2
     total: 2
 
   $ yamlWitnessStrip < witness.yml
-  - entry_type: precondition_loop_invariant
-    location:
-      file_name: 12-traces-min-rpb1.c
-      file_hash: $STRIPPED_FILE_HASH
-      line: 29
-      column: 2
-      function: main
-    loop_invariant:
-      string: 2147483648LL + (long long )g >= 0LL
-      type: assertion
-      format: C
-    precondition:
-      string: -1LL + (long long )h == 0LL && -1LL + (long long )g == 0LL
-      type: assertion
-      format: C
-  - entry_type: precondition_loop_invariant
-    location:
-      file_name: 12-traces-min-rpb1.c
-      file_hash: $STRIPPED_FILE_HASH
-      line: 29
-      column: 2
-      function: main
-    loop_invariant:
-      string: 2147483647LL - (long long )g >= 0LL
-      type: assertion
-      format: C
-    precondition:
-      string: -1LL + (long long )h == 0LL && -1LL + (long long )g == 0LL
-      type: assertion
-      format: C
-  - entry_type: precondition_loop_invariant
-    location:
-      file_name: 12-traces-min-rpb1.c
-      file_hash: $STRIPPED_FILE_HASH
-      line: 29
-      column: 2
-      function: main
-    loop_invariant:
-      string: (0LL - (long long )g) + (long long )h == 0LL
-      type: assertion
-      format: C
-    precondition:
-      string: -1LL + (long long )h == 0LL && -1LL + (long long )g == 0LL
-      type: assertion
-      format: C
-  - entry_type: loop_invariant
-    location:
-      file_name: 12-traces-min-rpb1.c
-      file_hash: $STRIPPED_FILE_HASH
-      line: 29
-      column: 2
-      function: main
-    loop_invariant:
-      string: 2147483648LL + (long long )g >= 0LL
-      type: assertion
-      format: C
-  - entry_type: loop_invariant
-    location:
-      file_name: 12-traces-min-rpb1.c
-      file_hash: $STRIPPED_FILE_HASH
-      line: 29
-      column: 2
-      function: main
-    loop_invariant:
-      string: 2147483647LL - (long long )g >= 0LL
-      type: assertion
-      format: C
   - entry_type: loop_invariant
     location:
       file_name: 12-traces-min-rpb1.c
@@ -100,28 +33,6 @@
       string: (0LL - (long long )g) + (long long )h == 0LL
       type: assertion
       format: C
-  - entry_type: loop_invariant
-    location:
-      file_name: 12-traces-min-rpb1.c
-      file_hash: $STRIPPED_FILE_HASH
-      line: 19
-      column: 2
-      function: t_fun
-    loop_invariant:
-      string: 2147483648LL + (long long )g >= 0LL
-      type: assertion
-      format: C
-  - entry_type: loop_invariant
-    location:
-      file_name: 12-traces-min-rpb1.c
-      file_hash: $STRIPPED_FILE_HASH
-      line: 19
-      column: 2
-      function: t_fun
-    loop_invariant:
-      string: 2147483647LL - (long long )g >= 0LL
-      type: assertion
-      format: C
   - entry_type: loop_invariant
     location:
       file_name: 12-traces-min-rpb1.c
@@ -133,28 +44,6 @@
       string: (0LL - (long long )g) + (long long )h == 0LL
       type: assertion
       format: C
-  - entry_type: loop_invariant
-    location:
-      file_name: 12-traces-min-rpb1.c
-      file_hash: $STRIPPED_FILE_HASH
-      line: 14
-      column: 2
-      function: t_fun
-    loop_invariant:
-      string: 2147483648LL + (long long )g >= 0LL
-      type: assertion
-      format: C
-  - entry_type: loop_invariant
-    location:
-      file_name: 12-traces-min-rpb1.c
-      file_hash: $STRIPPED_FILE_HASH
-      line: 14
-      column: 2
-      function: t_fun
-    loop_invariant:
-      string: 2147483647LL - (long long )g >= 0LL
-      type: assertion
-      format: C
   - entry_type: loop_invariant
     location:
       file_name: 12-traces-min-rpb1.c