No push pop

GillianCore/command_line/verification_console.ml

@@ -86,7 +86,7 @@ module Make
 
   let verify files already_compiled outfile_opt no_unfold incremental =
     Gillian_result.try_ @@ fun () ->
-    Verification.start_time := Sys.time ();
+    Verification.start_time := Unix.gettimeofday ();
     Fmt.pr "Parsing and compiling...\n@?";
     let* e_prog, init_data, source_files_opt =
       parse_eprog files already_compiled

GillianCore/command_line/wpst_console.ml

@@ -18,7 +18,7 @@ module Make
   module Common_args = Common_args.Make (PC)
   open Common_args
 
-  let start_time = ref (Sys.time ())
+  let start_time = ref (Unix.gettimeofday ())
 
   let json_ui =
     let doc = "Output some of the UI in JSON." in
@@ -95,7 +95,7 @@ module Make
         else result_before_leak_check
       in
       Printf.printf "Total time (Compilation + Symbolic testing): %fs\n"
-        (Sys.time () -. !start_time);
+        (Unix.gettimeofday () -. !start_time);
       print_json_results all_results;
       let first_error =
         List.find_map
@@ -194,7 +194,7 @@ module Make
       (e_prog, init_data, None)
 
   let process_files files already_compiled outfile_opt incremental =
-    let t = Sys.time () in
+    let t = Unix.gettimeofday () in
     let* e_prog, init_data, source_files_opt =
       parse_eprog files already_compiled
     in
@@ -215,7 +215,7 @@ module Make
     let () =
       L.normal (fun m -> m "\n*** Stage 2: DONE transforming the program.\n")
     in
-    Printf.printf "Compilation time: %fs\n" (Sys.time () -. t);
+    Printf.printf "Compilation time: %fs\n" (Unix.gettimeofday () -. t);
     let () = L.normal (fun m -> m "*** Stage 3: Symbolic Execution.\n") in
     let prog' = MP.init_prog prog in
     run prog' init_data incremental source_files_opt

GillianCore/engine/Abstraction/Verifier.ml

@@ -120,7 +120,7 @@ struct
       |> List.map (fun (name, test) -> `List [ `String name; to_yojson test ]))
 
   let global_results = VerificationResults.make ()
-  let start_time = ref 0.
+  let start_time = ref (Unix.gettimeofday ())
 
   let reset () =
     VerificationResults.reset global_results;
@@ -867,7 +867,7 @@ struct
       get_tests_to_verify ~init_data prog pnames_to_verify lnames_to_verify
     in
     (* STEP 6: Run the symbolic tests *)
-    let cur_time = Sys.time () in
+    let cur_time = Unix.gettimeofday () in
     Printf.printf "Running symbolic tests: %f\n" (cur_time -. !start_time);
     let result =
       let rec aux = function
