@ -15,8 +15,6 @@ open Dataflow
(* ERADICATE CHECKER. TODOS: *)
(* ERADICATE CHECKER. TODOS: *)
(* 1 ) add support for constructors for anonymous inner classes ( currently not checked ) *)
(* 1 ) add support for constructors for anonymous inner classes ( currently not checked ) *)
(* check that nonnullable fields are initialized in constructors *)
let check_field_initialization = true
(* * Type for a module that provides a main callback function *)
(* * Type for a module that provides a main callback function *)
module type CallBackT = sig
module type CallBackT = sig
@ -282,7 +280,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
if
if
not calls_this
not calls_this
(* if 'this ( ... ) ' is called, no need to check initialization *)
(* if 'this ( ... ) ' is called, no need to check initialization *)
&& check _field_initialization && check s. TypeCheck . eradicate
&& check s. TypeCheck . eradicate
then
then
EradicateChecks . check_constructor_initialization tenv find_canonical_duplicate curr_pname
EradicateChecks . check_constructor_initialization tenv find_canonical_duplicate curr_pname
curr_pdesc start_node Initializers . final_initializer_typestates_lazy
curr_pdesc start_node Initializers . final_initializer_typestates_lazy