[Eva] Traces domain: uses structural equality on expr

src/kernel_services/abstract_interp/bottom.ml

@@ -52,6 +52,12 @@ let equal equal x y = match x, y with
   | `Value vx, `Value vy -> equal vx vy
   | _                    -> false
 
+let compare compare a b = match a, b with
+  | `Bottom, `Bottom   -> 0
+  | `Bottom, _         -> -1
+  | _, `Bottom         -> 1
+  | `Value v, `Value w -> compare v w
+
 let is_included is_included x y = match x, y with
   | `Bottom, _           -> true
   | _, `Bottom           -> false
@@ -75,6 +81,10 @@ let pretty pretty fmt = function
   | `Bottom  -> Format.fprintf fmt "Bottom"
   | `Value v -> pretty fmt v
 
+let iter f = function
+  | `Bottom -> ()
+  | `Value v -> f v
+
 
 let counter = ref 0
 
@@ -163,7 +173,3 @@ module Top = struct
       (narrow vnarrow x y :> _ or_top_bottom)
 
 end
-
-let iter f = function
-  | `Bottom -> ()
-  | `Value v -> f v

src/kernel_services/abstract_interp/bottom.mli

@@ -41,6 +41,7 @@ val is_bottom: 'a or_bottom -> bool
 val non_bottom: 'a or_bottom -> 'a
 
 val equal:       ('a -> 'a -> bool) -> 'a or_bottom -> 'a or_bottom -> bool
+val compare:     ('a -> 'a -> int)  -> 'a or_bottom -> 'a or_bottom -> int
 val is_included: ('a -> 'a -> bool) -> 'a or_bottom -> 'a or_bottom -> bool
 val join:        ('a -> 'a -> 'a) -> 'a or_bottom -> 'a or_bottom -> 'a or_bottom
 val join_list:   ('a -> 'a -> 'a) -> 'a or_bottom list -> 'a or_bottom

src/plugins/value/value_parameters.ml

@@ -282,6 +282,21 @@ module TracesDomain = Domain_Parameter
       let default = false
     end)
 
+module TracesUnrollLoop = Domain_Parameter
+    (struct
+      let option_name = "-eva-traces-unroll-loop"
+      let help = "Specify if the traces domain should unroll the loops."
+      let default = true
+    end)
+
+module TracesUnifyLoop = Domain_Parameter
+    (struct
+      let option_name = "-eva-traces-unify-loop"
+      let help = "Specify if all the instances of a loop should try to share theirs traces."
+      let default = false
+    end)
+
+
 let () = Parameter_customize.set_group domains
 module Numerors_Real_Size =
   Int
@@ -313,6 +328,18 @@ let () =
   Numerors_Mode.set_possible_values ["relative"; "absolute"; "none"; "both"]
 let () = add_precision_dep Numerors_Mode.parameter
 
+let () = Parameter_customize.set_group domains
+module TracesStorage =
+  Bool
+    (struct
+      let option_name = "-eva-traces-storage"
+      let help = "Stores the states of the traces domain during the \
+                 analysis."
+      let default = true
+    end)
+let () = add_precision_dep TracesStorage.parameter
+
+
 (* -------------------------------------------------------------------------- *)
 (* --- Performance options                                                --- *)
 (* -------------------------------------------------------------------------- *)

src/plugins/value/value_parameters.mli

@@ -38,6 +38,8 @@ module SignDomain: Parameter_sig.Bool
 module PrinterDomain: Parameter_sig.Bool
 module NumerorsDomain: Parameter_sig.Bool
 module TracesDomain: Parameter_sig.Bool
+module TracesUnrollLoop: Parameter_sig.Bool
+module TracesUnifyLoop: Parameter_sig.Bool
 
 module ApronOctagon: Parameter_sig.Bool
 module ApronBox: Parameter_sig.Bool
@@ -55,6 +57,7 @@ module SymbolicLocsStorage: Parameter_sig.Bool
 module GaugesStorage: Parameter_sig.Bool
 module ApronStorage: Parameter_sig.Bool
 module BitwiseOffsmStorage: Parameter_sig.Bool
+module TracesStorage: Parameter_sig.Bool
 
 
 module AutomaticContextMaxDepth: Parameter_sig.Int

tests/value/traces/test4.i

@@ -2,6 +2,8 @@
    STDOPT: #"-eva-traces-domain -value-msg-key d-traces -slevel 10" +"-then-last -val -slevel 10 -print -no-eva-traces-domain"
 */
 
+/* Test of join inside a loop */
+
 int main(c){
   int tmp = 0;
   for(int i = 0; i < 100; i++){