@@ -879,7 +879,7 @@ struct
       in
       aux (tests' @ tests, Ok ())
     in
-    let end_time = Sys.time () in
+    let end_time = Unix.gettimeofday () in
     let cur_verified = SS.union pnames_to_verify lnames_to_verify in
     let success =
       Result.is_ok result && check_previously_verified prev_results cur_verified

GillianCore/engine/BiAbduction/Abductor.ml

@@ -303,13 +303,13 @@ struct
           in
           L.verbose (fun m -> m "Running bi-abduction on %s\n" test.name);
           Fmt.pr "Testing %s... @?" test.name;
-          let start_time = Sys.time () in
+          let start_time = Unix.gettimeofday () in
           let rets =
             run_test
               (process_sym_exec_result prog test.name test.params test.state)
               prog test
           in
-          let end_time = Sys.time () in
+          let end_time = Unix.gettimeofday () in
           let stats =
             get_stats test.name (fun () ->
                 match Hashtbl.find_opt prog.prog.procs test.name with
@@ -352,7 +352,7 @@ struct
           String.compare name1 name2)
     in
 
-    Fmt.pr "Ok 3 - %f@." (Sys.time ());
+    Fmt.pr "Ok 3 - %f@." (Unix.gettimeofday ());
     if !Config.specs_to_stdout then (
       let bug_specs_txt =
         Format.asprintf "@[<v 2>BUG SPECS:@\n%a@]@\n"

GillianCore/engine/FOLogic/FOSolver.ml

@@ -78,7 +78,7 @@ let check_satisfiability
     ?relevant_info
     (fs : Expr.t list)
     (gamma : Type_env.t) : bool =
-  (* let t = if time = "" then 0. else Sys.time () in *)
+  (* let t = if time = "" then 0. else Unix.gettimeofday () in *)
   L.verbose (fun m -> m "Entering FOSolver.check_satisfiability");
   let fs, gamma, _ = simplify_pfs_and_gamma ?relevant_info ~matching fs gamma in
   let axioms = get_axioms fs gamma in
@@ -93,7 +93,7 @@ let check_satisfiability
     in
     (* if time <> "" then
        Utils.Statistics.update_statistics ("FOS: CheckSat: " ^ time)
-         (Sys.time () -. t); *)
+         (Unix.gettimeofday () -. t); *)
     result
 
 let sat ~matching ~pfs ~gamma formula : bool =
@@ -135,7 +135,7 @@ let check_entailment
   (* SOUNDNESS !!DANGER!!: call to simplify_implication       *)
   (* Simplify maximally the implication to be checked         *)
   (* Remove from the typing environment the unused variables  *)
-  (* let t = Sys.time () in *)
+  (* let t = Unix.gettimeofday () in *)
   let left_fs = PFS.copy left_fs in
   let gamma = Type_env.copy gamma in
   let right_fs = PFS.of_list right_fs in
@@ -210,11 +210,11 @@ let check_entailment
                L.tmi (fun m -> m "Here's the model:\n%a" Smt.pp_sexp model))
       in
       (* Utils.Statistics.update_statistics "FOS: CheckEntailment"
-         (Sys.time () -. t); *)
+         (Unix.gettimeofday () -. t); *)
       ret
 
 let is_equal ?matching ~pfs ~gamma e1 e2 =
-  (* let t = Sys.time () in *)
+  (* let t = Unix.gettimeofday () in *)
   let feq =
     Reduction.reduce_lexpr ?matching ~gamma ~pfs (BinOp (e1, Equal, e2))
   in
@@ -229,11 +229,11 @@ let is_equal ?matching ~pfs ~gamma e1 e2 =
              ("Equality reduced to something unexpected: "
              ^ (Fmt.to_to_string Expr.pp) feq))
   in
-  (* Utils.Statistics.update_statistics "FOS: is_equal" (Sys.time () -. t); *)
+  (* Utils.Statistics.update_statistics "FOS: is_equal" (Unix.gettimeofday () -. t); *)
   result
 
 let is_different ~pfs ~gamma e1 e2 =
-  (* let t = Sys.time () in *)
+  (* let t = Unix.gettimeofday () in *)
   let feq =
     Reduction.reduce_lexpr ~gamma ~pfs (UnOp (Not, BinOp (e1, Equal, e2)))
   in
@@ -247,7 +247,7 @@ let is_different ~pfs ~gamma e1 e2 =
              ("Inequality reduced to something unexpected: "
              ^ (Fmt.to_to_string Expr.pp) feq))
   in
-  (* Utils.Statistics.update_statistics "FOS: is different" (Sys.time () -. t); *)
+  (* Utils.Statistics.update_statistics "FOS: is different" (Unix.gettimeofday () -. t); *)
   result
 
 let num_is_less_or_equal ~pfs ~gamma e1 e2 =

GillianCore/engine/FOLogic/Reduction.ml

@@ -2316,9 +2316,9 @@ and reduce_lexpr
     ?(pfs = PFS.init ())
     ?(gamma = Type_env.init ())
     (le : Expr.t) =
