[Eva] Allow the partitioning to survive function returns

src/plugins/value/engine/compute_functions.ml

@@ -164,7 +164,7 @@ module Make (Abstract: Abstractions.Eva) = struct
      is the instruction at which the call takes place, and is used to update
      the statuses of the preconditions of [kf]. If [show_progress] is true,
      the callstack and additional information are printed. *)
-  let compute_using_spec_or_body call_kinstr call recursion state =
+  let compute_using_spec_or_body call_kinstr call recursion pkey state =
     let kf = call.kf in
     Value_results.mark_kf_as_called kf;
     let global = match call_kinstr with Kglobal -> true | _ -> false in
@@ -199,7 +199,8 @@ module Make (Abstract: Abstractions.Eva) = struct
         let vi = Kernel_function.get_vi kf in
         if Cil.is_in_libc vi.vattr then
           Library_functions.warn_unsupported_spec vi.vorig_name;
-        Spec.compute_using_specification ~warn:true call_kinstr call spec state,
+        Spec.compute_using_specification ~warn:true
+          call_kinstr call spec (pkey,state),
         Eval.Cacheable
       | `Def _fundec ->
         Db.Value.Call_Type_Value_Callbacks.apply (`Def, cvalue_state, call_stack);
@@ -215,9 +216,9 @@ module Make (Abstract: Abstractions.Eva) = struct
 
   module MemExec = Mem_exec.Make (Abstract.Val) (Abstract.Dom)
 
-  let compute_and_cache_call stmt call recursion init_state =
+  let compute_and_cache_call stmt call recursion pkey init_state =
     let default () =
-      compute_using_spec_or_body (Kstmt stmt) call recursion init_state
+      compute_using_spec_or_body (Kstmt stmt) call recursion pkey init_state
     in
     if Value_parameters.MemExecAll.get () then
       let args =
@@ -274,14 +275,14 @@ module Make (Abstract: Abstractions.Eva) = struct
     let rest = List.map (fun (e, assgn) -> e, lift_assigned assgn) call.rest in
     { call with arguments; rest }
 
-  let join_states = function
+  let join_states default_key = function
     | [] -> `Bottom
-    | [state] -> `Value state
-    | s :: l  -> `Value (List.fold_left Abstract.Dom.join s l)
+    | (_k,s) :: l  ->
+      `Value (default_key, List.fold_left Abstract.Dom.join s (List.map snd l))
 
-  let compute_call_or_builtin stmt call recursion state =
+  let compute_call_or_builtin stmt call recursion pkey state =
     match Builtins.find_builtin_override call.kf with
-    | None -> compute_and_cache_call stmt call recursion state
+    | None -> compute_and_cache_call stmt call recursion pkey state
     | Some (name, builtin, cacheable, spec) ->
       Value_results.mark_kf_as_called call.kf;
       let kinstr = Kstmt stmt in
@@ -293,11 +294,10 @@ module Make (Abstract: Abstractions.Eva) = struct
       (* Do not track garbled mixes created when interpreting the specification,
          as the result of the cvalue builtin will overwrite them. *)
       Locations.Location_Bytes.do_track_garbled_mix false;
-      let states =
-        Spec.compute_using_specification ~warn:false kinstr call spec state
-      in
+      let states = Spec.compute_using_specification
+          ~warn:false kinstr call spec (pkey,state) in
       Locations.Location_Bytes.do_track_garbled_mix true;
-      let final_state = states >>- join_states in
+      let final_state = join_states pkey states in
       let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
       match final_state with
       | `Bottom ->
@@ -305,24 +305,32 @@ module Make (Abstract: Abstractions.Eva) = struct
         Db.Value.Call_Type_Value_Callbacks.apply (`Spec spec, cvalue_state, cs);
         let cacheable = Eval.Cacheable in
         Transfer.{states; cacheable; builtin=true}
-      | `Value final_state ->
+      | `Value (pkey,final_state) ->
         let cvalue_call = get_cvalue_call call in
         let post = Abstract.Dom.get_cvalue_or_top final_state in
         let cvalue_states =
           Builtins.apply_builtin builtin cvalue_call ~pre:cvalue_state ~post
         in
         let insert cvalue_state =
-          Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state
+          pkey,Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state
         in
-        let states = Bottom.bot_of_list (List.map insert cvalue_states) in
+        let states = List.map insert cvalue_states in
         Transfer.{states; cacheable; builtin=true}
 
+  let recombine_keys compute =
+    fun stmt call recursion pkey state ->
+    let result = compute stmt call recursion Partition.Key.zero state in
+    let recombine (pkey',state') =
+      Partition.Key.recombine pkey pkey', state'
+    in
+    Transfer.{ result with states = List.map recombine result.states }
+
   let compute_call =
     if Abstract.Dom.mem Cvalue_domain.State.key
     && Abstract.Val.mem Main_values.CVal.key
     && Abstract.Loc.mem Main_locations.PLoc.key
-    then compute_call_or_builtin
-    else compute_and_cache_call
+    then recombine_keys compute_call_or_builtin
+    else recombine_keys compute_and_cache_call
 
   let () = Transfer.compute_call_ref := compute_call
 
@@ -339,11 +347,12 @@ module Make (Abstract: Abstractions.Eva) = struct
       let call =
         { kf; callstack = []; arguments = []; rest = []; return = None; }
       in
+      let pkey = Partition.Key.zero in
       let final_result =
-        compute_using_spec_or_body Kglobal call None init_state
+        compute_using_spec_or_body Kglobal call None pkey init_state
       in
-      let final_states = final_result.Transfer.states in
-      let final_state = PowersetDomain.(final_states >>-: of_list >>- join) in
+      let final_states = List.map snd (final_result.Transfer.states) in
+      let final_state = PowersetDomain.(final_states |> of_list |> join) in
       Value_util.pop_call_stack ();
       Value_parameters.feedback "done for function %a" Kernel_function.pretty kf;
       Abstract.Dom.Store.mark_as_computed ();

src/plugins/value/engine/iterator.ml

@@ -95,12 +95,12 @@ module Make_Dataflow
 
   (* --- Abstract values storage --- *)
 
-  module Partition = Trace_partitioning.Make (Abstract) (AnalysisParam)
+  module Partitioning = Trace_partitioning.Make (Abstract) (AnalysisParam)
 
