@ -19,11 +19,6 @@ type visibility =
let equal_visibility = [ % compare . equal : visibility ]
let equal_visibility = [ % compare . equal : visibility ]
(* * class of error/warning *)
type err_class = Checker | Prover | Nocat | Linters [ @@ deriving compare ]
let equal_err_class = [ % compare . equal : err_class ]
(* * severity of the report *)
(* * severity of the report *)
type severity = Like | Info | Advice | Warning | Error [ @@ deriving compare ]
type severity = Like | Info | Advice | Warning | Error [ @@ deriving compare ]
@ -119,8 +114,7 @@ type 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 *)
; visibility : visibility
; visibility : visibility
; severity : severity option
; severity : severity option }
; category : err_class }
let recognize_exception exn =
let recognize_exception exn =
match exn with
match exn with
@ -129,80 +123,69 @@ let recognize_exception exn =
; description = Localise . no_desc
; description = Localise . no_desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Nocat }
| Analysis_stops ( desc , ocaml_pos_opt ) ->
| Analysis_stops ( desc , ocaml_pos_opt ) ->
let visibility = if Config . analysis_stops then Exn_user else Exn_developer in
let visibility = if Config . analysis_stops then Exn_user else Exn_developer in
{ issue_type = IssueType . analysis_stops
{ issue_type = IssueType . analysis_stops
; description = desc
; description = desc
; ocaml_pos = ocaml_pos_opt
; ocaml_pos = ocaml_pos_opt
; visibility
; visibility
; severity = None
; severity = None }
; category = Nocat }
| 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
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Nocat }
| 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_developer
; visibility = Exn_developer
; severity = Some Error
; severity = Some Error }
; category = Checker }
| 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Nocat }
| 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Nocat }
| 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
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Nocat }
| Bad_footprint ocaml_pos ->
| Bad_footprint ocaml_pos ->
{ issue_type = IssueType . bad_footprint
{ issue_type = IssueType . bad_footprint
; description = Localise . no_desc
; description = Localise . no_desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Nocat }
| 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_user
; visibility = Exn_user
; severity = None
; severity = None }
; category = Prover }
| Cannot_star ocaml_pos ->
| Cannot_star ocaml_pos ->
{ issue_type = IssueType . cannot_star
{ issue_type = IssueType . cannot_star
; description = Localise . no_desc
; description = Localise . no_desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Nocat }
| 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Prover }
| 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
@ -211,143 +194,115 @@ let recognize_exception exn =
; description = desc
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_user
; visibility = Exn_user
; severity = None
; severity = None }
; category = Nocat }
| Custom_error ( error_msg , desc ) ->
| Custom_error ( error_msg , desc ) ->
{ issue_type = IssueType . register_from_string ~ id : error_msg Biabduction
{ issue_type = IssueType . register_from_string ~ id : error_msg Biabduction
; description = desc
; description = desc
; ocaml_pos = None
; ocaml_pos = None
; visibility = Exn_user
; visibility = Exn_user
; severity = None
; severity = None }
; category = Checker }
| Dummy_exception desc ->
| Dummy_exception desc ->
{ issue_type = IssueType . analysis_stops
{ issue_type = IssueType . analysis_stops
; description = desc
; description = desc
; ocaml_pos = None
; ocaml_pos = None
; visibility = Exn_developer
; visibility = Exn_developer
; severity = Some Info
; severity = Some Info }
; category = Checker }
| Dangling_pointer_dereference ( user_visible , desc , ocaml_pos ) ->
| Dangling_pointer_dereference ( user_visible , desc , ocaml_pos ) ->
let visibility = if user_visible then Exn_user else Exn_developer in
let visibility = if user_visible then Exn_user else Exn_developer in
{ issue_type = IssueType . dangling_pointer_dereference
{ issue_type = IssueType . dangling_pointer_dereference
; description = desc
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility
; visibility
; severity = None
; severity = None }
; category = Prover }
| Deallocate_stack_variable desc ->
| Deallocate_stack_variable desc ->
{ issue_type = IssueType . deallocate_stack_variable
{ issue_type = IssueType . deallocate_stack_variable
; description = desc
; description = desc
; ocaml_pos = None
; ocaml_pos = None
; visibility = Exn_user
; visibility = Exn_user
; severity = None
; severity = None }
; category = Prover }
| Deallocate_static_memory desc ->
| Deallocate_static_memory desc ->
{ issue_type = IssueType . deallocate_static_memory
{ issue_type = IssueType . deallocate_static_memory
; description = desc
; description = desc
; ocaml_pos = None
; ocaml_pos = None
; visibility = Exn_user
; visibility = Exn_user
; severity = None
; severity = None }
; category = Prover }
| Deallocation_mismatch ( desc , ocaml_pos ) ->
| Deallocation_mismatch ( desc , ocaml_pos ) ->
{ issue_type = IssueType . deallocation_mismatch
{ issue_type = IssueType . deallocation_mismatch
; description = desc
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_user
; visibility = Exn_user
; severity = None
; severity = None }
; category = Prover }
| 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_user
; visibility = Exn_user
; severity = Some Error
; severity = Some Error }
; category = Checker }
| Eradicate ( kind , desc ) ->
| Eradicate ( kind , desc ) ->
{ issue_type = kind
{ issue_type = kind ; description = desc ; ocaml_pos = None ; visibility = Exn_user ; severity = None }
; description = desc
; ocaml_pos = None
; visibility = Exn_user
; severity = None
; category = Prover }
| 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_user
; visibility = Exn_user
; severity = Some Error
; severity = Some Error }
; category = Prover }
| 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_user
; visibility = Exn_user
; severity = Some Warning
; severity = Some Warning }
; category = Nocat }
| Frontend_warning ( issue_type , desc , ocaml_pos ) ->
| Frontend_warning ( issue_type , desc , ocaml_pos ) ->
{ issue_type
{ issue_type
; description = desc
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_user
; visibility = Exn_user
; severity = None
; severity = None }
; category = Linters }
| Checkers ( kind , desc ) ->
| Checkers ( kind , desc ) ->
{ issue_type = kind
{ issue_type = kind ; description = desc ; ocaml_pos = None ; visibility = Exn_user ; severity = None }
; description = desc
; ocaml_pos = None
; visibility = Exn_user
; severity = None
; category = Prover }
| Null_dereference ( desc , ocaml_pos ) ->
| Null_dereference ( desc , ocaml_pos ) ->
{ issue_type = IssueType . null_dereference
{ issue_type = IssueType . null_dereference
; description = desc
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_user
; visibility = Exn_user
; severity = None
; severity = None }
; category = Prover }
| 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
; visibility = Exn_user
; visibility = Exn_user
; severity = None
; severity = None }
; category = Nocat }
| 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_user
; visibility = Exn_user
; severity = Some Error
; severity = Some Error }
; category = Checker }
| Inherently_dangerous_function desc ->
| Inherently_dangerous_function desc ->
{ issue_type = IssueType . inherently_dangerous_function
{ issue_type = IssueType . inherently_dangerous_function
; description = desc
; description = desc
; ocaml_pos = None
; ocaml_pos = None
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Nocat }
| Internal_error desc ->
| Internal_error desc ->
{ issue_type = IssueType . internal_error
{ issue_type = IssueType . internal_error
; description = desc
; description = desc
; ocaml_pos = None
; ocaml_pos = None
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Nocat }
| Leak ( fp_part , ( exn_vis , error_desc ) , done_array_abstraction , resource , ocaml_pos ) ->
| Leak ( fp_part , ( exn_vis , 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
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Prover }
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
; description = error_desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Prover }
else
else
let issue_type =
let issue_type =
match resource with
match resource with
@ -364,117 +319,101 @@ let recognize_exception exn =
; description = error_desc
; description = error_desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = exn_vis
; visibility = exn_vis
; severity = None
; severity = None }
; category = Prover }
| 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Nocat }
| 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_user
; visibility = Exn_user
; severity = None
; severity = None }
; category = Prover }
| 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
; visibility = Exn_user
; visibility = Exn_user
; severity = Some Warning
; severity = Some Warning }
; category = Nocat }
| 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Nocat }
| 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_developer
; visibility = Exn_developer
; severity = Some Warning
; severity = Some Warning }
; category = Nocat }
(* always a 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_user
; visibility = Exn_user
; severity = None
; severity = None }
; category = Prover }
| 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
; visibility = Exn_user
; visibility = Exn_user
; severity = Some Error
; severity = Some Error }
; category = Nocat }
| 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
; visibility = Exn_user
; visibility = Exn_user
; severity = Some Error
; severity = Some Error }
; category = Nocat }
| SymOp . Analysis_failure_exe _ ->
| SymOp . Analysis_failure_exe _ ->
{ issue_type = IssueType . failure_exe
{ issue_type = IssueType . failure_exe
; description = Localise . no_desc
; description = Localise . no_desc
; ocaml_pos = None
; ocaml_pos = None
; visibility = Exn_system
; visibility = Exn_system
; severity = None
; severity = None }
; category = Nocat }
| Skip_function desc ->
| Skip_function desc ->
{ issue_type = IssueType . skip_function
{ issue_type = IssueType . skip_function
; description = desc
; description = desc
; ocaml_pos = None
; ocaml_pos = None
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Nocat }
| 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
; description = desc
; ocaml_pos = Some ocaml_pos
; ocaml_pos = Some ocaml_pos
; visibility = Exn_user
; visibility = Exn_user
; severity = Some Info
; severity = Some Info }
; category = Nocat }
(* always an 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
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Nocat }
| 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
; visibility = Exn_user
; visibility = Exn_user
; severity = None
; severity = None }
; category = Nocat }
| 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
; visibility = Exn_developer
; visibility = Exn_developer
; severity = None
; severity = None }
; category = Nocat }
| 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
; visibility = Exn_system
; visibility = Exn_system
; severity = None
; severity = None }
; category = Nocat }
(* * print a description of the exception to the html output *)
(* * print a description of the exception to the html output *)