File tree Expand file tree Collapse file tree 1 file changed +5
-1
lines changed Expand file tree Collapse file tree 1 file changed +5
-1
lines changed Original file line number Diff line number Diff line change @@ -93,7 +93,10 @@ let check_fndefn
9393 let rng = body . range in
9494 debug_main g ( fun _ -> Printf. sprintf " \n body after mk_abs:\n %s\n " ( P. st_term_to_string body ));
9595
96- let (| body , c , t_typing |) = Pulse.Checker.Abs. check_abs g body Pulse.Checker. check in
96+ let (| body , c , t_typing |) =
97+ stats_record " top_level check_abs" fun () ->
98+ Pulse.Checker.Abs. check_abs g body Pulse.Checker. check
99+ in
97100
98101 Pulse.Checker.Prover. debug_prover g
99102 ( fun _ -> Printf. sprintf " \n check call returned in main with:\n %s\n at type %s\n "
@@ -112,6 +115,7 @@ let check_fndefn
112115 let cur_module = T. cur_module () in
113116
114117 let maybe_add_impl t ( se : RT. sigelt_for ( fstar_env g ) t ) : Tac ( RT. sigelt_for ( fstar_env g ) t ) =
118+ stats_record " pulse_extraction" fun () ->
115119 let open Pulse.Extract.Main in begin
116120 if C_STGhost ? comp then
117121 se
You can’t perform that action at this time.
0 commit comments