-  type store = Partition.store
-  type flow = Partition.flow
-  type tank = Partition.tank
-  type widening = Partition.widening
+  type store = Partitioning.store
+  type flow = Partitioning.flow
+  type tank = Partitioning.tank
+  type widening = Partitioning.widening
 
   type edge_info = {
     mutable fireable : bool (* Does any states survive the transition ? *)
@@ -141,9 +141,9 @@ module Make_Dataflow
     | `Value state -> state
 
   let initial_tank =
-    Partition.initial_tank (States.to_list initial_states)
+    Partitioning.initial_tank (States.to_list initial_states)
   let get_initial_flow () =
-    -1 (* Dummy edge id *), Partition.drain initial_tank
+    -1 (* Dummy edge id *), Partitioning.drain initial_tank
 
   let post_conditions = ref false
 
@@ -180,11 +180,11 @@ module Make_Dataflow
 
   (* Default (Initial) stores on vertex and edges *)
   let default_vertex_store (v : vertex) () : store =
-    Partition.empty_store ~stmt:v.vertex_start_of
+    Partitioning.empty_store ~stmt:v.vertex_start_of
   let default_vertex_widening (v : vertex) () : widening =
-    Partition.empty_widening ~stmt:v.vertex_start_of
+    Partitioning.empty_widening ~stmt:v.vertex_start_of
   let default_edge_tank () : tank * edge_info =
-    Partition.empty_tank (), { fireable = false }
+    Partitioning.empty_tank (), { fireable = false }
 
   (* Get the stores associated to a control point or edge *)
   let get_vertex_store (v : vertex) : store =
@@ -217,24 +217,28 @@ module Make_Dataflow
 
   (* --- Transfer functions application --- *)
 
+  type key = Partition.key
   type state = Domain.t
 
-  type transfer_function = state -> state list
+  type transfer_function = (key * state) -> (key * state) list
 
-  let id : transfer_function = fun x -> [x]
+  let id : transfer_function = fun (k,x) -> [(k,x)]
 
   (* Thse lifting function helps to uniformize the transfer functions to a
      common signature *)
 
   let lift (f : state -> state) : transfer_function =
-    fun x -> [f x]
+    fun (k,x) -> [(k,f x)]
 
   let lift' (f : state -> state or_bottom) : transfer_function =
-    fun x -> Bottom.to_list (f x)
+    fun (k,x) -> Bottom.to_list (f x >>-: fun y -> k,y)
+
+  let lift'' (f : state -> state list) : transfer_function =
+    fun (k,x) -> List.map (fun y -> k,y) (f x)
 
   let sequence (f1 : transfer_function) (f2 : transfer_function)
     : transfer_function =
-    fun x -> List.fold_left (fun acc y -> f2 y @ acc) [] (f1 x)
+    fun (k,x) -> List.fold_left (fun acc (k',y) -> f2 (k',y) @ acc) [] (f1 (k,x))
 
 
   (* Tries to evaluate \assigns … \from … clauses for assembly code. *)
@@ -269,14 +273,14 @@ module Make_Dataflow
     if vars = [] then id else lift (Domain.leave_scope kf vars)
 
   let transfer_call (stmt : stmt) (dest : lval option) (callee : exp)
-      (args : exp list) (state : state) : state list =
+      (args : exp list) (key,state : key * state) : (key*state) list =
     let result, call_cacheable =
-      Transfer.call stmt dest callee args state
+      Transfer.call stmt dest callee args key state
     in
     if call_cacheable = Eval.NoCacheCallers then
       (* Propagate info that the current call cannot be cached either *)
       cacheable := Eval.NoCacheCallers;
-    Bottom.list_of_bot result
+    result
 
   let transfer_instr (stmt : stmt) (instr : instr) : transfer_function =
     match instr with
@@ -289,13 +293,13 @@ module Make_Dataflow
       lift' transfer
     | Local_init (vi, ConsInit (f, args, k), loc) ->
       let kind = Abstract_domain.Local kf in
-      let as_func dest callee args _loc state =
+      let as_func dest callee args _loc (key,state) =
         (* This variable enters the scope too early, as it should
            be introduced after the call to [f] but before the assignment
            to [v]. This is currently not possible, at least without
            splitting Transfer.call in two. *)
         let state = Domain.enter_scope kind [vi] state in
-        transfer_call stmt dest callee args state
+        transfer_call stmt dest callee args (key,state)
       in
       Cil.treat_constructor_as_func as_func vi f args k loc
     | Set (dest, exp, _loc) ->
@@ -331,7 +335,7 @@ module Make_Dataflow
     (* Assign the return value *)
     and assign_retval =
       match return_exp with
-      | None -> id
+      | None -> fun state -> [state]
       | Some return_exp ->
         let vi_ret = Option.get (Library_functions.get_retres_vi kf) in
         let return_lval = Var vi_ret, NoOffset in
@@ -342,7 +346,7 @@ module Make_Dataflow
           let state' = Transfer.assign state kstmt return_lval return_exp in
           Bottom.to_list state'
     in
-    sequence check_postconditions assign_retval
+    sequence (lift'' check_postconditions) (lift'' assign_retval)
 
   let transfer_transition (t : vertex transition) : transfer_function =
     match t with
@@ -357,7 +361,8 @@ module Make_Dataflow
     | Leave (block) ->            transfer_leave block
     | Prop _ -> id (* Annotations are interpreted in [transfer_statement]. *)
 
-  let transfer_annotations (stmt : stmt) ~(record : bool) : transfer_function =
+  let transfer_annotations (stmt : stmt) ~(record : bool)
+    : state -> state list =
     let annots =
       (* We do not interpret annotations that come from statement contracts
          and everything previously emitted by Value (currently, alarms) *)
@@ -395,20 +400,20 @@ module Make_Dataflow
       (transition : vertex transition) (flow : flow) : flow =
     (* Split return *)
     let flow = match transition with
-      | Return (return_exp, _) -> Partition.split_return flow return_exp
+      | Return (return_exp, _) -> Partitioning.split_return flow return_exp
       | _ -> flow
     in
     (* Loop transitions *)
     let the_stmt v = Option.get v.vertex_start_of in
     let enter_loop f v =
-      let f = Partition.enter_loop f (the_stmt v) in
-      Partition.transfer (lift (Domain.enter_loop (the_stmt v))) f
+      let f = Partitioning.enter_loop f (the_stmt v) in
+      Partitioning.transfer (lift (Domain.enter_loop (the_stmt v))) f
     and leave_loop f v =
-      let f = Partition.leave_loop f (the_stmt v) in
-      Partition.transfer (lift (Domain.leave_loop (the_stmt v))) f
+      let f = Partitioning.leave_loop f (the_stmt v) in
+      Partitioning.transfer (lift (Domain.leave_loop (the_stmt v))) f
     and incr_loop_counter f v =
-      let f = Partition.next_loop_iteration f (the_stmt v) in
-      Partition.transfer (lift (Domain.incr_loop_counter (the_stmt v))) f
+      let f = Partitioning.next_loop_iteration f (the_stmt v) in
+      Partitioning.transfer (lift (Domain.incr_loop_counter (the_stmt v))) f
     in
     let loops_left, loops_entered =
       Interpreted_automata.get_wto_index_diff kf v1 v2
@@ -422,14 +427,14 @@ module Make_Dataflow
   let process_edge (v1,e,v2 : G.edge) : flow =
     let {edge_transition=transition; edge_kinstr=kinstr} = e in
     let tank,edge_info = get_edge_data e in
-    let flow = Partition.drain tank in
+    let flow = Partitioning.drain tank in
     Db.yield ();
     check_signals ();
     current_ki := kinstr;
     Cil.CurrentLoc.set e.edge_loc;
-    let flow = Partition.transfer (transfer_transition transition) flow in
+    let flow = Partitioning.transfer (transfer_transition transition) flow in
     let flow = process_partitioning_transitions v1 v2 transition flow in
-    if not (Partition.is_empty_flow flow) then
+    if not (Partitioning.is_empty_flow flow) then
       edge_info.fireable <- true;
     flow
 
@@ -439,7 +444,7 @@ module Make_Dataflow
 
   let call_statement_callbacks (stmt : stmt) (f : flow) : unit =
     (* TODO: apply on all domains. *)
-    let states = Partition.contents f in
+    let states = Partitioning.contents f in
     let cvalue_states = gather_cvalues states in
     Db.Value.Compute_Statement_Callbacks.apply
       (stmt, Value_util.call_stack (), cvalue_states)
@@ -457,36 +462,37 @@ module Make_Dataflow
     (* Get vertex store *)
     let store = get_vertex_store v in
     (* Join incoming s tates *)
-    let flow = Partition.join sources store in
+    let flow = Partitioning.join sources store in
     let flow =
       match v.vertex_start_of with
       | Some stmt ->
         (* Callbacks *)
         call_statement_callbacks stmt flow;
         (* Transfer function associated to the statement *)
-        Partition.transfer (transfer_statement stmt) flow
+        Partitioning.transfer (lift'' (transfer_statement stmt)) flow
       | _ -> flow
     in
     (* Widen if necessary *)
     let flow =
-      if widening && not (Partition.is_empty_flow flow) then begin
-        let flow = Partition.widen (get_vertex_widening v) flow in
+      if widening && not (Partitioning.is_empty_flow flow) then begin
+        let flow = Partitioning.widen (get_vertex_widening v) flow in
         (* Try to correct over-widenings *)
         let correct_over_widening stmt =
           (* Do *not* record the status after interpreting the annotation
              here. Possible unproven assertions have already been recorded
              when the assertion has been interpreted the first time higher
              in this function. *)
-          Partition.transfer (transfer_annotations stmt ~record:false) flow
+          Partitioning.transfer
+            (lift'' (transfer_annotations stmt ~record:false)) flow
         in
         Option.fold ~some:correct_over_widening ~none:flow v.vertex_start_of
       end else
         flow
     in
     (* Dispatch to successors *)
-    List.iter (fun into -> Partition.fill flow ~into) (get_succ_tanks v);
+    List.iter (fun into -> Partitioning.fill flow ~into) (get_succ_tanks v);
     (* Return whether the iterator should stop or not *)
-    Partition.is_empty_flow flow
+    Partitioning.is_empty_flow flow
 
   let process_vertex ?(widening : bool = false) (v : vertex) : bool =
     (* Process predecessors *)
@@ -509,7 +515,7 @@ module Make_Dataflow
     (* Try every possible successor *)
     let add_if_fireable (_,e,succ as edge) acc =
       let f = process_edge edge in
-      if Partition.is_empty_flow f
+      if Partitioning.is_empty_flow f
       then acc
       else (e.edge_key,f,succ) :: acc
     in
@@ -525,13 +531,13 @@ module Make_Dataflow
   let reset_component (vertex_list : vertex list) : unit =
     let reset_edge (_,e,_) =
       let t,_ = get_edge_data e in
-      Partition.reset_tank t
+      Partitioning.reset_tank t
     in
     let reset_vertex v =
       let s = get_vertex_store v
       and w = get_vertex_widening v in
-      Partition.reset_store s;
-      Partition.reset_widening w;
+      Partitioning.reset_store s;
+      Partitioning.reset_widening w;
       List.iter reset_edge (G.succ_e graph v)
     in
     List.iter reset_vertex vertex_list
@@ -547,7 +553,7 @@ module Make_Dataflow
          is especially useful for nested loops. *)
       if hierachical_convergence
       then reset_component (v :: Wto.flatten w)
-      else Partition.reset_widening_counter (get_vertex_widening v);
+      else Partitioning.reset_widening_counter (get_vertex_widening v);
       (* Iterate until convergence *)
       let iteration_count = ref 0 in
       while
@@ -578,7 +584,7 @@ module Make_Dataflow
   let mark_degeneration () =
     let f stmt (v,_) =
       let l = get_succ_tanks v in
-      if not (List.for_all Partition.is_empty_tank l) then
+      if not (List.for_all Partitioning.is_empty_tank l) then
         Value_util.DegenerationPoints.replace stmt false
     in
     StmtTable.iter f automaton.stmt_table;
@@ -594,7 +600,7 @@ module Make_Dataflow
     ignore (Logic.check_fct_postconditions kf active_behaviors Normal
               ~pre_state:initial_state ~post_states:States.empty ~result:None)
 
-  let compute () : state list or_bottom =
+  let compute () : (key*state) list =
     if interpreter_mode then
       simulate automaton.entry_point (get_initial_flow ())
     else begin
@@ -603,7 +609,7 @@ module Make_Dataflow
     end;
     if not !post_conditions then mark_postconds_as_true ();
     let final_store = get_vertex_store automaton.return_point in
-    Bottom.bot_of_list (Partition.expanded final_store)
+    Partitioning.expanded final_store
 
 
   (* --- Results conversion --- *)
@@ -664,7 +670,7 @@ module Make_Dataflow
       let merged_states = VertexTable.create control_point_count
       and get_smashed_store v =
         let store = get_vertex_store v in
-        Partition.smashed store
+        Partitioning.smashed store
       in
       fun ~all stmt (v : vertex) ->
         if all || is_instr stmt
@@ -685,8 +691,8 @@ module Make_Dataflow
     let unmerged_pre_cvalues = lazy
       (StmtTable.map (fun _stmt (v,_) ->
            let store = get_vertex_store v in
-           let states = Partition.expanded store in
-           List.map (fun x -> Domain.get_cvalue_or_top x) states)
+           let states = Partitioning.expanded store in
+           List.map (fun (_k,x) -> Domain.get_cvalue_or_top x) states)
           automaton.stmt_table)
     in
     let merged_pre_cvalues = lazy (lift_to_cvalues merged_pre_states)
@@ -772,12 +778,10 @@ module Computer
           Kernel_function.pretty kf;
       Dataflow.merge_results ();
       let f = Kernel_function.get_definition kf in
-      (match results with
-       | `Value (_::_) when Cil.hasAttribute "noreturn" f.svar.vattr ->
-         Value_util.warning_once_current
-           "function %a may terminate but has the noreturn attribute"
-           Kernel_function.pretty kf;
-       | _ -> ());
+      if Cil.hasAttribute "noreturn" f.svar.vattr && results <> [] then
+        Value_util.warning_once_current
+          "function %a may terminate but has the noreturn attribute"
+          Kernel_function.pretty kf;
       results, !Dataflow.cacheable
     in
     let cleanup () =

