From 6ace3838baf1fd3e9f95885efa38d3d8ac716fbc Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 19 Jan 2017 08:09:33 -0800 Subject: [PATCH] [absint] support HTML debug output Reviewed By: jeremydubreil, cristianoc, jvillard Differential Revision: D4432646 fbshipit-source-id: 2348c17 --- infer/src/checkers/AbstractInterpreter.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/infer/src/checkers/AbstractInterpreter.ml b/infer/src/checkers/AbstractInterpreter.ml index 0a1dc21a4..416aaf557 100644 --- a/infer/src/checkers/AbstractInterpreter.ml +++ b/infer/src/checkers/AbstractInterpreter.ml @@ -81,7 +81,19 @@ module MakeNoCFG let instr_ids = match CFG.instr_ids node with | [] -> [Sil.skip_instr, None] | l -> l in + let underlying_node = CFG.underlying_node node in + NodePrinter.start_session underlying_node; let astate_post, inv_map_post = IList.fold_left compute_post (pre, inv_map) instr_ids in + if Config.write_html + then + begin + let str = + let instrs = IList.map fst instr_ids in + Format.asprintf "PRE: %a@.INSTRS: %aPOST: %a@." + Domain.pp pre (Sil.pp_instr_list Pp.text) instrs Domain.pp astate_post in + L.d_strln str + end; + NodePrinter.finish_session underlying_node; let inv_map'' = InvariantMap.add node_id { pre; post=astate_post; visit_count; } inv_map_post in inv_map'', Scheduler.schedule_succs work_queue node in