File tree Expand file tree Collapse file tree 4 files changed +20
-0
lines changed
Expand file tree Collapse file tree 4 files changed +20
-0
lines changed Original file line number Diff line number Diff line change @@ -1638,6 +1638,10 @@ INTERNAL OPTIONS
16381638 Activates: Print the builtin functions and exit (Conversely:
16391639 --no-print-builtins)
16401640
1641+ --print-jbir
1642+ Activates: Print JBir translation of Java bytecode in logs
1643+ (Conversely: --no-print-jbir)
1644+
16411645 --print-types
16421646 Activates: Print types in symbolic heaps (Conversely:
16431647 --no-print-types)
Original file line number Diff line number Diff line change @@ -982,6 +982,7 @@ and ( bo_debug
982982 , linters_developer_mode
983983 , only_cheap_debug
984984 , print_buckets
985+ , print_jbir
985986 , print_logs
986987 , print_types
987988 , reports_include_ml_loc
@@ -1032,6 +1033,8 @@ and ( bo_debug
10321033 and print_buckets =
10331034 CLOpt. mk_bool ~long: " print-buckets"
10341035 " Show the internal bucket of Infer reports in their textual description"
1036+ and print_jbir =
1037+ CLOpt. mk_bool ~long: " print-jbir" " Print JBir translation of Java bytecode in logs"
10351038 and print_types = CLOpt. mk_bool ~long: " print-types" ~default: false " Print types in symbolic heaps"
10361039 and keep_going =
10371040 CLOpt. mk_bool ~deprecated_no: [" -no-failures-allowed" ] ~long: " keep-going"
@@ -1135,6 +1138,7 @@ and ( bo_debug
11351138 , linters_developer_mode
11361139 , only_cheap_debug
11371140 , print_buckets
1141+ , print_jbir
11381142 , print_logs
11391143 , print_types
11401144 , reports_include_ml_loc
@@ -3066,6 +3070,8 @@ and select = !select
30663070
30673071and show_buckets = ! print_buckets
30683072
3073+ and print_jbir = ! print_jbir
3074+
30693075and siof_check_iostreams = ! siof_check_iostreams
30703076
30713077and siof_safe_methods = ! siof_safe_methods
Original file line number Diff line number Diff line change @@ -417,6 +417,8 @@ val print_active_checkers : bool
417417
418418val print_builtins : bool
419419
420+ val print_jbir : bool
421+
420422val print_logs : bool
421423
422424val print_types : bool
Original file line number Diff line number Diff line change @@ -282,6 +282,11 @@ let get_jbir_representation cm bytecode =
282282 bytecode
283283
284284
285+ let pp_jbir fmt jbir =
286+ (Format. pp_print_list ~pp_sep: Format. pp_print_newline Format. pp_print_string)
287+ fmt (JBir. print jbir)
288+
289+
285290let trans_access = function
286291 | `Default ->
287292 PredSymb. Default
@@ -423,6 +428,9 @@ let create_cm_procdesc source_file program icfg cm proc_name =
423428 try
424429 let bytecode = get_bytecode cm in
425430 let jbir_code = get_jbir_representation cm bytecode in
431+ if Config. print_jbir then
432+ L. (debug Capture Verbose )
433+ " Printing JBir of: %a@\n @[%a@]@." Procname. pp proc_name pp_jbir jbir_code ;
426434 let loc_start = get_start_location source_file proc_name bytecode in
427435 let loc_exit = get_exit_location source_file bytecode in
428436 let formals = translate_formals program tenv cn jbir_code in
You can’t perform that action at this time.
0 commit comments