src/plugins/value/engine/iterator.mli

@@ -21,7 +21,6 @@
 (**************************************************************************)
 
 open Cil_types
-open Eval
 
 (** Mark the analysis as aborted. It will be stopped at the next safe point *)
 val signal_abort: unit -> unit
@@ -46,7 +45,7 @@ module Computer
 
     val compute:
       kernel_function -> kinstr -> Abstract.Dom.t ->
-      Abstract.Dom.t list or_bottom * Eval.cacheable
+      (Partition.key * Abstract.Dom.t) list * Eval.cacheable
 
   end
 

src/plugins/value/engine/mem_exec.ml

@@ -53,7 +53,7 @@ module Make
 
   incr counter;
 
-  module CallOutput = Datatype.List (Domain)
+  module CallOutput = Datatype.List (Datatype.Pair (Partition.Key) (Domain))
 
   module StoredResult =
     Datatype.Triple
@@ -145,7 +145,7 @@ module Make
       else expand_inputs_with_relations (count - 1) kf expanded_bases state
 
   let store_computed_call kf input_state args
-      (call_result: Domain.t list Bottom.or_bottom) =
+      (call_result: (Partition.key * Domain.t) list) =
     match Transfer_stmt.current_kf_inout () with
     | None -> ()
     | Some inout ->
