File tree Expand file tree Collapse file tree 4 files changed +13
-22
lines changed Expand file tree Collapse file tree 4 files changed +13
-22
lines changed Original file line number Diff line number Diff line change 1010 goblint-cil
1111 goblint-cil.syntacticsearch
1212 goblint.lib
13+ goblint.timing
1314 goblint.sites.js
1415 integers_stubs_js
1516 ctypes_stubs_js
Original file line number Diff line number Diff line change @@ -22,7 +22,7 @@ type t = {
2222 goblint : GvGoblint .solver_state ;
2323 warnings : GvMessages .t ;
2424 meta : Yojson.Safe .t ;
25- stats : Timing .tree * Gc .stat ;
25+ stats : Goblint_timing .tree * Gc .stat ;
2626 file_loc : (string , string ) Hashtbl .t ;
2727 display : display option ;
2828 inspect : inspect option ;
@@ -31,13 +31,21 @@ type t = {
3131 search : Search .t ;
3232}
3333
34+ let timing_default : Goblint_timing.tree = {
35+ name = " " ;
36+ cputime = 0.0 ;
37+ walltime = 0.0 ;
38+ allocated = 0.0 ;
39+ count = 0 ;
40+ children = [] ;
41+ }
3442let default =
3543 {
3644 cil = Cil. dummyFile;
3745 goblint = GvGoblint. empty;
3846 warnings = [] ;
3947 meta = `Null ;
40- stats = (Timing. create_tree " default " , Gc. quick_stat () );
48+ stats = (timing_default , Gc. quick_stat () );
4149 file_loc = Hashtbl. create 113 ;
4250 display = None ;
4351 inspect = None ;
Load Diff This file was deleted.
Original file line number Diff line number Diff line change 11open Batteries ;
22
3+ module Timing = Goblint_timing
4+
35let rec make_task_list = tasks =>
46 if (List . is_empty(tasks)) {
57 React . null;
You can’t perform that action at this time.
0 commit comments