-  (* let t = Sys.time () in *)
+  (* let t = Unix.gettimeofday () in *)
   let result = reduce_lexpr_loop ~matching ~reduce_lvars pfs gamma le in
-  (* Utils.Statistics.update_statistics "Reduce Expression" (Sys.time () -. t); *)
+  (* Utils.Statistics.update_statistics "Reduce Expression" (Unix.gettimeofday () -. t); *)
   if not @@ Expr.equal le result then
     Logging.normal (fun f ->
         f "reduce_lexpr: @[%a -> %a@]" Expr.pp le Expr.pp result);

GillianCore/engine/FOLogic/Simplifications.ml

@@ -311,7 +311,7 @@ let simplify_pfs_and_gamma
     (lpfs : PFS.t)
     ?(rpfs : PFS.t option)
     (gamma : Type_env.t) : SESubst.t * SS.t =
-  (* let t = Sys.time () in *)
+  (* let t = Unix.gettimeofday () in *)
   let rpfs : PFS.t = Option.value ~default:(PFS.init ()) rpfs in
   let existentials : SS.t ref =
     ref (Option.value ~default:SS.empty existentials)
@@ -935,7 +935,7 @@ let simplify_pfs_and_gamma
       Hashtbl.replace simplification_cache key cached_simplification;
 
       (* Utils.Statistics.update_statistics "FOS: SimplifyPFSandGamma"
-         (Sys.time () -. t); *)
+         (Unix.gettimeofday () -. t); *)
 
       (* Step 5 - Sort ALoc transitivity *)
       let rec find_loc_all_the_way aloc res =
@@ -971,7 +971,7 @@ let simplify_implication
     (lpfs : PFS.t)
     (rpfs : PFS.t)
     (gamma : Type_env.t) =
-  (* let t = Sys.time () in *)
+  (* let t = Unix.gettimeofday () in *)
   List.iter
     (fun (pf : Expr.t) ->
       match pf with
@@ -1011,7 +1011,7 @@ let simplify_implication
           (Fmt.iter ~sep:Fmt.comma SS.iter Fmt.string)
           exists PFS.pp lpfs PFS.pp rpfs Type_env.pp gamma));
   (* Utils.Statistics.update_statistics "FOS: SimplifyImplication"
-     (Sys.time () -. t); *)
+     (Unix.gettimeofday () -. t); *)
   exists
 
 let admissible_assertion (a : Asrt.t) : bool =

GillianCore/engine/general_semantics/general/g_interpreter.ml

@@ -311,8 +311,8 @@ struct
             State.pp_by_need pvars lvars locs
       in
       ConfigReport.log state_printer
-        (ConfigReport.make ~proc_name ~proc_line:i ~time:(Sys.time ()) ~cmd
-           ~callstack:cs ~annot ~branching:b_counter ~state ?branch_case ())
+        (ConfigReport.make ~proc_name ~proc_line:i ~time:(Unix.gettimeofday ())
+           ~cmd ~callstack:cs ~annot ~branching:b_counter ~state ?branch_case ())
 
     let print_lconfiguration
         (lcmd : LCmd.t)
@@ -328,7 +328,8 @@ struct
              @\n\
              %a@\n\
              ------------------------------------------------------@]@\n"
-            (Sys.time ()) LCmd.pp lcmd Location.pp_log_opt loc State.pp state)
+            (Unix.gettimeofday ()) LCmd.pp lcmd Location.pp_log_opt loc State.pp
+            state)
 
     let pp_err = Exec_err.pp Val.pp State.pp_err
     let pp_single_result ft res = Exec_res.pp State.pp Val.pp pp_err ft res

GillianCore/logging/report_builder.ml

@@ -62,7 +62,7 @@ let make
     {
       id = Report_id.next ();
       title;
-      elapsed_time = Sys.time ();
+      elapsed_time = Unix.gettimeofday ();
       previous = get_previous ();
       parent = get_parent ();
       content;