@@ -196,10 +196,8 @@ module Make
         let all_output_bases =
           Extlib.opt_fold Base.Hptset.add return_base all_output_bases
         in
-        let clear state = Domain.filter kf `Post all_output_bases state in
-        let call_result = match call_result with
-          | `Bottom -> []
-          | `Value list -> list
+        let clear (key,state) =
+          key, Domain.filter kf `Post all_output_bases state
         in
         let outputs = List.map clear call_result in
         let call_number = current_counter () in
@@ -248,7 +246,8 @@ module Make
           let bases, outputs, i = Domain.Hashtbl.find hstates st_filtered in
           (* We have found a previous execution, in which the outputs are
              [outputs]. Copy them in [state] and return this result. *)
-          let process output =
+          let process (key,output) =
+            key,
             Domain.reuse kf bases ~current_input:state ~previous_output:output
           in
           let outputs = List.map process outputs in
@@ -268,7 +267,7 @@ module Make
     | Not_found -> None
     | Result_found (outputs, i) ->
       let call_result = outputs in
-      Some (Bottom.bot_of_list call_result, i)
+      Some (call_result, i)
 
 end
 

src/plugins/value/engine/mem_exec.mli

@@ -41,7 +41,7 @@ module Make
         to be reused in subsequent calls *)
     val store_computed_call:
       kernel_function -> Domain.t -> Value.t or_bottom list ->
-      Domain.t list or_bottom ->
+      (Partition.key * Domain.t) list ->
       unit
 
     (** [reuse_previous_call kf init_state args] searches amongst the previous
@@ -52,7 +52,7 @@ module Make
         by the plugins that have registered Value callbacks.) *)
     val reuse_previous_call:
       kernel_function -> Domain.t -> Value.t or_bottom list ->
-      (Domain.t list or_bottom * int) option
+      ((Partition.key * Domain.t) list * int) option
   end
 
 

src/plugins/value/engine/transfer_specification.ml

@@ -564,10 +564,10 @@ module Make
      evaluates the assigns, and finally reduces by the post-conditions.
      [warn] is false for the specification of cvalue builtins — in this case,
      some warnings are disabled, such as warnings about new garbled mixes. *)
-  let compute_using_specification ~warn kinstr call spec state =
+  let compute_using_specification ~warn kinstr call spec (key,state) =
     let vi = Kernel_function.get_vi call.kf in
     if Cil.hasAttribute "noreturn" vi.vattr
-    then `Bottom
+    then []
     else
       (* Initializes the variable returned by the function. *)
       let state = match call.return with
@@ -582,8 +582,6 @@ module Make
       let states =
         compute_specification ~warn kinstr call.kf call.return spec state
       in
-      if States.is_empty states
-      then `Bottom
-      else `Value (States.to_list states)
+      List.map (fun x -> key,x) (States.to_list states)
 
 end

src/plugins/value/engine/transfer_specification.mli

@@ -35,6 +35,6 @@ module Make
     val compute_using_specification:
       warn:bool ->
       kinstr -> (Abstract.Loc.location, Abstract.Val.t) call -> spec ->
-      Abstract.Dom.t -> Abstract.Dom.t list or_bottom
+      (Partition.key * Abstract.Dom.t) -> (Partition.key * Abstract.Dom.t) list
 
   end

src/plugins/value/engine/transfer_stmt.ml

@@ -25,26 +25,28 @@ open Cil_datatype
 open Eval
 
 module type S = sig
+  type pkey = Partition.key
   type state
   type value
   type loc
   val assign: state -> kinstr -> lval -> exp -> state or_bottom
   val assume: state -> stmt -> exp -> bool -> state or_bottom
   val call:
-    stmt -> lval option -> exp -> exp list -> state ->
-    state list or_bottom * Eval.cacheable
+    stmt -> lval option -> exp -> exp list -> pkey -> state ->
+    (pkey*state) list * Eval.cacheable
   val check_unspecified_sequence:
     stmt ->
     state -> (stmt * lval list * lval list * lval list * stmt ref list) list ->
     unit or_bottom
   val enter_scope: kernel_function -> varinfo list -> state -> state
   type call_result = {
-    states: state list or_bottom;
+    states: (pkey * state) list;
     cacheable: Eval.cacheable;
     builtin: bool;
   }
   val compute_call_ref:
-    (stmt -> (loc, value) call -> recursion option ->state -> call_result) ref
+    (stmt -> (loc, value) call -> recursion option -> pkey -> state ->
+     call_result) ref
 end
 
 (* Reference filled in by the callwise-inout callback *)
@@ -119,6 +121,7 @@ module Make (Abstract: Abstractions.Eva) = struct
   module Domain = Abstract.Dom
   module Eval = Abstract.Eval
 
+  type pkey = Partition.key
   type state = Domain.t
   type value = Value.t
   type loc = Location.location
@@ -296,19 +299,20 @@ module Make (Abstract: Abstractions.Eva) = struct
   (* ------------------------------------------------------------------------ *)
 
   type call_result = {
-    states: state list or_bottom;
+    states: (pkey * state) list;
     cacheable: cacheable;
     builtin: bool;
   }
 
   (* Forward reference to [Eval_funs.compute_call] *)
   let compute_call_ref :
-    (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
+    (stmt -> (loc, value) call -> recursion option -> pkey -> state ->
+     call_result) ref
     = ref (fun _ -> assert false)
 
   (* Returns the result of a call, and a boolean that indicates whether a
      builtin has been used to interpret the call. *)
-  let process_call stmt call recursion valuation state =
+  let process_call stmt call recursion valuation pkey state =
     Value_util.push_call_stack call.kf (Kstmt stmt);
     let cleanup () =
       Value_util.pop_call_stack ();
@@ -322,9 +326,9 @@ module Make (Abstract: Abstractions.Eva) = struct
         match Domain.start_call stmt call recursion domain_valuation state with
         | `Value state ->
           Domain.Store.register_initial_state (Value_util.call_stack ()) state;
