Skip to content

Cleanup of the Code #19

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Cleanup of the Code #19

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9015a9e
change output to be in markdown format
spiessimon Jun 10, 2025
c13b0ae
fix warnings
spiessimon Jun 10, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion analyzer/framework/core/alarm.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -789,7 +789,7 @@ let report_to_alarms report =
(fun check diag acc ->
match diag.diag_kind with
| Error | Warning -> AlarmSet.elements diag.diag_alarms @ acc
| Safe | Unreachable -> acc
| Safe | Unreachable | Info | Unimplemented -> acc
) checks acc
) report.report_diagnostics []

Expand Down
2 changes: 1 addition & 1 deletion analyzer/framework/engines/interactive/engine.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -189,7 +189,7 @@ struct
(fun diag acc ->
match diag.diag_kind with
| Error | Warning -> AlarmSet.union diag.diag_alarms acc
| Safe | Unreachable -> acc
| Safe | Unreachable | Info | Unimplemented -> acc
) report acc
) AlarmSet.empty cases
in
Expand Down
17 changes: 7 additions & 10 deletions analyzer/framework/output/text.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,7 @@ let pp_diagnostic out n diag callstacks kinds =
| c::_ -> Some c.call_fun_orig_name
| _ -> None in
let len = CallstackSet.cardinal callstacks in
print out "@.%a Check%s:%a@,@[<v 2>%a: %a: %a%a%a%a@]@.@."
print out "```@.%a Check%s:%a@,@[<v 2>%a: %a: %a%a%a%a@]@.```@."
(Debug.color_str (color_of_diag diag.diag_kind)) (icon_of_diag diag.diag_kind)
(if len <= 1 then Format.asprintf " #%d" (n+1) else Format.asprintf "s #%d-#%d" (n+1) (n+len))
(fun fmt -> function
Expand Down Expand Up @@ -310,20 +310,19 @@ let print_checks_summary checks_map total safe error warning info unimplemented
if n = 1 then fprintf fmt ", %a" (Debug.color (color_of_diag diag) (fun fmt n -> fprintf fmt "%s %d %s" (icon_of_diag diag) n singluar)) n
else fprintf fmt ", %a" (Debug.color (color_of_diag diag) (fun fmt n -> fprintf fmt "%s %d %s" (icon_of_diag diag) n plural)) n
in
print out "@[<v2>Checks summary: %a%a%a%a%a%a (selectivity: %.2f%%)@,%a@]@.@."
print out "@[<v2>## Statistics\n\n**Summary:** %a%a%a%a%a%a@,%a@]@.@."
(Debug.bold (fun fmt total -> fprintf fmt "%d total" total)) total
(pp Safe "safe" "safe") safe
(pp Safe "check passed" "checks passed") safe
(pp Error "error" "errors") error
(pp Warning "warning" "warnings") warning
(pp Info "info" "info") info
(pp Unimplemented "unimplemented" "unimplemented") unimplemented
(float_of_int (100 * safe) /. (float_of_int @@ safe + error + warning))
(pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@,")
(fun fmt (check,(safe,error,warning,info, unimplemented)) ->
fprintf fmt "%a: %d total%a%a%a%a%a"
fprintf fmt "- %a: %d total%a%a%a%a%a"
pp_check check
(safe+error+warning)
(pp Safe "safe" "safe") safe
(pp Safe "check passed" "checks passed") safe
(pp Error "error" "errors") error
(pp Warning "warning" "warnings") warning
(pp Info "info" "info") info
Expand All @@ -333,10 +332,7 @@ let print_checks_summary checks_map total safe error warning info unimplemented

let report man flow ~time ~files ~out =
let rep = Flow.get_report flow in
if is_sound_report rep
then print out "%a@." (Debug.color_str Debug.green) "Analysis terminated successfully"
else print out "%a@." (Debug.color_str Debug.orange) "Analysis terminated successfully (with assumptions)";

print out "## Issues Found@.";
if !opt_display_lastflow then
print out "Last flow =@[@\n%a@]@\n"
(* "Context = @[@\n%a@]@\n" *)
Expand All @@ -351,6 +347,7 @@ let report man flow ~time ~files ~out =

let total, safe, error, warning, info, unimplemented, checks_map = construct_checks_summary ~print:(not (!opt_no_detailed_checks)) rep out in

print out "@.";
if not (!opt_no_analysis_summary) then print_checks_summary checks_map total safe error warning info unimplemented out;
if not (is_sound_report rep) then
let nb = AssumptionSet.cardinal rep.report_assumptions in
Expand Down
16 changes: 9 additions & 7 deletions analyzer/languages/c/iterators/program.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -307,31 +307,33 @@ struct


let output_results skipped_functions unimplemented_functions results to_test =
let pp_markdown_function fmt name = Format.fprintf fmt "`%s`" name in
let pp_unknown_functions fmt set =
Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt ","; Format.pp_print_space fmt ()) Format.pp_print_string fmt (StringSet.elements set)
Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt ","; Format.pp_print_space fmt ()) pp_markdown_function fmt (StringSet.elements set)
in
let pp_runtime_analysis_results fmt results =
List.iter (fun (f, res) -> Format.fprintf fmt "%s (%s)\n" f (Output.Text.icon_of_diag res)) results
List.iter (fun (f, res) -> Format.fprintf fmt "- %a (%s)\n" pp_markdown_function f (Output.Text.icon_of_diag res)) results
in
let pp_missing_functions fmt map =
Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt ","; Format.pp_print_space fmt ()) Format.pp_print_string fmt (StringMap.fold (fun name _ names -> name :: names) map [])
Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt ","; Format.pp_print_space fmt ()) pp_markdown_function fmt (StringMap.fold (fun name _ names -> name :: names) map [])
in
let pp_unimplemented_functions fmt set =
Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt ","; Format.pp_print_space fmt ()) Format.pp_print_string fmt (StringSet.elements set)
Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_string fmt ","; Format.pp_print_space fmt ()) pp_markdown_function fmt (StringSet.elements set)
in
let results_map = StringMap.of_list results in
let missing_functions = StringMap.filter (fun name _ -> not (StringMap.mem name results_map)) to_test in
if not (!Output.Text.opt_no_ffi_report) then
Format.printf
"**Analyzed functions:**\n%a\n**Skipped C functions:**@\n@[%a@]@\n\n**Missing external functions:**@\n@[%a@]@\n\n**Unimplemented OCaml FFI functions:**@\n@[%a@]@\n\n"
(Format.printf "Analysis completed successfully.\n\n";
Format.printf
"**Analyzed functions:**\n%a\n**Skipped C functions:**@\n\n@[%a@]@\n\n**Missing external functions:**@\n@[%a@]@\n\n**Unimplemented OCaml FFI functions:**@\n@[%a@]@\n\n"
pp_runtime_analysis_results
results
pp_unknown_functions
skipped_functions
pp_missing_functions
missing_functions
pp_unimplemented_functions
unimplemented_functions
unimplemented_functions)

let exec_runtime_tests c_functions man flow =
(* Determine the runtime functions to execute; we sort them by program order *)
Expand Down
1 change: 0 additions & 1 deletion analyzer/languages/c/memory/machine_numbers.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -376,7 +376,6 @@ struct
let check_float_valid cexp ?(nexp=c2num cexp) range man flow =
let typ = cexp.etyp in
let prec = get_c_float_precision typ in
let itv = ask_and_reduce man.ask (Universal.Numeric.Common.mk_float_interval_query ~prec nexp) flow in
let flow', nexp' =
if !opt_float_invalid_operation then
(* This interval query is duplicated, because it can fail and is not necessary if [opt_float_invalid_operation] is false. *)
Expand Down