@ -100,155 +100,93 @@ exception Wrong_argument_number of L.ocaml_pos
type t =
type t =
{ issue_type : IssueType . t
{ issue_type : IssueType . t
; description : Localise . error_desc
; description : Localise . error_desc
; ocaml_pos : L . ocaml_pos option (* * location in the infer source code *)
; ocaml_pos : L . ocaml_pos option (* * location in the infer source code *) }
; severity : IssueType . severity option }
let recognize_exception exn =
let recognize_exception exn =
match exn with
match exn with
| Abduction_case_not_implemented ocaml_pos ->
| Abduction_case_not_implemented ocaml_pos ->
{ issue_type = IssueType . abduction_case_not_implemented
{ issue_type = IssueType . abduction_case_not_implemented
; description = Localise . no_desc
; description = Localise . no_desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos }
; severity = None }
| Analysis_stops ( desc , ocaml_pos_opt ) ->
| Analysis_stops ( desc , ocaml_pos_opt ) ->
{ issue_type = IssueType . biabduction_analysis_stops
{ issue_type = IssueType . biabduction_analysis_stops ; description = desc ; ocaml_pos = ocaml_pos_opt }
; description = desc
; ocaml_pos = ocaml_pos_opt
; severity = None }
| Array_of_pointsto ocaml_pos ->
| Array_of_pointsto ocaml_pos ->
{ issue_type = IssueType . array_of_pointsto
{ issue_type = IssueType . array_of_pointsto
; description = Localise . no_desc
; description = Localise . no_desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos }
; severity = None }
| Array_out_of_bounds_l1 ( desc , ocaml_pos ) ->
| Array_out_of_bounds_l1 ( desc , ocaml_pos ) ->
{ issue_type = IssueType . array_out_of_bounds_l1
{ issue_type = IssueType . array_out_of_bounds_l1 ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = Some Error }
| Array_out_of_bounds_l2 ( desc , ocaml_pos ) ->
| Array_out_of_bounds_l2 ( desc , ocaml_pos ) ->
{ issue_type = IssueType . array_out_of_bounds_l2
{ issue_type = IssueType . array_out_of_bounds_l2 ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = None }
| Array_out_of_bounds_l3 ( desc , ocaml_pos ) ->
| Array_out_of_bounds_l3 ( desc , ocaml_pos ) ->
{ issue_type = IssueType . array_out_of_bounds_l3
{ issue_type = IssueType . array_out_of_bounds_l3 ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = None }
| Assert_failure ( f , l , c ) ->
| Assert_failure ( f , l , c ) ->
let ocaml_pos = ( f , l , c , c ) in
let ocaml_pos = ( f , l , c , c ) in
{ issue_type = IssueType . assert_failure
{ issue_type = IssueType . assert_failure
; description = Localise . no_desc
; description = Localise . no_desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos }
; severity = None }
| Bad_footprint ocaml_pos ->
| Bad_footprint ocaml_pos ->
{ issue_type = IssueType . bad_footprint
{ issue_type = IssueType . bad_footprint ; description = Localise . no_desc ; ocaml_pos = Some ocaml_pos }
; description = Localise . no_desc
; ocaml_pos = Some ocaml_pos
; severity = None }
| Biabd_use_after_free ( desc , ocaml_pos ) ->
| Biabd_use_after_free ( desc , ocaml_pos ) ->
{ issue_type = IssueType . biabd_use_after_free
{ issue_type = IssueType . biabd_use_after_free ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = None }
| Cannot_star ocaml_pos ->
| Cannot_star ocaml_pos ->
{ issue_type = IssueType . cannot_star
{ issue_type = IssueType . cannot_star ; description = Localise . no_desc ; ocaml_pos = Some ocaml_pos }
; description = Localise . no_desc
; ocaml_pos = Some ocaml_pos
; severity = None }
| Class_cast_exception ( desc , ocaml_pos ) ->
| Class_cast_exception ( desc , ocaml_pos ) ->
{ issue_type = IssueType . class_cast_exception
{ issue_type = IssueType . class_cast_exception ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = None }
| Condition_always_true_false ( desc , b , ocaml_pos ) ->
| Condition_always_true_false ( desc , b , ocaml_pos ) ->
let issue_type =
let issue_type =
if b then IssueType . biabd_condition_always_true else IssueType . biabd_condition_always_false
if b then IssueType . biabd_condition_always_true else IssueType . biabd_condition_always_false
in
in
{ issue_type ; description = desc ; ocaml_pos = Some ocaml_pos ; severity = None }
{ issue_type ; description = desc ; ocaml_pos = Some ocaml_pos }
| Custom_error ( error_msg , severity , desc ) ->
| Custom_error ( error_msg , severity , desc ) ->
{ issue_type = IssueType . register_from_string ~ id : error_msg severity Biabduction
{ issue_type = IssueType . register_from_string ~ id : error_msg severity Biabduction
; description = desc
; description = desc
; ocaml_pos = None
; ocaml_pos = None }
; severity = None }
| Dangling_pointer_dereference ( user_visible , desc , ocaml_pos ) ->
| Dangling_pointer_dereference ( user_visible , desc , ocaml_pos ) ->
let issue_type =
let issue_type =
if user_visible then IssueType . dangling_pointer_dereference
if user_visible then IssueType . dangling_pointer_dereference
else IssueType . dangling_pointer_dereference_maybe
else IssueType . dangling_pointer_dereference_maybe
in
in
{ issue_type ; description = desc ; ocaml_pos = Some ocaml_pos ; severity = None }
{ issue_type ; description = desc ; ocaml_pos = Some ocaml_pos }
| Deallocate_stack_variable desc ->
| Deallocate_stack_variable desc ->
{ issue_type = IssueType . deallocate_stack_variable
{ issue_type = IssueType . deallocate_stack_variable ; description = desc ; ocaml_pos = None }
; description = desc
; ocaml_pos = None
; severity = None }
| Deallocate_static_memory desc ->
| Deallocate_static_memory desc ->
{ issue_type = IssueType . deallocate_static_memory
{ issue_type = IssueType . deallocate_static_memory ; description = desc ; ocaml_pos = None }
; description = desc
; ocaml_pos = None
; severity = None }
| Deallocation_mismatch ( desc , ocaml_pos ) ->
| Deallocation_mismatch ( desc , ocaml_pos ) ->
{ issue_type = IssueType . deallocation_mismatch
{ issue_type = IssueType . deallocation_mismatch ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = None }
| Divide_by_zero ( desc , ocaml_pos ) ->
| Divide_by_zero ( desc , ocaml_pos ) ->
{ issue_type = IssueType . divide_by_zero
{ issue_type = IssueType . divide_by_zero ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = Some Error }
| Empty_vector_access ( desc , ocaml_pos ) ->
| Empty_vector_access ( desc , ocaml_pos ) ->
{ issue_type = IssueType . empty_vector_access
{ issue_type = IssueType . empty_vector_access ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = Some Error }
| Field_not_null_checked ( desc , ocaml_pos ) ->
| Field_not_null_checked ( desc , ocaml_pos ) ->
{ issue_type = IssueType . field_not_null_checked
{ issue_type = IssueType . field_not_null_checked ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = Some Warning }
| Frontend_warning ( issue_type , desc , ocaml_pos ) ->
| Frontend_warning ( issue_type , desc , ocaml_pos ) ->
{ issue_type ; description = desc ; ocaml_pos = Some ocaml_pos ; severity = None }
{ issue_type ; description = desc ; ocaml_pos = Some ocaml_pos }
| Checkers ( kind , desc ) ->
| Checkers ( kind , desc ) ->
{ issue_type = kind ; description = desc ; ocaml_pos = None ; severity = None }
{ issue_type = kind ; description = desc ; ocaml_pos = None }
| Null_dereference ( desc , ocaml_pos ) ->
| Null_dereference ( desc , ocaml_pos ) ->
{ issue_type = IssueType . null_dereference
{ issue_type = IssueType . null_dereference ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = None }
| Null_test_after_dereference ( desc , ocaml_pos ) ->
| Null_test_after_dereference ( desc , ocaml_pos ) ->
{ issue_type = IssueType . null_test_after_dereference
{ issue_type = IssueType . null_test_after_dereference
; description = desc
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos }
; severity = None }
| Pointer_size_mismatch ( desc , ocaml_pos ) ->
| Pointer_size_mismatch ( desc , ocaml_pos ) ->
{ issue_type = IssueType . pointer_size_mismatch
{ issue_type = IssueType . pointer_size_mismatch ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = Some Error }
| Inherently_dangerous_function desc ->
| Inherently_dangerous_function desc ->
{ issue_type = IssueType . inherently_dangerous_function
{ issue_type = IssueType . inherently_dangerous_function ; description = desc ; ocaml_pos = None }
; description = desc
; ocaml_pos = None
; severity = None }
| Internal_error desc ->
| Internal_error desc ->
{ issue_type = IssueType . internal_error ; description = desc ; ocaml_pos = None ; severity = None }
{ issue_type = IssueType . internal_error ; description = desc ; ocaml_pos = None }
| Leak ( fp_part , ( user_visible , error_desc ) , done_array_abstraction , resource , ocaml_pos ) ->
| Leak ( fp_part , ( user_visible , error_desc ) , done_array_abstraction , resource , ocaml_pos ) ->
if done_array_abstraction then
if done_array_abstraction then
{ issue_type = IssueType . leak_after_array_abstraction
{ issue_type = IssueType . leak_after_array_abstraction
; description = error_desc
; description = error_desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos }
; severity = None }
else if fp_part then
else if fp_part then
{ issue_type = IssueType . leak_in_footprint
{ issue_type = IssueType . leak_in_footprint ; description = error_desc ; ocaml_pos = Some ocaml_pos }
; description = error_desc
; ocaml_pos = Some ocaml_pos
; severity = None }
else if not user_visible then
else if not user_visible then
{ issue_type = IssueType . leak_unknown_origin
{ issue_type = IssueType . leak_unknown_origin
; description = error_desc
; description = error_desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos }
; severity = None }
else
else
let issue_type =
let issue_type =
match resource with
match resource with
@ -261,83 +199,53 @@ let recognize_exception exn =
| PredSymb . Rignore ->
| PredSymb . Rignore ->
IssueType . memory_leak
IssueType . memory_leak
in
in
{ issue_type ; description = error_desc ; ocaml_pos = Some ocaml_pos ; severity = None }
{ issue_type ; description = error_desc ; ocaml_pos = Some ocaml_pos }
| Missing_fld ( fld , ocaml_pos ) ->
| Missing_fld ( fld , ocaml_pos ) ->
let desc = Localise . verbatim_desc ( Fieldname . to_full_string fld ) in
let desc = Localise . verbatim_desc ( Fieldname . to_full_string fld ) in
{ issue_type = IssueType . missing_fld
{ issue_type = IssueType . missing_fld ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = None }
| Premature_nil_termination ( desc , ocaml_pos ) ->
| Premature_nil_termination ( desc , ocaml_pos ) ->
{ issue_type = IssueType . premature_nil_termination
{ issue_type = IssueType . premature_nil_termination ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = None }
| Parameter_not_null_checked ( desc , ocaml_pos ) ->
| Parameter_not_null_checked ( desc , ocaml_pos ) ->
{ issue_type = IssueType . parameter_not_null_checked
{ issue_type = IssueType . parameter_not_null_checked
; description = desc
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos }
; severity = Some Warning }
| Precondition_not_found ( desc , ocaml_pos ) ->
| Precondition_not_found ( desc , ocaml_pos ) ->
{ issue_type = IssueType . precondition_not_found
{ issue_type = IssueType . precondition_not_found ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = None }
| Precondition_not_met ( desc , ocaml_pos ) ->
| Precondition_not_met ( desc , ocaml_pos ) ->
{ issue_type = IssueType . precondition_not_met
{ issue_type = IssueType . precondition_not_met ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = Some Warning }
(* always a warning *)
| Retain_cycle ( desc , ocaml_pos ) ->
| Retain_cycle ( desc , ocaml_pos ) ->
{ issue_type = IssueType . retain_cycle
{ issue_type = IssueType . retain_cycle ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = None }
| Registered_observer_being_deallocated ( desc , ocaml_pos ) ->
| Registered_observer_being_deallocated ( desc , ocaml_pos ) ->
{ issue_type = IssueType . biabd_registered_observer_being_deallocated
{ issue_type = IssueType . biabd_registered_observer_being_deallocated
; description = desc
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos }
; severity = Some Error }
| Stack_variable_address_escape ( desc , ocaml_pos ) ->
| Stack_variable_address_escape ( desc , ocaml_pos ) ->
{ issue_type = IssueType . biabd_stack_variable_address_escape
{ issue_type = IssueType . biabd_stack_variable_address_escape
; description = desc
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos }
; severity = Some Error }
| SymOp . Analysis_failure_exe _ ->
| SymOp . Analysis_failure_exe _ ->
{ issue_type = IssueType . failure_exe
{ issue_type = IssueType . failure_exe ; description = Localise . no_desc ; ocaml_pos = None }
; description = Localise . no_desc
; ocaml_pos = None
; severity = None }
| Skip_function desc ->
| Skip_function desc ->
{ issue_type = IssueType . skip_function ; description = desc ; ocaml_pos = None ; severity = None }
{ issue_type = IssueType . skip_function ; description = desc ; ocaml_pos = None }
| Skip_pointer_dereference ( desc , ocaml_pos ) ->
| Skip_pointer_dereference ( desc , ocaml_pos ) ->
{ issue_type = IssueType . skip_pointer_dereference
{ issue_type = IssueType . skip_pointer_dereference ; description = desc ; ocaml_pos = Some ocaml_pos }
; description = desc
; ocaml_pos = Some ocaml_pos
; severity = Some Info }
(* always an info *)
| Symexec_memory_error ocaml_pos ->
| Symexec_memory_error ocaml_pos ->
{ issue_type = IssueType . symexec_memory_error
{ issue_type = IssueType . symexec_memory_error
; description = Localise . no_desc
; description = Localise . no_desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos }
; severity = None }
| Unary_minus_applied_to_unsigned_expression ( desc , ocaml_pos ) ->
| Unary_minus_applied_to_unsigned_expression ( desc , ocaml_pos ) ->
{ issue_type = IssueType . unary_minus_applied_to_unsigned_expression
{ issue_type = IssueType . unary_minus_applied_to_unsigned_expression
; description = desc
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos }
; severity = None }
| Wrong_argument_number ocaml_pos ->
| Wrong_argument_number ocaml_pos ->
{ issue_type = IssueType . wrong_argument_number
{ issue_type = IssueType . wrong_argument_number
; description = Localise . no_desc
; description = Localise . no_desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos }
; severity = None }
| exn ->
| exn ->
{ issue_type = IssueType . failure_exe
{ issue_type = IssueType . failure_exe
; description =
; description =
Localise . verbatim_desc ( F . asprintf " %a: %s " Exn . pp exn ( Caml . Printexc . get_backtrace () ) )
Localise . verbatim_desc ( F . asprintf " %a: %s " Exn . pp exn ( Caml . Printexc . get_backtrace () ) )
; ocaml_pos = None
; ocaml_pos = None }
; severity = None }
(* * print a description of the exception to the html output *)
(* * print a description of the exception to the html output *)
@ -355,7 +263,8 @@ let print_exception_html s exn =
(* * pretty print an error *)
(* * pretty print an error *)
let pp_err loc severity issue_type desc ocaml_pos_opt fmt () =
let pp_err ? severity_override loc issue_type desc ocaml_pos_opt fmt () =
let severity = Option . value severity_override ~ default : issue_type . IssueType . default_severity in
let kind =
let kind =
IssueType . string_of_severity
IssueType . string_of_severity
( if IssueType . equal_severity severity Info then Warning else severity )
( if IssueType . equal_severity severity Info then Warning else severity )