-          !compute_call_ref stmt call recursion state
+          !compute_call_ref stmt call recursion pkey state
         | `Bottom ->
-          { states = `Bottom; cacheable = Cacheable; builtin=false }
+          { states = []; cacheable = Cacheable; builtin=false }
       in
       cleanup ();
       res
@@ -455,13 +459,11 @@ module Make (Abstract: Abstractions.Eva) = struct
     Kernel_function.get_formals kf @ locals
 
   (* Do the call to one function. *)
-  let do_one_call valuation stmt lv call recursion state =
+  let do_one_call valuation stmt lv call recursion key state =
     let kf_callee = call.kf in
     let pre = state in
     (* Process the call according to the domain decision. *)
-    let call_result = process_call stmt call recursion valuation state in
-    call_result.cacheable,
-    call_result.states >>- fun result ->
+    let call_result = process_call stmt call recursion valuation key state in
     let leaving_vars = leaving_vars kf_callee in
     (* Do not try to reduce concrete arguments if a builtin was used. *)
     let gather_reduced_arguments =
@@ -488,11 +490,11 @@ module Make (Abstract: Abstractions.Eva) = struct
     in
     let states =
       List.fold_left
-        (fun acc return -> Bottom.add_to_list (process return) acc)
-        [] result
+        (fun acc (k,x) -> Bottom.add_to_list (process x >>-: fun y -> k,y) acc)
+        [] call_result.states
     in
     InOutCallback.clear ();
-    Bottom.bot_of_list states
+    call_result.cacheable, states
 
 
   (* ------------------- Evaluation of the arguments ------------------------ *)
@@ -737,7 +739,7 @@ module Make (Abstract: Abstractions.Eva) = struct
 
   (* --------------------- Process the call statement ---------------------- *)
 
-  let call stmt lval_option funcexp args state =
+  let call stmt lval_option funcexp args pkey state =
     let ki_call = Kstmt stmt in
     let subdivnb = subdivide_stmt stmt in
     (* Resolve [funcexp] into the called kernel functions. *)
@@ -747,39 +749,39 @@ module Make (Abstract: Abstractions.Eva) = struct
     Alarmset.emit ki_call alarms;
     let cacheable = ref Cacheable in
     let eval =
-      functions >>- fun functions ->
+      functions >>-: fun functions ->
       let current_kf = Value_util.current_kf () in
       let process_one_function kf valuation =
         (* The special Frama_C_ functions to print states are handled here. *)
         if apply_special_directives ~subdivnb kf args state
         then
           let () = apply_cvalue_callback kf ki_call state in
-          `Value ([state])
+          [(pkey,state)]
         else
           (* Create the call. *)
           let eval, alarms = make_call ~subdivnb kf args valuation state in
           Alarmset.emit ki_call alarms;
-          eval >>- fun (call, recursion, valuation) ->
-          (* Register the call. *)
-          Value_results.add_kf_caller call.kf ~caller:(current_kf, stmt);
-          (* Do the call. *)
-          let c, states =
-            do_one_call valuation stmt lval_option call recursion state
+          let states = eval >>-: fun (call, recursion, valuation) ->
+            (* Register the call. *)
+            Value_results.add_kf_caller call.kf ~caller:(current_kf, stmt);
+            (* Do the call. *)
+            let c, states =
+              do_one_call valuation stmt lval_option call recursion pkey state
+            in
+            (* If needed, propagate that callers cannot be cached. *)
+            if c = NoCacheCallers then
+              cacheable := NoCacheCallers;
+            states
           in
-          (* If needed, propagate that callers cannot be cached. *)
-          if c = NoCacheCallers then
-            cacheable := NoCacheCallers;
-          states
+          Bottom.list_of_bot states
       in
       (* Process each possible function apart, and append the result list. *)
       let process acc (kf, valuation) =
-        let res = process_one_function kf valuation in
-        (Bottom.list_of_bot res) @ acc
+        process_one_function kf valuation @ acc
       in
-      let states_list = List.fold_left process [] functions in
-      Bottom.bot_of_list states_list
+      List.fold_left process [] functions
     in
-    eval, !cacheable
+    Bottom.list_of_bot eval, !cacheable
 
   (* ------------------------------------------------------------------------ *)
   (*                            Unspecified Sequence                          *)

src/plugins/value/engine/transfer_stmt.mli

@@ -27,6 +27,7 @@ val current_kf_inout: unit -> Inout_type.t option
 
 module type S = sig
 
+  type pkey = Partition.key
   type state
   type value
   type loc
@@ -36,8 +37,8 @@ module type S = sig
   val assume: state -> stmt -> exp -> bool -> state or_bottom
 
   val call:
-    stmt -> lval option -> exp -> exp list -> state ->
-    state list or_bottom * Eval.cacheable
+    stmt -> lval option -> exp -> exp list -> pkey -> state ->
+    (pkey*state) list * Eval.cacheable
 
   val check_unspecified_sequence:
     Cil_types.stmt ->
@@ -49,13 +50,13 @@ module type S = sig
   val enter_scope: kernel_function -> varinfo list -> state -> state
 
   type call_result = {
-    states: state list or_bottom;
+    states: (pkey * state) list;
     cacheable: Eval.cacheable;
     builtin: bool;
   }
 
   val compute_call_ref:
-    (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
+    (stmt -> (loc, value) call -> recursion option -> pkey -> state -> call_result) ref
 end
 
 module Make (Abstract: Abstractions.Eva)

src/plugins/value/partitioning/partition.ml

@@ -34,6 +34,38 @@ let new_monitor ~split_limit = {
   split_values = Datatype.Integer.Set.empty;
 }
 
+module SplitMonitor = Datatype.Make_with_collections (
+  struct
+    open Datatype
+    include Serializable_undefined
+
+    module Values = Integer.Set
+
+    type t = split_monitor
+
+    let name = "Partition.SplitMonitor"
+
+    let reprs = [ new_monitor ~split_limit:0 ]
+
+    let structural_descr =
+      Structural_descr.t_record [| Int.packed_descr; Values.packed_descr |]
+
+    let compare m1 m2 =
+      let c = Int.compare m1.split_limit m2.split_limit in
+      if c <> 0 then c else Values.compare m1.split_values m2.split_values
+
+    let equal = from_compare
+
+    let pretty fmt m =
+      Format.fprintf fmt "%d/%d" (Values.cardinal m.split_values) m.split_limit
+
+    let hash m =
+      FCHashtbl.hash (Int.hash m.split_limit, Values.hash m.split_values)
+
+    let copy m =
+      { m with split_values = m.split_values }
+  end)
+
 (* --- Stamp rationing --- *)
 
 (* Stamps used to label states according to slevel.
@@ -57,24 +89,45 @@ type split_term = Eva_annotations.split_term =
   | Expression of Cil_types.exp
   | Predicate of Cil_types.predicate
 
-module SplitTerm = struct
-  type t = split_term
-  let compare x y =
-    match x, y with
-    | Expression e1, Expression e2 -> Cil_datatype.ExpStructEq.compare e1 e2
-    | Predicate p1, Predicate p2 -> Logic_utils.compare_predicate p1 p2
-    | Expression _, Predicate _ -> 1
-    | Predicate _, Expression _ -> -1
-
-  let pretty fmt = function
-    | Expression e -> Printer.pp_exp fmt e
-    | Predicate p -> Printer.pp_predicate fmt p
-end
+module SplitTerm = Datatype.Make_with_collections (struct
+    open Datatype
+    include Serializable_undefined
 
-module SplitMap = Map.Make (SplitTerm)
-module IntPair = Datatype.Pair (Datatype.Int) (Datatype.Int)
-module LoopList = Datatype.List (IntPair)
-module BranchList = Datatype.List (Datatype.Int)
+    module Expressions = Cil_datatype.ExpStructEq
+    module Predicates = Cil_datatype.PredicateStructEq
+
+    type t = split_term
+
+    let name = "Partition.SplitTerm"
+
+    let reprs =
+      Stdlib.List.map (fun e -> Expression e) Expressions.reprs @
+      Stdlib.List.map (fun p -> Predicate p) Predicates.reprs
+
+    let structural_descr =
+      Structural_descr.t_sum [|
+        [| Expressions.packed_descr |] ;
+        [| Predicates.packed_descr |] |]
+
+    let compare x y =
+      match x, y with
+      | Expression e1, Expression e2 -> Expressions.compare e1 e2
+      | Predicate p1, Predicate p2 -> Logic_utils.compare_predicate p1 p2
+      | Expression _, Predicate _ -> 1
+      | Predicate _, Expression _ -> -1
+
+    let equal = from_compare
+
+    let pretty fmt = function
+      | Expression e -> Printer.pp_exp fmt e
+      | Predicate p -> Printer.pp_predicate fmt p
+
+    let hash = function
+      | Expression e -> FCHashtbl.hash (1,Expressions.hash e)
+      | Predicate p -> FCHashtbl.hash (2,Predicates.hash p)
+  end)
+
+module SplitMap = SplitTerm.Map
 
 type branch = int
 
@@ -110,7 +163,14 @@ type key = {
 
 module Key =
 struct
-  type t = key
+  open Datatype
+
+  module IntPair = Pair (Int) (Int)
+  module Stamp = Option (IntPair)
+  module BranchList = List (Int)
+  module LoopList = List (IntPair)
+  module Splits = SplitMap.Make (Integer)
+  module DSplits = SplitMap.Make (SplitMonitor)
 
   (* Initial key, before any partitioning *)
   let zero = {
@@ -121,43 +181,88 @@ struct
     dynamic_splits = SplitMap.empty;
   }
 
-  let compare k1 k2 =
-    let (<?>) c (cmp,x,y) =
-      if c = 0 then cmp x y else c
-    in
-    Option.compare IntPair.compare k1.ration_stamp k2.ration_stamp
-    <?> (LoopList.compare, k1.loops, k2.loops)
-    <?> (SplitMap.compare Integer.compare, k1.splits, k2.splits)
-    <?> (SplitMap.compare (fun _ _ -> 0), k1.dynamic_splits, k2.dynamic_splits)
-    <?> (BranchList.compare, k1.branches, k2.branches)
-
-  let pretty fmt key =
-    begin match key.ration_stamp with
-      | Some (n,_) -> Format.fprintf fmt "#%d" n
-      | None -> ()
-    end;
-    Pretty_utils.pp_list ~pre:"[@[" ~sep:" ;@ " ~suf:"@]]"
-      Format.pp_print_int
-      fmt
-      key.branches;
-    Pretty_utils.pp_list ~pre:"(@[" ~sep:" ;@ " ~suf:"@])"
-      (fun fmt (i,_j) -> Format.pp_print_int fmt i)
-      fmt
-      key.loops;
-    Pretty_utils.pp_list ~pre:"{@[" ~sep:" ;@ " ~suf:"@]}"
-      (fun fmt (t, i) -> Format.fprintf fmt "%a:%a"
-          SplitTerm.pretty t
-          (Integer.pretty ~hexa:false) i)
-      fmt
-      (SplitMap.bindings key.splits)
+  include Make_with_collections (struct
+      include Serializable_undefined
+
+      type t = key
+
+      let name = "Partition.Key"
+
+      let reprs = [ zero ]
+
+      let structural_descr =
+        Structural_descr.t_record [|
+          Stamp.packed_descr;
+          BranchList.packed_descr;
+          LoopList.packed_descr;
+          Splits.packed_descr;
+          DSplits.packed_descr;
+        |]
+
+      let compare k1 k2 =
+        let (<?>) c (cmp,x,y) =
+          if c = 0 then cmp x y else c
+        in
+        Stamp.compare k1.ration_stamp k2.ration_stamp
+        <?> (LoopList.compare, k1.loops, k2.loops)
+        <?> (Splits.compare, k1.splits, k2.splits)
+        (* Ignore monitors in comparison *)
+        <?> (SplitMap.compare (fun _ _ -> 0), k1.dynamic_splits, k2.dynamic_splits)
+        <?> (BranchList.compare, k1.branches, k2.branches)
+
+      let equal = from_compare
+
+      let hash k =
+        Stdlib.Hashtbl.hash (
+          Stamp.hash k.ration_stamp,
+          BranchList.hash k.branches,
+          LoopList.hash k.loops,
+          Splits.hash k.splits,
+          DSplits.hash k.dynamic_splits) (* Monitors probably shouldn't be hashed *)
+
+      let pretty fmt key =
+        begin match key.ration_stamp with
+          | Some (n,_) -> Format.fprintf fmt "#%d" n
+          | None -> ()
+        end;
+        Pretty_utils.pp_list ~pre:"[@[" ~sep:" ;@ " ~suf:"@]]"
+          Format.pp_print_int
+          fmt
+          key.branches;
+        Pretty_utils.pp_list ~pre:"(@[" ~sep:" ;@ " ~suf:"@])"
+          (fun fmt (i,_j) -> Format.pp_print_int fmt i)
+          fmt
+          key.loops;
+        Pretty_utils.pp_list ~pre:"{@[" ~sep:" ;@ " ~suf:"@]}"
+          (fun fmt (t, i) -> Format.fprintf fmt "%a:%a"
+              SplitTerm.pretty t
+              Integer.pretty i)
+          fmt
+          (SplitMap.bindings key.splits)
+    end)
 
   let exceed_rationing key = key.ration_stamp = None
+
+  let recombine k1 k2 =
+    let merge_split _ v1 v2 =
+      match v1, v2 with
+      | None, None -> None
+      | Some v, None | None, Some v -> Some v
+      | Some _v1, Some v2 -> Some v2 (* Keep the newest split value *)
+    in {
+      ration_stamp = k2.ration_stamp;
+      branches = k2.branches @ k1.branches;
+      loops = k1.loops;
+      splits = SplitMap.merge merge_split k1.splits k2.splits;
+      dynamic_splits =
+        SplitMap.merge merge_split k1.dynamic_splits k2.dynamic_splits;
+    }
 end
 
 
 (* --- Partitions --- *)
 
-module KMap = Map.Make (Key)
+module KMap = Key.Map
 
 type 'a partition = 'a KMap.t
 
@@ -171,8 +276,8 @@ let map = KMap.map
 let filter = KMap.filter
 let merge = KMap.merge
 
-let to_list (p : 'a partition) : 'a list =
-  KMap.fold (fun _k x l -> x :: l) p []
+let to_list (p : 'a partition) : (key*'a) list =
+  KMap.fold (fun k x l -> (k,x) :: l) p []
 
 
 (* --- Partitioning actions --- *)
@@ -511,20 +616,20 @@ struct
       in
       map_keys transfer p
 
-  let transfer_states (f : state -> state list) (p : t) : t =
+  let transfer (f : (key * state) -> (key*state) list) (p : t) : t =
     let n = ref 0 in
     let transfer acc (k,x) =
-      let add =
+      let add l (k,y) =
         match k.ration_stamp with
         (* No ration stamp, just add the state to the list *)
-        | None -> fun l y -> (k,y) :: l
+        | None -> (k,y) :: l
         (* There is a ration stamp, set the second part of the stamp to a unique transfer number *)
-        | Some (s,_) -> fun l y ->
+        | Some (s,_) ->
           let k' = { k with ration_stamp = Some (s, !n) } in
           incr n;
           (k',y) :: l
       in
-      List.fold_left add acc (f x)
+      List.fold_left add acc (f (k,x))
     in
     List.fold_left transfer [] p
 

src/plugins/value/partitioning/partition.mli

@@ -42,10 +42,10 @@
 type key
 
 module Key : sig
-  val zero : key (** Initial key: no partitioning. *)
-  val compare : key -> key -> int
-  val pretty : Format.formatter -> key -> unit
-  val exceed_rationing: key -> bool
+  include Datatype.S_with_collections with type t = key
+  val zero : t (** Initial key: no partitioning. *)
+  val exceed_rationing: t -> bool
+  val recombine : t -> t -> t (** Recombinaison of keys after a call *)
 end
 
 (** Collection of states, each identified by a unique key. *)
@@ -54,7 +54,7 @@ type 'state partition
 val empty : 'a partition
 val is_empty : 'a partition -> bool
 val size : 'a partition -> int
-val to_list : 'a partition -> 'a list
+val to_list : 'a partition -> (key*'a) list
 val find : key -> 'a partition -> 'a
 val replace : key -> 'a -> 'a partition -> 'a partition
 val merge : (key -> 'a option -> 'b option -> 'c option) -> 'a partition ->
@@ -182,8 +182,8 @@ sig
 
   val union : t -> t -> t
 
+  val transfer : ((key * state) -> (key * state) list) -> t -> t
   val transfer_keys : t -> action -> t
-  val transfer_states : (state -> state list) -> t -> t
 
   val iter : (state -> unit) -> t -> unit
   val filter_map: (key -> state -> state option) -> t -> t

src/plugins/value/partitioning/trace_partitioning.ml

@@ -112,13 +112,13 @@ struct
 
   (* Accessors *)
 
-  let expanded (s : store) : state list =
+  let expanded (s : store) : (key*state) list =
     Partition.to_list s.store_partition
 
   let smashed (s : store) : state or_bottom =
     match expanded s with
     | [] -> `Bottom
-    | v1 :: l -> `Value (List.fold_left Domain.join v1 l)
+    | (_k,v1) :: l -> `Value (List.fold_left Domain.join v1 (List.map snd l))
 
   let contents (flow : flow) : state list =
     Flow.to_list flow
@@ -210,7 +210,7 @@ struct
     in
     into.tank_states <- Partition.merge join into.tank_states new_states
 
-  let transfer = Flow.transfer_states
+  let transfer = Flow.transfer
 
   let output_slevel : int -> unit =
     let slevel_display_step = Value_parameters.ShowSlevel.get () in
@@ -239,7 +239,8 @@ struct
     in
     (* Get every source flow *)
     let sources_states =
-      match sources with
+      (* Is there more than one non-empty incomming flow ? *)
+      match List.filter (fun (_b,f) -> not (Flow.is_empty f)) sources with
       | [(_,flow)] -> [flow]
       | sources ->
         (* Several branches -> partition according to the incoming branch *)

src/plugins/value/partitioning/trace_partitioning.mli

@@ -50,7 +50,7 @@ sig
 
   (* --- Accessors --- *)
 
-  val expanded : store -> state list
+  val expanded : store -> (Partition.key * state) list
   val smashed : store -> state or_bottom
   val contents : flow -> state list
   val is_empty_store : store -> bool
@@ -91,7 +91,8 @@ sig
   val fill : into:tank -> flow -> unit
 
   (** Apply a transfer function to all the states of a propagation. *)
-  val transfer : (state -> state list) -> flow -> flow
+  val transfer : ((Partition.key * state) -> (Partition.key * state) list) ->
+    flow -> flow
 
   (** Join all incoming propagations into the given store. This function returns
       a set of states which still need to be propagated past the store.

tests/value/oracle/partitioning-annots.2.res.oracle

@@ -11,9 +11,6 @@
 [eva] tests/value/partitioning-annots.c:127: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- test_loop_split.
-  Called from tests/value/partitioning-annots.c:127.
-[eva] Done for function Frama_C_interval
 [eva] tests/value/partitioning-annots.c:125: starting to merge loop iterations
 [eva] computing for function Frama_C_interval <- test_loop_split.
   Called from tests/value/partitioning-annots.c:127.

tests/value/oracle/partitioning-interproc.0.res.oracle

@@ -12,9 +12,9 @@
 [eva] Done for function Frama_C_nondet
 [eva] Recording results for cassign
 [eva] Done for function cassign
-[eva:alarm] tests/value/partitioning-interproc.c:25: Warning: 
-  accessing uninitialized left-value. assert \initialized(&x);
 [eva] tests/value/partitioning-interproc.c:26: Frama_C_show_each: {1}
+[eva] tests/value/partitioning-interproc.c:30: 
+  Reusing old results for call to cassign
 [eva] computing for function cassign <- cassign_test.
   Called from tests/value/partitioning-interproc.c:30.
 [eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
@@ -22,15 +22,6 @@
 [eva] Done for function Frama_C_nondet
 [eva] Recording results for cassign
 [eva] Done for function cassign
-[eva] computing for function cassign <- cassign_test.
-  Called from tests/value/partitioning-interproc.c:30.
-[eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
-  Called from tests/value/partitioning-interproc.c:11.
-[eva] Done for function Frama_C_nondet
-[eva] Recording results for cassign
-[eva] Done for function cassign
-[eva:alarm] tests/value/partitioning-interproc.c:31: Warning: 
-  accessing uninitialized left-value. assert \initialized(&x);
 [eva] tests/value/partitioning-interproc.c:32: Frama_C_show_each: {1}
 [eva] tests/value/partitioning-interproc.c:32: Frama_C_show_each: {1}
 [eva] Recording results for cassign_test

tests/value/oracle/partitioning-interproc.1.res.oracle

@@ -14,7 +14,7 @@
 [eva:final-states] Values at end of function fabs:
   __retres ∈ [-0. .. 1.79769313486e+308]
 [eva:final-states] Values at end of function fabs_test:
-  x ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+  x ∈ [-1. .. 1.]
 [from] Computing for function fabs
 [from] Done for function fabs
 [from] Computing for function fabs_test

tests/value/oracle/split_return.0.res.oracle

@@ -32,8 +32,8 @@
   Called from tests/value/split_return.i:51.
 [eva] Recording results for f2
 [eva] Done for function f2
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
 [eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
 [eva] tests/value/split_return.i:54: assertion got status valid.
 [eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
 [eva] tests/value/split_return.i:57: assertion got status valid.
@@ -72,8 +72,8 @@
   Called from tests/value/split_return.i:120.
 [eva] Recording results for f5
 [eva] Done for function f5
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
 [eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
 [eva] tests/value/split_return.i:123: assertion got status valid.
 [eva] tests/value/split_return.i:125: assertion got status valid.
 [eva] Recording results for main5

tests/value/oracle/split_return.1.res.oracle

@@ -34,8 +34,8 @@
   Called from tests/value/split_return.i:51.
 [eva] Recording results for f2
 [eva] Done for function f2
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
 [eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
 [eva] tests/value/split_return.i:54: assertion got status valid.
 [eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
 [eva] tests/value/split_return.i:57: assertion got status valid.
@@ -47,8 +47,8 @@
   Called from tests/value/split_return.i:76.
 [eva] Recording results for f3
 [eva] Done for function f3
-[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
 [eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {7}, {5}
+[eva] tests/value/split_return.i:77: Frama_C_show_each_f3: {-2}, {0}
 [eva] tests/value/split_return.i:79: assertion got status valid.
 [eva] tests/value/split_return.i:81: assertion got status valid.
 [eva] Recording results for main3
@@ -59,8 +59,8 @@
   Called from tests/value/split_return.i:97.
 [eva] Recording results for f4
 [eva] Done for function f4
-[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {7}, {5}
+[eva] tests/value/split_return.i:98: Frama_C_show_each_f4: {4}, {0}
 [eva] tests/value/split_return.i:100: assertion got status valid.
 [eva] tests/value/split_return.i:102: assertion got status valid.
 [eva] Recording results for main4
@@ -71,8 +71,8 @@
   Called from tests/value/split_return.i:120.
 [eva] Recording results for f5
 [eva] Done for function f5
-[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
 [eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {7}, {5}
+[eva] tests/value/split_return.i:121: Frama_C_show_each_f5: {-2}, {0}
 [eva] tests/value/split_return.i:123: assertion got status valid.
 [eva] tests/value/split_return.i:125: assertion got status valid.
 [eva] Recording results for main5
@@ -104,8 +104,8 @@
   Called from tests/value/split_return.i:174.
 [eva] Recording results for f8
 [eva] Done for function f8
-[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
 [eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {4}, {{ &x }}
+[eva] tests/value/split_return.i:175: Frama_C_show_each_then8: {-1}, {0}
 [eva] Recording results for main8
 [eva] Done for function main8
 [eva] computing for function main9 <- main.

tests/value/oracle/split_return.4.res.oracle

@@ -472,8 +472,8 @@
   Called from tests/value/split_return.i:51.
 [eva] Recording results for f2
 [eva] Done for function f2
-[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
 [eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {5; 7}, {5}
+[eva] tests/value/split_return.i:52: Frama_C_show_each_f2: {0}, {0}
 [eva] tests/value/split_return.i:56: Frama_C_show_each_f2_2: {5; 7}, {5}
 [eva] Recording results for main2
 [eva] Done for function main2

tests/value/partitioning-interproc.c

 /* run.config*
    GCC:
    STDOPT: #"-main cassign_test -eva-partition-history 1"
-   STDOPT: #"-main fabs_test -eva-partition-history 1 -eva-equality-domain"
+   STDOPT: #"-main fabs_test -eva-partition-history 1 -eva-domains equality"
    */
 
 #include "__fc_builtin.h"