pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Remove uses of assert false to get original ml location.

Browse Source 
Reviewed By: jvillard, jberdine

Differential Revision: D2922516

fb-gh-sync-id: 153a2dd
shipit-source-id: 153a2dd
master
Cristiano Calcagno 9 years ago committed by facebook-github-bot-1
parent 8d78670bd8
commit 2a926d8294
26 changed files with 452 additions and 379 deletions
Show Stats Download Patch File Download Diff File

15
infer/lib/python/inferlib/issues.py
Unescape View File

@ -95,8 +95,10 @@ JSON_INDEX_TRACE_NODE_TAGS_TAG = 'tags'
JSON_INDEX_TRACE_NODE_TAGS_VALUE = 'value'
JSON_INDEX_INFER_SOURCE_LOC = 'infer_source_loc'
JSON_INDEX_ISL_FILE = 'file'
JSON_INDEX_ISL_LINE = 'line'
JSON_INDEX_ISL_COLUMN = 'column'
JSON_INDEX_ISL_LNUM = 'lnum'
JSON_INDEX_ISL_CNUM = 'cnum'
JSON_INDEX_ISL_ENUM = 'enum'
QUALIFIER_TAGS = 'qualifier_tags'
BUCKET_TAGS = 'bucket'
@ -143,14 +145,15 @@ def clean_json(args, json_report):
utils.dump_json_to_path(rows, temporary_file)
shutil.move(temporary_file, json_report)
def _text_of_infer_loc(loc):
return u' (%s:%d:%d)' % (
return u' (%s:%d:%d-%d:)' % (
loc[JSON_INDEX_ISL_FILE],
loc[JSON_INDEX_ISL_LINE],
loc[JSON_INDEX_ISL_COLUMN],
loc[JSON_INDEX_ISL_LNUM],
loc[JSON_INDEX_ISL_CNUM],
loc[JSON_INDEX_ISL_ENUM],
)
def text_of_report(report):
filename = report[JSON_INDEX_FILENAME]
kind = report[JSON_INDEX_KIND]

5
infer/src/backend/abs.ml
Unescape View File

@ -1298,14 +1298,13 @@ let check_junk ?original_prop pname tenv prop =
let desc = Errdesc.explain_retain_cycle
(remove_opt original_prop) cycle (State.get_loc ()) cycle_dotty in
Exceptions.Retain_cycle
(remove_opt original_prop, hpred, desc,
try assert false with Assert_failure x -> x) in
(remove_opt original_prop, hpred, desc, __POS__) in
let exn_leak = Exceptions.Leak
(fp_part, prop, hpred,
Errdesc.explain_leak tenv hpred prop alloc_attribute ml_bucket_opt,
!Absarray.array_abstraction_performed,
resource,
try assert false with Assert_failure x -> x) in
__POS__) in
let ignore_resource, exn =
(match alloc_attribute, resource with
| Some _, Sil.Rmemory Sil.Mobjc when (hpred_in_cycle hpred) ->

27
infer/src/backend/errlog.ml
Unescape View File

@ -24,12 +24,12 @@ type loc_trace = loc_trace_elem list
(** Data associated to a specific error *)
type err_data =
(int * int) * int * Location.t * ml_location option * loc_trace *
(int * int) * int * Location.t * ml_loc option * loc_trace *
Prop.normal Prop.t option * Exceptions.err_class
let err_data_compare
((nodeid1, key1), session1, loc1, mloco1, ltr1, po1, ec1)
((nodeid2, key2), session2, loc2, mloco2, ltr2, po2, ec2) =
((nodeid1, key1), session1, loc1, ml_loc_opt1, ltr1, po1, ec1)
((nodeid2, key2), session2, loc2, ml_loc_opt2, ltr2, po2, ec2) =
Location.compare loc1 loc2
module ErrDataSet = (* set err_data with no repeated loc *)
@ -66,7 +66,7 @@ let empty () = ErrLogHash.create 13
type iter_fun =
(int * int) ->
Location.t ->
ml_location option ->
ml_loc option ->
Exceptions.err_kind ->
bool ->
Localise.t -> Localise.error_desc -> string ->
@ -79,9 +79,9 @@ type iter_fun =
let iter (f: iter_fun) (err_log: t) =
ErrLogHash.iter (fun (ekind, in_footprint, err_name, desc, severity) set ->
ErrDataSet.iter
(fun (node_id_key, section, loc, mloco, ltr, pre_opt, eclass) ->
(fun (node_id_key, section, loc, ml_loc_opt, ltr, pre_opt, eclass) ->
f
node_id_key loc mloco ekind in_footprint err_name
node_id_key loc ml_loc_opt ekind in_footprint err_name
desc severity ltr pre_opt eclass)
set)
err_log
@ -110,7 +110,8 @@ let pp_warnings fmt (errlog : t) =
(** Print an error log in html format *)
let pp_html path_to_root fmt (errlog: t) =
let pp_eds fmt eds =
let pp_nodeid_session_loc fmt ((nodeid, nodekey), session, loc, mloco, ltr, pre_opt, eclass) =
let pp_nodeid_session_loc
fmt ((nodeid, nodekey), session, loc, ml_loc_opt, ltr, pre_opt, eclass) =
Io_infer.Html.pp_session_link path_to_root fmt (nodeid, session, loc.Location.line) in
ErrDataSet.iter (pp_nodeid_session_loc fmt) eds in
let f do_fp ek (ekind, infp, err_name, desc, severity) eds =
@ -167,7 +168,7 @@ let update errlog_old errlog_new =
let log_issue _ekind err_log loc node_id_key session ltr pre_opt exn =
let err_name, desc, mloco, visibility, severity, force_kind, eclass =
let err_name, desc, ml_loc_opt, visibility, severity, force_kind, eclass =
Exceptions.recognize_exception exn in
let ekind = match force_kind with
| Some ekind -> ekind
@ -188,14 +189,14 @@ let log_issue _ekind err_log loc node_id_key session ltr pre_opt exn =
let added =
add_issue err_log
(ekind, !Config.footprint, err_name, desc, severity_to_str severity)
(ErrDataSet.singleton (node_id_key, session, loc, mloco, ltr, pre_opt, eclass)) in
(ErrDataSet.singleton (node_id_key, session, loc, ml_loc_opt, ltr, pre_opt, eclass)) in
let should_print_now =
match exn with
| Exceptions.Internal_error _ -> true
| _ -> added in
let print_now () =
let ex_name, desc, mloco, _, _, _, _ = Exceptions.recognize_exception exn in
L.err "%a@?" (Exceptions.pp_err node_id_key loc ekind ex_name desc mloco) ();
let ex_name, desc, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in
L.err "%a@?" (Exceptions.pp_err node_id_key loc ekind ex_name desc ml_loc_opt) ();
if _ekind <> Exceptions.Kerror then begin
let warn_str =
let pp fmt () =
@ -265,9 +266,9 @@ module Err_table = struct
ErrDataSet.iter (fun loc -> add_err loc err_name) eds in
ErrLogHash.iter f err_table;
let pp ekind (nodeidkey, session, loc, mloco, ltr, pre_opt, eclass) fmt err_names =
let pp ekind (nodeidkey, session, loc, ml_loc_opt, ltr, pre_opt, eclass) fmt err_names =
IList.iter (fun (err_name, desc) ->
Exceptions.pp_err nodeidkey loc ekind err_name desc mloco fmt ()) err_names in
Exceptions.pp_err nodeidkey loc ekind err_name desc ml_loc_opt fmt ()) err_names in
F.fprintf fmt "@.Detailed errors during footprint phase:@.";
LocMap.iter (fun nslm err_names ->
F.fprintf fmt "%a" (pp Exceptions.Kerror nslm) err_names) !map_err_fp;

2
infer/src/backend/errlog.mli
Unescape View File

@ -32,7 +32,7 @@ val empty : unit -> t
type iter_fun =
(int * int) ->
Location.t ->
ml_location option ->
ml_loc option ->
Exceptions.err_kind ->
bool ->
Localise.t -> Localise.error_desc -> string ->

361
infer/src/backend/exceptions.ml
Unescape View File

@ -29,56 +29,62 @@ type err_class = Checker | Prover | Nocat
type err_kind =
Kwarning | Kerror | Kinfo
exception Abduction_case_not_implemented of ml_location
exception Analysis_stops of Localise.error_desc * ml_location option
exception Array_out_of_bounds_l1 of Localise.error_desc * ml_location
exception Array_out_of_bounds_l2 of Localise.error_desc * ml_location
exception Array_out_of_bounds_l3 of Localise.error_desc * ml_location
exception Array_of_pointsto of ml_location
exception Bad_footprint of ml_location
exception Bad_pointer_comparison of Localise.error_desc * ml_location
exception Class_cast_exception of Localise.error_desc * ml_location
exception Abduction_case_not_implemented of ml_loc
exception Analysis_stops of Localise.error_desc * ml_loc option
exception Array_out_of_bounds_l1 of Localise.error_desc * ml_loc
exception Array_out_of_bounds_l2 of Localise.error_desc * ml_loc
exception Array_out_of_bounds_l3 of Localise.error_desc * ml_loc
exception Array_of_pointsto of ml_loc
exception Bad_footprint of ml_loc
exception Bad_pointer_comparison of Localise.error_desc * ml_loc
exception Class_cast_exception of Localise.error_desc * ml_loc
exception Codequery of Localise.error_desc
exception Comparing_floats_for_equality of Localise.error_desc * ml_location
exception Condition_is_assignment of Localise.error_desc * ml_location
exception Condition_always_true_false of Localise.error_desc * bool * ml_location
exception Context_leak of Localise.error_desc * ml_location
exception Comparing_floats_for_equality of Localise.error_desc * ml_loc
exception Condition_is_assignment of Localise.error_desc * ml_loc
exception Condition_always_true_false of Localise.error_desc * bool * ml_loc
exception Context_leak of Localise.error_desc * ml_loc
exception Custom_error of string * Localise.error_desc
exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * ml_location
exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * ml_loc
exception Deallocate_stack_variable of Localise.error_desc
exception Deallocate_static_memory of Localise.error_desc
exception Deallocation_mismatch of Localise.error_desc * ml_location
exception Divide_by_zero of Localise.error_desc * ml_location
exception Deallocation_mismatch of Localise.error_desc * ml_loc
exception Divide_by_zero of Localise.error_desc * ml_loc
exception Eradicate of string * Localise.error_desc
exception Field_not_null_checked of Localise.error_desc * ml_location
exception Frontend_warning of string * Localise.error_desc * ml_location
exception Field_not_null_checked of Localise.error_desc * ml_loc
exception Frontend_warning of string * Localise.error_desc * ml_loc
exception Checkers of string * Localise.error_desc
exception Inherently_dangerous_function of Localise.error_desc
exception Internal_error of Localise.error_desc
exception Java_runtime_exception of Typename.t * string * Localise.error_desc
exception Leak of bool * Prop.normal Prop.t * Sil.hpred * (exception_visibility * Localise.error_desc) * bool * Sil.resource * ml_location
exception Missing_fld of Ident.fieldname * ml_location
exception Premature_nil_termination of Localise.error_desc * ml_location
exception Null_dereference of Localise.error_desc * ml_location
exception Null_test_after_dereference of Localise.error_desc * ml_location
exception Parameter_not_null_checked of Localise.error_desc * ml_location
exception Pointer_size_mismatch of Localise.error_desc * ml_location
exception Precondition_not_found of Localise.error_desc * ml_location
exception Precondition_not_met of Localise.error_desc * ml_location
exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * ml_location
exception Return_expression_required of Localise.error_desc * ml_location
exception Return_statement_missing of Localise.error_desc * ml_location
exception Return_value_ignored of Localise.error_desc * ml_location
exception Leak of
bool * Prop.normal Prop.t * Sil.hpred * (exception_visibility * Localise.error_desc)
* bool * Sil.resource * ml_loc
exception Missing_fld of Ident.fieldname * ml_loc
exception Premature_nil_termination of Localise.error_desc * ml_loc
exception Null_dereference of Localise.error_desc * ml_loc
exception Null_test_after_dereference of Localise.error_desc * ml_loc
exception Parameter_not_null_checked of Localise.error_desc * ml_loc
exception Pointer_size_mismatch of Localise.error_desc * ml_loc
exception Precondition_not_found of Localise.error_desc * ml_loc
exception Precondition_not_met of Localise.error_desc * ml_loc
exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * ml_loc
exception Return_expression_required of Localise.error_desc * ml_loc
exception Return_statement_missing of Localise.error_desc * ml_loc
exception Return_value_ignored of Localise.error_desc * ml_loc
exception Skip_function of Localise.error_desc
exception Skip_pointer_dereference of Localise.error_desc * ml_location
exception Stack_variable_address_escape of Localise.error_desc * ml_location
exception Symexec_memory_error of ml_location
exception Tainted_value_reaching_sensitive_function of Localise.error_desc * ml_location
exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * ml_location
exception Uninitialized_value of Localise.error_desc * ml_location
exception Skip_pointer_dereference of Localise.error_desc * ml_loc
exception Stack_variable_address_escape of Localise.error_desc * ml_loc
exception Symexec_memory_error of ml_loc
exception Tainted_value_reaching_sensitive_function of Localise.error_desc * ml_loc
exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * ml_loc
exception Uninitialized_value of Localise.error_desc * ml_loc
exception Unknown_proc
exception Use_after_free of Localise.error_desc * ml_location
exception Wrong_argument_number of ml_location
exception Use_after_free of Localise.error_desc * ml_loc
exception Wrong_argument_number of ml_loc
let file_line_column_string (file, line, column) =
Printf.sprintf "file %s line %d column %d" file line column
(** Turn an exception into a descriptive string, error description, location in ml source, and category *)
let recognize_exception exn =
@ -87,161 +93,220 @@ let recognize_exception exn =
match Localise.error_desc_get_bucket desc with
| None -> false
| Some bucket -> bucket <> Localise.BucketLevel.b1 in
let err_name, desc, mloco, visibility, severity, force_kind, eclass = match exn with (* all the names of Exn_user errors must be defined in Localise *)
| Abduction_case_not_implemented mloc ->
(Localise.from_string "Abduction_case_not_implemented", Localise.no_desc, Some mloc, Exn_developer, Low, None, Nocat)
let err_name, desc, (ml_loc_opt : ml_loc option), visibility, severity, force_kind, eclass =
match exn with (* all the names of Exn_user errors must be defined in Localise *)
| Abduction_case_not_implemented ml_loc ->
(Localise.from_string "Abduction_case_not_implemented",
Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat)
| Context_leak (desc, _) ->
(Localise.context_leak, desc, None, Exn_user, High, None, Nocat)
| Analysis_stops (desc, mloco) ->
(Localise.context_leak,
desc, None, Exn_user, High, None, Nocat)
| Analysis_stops (desc, ml_loc_opt) ->
let visibility = if !Config.analysis_stops then Exn_user else Exn_developer in
(Localise.analysis_stops, desc, mloco, visibility, Medium, None, Nocat)
| Array_of_pointsto mloc ->
(Localise.from_string "Array_of_pointsto", Localise.no_desc, Some mloc, Exn_developer, Low, None, Nocat)
| Array_out_of_bounds_l1 (desc, mloc) ->
(Localise.array_out_of_bounds_l1, desc, Some mloc, Exn_user, High, Some Kerror, Checker)
| Array_out_of_bounds_l2 (desc, mloc) ->
(Localise.array_out_of_bounds_l2, desc, Some mloc, Exn_user, Medium, None, Nocat)
| Array_out_of_bounds_l3 (desc, mloc) ->
(Localise.array_out_of_bounds_l3, desc, Some mloc, Exn_developer, Medium, None, Nocat)
| Assert_failure mloc ->
(Localise.from_string "Assert_failure", Localise.no_desc, Some mloc, Exn_developer, High, None, Nocat)
| Bad_pointer_comparison (desc, mloc) ->
(Localise.bad_pointer_comparison, desc, Some mloc, Exn_user, High, Some Kerror, Prover)
| Bad_footprint mloc ->
(Localise.from_string "Bad_footprint", Localise.no_desc, Some mloc, Exn_developer, Low, None, Nocat)
| Prop.Cannot_star mloc ->
(Localise.from_string "Cannot_star", Localise.no_desc, Some mloc, Exn_developer, Low, None, Nocat)
| Class_cast_exception (desc, mloc) ->
(Localise.class_cast_exception, desc, Some mloc, Exn_user, High, None, Prover)
(Localise.analysis_stops, desc, ml_loc_opt, visibility, Medium, None, Nocat)
| Array_of_pointsto ml_loc ->
(Localise.from_string "Array_of_pointsto",
Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat)
| Array_out_of_bounds_l1 (desc, ml_loc) ->
(Localise.array_out_of_bounds_l1,
desc, Some ml_loc, Exn_user, High, Some Kerror, Checker)
| Array_out_of_bounds_l2 (desc, ml_loc) ->
(Localise.array_out_of_bounds_l2,
desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Array_out_of_bounds_l3 (desc, ml_loc) ->
(Localise.array_out_of_bounds_l3,
desc, Some ml_loc, Exn_developer, Medium, None, Nocat)
| Assert_failure (f, l, c) ->
let ml_loc = (f, l, c, c) in
(Localise.from_string "Assert_failure",
Localise.no_desc, Some ml_loc, Exn_developer, High, None, Nocat)
| Bad_pointer_comparison (desc, ml_loc) ->
(Localise.bad_pointer_comparison,
desc, Some ml_loc, Exn_user, High, Some Kerror, Prover)
| Bad_footprint ml_loc ->
(Localise.from_string "Bad_footprint",
Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat)
| Prop.Cannot_star ml_loc ->
(Localise.from_string "Cannot_star",
Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat)
| Class_cast_exception (desc, ml_loc) ->
(Localise.class_cast_exception,
desc, Some ml_loc, Exn_user, High, None, Prover)
| Codequery desc ->
(Localise.from_string "Codequery", desc, None, Exn_user, High, None, Prover)
| Comparing_floats_for_equality(desc, mloc) ->
(Localise.comparing_floats_for_equality, desc, Some mloc, Exn_user, Medium, None, Nocat)
| Condition_always_true_false (desc, b, mloc) ->
let name = if b then Localise.condition_always_true else Localise.condition_always_false in
(name, desc, Some mloc, Exn_user, Medium, None, Nocat)
(Localise.from_string "Codequery",
desc, None, Exn_user, High, None, Prover)
| Comparing_floats_for_equality(desc, ml_loc) ->
(Localise.comparing_floats_for_equality,
desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Condition_always_true_false (desc, b, ml_loc) ->
let name =
if b then Localise.condition_always_true
else Localise.condition_always_false in
(name, desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Custom_error (error_msg, desc) ->
(Localise.from_string error_msg, desc, None, Exn_user, High, None, Checker)
| Condition_is_assignment(desc, mloc) ->
(Localise.condition_is_assignment, desc, Some mloc, Exn_user, Medium, None, Nocat)
| Dangling_pointer_dereference (dko, desc, mloc) ->
(Localise.from_string error_msg,
desc, None, Exn_user, High, None, Checker)
| Condition_is_assignment(desc, ml_loc) ->
(Localise.condition_is_assignment,
desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Dangling_pointer_dereference (dko, desc, ml_loc) ->
let visibility = match dko with
| Some dk -> Exn_user (* only show to the user if the category was identified *)
| None -> Exn_developer in
(Localise.dangling_pointer_dereference, desc, Some mloc, visibility, High, None, Prover)
(Localise.dangling_pointer_dereference,
desc, Some ml_loc, visibility, High, None, Prover)
| Deallocate_stack_variable desc ->
(Localise.deallocate_stack_variable, desc, None, Exn_user, High, None, Prover)
(Localise.deallocate_stack_variable,
desc, None, Exn_user, High, None, Prover)
| Deallocate_static_memory desc ->
(Localise.deallocate_static_memory, desc, None, Exn_user, High, None, Prover)
| Deallocation_mismatch (desc, mloc) ->
(Localise.deallocation_mismatch, desc, Some mloc, Exn_user, High, None, Prover)
| Divide_by_zero (desc, mloc) ->
(Localise.divide_by_zero, desc, Some mloc, Exn_user, High, Some Kerror, Checker)
(Localise.deallocate_static_memory,
desc, None, Exn_user, High, None, Prover)
| Deallocation_mismatch (desc, ml_loc) ->
(Localise.deallocation_mismatch,
desc, Some ml_loc, Exn_user, High, None, Prover)
| Divide_by_zero (desc, ml_loc) ->
(Localise.divide_by_zero,
desc, Some ml_loc, Exn_user, High, Some Kerror, Checker)
| Eradicate (kind_s, desc) ->
(Localise.from_string kind_s, desc, None, Exn_user, High, None, Prover)
| Field_not_null_checked (desc, mloc) ->
(Localise.field_not_null_checked, desc, Some mloc, Exn_user, Medium, Some Kwarning, Nocat)
| Frontend_warning (name, desc, mloc) ->
(Localise.from_string name, desc, Some mloc, Exn_user, Medium, Some Kwarning, Nocat)
| Field_not_null_checked (desc, ml_loc) ->
(Localise.field_not_null_checked,
desc, Some ml_loc, Exn_user, Medium, Some Kwarning, Nocat)
| Frontend_warning (name, desc, ml_loc) ->
(Localise.from_string name,
desc, Some ml_loc, Exn_user, Medium, Some Kwarning, Nocat)
| Checkers (kind_s, desc) ->
(Localise.from_string kind_s, desc, None, Exn_user, High, None, Prover)
| Null_dereference (desc, mloc) ->
(Localise.null_dereference, desc, Some mloc, Exn_user, High, None, Prover)
| Null_test_after_dereference (desc, mloc) ->
(Localise.null_test_after_dereference, desc, Some mloc, Exn_user, High, None, Nocat)
| Pointer_size_mismatch (desc, mloc) ->
(Localise.pointer_size_mismatch, desc, Some mloc, Exn_user, High, Some Kerror, Checker)
(Localise.from_string kind_s,
desc, None, Exn_user, High, None, Prover)
| Null_dereference (desc, ml_loc) ->
(Localise.null_dereference,
desc, Some ml_loc, Exn_user, High, None, Prover)
| Null_test_after_dereference (desc, ml_loc) ->
(Localise.null_test_after_dereference,
desc, Some ml_loc, Exn_user, High, None, Nocat)
| Pointer_size_mismatch (desc, ml_loc) ->
(Localise.pointer_size_mismatch,
desc, Some ml_loc, Exn_user, High, Some Kerror, Checker)
| Inherently_dangerous_function desc ->
(Localise.inherently_dangerous_function, desc, None, Exn_developer, Medium, None, Nocat)
(Localise.inherently_dangerous_function,
desc, None, Exn_developer, Medium, None, Nocat)
| Internal_error desc ->
(Localise.from_string "Internal_error", desc, None, Exn_developer, High, None, Nocat)
(Localise.from_string "Internal_error",
desc, None, Exn_developer, High, None, Nocat)
| Invalid_argument s ->
let desc = Localise.verbatim_desc s in
(Localise.from_string "Invalid_argument", desc, None, Exn_system, Low, None, Nocat)
| Java_runtime_exception (exn_name, pre_str, desc) ->
let exn_str = Typename.name exn_name in
(Localise.from_string exn_str, desc, None, Exn_user, High, None, Prover)
| Leak (fp_part, _, _, (exn_vis, error_desc), done_array_abstraction, resource, mloc) ->
| Leak (fp_part, _, _, (exn_vis, error_desc), done_array_abstraction, resource, ml_loc) ->
if done_array_abstraction
then (Localise.from_string "Leak_after_array_abstraction", error_desc, Some mloc, Exn_developer, High, None, Prover)
then (Localise.from_string "Leak_after_array_abstraction",
error_desc, Some ml_loc, Exn_developer, High, None, Prover)
else if fp_part
then (Localise.from_string "Leak_in_footprint", error_desc, Some mloc, Exn_developer, High, None, Prover)
then (Localise.from_string "Leak_in_footprint",
error_desc, Some ml_loc, Exn_developer, High, None, Prover)
else
let loc_str = match resource with
| Sil.Rmemory _ -> Localise.memory_leak
| Sil.Rfile -> Localise.resource_leak
| Sil.Rlock -> Localise.resource_leak
| Sil.Rignore -> Localise.memory_leak in
(loc_str, error_desc, Some mloc, exn_vis, High, None, Prover)
| Match_failure mloc ->
(Localise.from_string "Match failure", Localise.no_desc, Some mloc, Exn_developer, High, None, Nocat)
| Missing_fld (fld, mloc) ->
(loc_str, error_desc, Some ml_loc, exn_vis, High, None, Prover)
| Match_failure (f, l, c) ->
let ml_loc = (f, l, c, c) in
(Localise.from_string "Match failure",
Localise.no_desc, Some ml_loc, Exn_developer, High, None, Nocat)
| Missing_fld (fld, ml_loc) ->
let desc = Localise.verbatim_desc (Ident.fieldname_to_string fld) in
(Localise.from_string "Missing_fld", desc, Some mloc, Exn_developer, Medium, None, Nocat)
| Premature_nil_termination (desc, mloc) ->
(Localise.premature_nil_termination, desc, Some mloc, Exn_user, High, None, Prover)
(Localise.from_string "Missing_fld", desc, Some ml_loc, Exn_developer, Medium, None, Nocat)
| Premature_nil_termination (desc, ml_loc) ->
(Localise.premature_nil_termination,
desc, Some ml_loc, Exn_user, High, None, Prover)
| Not_found ->
(Localise.from_string "Not_found", Localise.no_desc, None, Exn_system, Low, None, Nocat)
| Parameter_not_null_checked (desc, mloc) ->
(Localise.parameter_not_null_checked, desc, Some mloc, Exn_user, Medium, Some Kwarning, Nocat)
| Precondition_not_found (desc, mloc) ->
(Localise.precondition_not_found, desc, Some mloc, Exn_developer, Low, None, Nocat)
| Precondition_not_met (desc, mloc) ->
(Localise.precondition_not_met, desc, Some mloc, Exn_user, Medium, Some Kwarning, Nocat) (** always a warning *)
| Retain_cycle (prop, hpred, desc, mloc) ->
(Localise.retain_cycle, desc, Some mloc, Exn_user, High, None, Prover)
| Return_expression_required (desc, mloc) ->
(Localise.return_expression_required, desc, Some mloc, Exn_user, Medium, None, Nocat)
| Stack_variable_address_escape (desc, mloc) ->
(Localise.stack_variable_address_escape, desc, Some mloc, Exn_user, High, Some Kerror, Nocat)
| Return_statement_missing (desc, mloc) ->
(Localise.return_statement_missing, desc, Some mloc, Exn_user, Medium, None, Nocat)
| Return_value_ignored (desc, mloc) ->
(Localise.return_value_ignored, desc, Some mloc, Exn_user, Medium, None, Nocat)
(Localise.from_string "Not_found",
Localise.no_desc, None, Exn_system, Low, None, Nocat)
| Parameter_not_null_checked (desc, ml_loc) ->
(Localise.parameter_not_null_checked,
desc, Some ml_loc, Exn_user, Medium, Some Kwarning, Nocat)
| Precondition_not_found (desc, ml_loc) ->
(Localise.precondition_not_found,
desc, Some ml_loc, Exn_developer, Low, None, Nocat)
| Precondition_not_met (desc, ml_loc) ->
(Localise.precondition_not_met,
desc, Some ml_loc, Exn_user, Medium, Some Kwarning, Nocat) (** always a warning *)
| Retain_cycle (prop, hpred, desc, ml_loc) ->
(Localise.retain_cycle,
desc, Some ml_loc, Exn_user, High, None, Prover)
| Return_expression_required (desc, ml_loc) ->
(Localise.return_expression_required,
desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Stack_variable_address_escape (desc, ml_loc) ->
(Localise.stack_variable_address_escape,
desc, Some ml_loc, Exn_user, High, Some Kerror, Nocat)
| Return_statement_missing (desc, ml_loc) ->
(Localise.return_statement_missing,
desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Return_value_ignored (desc, ml_loc) ->
(Localise.return_value_ignored,
desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Analysis_failure_exe _ ->
(Localise.from_string "Failure_exe", Localise.no_desc, None, Exn_system, Low, None, Nocat)
(Localise.from_string "Failure_exe",
Localise.no_desc, None, Exn_system, Low, None, Nocat)
| Skip_function desc ->
(Localise.skip_function, desc, None, Exn_developer, Low, None, Nocat)
| Skip_pointer_dereference (desc, mloc) ->
(Localise.skip_pointer_dereference, desc, Some mloc, Exn_user, Medium, Some Kinfo, Nocat) (** always an info *)
| Symexec_memory_error mloc ->
(Localise.from_string "Symexec_memory_error", Localise.no_desc, Some mloc, Exn_developer, Low, None, Nocat)
| Skip_pointer_dereference (desc, ml_loc) ->
(Localise.skip_pointer_dereference,
desc, Some ml_loc, Exn_user, Medium, Some Kinfo, Nocat) (** always an info *)
| Symexec_memory_error ml_loc ->
(Localise.from_string "Symexec_memory_error",
Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat)
| Sys_error s ->
let desc = Localise.verbatim_desc s in
(Localise.from_string "Sys_error", desc, None, Exn_system, Low, None, Nocat)
| Tainted_value_reaching_sensitive_function (desc, mloc) ->
(Localise.tainted_value_reaching_sensitive_function, desc, Some mloc,
Exn_user, Medium, Some Kerror, Nocat)
(Localise.from_string "Sys_error",
desc, None, Exn_system, Low, None, Nocat)
| Tainted_value_reaching_sensitive_function (desc, ml_loc) ->
(Localise.tainted_value_reaching_sensitive_function,
desc, Some ml_loc, Exn_user, Medium, Some Kerror, Nocat)
| Unix.Unix_error (_, s1, s2) ->
let desc = Localise.verbatim_desc (s1 ^ s2) in
(Localise.from_string "Unix_error", desc, None, Exn_system, Low, None, Nocat)
| Uninitialized_value (desc, mloc) ->
(Localise.uninitialized_value, desc, Some mloc, Exn_user, Medium, None, Nocat)
| Unary_minus_applied_to_unsigned_expression(desc, mloc) ->
(Localise.unary_minus_applied_to_unsigned_expression, desc, Some mloc, Exn_user, Medium, None, Nocat)
(Localise.from_string "Unix_error",
desc, None, Exn_system, Low, None, Nocat)
| Uninitialized_value (desc, ml_loc) ->
(Localise.uninitialized_value,
desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Unary_minus_applied_to_unsigned_expression(desc, ml_loc) ->
(Localise.unary_minus_applied_to_unsigned_expression,
desc, Some ml_loc, Exn_user, Medium, None, Nocat)
| Unknown_proc ->
(Localise.from_string "Unknown_proc", Localise.no_desc, None, Exn_developer, Low, None, Nocat)
| Use_after_free (desc, mloc) ->
(Localise.use_after_free, desc, Some mloc, Exn_user, High, None, Prover)
| Wrong_argument_number mloc ->
(Localise.from_string "Wrong_argument_number", Localise.no_desc, Some mloc, Exn_developer, Low, None, Nocat)
(Localise.from_string "Unknown_proc",
Localise.no_desc, None, Exn_developer, Low, None, Nocat)
| Use_after_free (desc, ml_loc) ->
(Localise.use_after_free,
desc, Some ml_loc, Exn_user, High, None, Prover)
| Wrong_argument_number ml_loc ->
(Localise.from_string "Wrong_argument_number",
Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat)
| Failure _ as f ->
raise f
| exn ->
let exn_name = Printexc.to_string exn in
(Localise.from_string exn_name, Localise.no_desc, None, Exn_developer, Low, None, Nocat) in
(Localise.from_string exn_name,
Localise.no_desc, None, Exn_developer, Low, None, Nocat) in
let visibility' =
if visibility = Exn_user && filter_out_bucket desc then Exn_developer else visibility in
(err_name, desc, mloco, visibility', severity, force_kind, eclass)
if visibility = Exn_user && filter_out_bucket desc
then Exn_developer
else visibility in
(err_name, desc, ml_loc_opt, visibility', severity, force_kind, eclass)
(** print a description of the exception to the html output *)
let print_exception_html s exn =
let err_name, desc, mloco, _, _, _, _ = recognize_exception exn in
let mloc_string = match mloco with
let err_name, desc, ml_loc_opt, _, _, _, _ = recognize_exception exn in
let ml_loc_string = match ml_loc_opt with
| None -> ""
| Some mloc -> " " ^ ml_location_string mloc in
| Some ml_loc -> " " ^ ml_loc_to_string ml_loc in
let desc_str = pp_to_string Localise.pp_error_desc desc in
(L.d_strln_color Red) (s ^ (Localise.to_string err_name) ^ " " ^ desc_str ^ mloc_string)
(L.d_strln_color Red) (s ^ (Localise.to_string err_name) ^ " " ^ desc_str ^ ml_loc_string)
(** string describing an error kind *)
let err_kind_string = function
@ -259,7 +324,7 @@ let err_class_string = function
let print_key = false
(** pretty print an error given its (id,key), location, kind, name, description, and optional ml location *)
let pp_err (node_id, node_key) loc ekind ex_name desc mloco fmt () =
let pp_err (node_id, node_key) loc ekind ex_name desc ml_loc_opt fmt () =
let kind = err_kind_string (if ekind = Kinfo then Kwarning else ekind) (* eclipse does not know about infos: treat as warning *) in
let pp_key fmt k = if print_key then F.fprintf fmt " key: %d " k else () in
F.fprintf fmt "%s:%d: %s: %a %a%a%a@\n"
@ -269,7 +334,7 @@ let pp_err (node_id, node_key) loc ekind ex_name desc mloco fmt () =
Localise.pp ex_name
Localise.pp_error_desc desc
pp_key node_key
pp_ml_location_opt mloco
pp_ml_loc_opt ml_loc_opt
(** Return true if the exception is not serious and should be handled in timeout mode *)
let handle_exception exn =

84
infer/src/backend/exceptions.mli
Unescape View File

@ -29,56 +29,58 @@ type err_kind =
(** class of error *)
type err_class = Checker | Prover | Nocat
exception Abduction_case_not_implemented of ml_location
exception Analysis_stops of Localise.error_desc * ml_location option
exception Array_of_pointsto of ml_location
exception Array_out_of_bounds_l1 of Localise.error_desc * ml_location
exception Array_out_of_bounds_l2 of Localise.error_desc * ml_location
exception Array_out_of_bounds_l3 of Localise.error_desc * ml_location
exception Bad_footprint of ml_location
exception Bad_pointer_comparison of Localise.error_desc * ml_location
exception Class_cast_exception of Localise.error_desc * ml_location
exception Abduction_case_not_implemented of ml_loc
exception Analysis_stops of Localise.error_desc * ml_loc option
exception Array_of_pointsto of ml_loc
exception Array_out_of_bounds_l1 of Localise.error_desc * ml_loc
exception Array_out_of_bounds_l2 of Localise.error_desc * ml_loc
exception Array_out_of_bounds_l3 of Localise.error_desc * ml_loc
exception Bad_footprint of ml_loc
exception Bad_pointer_comparison of Localise.error_desc * ml_loc
exception Class_cast_exception of Localise.error_desc * ml_loc
exception Codequery of Localise.error_desc
exception Comparing_floats_for_equality of Localise.error_desc * ml_location
exception Condition_always_true_false of Localise.error_desc * bool * ml_location
exception Condition_is_assignment of Localise.error_desc * ml_location
exception Context_leak of Localise.error_desc * ml_location
exception Comparing_floats_for_equality of Localise.error_desc * ml_loc
exception Condition_always_true_false of Localise.error_desc * bool * ml_loc
exception Condition_is_assignment of Localise.error_desc * ml_loc
exception Context_leak of Localise.error_desc * ml_loc
exception Custom_error of string * Localise.error_desc
exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * ml_location
exception Dangling_pointer_dereference of Sil.dangling_kind option * Localise.error_desc * ml_loc
exception Deallocate_stack_variable of Localise.error_desc
exception Deallocate_static_memory of Localise.error_desc
exception Deallocation_mismatch of Localise.error_desc * ml_location
exception Divide_by_zero of Localise.error_desc * ml_location
exception Field_not_null_checked of Localise.error_desc * ml_location
exception Deallocation_mismatch of Localise.error_desc * ml_loc
exception Divide_by_zero of Localise.error_desc * ml_loc
exception Field_not_null_checked of Localise.error_desc * ml_loc
exception Eradicate of string * Localise.error_desc
exception Checkers of string * Localise.error_desc
exception Frontend_warning of string * Localise.error_desc * ml_location
exception Frontend_warning of string * Localise.error_desc * ml_loc
exception Inherently_dangerous_function of Localise.error_desc
exception Internal_error of Localise.error_desc
exception Java_runtime_exception of Typename.t * string * Localise.error_desc
exception Leak of bool * Prop.normal Prop.t * Sil.hpred * (exception_visibility * Localise.error_desc) * bool * Sil.resource * ml_location
exception Missing_fld of Ident.fieldname * ml_location
exception Premature_nil_termination of Localise.error_desc * ml_location
exception Null_dereference of Localise.error_desc * ml_location
exception Null_test_after_dereference of Localise.error_desc * ml_location
exception Parameter_not_null_checked of Localise.error_desc * ml_location
exception Pointer_size_mismatch of Localise.error_desc * ml_location
exception Precondition_not_found of Localise.error_desc * ml_location
exception Precondition_not_met of Localise.error_desc * ml_location
exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * ml_location
exception Return_expression_required of Localise.error_desc * ml_location
exception Return_statement_missing of Localise.error_desc * ml_location
exception Return_value_ignored of Localise.error_desc * ml_location
exception Leak of
bool * Prop.normal Prop.t * Sil.hpred * (exception_visibility * Localise.error_desc)
* bool * Sil.resource * ml_loc
exception Missing_fld of Ident.fieldname * ml_loc
exception Premature_nil_termination of Localise.error_desc * ml_loc
exception Null_dereference of Localise.error_desc * ml_loc
exception Null_test_after_dereference of Localise.error_desc * ml_loc
exception Parameter_not_null_checked of Localise.error_desc * ml_loc
exception Pointer_size_mismatch of Localise.error_desc * ml_loc
exception Precondition_not_found of Localise.error_desc * ml_loc
exception Precondition_not_met of Localise.error_desc * ml_loc
exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * ml_loc
exception Return_expression_required of Localise.error_desc * ml_loc
exception Return_statement_missing of Localise.error_desc * ml_loc
exception Return_value_ignored of Localise.error_desc * ml_loc
exception Skip_function of Localise.error_desc
exception Skip_pointer_dereference of Localise.error_desc * ml_location
exception Stack_variable_address_escape of Localise.error_desc * ml_location
exception Symexec_memory_error of ml_location
exception Tainted_value_reaching_sensitive_function of Localise.error_desc * ml_location
exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * ml_location
exception Uninitialized_value of Localise.error_desc * ml_location
exception Skip_pointer_dereference of Localise.error_desc * ml_loc
exception Stack_variable_address_escape of Localise.error_desc * ml_loc
exception Symexec_memory_error of ml_loc
exception Tainted_value_reaching_sensitive_function of Localise.error_desc * ml_loc
exception Unary_minus_applied_to_unsigned_expression of Localise.error_desc * ml_loc
exception Uninitialized_value of Localise.error_desc * ml_loc
exception Unknown_proc
exception Use_after_free of Localise.error_desc * ml_location
exception Wrong_argument_number of ml_location
exception Use_after_free of Localise.error_desc * ml_loc
exception Wrong_argument_number of ml_loc
(** string describing an error class *)
val err_class_string : err_class -> string
@ -94,10 +96,10 @@ val print_exception_html : string -> exn -> unit
(** pretty print an error given its (id,key), location, kind, name, description, and optional ml location *)
val pp_err : int * int -> Location.t -> err_kind -> Localise.t -> Localise.error_desc ->
Utils.ml_location option -> Format.formatter -> unit -> unit
Utils.ml_loc option -> Format.formatter -> unit -> unit
(** Turn an exception into an error name, error description,
location in ml source, and category *)
val recognize_exception : exn ->
(Localise.t * Localise.error_desc * (ml_location option) * exception_visibility *
(Localise.t * Localise.error_desc * (ml_loc option) * exception_visibility *
exception_severity * err_kind option * err_class)

2
infer/src/backend/fork.ml
Unescape View File

@ -431,7 +431,7 @@ let interprocedural_algorithm
(* wrap _process_result and handle exceptions *)
try _process_result exe_env (pname, calls) summary with
| exn ->
let err_name, _, mloco, _, _, _, _ = Exceptions.recognize_exception exn in
let err_name, _, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in
let err_str = "process_result raised " ^ (Localise.to_string err_name) in
L.err "Error: %s@." err_str;
let exn' = Exceptions.Internal_error (Localise.verbatim_desc err_str) in

8
infer/src/backend/inferprint.ml
Unescape View File

@ -590,9 +590,9 @@ module BugsJson = struct
let procedure_id = Procname.to_filename (Specs.get_proc_name summary) in
let file =
DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file in
let json_mloc = match ml_loc_opt with
| Some (file, line, column) when !reports_include_ml_loc ->
Some Jsonbug_j.{ file; line; column }
let json_ml_loc = match ml_loc_opt with
| Some (file, lnum, cnum, enum) when !reports_include_ml_loc ->
Some Jsonbug_j.{ file; lnum; cnum; enum; }
| _ -> None in
let bug = {
bug_class = Exceptions.err_class_string eclass;
@ -609,7 +609,7 @@ module BugsJson = struct
qualifier_tags = error_desc_to_qualifier_tags_records error_desc;
hash = get_bug_hash kind bug_type procedure_id file node_key error_desc;
dotty = error_desc_to_dotty_string error_desc;
infer_source_loc = json_mloc;
infer_source_loc = json_ml_loc;
} in
if not !is_first_item then pp "," else is_first_item := false;
pp "%s@?" (string_of_jsonbug bug) in

11
infer/src/backend/interproc.ml
Unescape View File

@ -439,7 +439,7 @@ let check_assignement_guard node =
| [Sil.Set(e, _, _, _)] -> (* we now check if e is the same expression used to prune*)
if (is_prune_exp e) && not ((node_contains_call node) && (is_cil_tmp e)) && not (is_edg_tmp e) then (
let desc = Errdesc.explain_condition_is_assignment l_node in
let exn = Exceptions.Condition_is_assignment (desc, try assert false with Assert_failure x -> x) in
let exn = Exceptions.Condition_is_assignment (desc, __POS__) in
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
Reporting.log_warning pname ~loc: (Some l_node) ~pre: pre_opt exn
)
@ -601,8 +601,7 @@ let report_context_leaks pname sigma tenv =
| Some path -> path
| None -> assert false in (* a path must exist in order for a leak to be reported *)
let err_desc = Errdesc.explain_context_leak pname typ fld_name leak_path in
let exn = Exceptions.Context_leak
(err_desc, try assert false with Assert_failure x -> x) in
let exn = Exceptions.Context_leak (err_desc, __POS__) in
Reporting.log_error pname exn)
context_exps in
(* get the set of pointed-to expressions of type T <: Context *)
@ -634,7 +633,7 @@ let remove_locals_formals_and_check pdesc p =
let loc = Cfg.Node.get_loc (Cfg.Procdesc.get_exit_node pdesc) in
let dexp_opt, _ = Errdesc.vpath_find p (Sil.Lvar pvar) in
let desc = Errdesc.explain_stack_variable_address_escape loc pvar dexp_opt in
let exn = Exceptions.Stack_variable_address_escape (desc, try assert false with Assert_failure x -> x) in
let exn = Exceptions.Stack_variable_address_escape (desc, __POS__) in
Reporting.log_warning pname exn in
IList.iter check_pvar pvars;
p'
@ -1162,9 +1161,9 @@ let perform_transition exe_env cg proc_name =
apply_start_node do_after_node;
Config.allowleak := allowleak;
L.err "Error in collect_preconditions for %a@." Procname.pp proc_name;
let err_name, _, mloco, _, _, _, _ = Exceptions.recognize_exception exn in
let err_name, _, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in
let err_str = "exception raised " ^ (Localise.to_string err_name) in
L.err "Error: %s %a@." err_str pp_ml_location_opt mloco;
L.err "Error: %s %a@." err_str pp_ml_loc_opt ml_loc_opt;
[] in
Fork.transition_footprint_re_exe pname joined_pres in
IList.iter transition proc_names

5
infer/src/backend/jsonbug.atd
Unescape View File

@ -13,8 +13,9 @@ type json_trace_item = {
type loc = {
file: string;
line: int;
column: int;
lnum: int;
cnum: int;
enum: int;
}
type jsonbug = {

4
infer/src/backend/logging.ml
Unescape View File

@ -133,8 +133,8 @@ let stdout fmt_string =
(** print a warning with information of the position in the ml source where it oririnated.
use as: warning_position "description" (try assert false with Assert_failure x -> x); *)
let warning_position (s: string) (mloc: ml_location) =
err "WARNING: %s in %a@." s pp_ml_location_opt (Some mloc)
let warning_position (s: string) (ml_loc: ml_loc) =
err "WARNING: %s in %a@." s pp_ml_loc_opt (Some ml_loc)
(** dump a string *)
let d_str (s: string) = add_print_action (PTstr, Obj.repr s)

2
infer/src/backend/logging.mli
Unescape View File

@ -97,7 +97,7 @@ val flush_streams : unit -> unit
(** print a warning with information of the position in the ml source where it oririnated.
use as: warning_position "description" (try assert false with Assert_failure x -> x); *)
val warning_position: string -> ml_location -> unit
val warning_position: string -> ml_loc -> unit
(** dump a string *)
val d_str : string -> unit

2
infer/src/backend/prop.ml
Unescape View File

@ -46,7 +46,7 @@ type 'a t =
foot_pi: Sil.atom list; (** abduced pure part *)
}
exception Cannot_star of ml_location
exception Cannot_star of ml_loc
(** Pure proposition. *)
type pure_prop = Sil.subst * Sil.atom list

2
infer/src/backend/prop.mli
Unescape View File

@ -26,7 +26,7 @@ type struct_init_mode =
| No_init
| Fld_init
exception Cannot_star of ml_location
exception Cannot_star of ml_loc
(** {2 Basic Functions for propositions} *)

18
infer/src/backend/prover.ml
Unescape View File

@ -1165,7 +1165,7 @@ let exp_imply calc_missing subs e1_in e2_in : subst2 =
do_imply (do_imply subs e1 e2) f1 f2
| _ ->
d_impl_err ("exp_imply not implemented", subs, (EXC_FALSE_EXPS (e1, e2)));
raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x)) in
raise (Exceptions.Abduction_case_not_implemented __POS__) in
do_imply subs e1 e2
(** Convert a path (from lhs of a |-> to a field name present only in
@ -1237,7 +1237,7 @@ let rec sexp_imply source calc_index_frame calc_missing subs se1 se2 typ2 : subs
(fst subs, sub2'), None, None
| _ ->
d_impl_err ("sexp_imply not implemented", subs, (EXC_FALSE_SEXPS (se1, se2)));
raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x))
raise (Exceptions.Abduction_case_not_implemented __POS__)
end
| Sil.Earray (size1, esel1, inst1), Sil.Earray (size2, esel2, _) ->
let indices2 = IList.map fst esel2 in
@ -1265,7 +1265,7 @@ let rec sexp_imply source calc_index_frame calc_missing subs se1 se2 typ2 : subs
sexp_imply source true calc_missing subs se1 se2' typ2' (* calculate index_frame because the rhs is a singleton array *)
| _ ->
d_impl_err ("sexp_imply not implemented", subs, (EXC_FALSE_SEXPS (se1, se2)));
raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x))
raise (Exceptions.Abduction_case_not_implemented __POS__)
and struct_imply source calc_missing subs fsel1 fsel2 typ2 : subst2 * ((Ident.fieldname * Sil.strexp) list) * ((Ident.fieldname * Sil.strexp) list) =
match fsel1, fsel2 with
@ -1727,7 +1727,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
| Sil.Lvar p -> ()
| Sil.Var v -> if Ident.is_primed v then
(d_impl_err ("rhs |-> not implemented", subs, (EXC_FALSE_HPRED hpred2));
raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x)))
raise (Exceptions.Abduction_case_not_implemented __POS__))
| _ -> () in
(match Prop.prop_iter_create prop1 with
| None -> raise (IMPL_EXC ("lhs is empty", subs, EXC_FALSE))
@ -1812,7 +1812,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
| Sil.Lvar p -> ()
| Sil.Var v -> if Ident.is_primed v then
(d_impl_err ("rhs |-> not implemented", subs, (EXC_FALSE_HPRED hpred2));
raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x)))
raise (Exceptions.Abduction_case_not_implemented __POS__))
| _ -> ()
in
if Sil.exp_equal e2 f2 && k == Sil.Lseg_PE then (subs, prop1)
@ -1863,7 +1863,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
)
| Sil.Hdllseg (Sil.Lseg_PE, _, _, _, _, _, _) ->
(d_impl_err ("rhs dllsegPE not implemented", subs, (EXC_FALSE_HPRED hpred2));
raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x)))
raise (Exceptions.Abduction_case_not_implemented __POS__))
| Sil.Hdllseg (k, para2, iF2, oB2, oF2, iB2, elist2) -> (* for now ignore implications between PE and NE *)
let iF2, oF2 = Sil.exp_sub (snd subs) iF2, Sil.exp_sub (snd subs) oF2 in
let iB2, oB2 = Sil.exp_sub (snd subs) iB2, Sil.exp_sub (snd subs) oB2 in
@ -1871,14 +1871,14 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
| Sil.Lvar p -> ()
| Sil.Var v -> if Ident.is_primed v then
(d_impl_err ("rhs dllseg not implemented", subs, (EXC_FALSE_HPRED hpred2));
raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x)))
raise (Exceptions.Abduction_case_not_implemented __POS__))
| _ -> ()
in
let _ = match oB2 with
| Sil.Lvar p -> ()
| Sil.Var v -> if Ident.is_primed v then
(d_impl_err ("rhs dllseg not implemented", subs, (EXC_FALSE_HPRED hpred2));
raise (Exceptions.Abduction_case_not_implemented (try assert false with Assert_failure x -> x)))
raise (Exceptions.Abduction_case_not_implemented __POS__))
| _ -> ()
in
(match Prop.prop_iter_create prop1 with
@ -2144,7 +2144,7 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2
| MISSING_EXC s ->
L.d_strln ("WARNING: footprint failed to find MISSING because: " ^ s);
None
| (Exceptions.Abduction_case_not_implemented mloc as exn) ->
| (Exceptions.Abduction_case_not_implemented _ as exn) ->
Reporting.log_error pname exn;
None

55
infer/src/backend/rearrange.ml
Unescape View File

@ -65,15 +65,17 @@ let check_bad_index pname tenv p size index loc =
let index_const_opt = get_const_opt index in
if index_provably_out_of_bound () then
let deref_str = Localise.deref_str_array_bound size_const_opt index_const_opt in
let exn = Exceptions.Array_out_of_bounds_l1 (Errdesc.explain_array_access deref_str p loc, try assert false with Assert_failure x -> x) in
let exn =
Exceptions.Array_out_of_bounds_l1
(Errdesc.explain_array_access deref_str p loc, __POS__) in
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
Reporting.log_warning pname ~pre: pre_opt exn
else if size_is_constant then
let deref_str = Localise.deref_str_array_bound size_const_opt index_const_opt in
let desc = Errdesc.explain_array_access deref_str p loc in
let exn = if index_has_bounds ()
then Exceptions.Array_out_of_bounds_l2 (desc, try assert false with Assert_failure x -> x)
else Exceptions.Array_out_of_bounds_l3 (desc, try assert false with Assert_failure x -> x) in
then Exceptions.Array_out_of_bounds_l2 (desc, __POS__)
else Exceptions.Array_out_of_bounds_l3 (desc, __POS__) in
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
Reporting.log_warning pname ~pre: pre_opt exn
end
@ -111,7 +113,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
IList.find (fun (f', _, _) -> Ident.fieldname_equal f f')
(instance_fields @ static_fields)
with Not_found ->
raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x)) in
raise (Exceptions.Bad_footprint __POS__) in
let atoms', se', res_t' =
create_struct_values
pname tenv orig_prop footprint_part kind max_stamp t' off' inst in
@ -165,7 +167,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
(Sil.Aeq(e, e'):: atoms', se, res_t)
| Sil.Tint _, _ | Sil.Tfloat _, _ | Sil.Tvoid, _ | Sil.Tfun _, _ | Sil.Tptr _, _ ->
L.d_str "create_struct_values type:"; Sil.d_typ_full t; L.d_str " off: "; Sil.d_offset_list off; L.d_ln();
raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x))
raise (Exceptions.Bad_footprint __POS__)
| Sil.Tvar _, _ | Sil.Tenum _, _ ->
L.d_str "create_struct_values type:"; Sil.d_typ_full t; L.d_str " off: "; Sil.d_offset_list off; L.d_ln();
@ -209,7 +211,7 @@ let rec _strexp_extend_values
IList.find (fun (f', t', a') -> Ident.fieldname_equal f f')
(instance_fields @ static_fields)
with Not_found ->
raise (Exceptions.Missing_fld (f, try assert false with Assert_failure x -> x)) in
raise (Exceptions.Missing_fld (f, __POS__)) in
begin
try
let _, se' = IList.find (fun (f', _) -> Ident.fieldname_equal f f') fsel in
@ -238,7 +240,7 @@ let rec _strexp_extend_values
[(atoms', Sil.Estruct (res_fsel', inst'), struct_typ)]
end
| (Sil.Off_fld (f, _)):: off', _, _ ->
raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x))
raise (Exceptions.Bad_footprint __POS__)
| (Sil.Off_index _):: _, Sil.Eexp _, Sil.Tint _
| (Sil.Off_index _):: _, Sil.Eexp _, Sil.Tfloat _
@ -270,7 +272,7 @@ let rec _strexp_extend_values
let res_esel' = IList.map replace_ise esel in
if (Sil.typ_equal res_typ' typ') || (IList.length res_esel' = 1)
then (res_atoms', Sil.Earray(size, res_esel', inst_arr), Sil.Tarray(res_typ', size_for_typ')) :: acc
else raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x)) in
else raise (Exceptions.Bad_footprint __POS__) in
IList.fold_left replace [] atoms_se_typ_list'
with Not_found ->
array_case_analysis_index pname tenv orig_prop
@ -280,7 +282,7 @@ let rec _strexp_extend_values
e off' inst_arr inst
end
| _, _, _ ->
raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x))
raise (Exceptions.Bad_footprint __POS__)
and array_case_analysis_index pname tenv orig_prop
footprint_part kind max_stamp
@ -290,7 +292,7 @@ and array_case_analysis_index pname tenv orig_prop
=
let check_sound t' =
if not (Sil.typ_equal typ_cont t' || array_cont == [])
then raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x)) in
then raise (Exceptions.Bad_footprint __POS__) in
let index_in_array =
IList.exists (fun (i, _) -> Prover.check_equal Prop.prop_emp index i) array_cont in
let array_is_full =
@ -421,7 +423,7 @@ let mk_ptsto_exp_footprint
Errdesc.explain_dereference deref_str orig_prop (State.get_loc ()) in
raise
(Exceptions.Dangling_pointer_dereference
(None, err_desc, try assert false with Assert_failure x -> x))
(None, err_desc, __POS__))
end
end;
let off_foot, eqs = laundry_offset_for_footprint max_stamp off in
@ -636,7 +638,7 @@ let rearrange_arith lexp prop =
if Prover.check_allocatedness prop root then
raise ARRAY_ACCESS
else
raise (Exceptions.Symexec_memory_error (try assert false with Assert_failure x -> x))
raise (Exceptions.Symexec_memory_error __POS__)
let pp_rearrangement_error message prop lexp =
L.d_strln (".... Rearrangement Error .... " ^ message);
@ -661,7 +663,7 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst =
| Some fld ->
begin
pp_rearrangement_error "field splitting check failed" orig_prop lexp;
raise (Exceptions.Missing_fld (fld, try assert false with Assert_failure x -> x))
raise (Exceptions.Missing_fld (fld, __POS__))
end in
let res =
if !Config.footprint
@ -836,8 +838,7 @@ let check_type_size pname prop texp off typ_from_instr =
let loc = State.get_loc () in
let exn =
Exceptions.Pointer_size_mismatch (
Errdesc.explain_dereference deref_str prop loc,
try assert false with Assert_failure x -> x) in
Errdesc.explain_dereference deref_str prop loc, __POS__) in
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
Reporting.log_warning pname ~pre: pre_opt exn
end
@ -888,7 +889,7 @@ let rec iter_rearrange
else begin
pp_rearrangement_error "cannot find predicate with root" prop lexp;
if not !Config.footprint then Printer.force_delayed_prints ();
raise (Exceptions.Symexec_memory_error (try assert false with Assert_failure x -> x))
raise (Exceptions.Symexec_memory_error __POS__)
end in
let recurse_on_iters iters =
let f_one_iter iter' =
@ -1013,31 +1014,31 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
Errdesc.explain_dereference ~use_buckets: true ~is_nullable: is_deref_of_nullable
deref_str prop loc in
if Localise.is_parameter_not_null_checked_desc err_desc then
raise (Exceptions.Parameter_not_null_checked (err_desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Parameter_not_null_checked (err_desc, __POS__))
else if Localise.is_field_not_null_checked_desc err_desc then
raise (Exceptions.Field_not_null_checked (err_desc, try assert false with Assert_failure x -> x))
else raise (Exceptions.Null_dereference (err_desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Field_not_null_checked (err_desc, __POS__))
else raise (Exceptions.Null_dereference (err_desc, __POS__))
end;
match attribute_opt with
| Some (Sil.Adangling dk) ->
let deref_str = Localise.deref_str_dangling (Some dk) in
let err_desc = Errdesc.explain_dereference deref_str prop (State.get_loc ()) in
raise (Exceptions.Dangling_pointer_dereference (Some dk, err_desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Dangling_pointer_dereference (Some dk, err_desc, __POS__))
| Some (Sil.Aundef (s, undef_loc, _)) ->
if !Config.angelic_execution then ()
else
let deref_str = Localise.deref_str_undef (s, undef_loc) in
let err_desc = Errdesc.explain_dereference deref_str prop loc in
raise (Exceptions.Skip_pointer_dereference (err_desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Skip_pointer_dereference (err_desc, __POS__))
| Some (Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease } as ra)) ->
let deref_str = Localise.deref_str_freed ra in
let err_desc = Errdesc.explain_dereference ~use_buckets: true deref_str prop loc in
raise (Exceptions.Use_after_free (err_desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Use_after_free (err_desc, __POS__))
| _ ->
if Prover.check_equal Prop.prop_emp (Sil.root_of_lexp root) Sil.exp_minus_one then
let deref_str = Localise.deref_str_dangling None in
let err_desc = Errdesc.explain_dereference deref_str prop loc in
raise (Exceptions.Dangling_pointer_dereference (None, err_desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Dangling_pointer_dereference (None, err_desc, __POS__))
(* Check that an expression representin an objc block can be null and raise a [B1] null exception.*)
(* It's used to check that we don't call possibly null blocks *)
@ -1087,11 +1088,11 @@ let check_call_to_objc_block_error pdesc prop fun_exp loc =
if is_field_deref then
raise
(Exceptions.Field_not_null_checked
(err_desc, try assert false with Assert_failure x -> x))
(err_desc, __POS__))
else
raise
(Exceptions.Parameter_not_null_checked
(err_desc, try assert false with Assert_failure x -> x))
(err_desc, __POS__))
| _ ->
(* HP: fun_exp is not a footprint therefore,
either is a local or it's a modified param *)
@ -1099,7 +1100,7 @@ let check_call_to_objc_block_error pdesc prop fun_exp loc =
Localise.error_desc_set_bucket
err_desc_nobuckets Localise.BucketLevel.b1 !Config.show_buckets in
raise (Exceptions.Null_dereference
(err_desc, try assert false with Assert_failure x -> x))
(err_desc, __POS__))
end
(** [rearrange lexp prop] rearranges [prop] into the form [prop' * lexp|->strexp:typ].
@ -1127,6 +1128,6 @@ let rearrange ?(report_deref_errors=true) pdesc tenv lexp typ prop loc
else
begin
pp_rearrangement_error "sigma is empty" prop nlexp;
raise (Exceptions.Symexec_memory_error (try assert false with Assert_failure x -> x))
raise (Exceptions.Symexec_memory_error __POS__)
end
| Some iter -> iter_rearrange pname tenv nlexp typ prop iter inst

4
infer/src/backend/state.ml
Unescape View File

@ -330,9 +330,9 @@ let process_execution_failures (log_issue : log_issue) pname =
(* L.err "Node:%a node_ok:%d node_fail:%d@." Cfg.Node.pp node fs.node_ok fs.node_fail; *)
match fs.node_ok, fs.first_failure with
| 0, Some (loc, key, session, loc_trace, pre_opt, exn) ->
let ex_name, desc, mloco, _, _, _, _ = Exceptions.recognize_exception exn in
let ex_name, desc, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in
let desc' = Localise.verbatim_desc ("exception: " ^ Localise.to_string ex_name) in
let exn' = Exceptions.Analysis_stops (desc', mloco) in
let exn' = Exceptions.Analysis_stops (desc', ml_loc_opt) in
log_issue
pname ~loc: (Some loc) ~node_id: (Some key) ~ltr: (Some loc_trace) ~pre: pre_opt exn'
| _ -> () in

113
infer/src/backend/symExec.ml
Unescape View File

@ -49,7 +49,7 @@ let rec unroll_type tenv typ off =
L.d_strln ".... Invalid Field Access ....";
L.d_strln ("Fld : " ^ Ident.fieldname_to_string fld);
L.d_str "Type : "; Sil.d_typ_full typ; L.d_ln ();
raise (Exceptions.Bad_footprint (try assert false with Assert_failure x -> x))
raise (Exceptions.Bad_footprint __POS__)
end
| Sil.Tarray (typ', _), Sil.Off_index _ ->
typ'
@ -125,7 +125,7 @@ let rec apply_offlist
else Prop.get_undef_attribute p root_lexp in
let deref_str = Localise.deref_str_uninitialized alloc_attribute_opt in
let err_desc = Errdesc.explain_memory_access deref_str p (State.get_loc ()) in
let exn = (Exceptions.Uninitialized_value (err_desc, try assert false with Assert_failure x -> x)) in
let exn = (Exceptions.Uninitialized_value (err_desc, __POS__)) in
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
Reporting.log_warning pname ~pre: pre_opt exn;
Sil.update_inst inst_curr inst
@ -478,7 +478,11 @@ let report_raise_memory_leak tenv msg hpred prop =
let resource = match Errdesc.hpred_is_open_resource prop hpred with
| Some res -> res
| None -> Sil.Rmemory Sil.Mmalloc in
raise (Exceptions.Leak (footprint_part, prop, hpred, Errdesc.explain_leak tenv hpred prop None None, false, resource, try assert false with Assert_failure x -> x))
raise
(Exceptions.Leak
(footprint_part, prop, hpred,
Errdesc.explain_leak tenv hpred prop None None, false,
resource, __POS__))
(** In case of constant string dereference, return the result immediately *)
let check_constant_string_dereference lexp =
@ -502,13 +506,15 @@ let exp_norm_check_arith pname prop exp =
match Prop.find_arithmetic_problem (State.get_path_pos ()) prop exp with
| Some (Prop.Div0 div), prop' ->
let desc = Errdesc.explain_divide_by_zero div (State.get_node ()) (State.get_loc ()) in
let exn = Exceptions.Divide_by_zero (desc, try assert false with Assert_failure x -> x) in
let exn = Exceptions.Divide_by_zero (desc, __POS__) in
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
Reporting.log_warning pname ~pre: pre_opt exn;
Prop.exp_normalize_prop prop exp, prop'
| Some (Prop.UminusUnsigned (e, typ)), prop' ->
let desc = Errdesc.explain_unary_minus_applied_to_unsigned_expression e typ (State.get_node ()) (State.get_loc ()) in
let exn = Exceptions.Unary_minus_applied_to_unsigned_expression (desc, try assert false with Assert_failure x -> x) in
let desc =
Errdesc.explain_unary_minus_applied_to_unsigned_expression
e typ (State.get_node ()) (State.get_loc ()) in
let exn = Exceptions.Unary_minus_applied_to_unsigned_expression (desc, __POS__) in
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
Reporting.log_warning pname ~pre: pre_opt exn;
Prop.exp_normalize_prop prop exp, prop'
@ -543,7 +549,8 @@ let check_already_dereferenced pname cond prop =
match dereferenced_line with
| Some (id, (n, pos)) ->
let desc = Errdesc.explain_null_test_after_dereference (Sil.Var id) (State.get_node ()) n (State.get_loc ()) in
let exn = (Exceptions.Null_test_after_dereference (desc, try assert false with Assert_failure x -> x)) in
let exn =
(Exceptions.Null_test_after_dereference (desc, __POS__)) in
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
Reporting.log_warning pname ~pre: pre_opt exn
| None -> ()
@ -1054,7 +1061,8 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
| Sil.Const (Sil.Cint i) when report_condition_always_true_false i ->
let node = State.get_node () in
let desc = Errdesc.explain_condition_always_true_false i cond node loc in
let exn = Exceptions.Condition_always_true_false (desc, not (Sil.Int.iszero i), try assert false with Assert_failure x -> x) in
let exn =
Exceptions.Condition_always_true_false (desc, not (Sil.Int.iszero i), __POS__) in
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
Reporting.log_warning pname ~pre: pre_opt exn
| Sil.BinOp ((Sil.Eq | Sil.Ne), lhs, rhs)
@ -1075,8 +1083,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
if not (Sil.exp_is_zero lhs_normal) && lhs_is_ns_ptr () then
let node = State.get_node () in
let desc = Errdesc.explain_bad_pointer_comparison lhs node loc in
let fail = try assert false with Assert_failure x -> x in
let exn = Exceptions.Bad_pointer_comparison (desc, fail) in
let exn = Exceptions.Bad_pointer_comparison (desc, __POS__) in
Reporting.log_warning pname exn
| _ -> () in
check_already_dereferenced pname cond _prop;
@ -1235,7 +1242,7 @@ and sym_exec_generated mask_errors cfg tenv pdesc instrs ppl =
with exn when exn_not_failure exn && mask_errors ->
let err_name, _, ml_source, _ , _, _, _ = Exceptions.recognize_exception exn in
let loc = (match ml_source with
| Some (src, l, c) -> "at "^(src^" "^(string_of_int l))
| Some ml_loc -> "at " ^ (ml_loc_to_string ml_loc)
| None -> "") in
L.d_warning ("Generated Instruction Failed with: " ^ (Localise.to_string err_name)^loc ); L.d_ln();
[(p, path)] in
@ -1320,7 +1327,7 @@ and check_untainted exp caller_pname callee_pname prop =
callee_pname (State.get_loc ()) in
let exn =
Exceptions.Tainted_value_reaching_sensitive_function
(err_desc, try assert false with Assert_failure x -> x) in
(err_desc, __POS__) in
Reporting.log_warning caller_pname exn;
Prop.add_or_replace_exp_attribute prop exp (Sil.Auntaint)
| _ ->
@ -1413,8 +1420,7 @@ and sym_exe_check_variadic_sentinel ?(fails_on_nil = false) cfg pdesc tenv prop
let err_desc =
Errdesc.explain_dereference ~use_buckets: true ~is_premature_nil: true
deref_str prop loc in
raise (Exceptions.Premature_nil_termination
(err_desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Premature_nil_termination (err_desc, __POS__))
else
raise e in
(* IList.fold_left reverses the arguments back so that we report an *)
@ -1456,7 +1462,7 @@ and sym_exec_objc_getter field_name ret_typ_opt tenv cfg ret_ids pdesc pname loc
let field_access_exp = Sil.Lfield (lexp, field_name, typ') in
execute_letderef
~report_deref_errors:false pname pdesc tenv ret_id field_access_exp ret_typ loc prop
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
and sym_exec_objc_setter field_name ret_typ_opt tenv cfg ret_ids pdesc pname loc args prop =
L.d_strln ("No custom setter found. Executing the ObjC builtin setter with ivar "^
@ -1469,7 +1475,7 @@ and sym_exec_objc_setter field_name ret_typ_opt tenv cfg ret_ids pdesc pname loc
| _ -> assert false) in
let field_access_exp = Sil.Lfield (lexp1, field_name, typ1') in
execute_set ~report_deref_errors:false pname pdesc tenv field_access_exp typ2 lexp2 loc prop
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
and sym_exec_objc_accessor property_accesor ret_typ_opt tenv cfg ret_ids pdesc callee_pname loc args
prop path : Builtin.ret_typ =
@ -1501,7 +1507,7 @@ and sym_exec_call cfg pdesc tenv pre path ret_ids actual_pars summary loc =
if is_ignored
&& Specs.get_flag callee_pname proc_flag_ignore_return = None then
let err_desc = Localise.desc_return_value_ignored callee_pname loc in
let exn = (Exceptions.Return_value_ignored (err_desc, try assert false with Assert_failure x -> x)) in
let exn = (Exceptions.Return_value_ignored (err_desc, __POS__)) in
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop caller_pname) in
Reporting.log_warning caller_pname ~pre: pre_opt exn in
check_inherently_dangerous_function caller_pname callee_pname;
@ -1525,7 +1531,7 @@ and sym_exec_call cfg pdesc tenv pre path ret_ids actual_pars summary loc =
L.d_strln (" mismatch in the number of parameters ****");
L.d_str "actual parameters: "; Sil.d_exp_list (IList.map fst actual_pars); L.d_ln ();
L.d_str "formal parameters: "; Sil.d_typ_list formal_types; L.d_ln ();
raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) in
raise (Exceptions.Wrong_argument_number __POS__) in
let actual_params = comb actual_pars formal_types in
(* Actual parameters are associated to their formal
parameter type if there are enough formal parameters, and
@ -1662,7 +1668,7 @@ module ModelBuiltins = struct
| [(lexp1, typ1); (lexp2, typ2); (lexp3, typ3)], _ ->
let instr' = Sil.Set (lexp3, typ3, Sil.exp_zero, loc) in
sym_exec_generated true cfg tenv pdesc [instr'] [(prop, path)]
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
let mk_empty_array size =
Sil.Earray (size, [], Sil.inst_none)
@ -1715,7 +1721,7 @@ module ModelBuiltins = struct
[(return_result_for_array_size size prop'' ret_ids, path)]
| _ -> []
end
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute___set_array_size cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
: Builtin.ret_typ =
@ -1751,7 +1757,7 @@ module ModelBuiltins = struct
[(prop'', path)]
| _ -> []
end
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute___print_value cfg pdesc instr tenv prop path ret_ids args callee_pname loc
: Builtin.ret_typ =
@ -1838,7 +1844,7 @@ module ModelBuiltins = struct
with Not_found -> (return_result Sil.exp_zero prop ret_ids), path
end in
(IList.map aux props)
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** replace the type of the ptsto rooted at [root_e] with [texp] in [prop] *)
let replace_ptsto_texp prop root_e texp =
@ -1874,8 +1880,7 @@ module ModelBuiltins = struct
!Config.curr_language = Config.Java || is_cast_to_reference in
let deal_with_failed_cast val1 typ1 texp1 texp2 =
Tabulation.raise_cast_exception
(try assert false with Assert_failure ml_loc -> ml_loc)
None texp1 texp2 val1 in
__POS__ None texp1 texp2 val1 in
let exe_one_prop prop =
if Sil.exp_equal texp2 Sil.exp_zero then
[(return_result Sil.exp_zero prop ret_ids, path)]
@ -1930,7 +1935,7 @@ module ModelBuiltins = struct
end in
let props = create_type tenv val1 typ1 prop in
IList.flatten (IList.map exe_one_prop props)
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute___instanceof cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
: Builtin.ret_typ =
@ -1961,7 +1966,7 @@ module ModelBuiltins = struct
let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
set_resource_attribute prop path n_lexp loc Sil.Rfile
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** Set the attibute of the value as lock *)
let execute___set_lock_attribute cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
@ -1971,7 +1976,7 @@ module ModelBuiltins = struct
let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
set_resource_attribute prop path n_lexp loc Sil.Rlock
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** Set the resource attribute of the first real argument of method as ignore, the first argument is assumed to be "this" *)
let execute___method_set_ignore_attribute
@ -1982,7 +1987,7 @@ module ModelBuiltins = struct
let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
set_resource_attribute prop path n_lexp loc Sil.Rignore
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** Set the attibute of the value as memory *)
let execute___set_mem_attribute cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
@ -1992,7 +1997,7 @@ module ModelBuiltins = struct
let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
set_resource_attribute prop path n_lexp loc (Sil.Rmemory Sil.Mnew)
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** Set the attibute of the value as tainted *)
let execute___set_taint_attribute cfg pdesc instr tenv _prop path ret_ids args callee_name loc
@ -2002,7 +2007,7 @@ module ModelBuiltins = struct
let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
[(Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Ataint pname), path)]
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** Set the attibute of the value as untainted *)
let execute___set_untaint_attribute cfg pdesc instr tenv _prop path ret_ids args callee_name loc
@ -2012,7 +2017,7 @@ module ModelBuiltins = struct
let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
[(Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Auntaint), path)]
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** Set the attibute of the value as locked*)
let execute___set_locked_attribute cfg pdesc instr tenv _prop path ret_ids args callee_name loc
@ -2022,7 +2027,7 @@ module ModelBuiltins = struct
let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
[(Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Alocked), path)]
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** Set the attibute of the value as unlocked*)
let execute___set_unlocked_attribute cfg pdesc instr tenv _prop path ret_ids args callee_name loc
@ -2032,7 +2037,7 @@ module ModelBuiltins = struct
let pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith pname _prop lexp in
[(Prop.add_or_replace_exp_attribute prop n_lexp (Sil.Aunlocked), path)]
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** report an error if [lexp] is tainted; otherwise, add untained([lexp]) as a precondition *)
@ -2043,7 +2048,7 @@ module ModelBuiltins = struct
let caller_pname = Cfg.Procdesc.get_proc_name pdesc in
let n_lexp, prop = exp_norm_check_arith caller_pname prop lexp in
[(check_untainted n_lexp caller_pname callee_pname prop, path)]
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** take a pointer to a struct, and return the value of a hidden field in the struct *)
let execute___get_hidden_field cfg pdesc instr tenv _prop path ret_ids args callee_name loc
@ -2079,7 +2084,7 @@ module ModelBuiltins = struct
let prop' = Prop.replace_sigma_footprint sigma_fp' (Prop.replace_sigma sigma' prop) in
let prop'' = return_val (Prop.normalize prop') in
[(prop'', path)]
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** take a pointer to a struct and a value, and set a hidden field in the struct to the given value *)
let execute___set_hidden_field cfg pdesc instr tenv _prop path ret_ids args callee_name loc
@ -2108,7 +2113,7 @@ module ModelBuiltins = struct
let prop' = Prop.replace_sigma_footprint sigma_fp' (Prop.replace_sigma sigma' prop) in
let prop'' = Prop.normalize prop' in
[(prop'', path)]
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(* Update the objective-c hidden counter by applying the operation op and the operand delta.*)
(* Eg. op=+/- delta is an integer *)
@ -2133,7 +2138,7 @@ module ModelBuiltins = struct
let update_counter = Sil.Set(hidden_field, typ', Sil.BinOp(op, Sil.Var tmp, Sil.Const (Sil.Cint delta)), loc) in
let update_counter_instrs = [counter_to_tmp; update_counter; Sil.Remove_temps([tmp], loc)] in
sym_exec_generated suppress_npe_report cfg tenv pdesc update_counter_instrs [(_prop, path)]
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(* Given a list of args checks if the first is the flag indicating whether is a call to retain/release for which*)
(* we have to suppress NPE report or not. If the flag is present it is removed from the list of args. *)
@ -2151,7 +2156,7 @@ module ModelBuiltins = struct
let prop = return_result lexp _prop ret_ids in
execute___objc_counter_update suppress_npe_report (Sil.PlusA) (Sil.Int.one)
cfg pdesc instr tenv prop path ret_ids args' callee_name loc
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute___objc_retain cfg pdesc instr tenv _prop path ret_ids args callee_name loc
: Builtin.ret_typ =
@ -2192,7 +2197,7 @@ module ModelBuiltins = struct
let prop' = Prop.add_or_replace_exp_attribute prop n_lexp Sil.Aautorelease in
[(prop', path)]
else execute___no_op prop path
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(** Release all the objects in the pool *)
let execute___release_autorelease_pool
@ -2237,11 +2242,13 @@ module ModelBuiltins = struct
[(return_result val1 prop' ret_ids, path)]
| _ -> [(return_result val1 prop ret_ids, path)]
with Not_found -> [(return_result val1 prop ret_ids, path)])
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute_abort cfg pdesc instr tenv prop path ret_ids args callee_pname loc
: Builtin.ret_typ =
raise (Exceptions.Precondition_not_found (Localise.verbatim_desc (Procname.to_string callee_pname), try assert false with Assert_failure x -> x))
raise
(Exceptions.Precondition_not_found
(Localise.verbatim_desc (Procname.to_string callee_pname), __POS__))
let execute_exit cfg pdesc instr tenv prop path ret_ids args callee_pname loc
: Builtin.ret_typ =
@ -2283,7 +2290,7 @@ module ModelBuiltins = struct
L.d_strln ".... Array containing allocated heap cells ....";
L.d_str " Instr: "; Sil.d_instr instr; L.d_ln ();
L.d_str " PROP: "; Prop.d_prop prop; L.d_ln ();
raise (Exceptions.Array_of_pointsto (try assert false with Assert_failure x -> x))
raise (Exceptions.Array_of_pointsto __POS__)
end
let execute_free mk cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
@ -2304,7 +2311,7 @@ module ModelBuiltins = struct
(Prop.exp_normalize_prop p lexp) typ loc) prop_nonzero) in
IList.map (fun p -> (p, path)) plist
end
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute_alloc mk can_return_null cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
: Builtin.ret_typ =
@ -2327,7 +2334,7 @@ module ModelBuiltins = struct
| [(num_obj, _); (base_exp, _)] -> (* for __new_array *)
Sil.BinOp (Sil.Mult, num_obj, base_exp)
| _ ->
raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) in
raise (Exceptions.Wrong_argument_number __POS__) in
let ret_id = match ret_ids with
| [ret_id] -> ret_id
| _ -> Ident.create_fresh Ident.kprimed in
@ -2373,7 +2380,7 @@ module ModelBuiltins = struct
| _ ->
L.d_str "pthread_create: unknown function "; Sil.d_exp routine_name; L.d_strln ", skipping call.";
[(prop, path)])
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute_skip cfg pdesc instr tenv prop path ret_ids args callee_pname loc : Builtin.ret_typ =
[(prop, path)]
@ -2386,7 +2393,7 @@ module ModelBuiltins = struct
let varargs = ref args in
for i = 1 to skip_n_arguments do varargs := IList.tl !varargs done;
call_unknown_or_scan true cfg pdesc tenv prop path ret_ids None !varargs callee_pname loc
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute__unwrap_exception cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
: Builtin.ret_typ =
@ -2401,7 +2408,7 @@ module ModelBuiltins = struct
[(prop_with_exn, path)]
| _ -> assert false
end
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute_return_first_argument cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
: Builtin.ret_typ =
@ -2411,7 +2418,7 @@ module ModelBuiltins = struct
let arg1, prop = exp_norm_check_arith pname _prop _arg1 in
let prop' = return_result arg1 prop ret_ids in
[(prop', path)]
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute___split_get_nth cfg pdesc instr tenv _prop path ret_ids args callee_pname loc
: Builtin.ret_typ =
@ -2431,7 +2438,7 @@ module ModelBuiltins = struct
[(return_result res prop ret_ids, path)]
with Not_found -> assert false)
| _ -> [(prop, path)])
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
let execute___create_tuple cfg pdesc instr tenv prop path ret_ids args callee_pname loc
: Builtin.ret_typ =
@ -2452,7 +2459,7 @@ module ModelBuiltins = struct
let en = IList.nth el n in
[(return_result en prop ret_ids, path)]
| _ -> [(prop, path)])
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(* forces the expression passed as parameter to be assumed true at the point where this
builtin is called, blocks if this causes an inconsistency *)
@ -2463,7 +2470,7 @@ module ModelBuiltins = struct
let prop_assume = Prop.conjoin_eq lexp (Sil.exp_bool true) prop in
if Prover.check_inconsistency prop_assume then execute_diverge prop_assume path
else [(prop_assume, path)]
| _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(* creates a named error state *)
let execute___infer_fail cfg pdesc instr tenv prop path ret_ids args callee_pname loc
@ -2477,7 +2484,7 @@ module ModelBuiltins = struct
| _ -> assert false
end
| _ ->
raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) in
raise (Exceptions.Wrong_argument_number __POS__) in
let set_instr =
Sil.Set (Sil.Lvar Sil.custom_error, Sil.Tvoid, Sil.Const (Sil.Cstr error_str), loc) in
sym_exec_generated true cfg tenv pdesc [set_instr] [(prop, path)]
@ -2490,7 +2497,7 @@ module ModelBuiltins = struct
| l when IList.length l = 4 ->
Config.default_failure_name
| _ ->
raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) in
raise (Exceptions.Wrong_argument_number __POS__) in
let set_instr =
Sil.Set (Sil.Lvar Sil.custom_error, Sil.Tvoid, Sil.Const (Sil.Cstr error_str), loc) in
sym_exec_generated true cfg tenv pdesc [set_instr] [(prop, path)]

60
infer/src/backend/tabulation.ml
Unescape View File

@ -109,14 +109,16 @@ let spec_find_rename trace_call (proc_name : Procname.t) : (int * Prop.exposed S
if specs == [] then
begin
trace_call Specs.CallStats.CR_not_found;
raise (Exceptions.Precondition_not_found (Localise.verbatim_desc (Procname.to_string proc_name), try assert false with Assert_failure x -> x))
raise (Exceptions.Precondition_not_found
(Localise.verbatim_desc (Procname.to_string proc_name), __POS__))
end;
let formal_parameters =
IList.map (fun (x, _) -> Sil.mk_pvar_callee x proc_name) formals in
IList.map f specs, formal_parameters
with Not_found -> begin
L.d_strln ("ERROR: found no entry for procedure " ^ Procname.to_string proc_name ^ ". Give up...");
raise (Exceptions.Precondition_not_found (Localise.verbatim_desc (Procname.to_string proc_name), try assert false with Assert_failure x -> x))
raise (Exceptions.Precondition_not_found
(Localise.verbatim_desc (Procname.to_string proc_name), __POS__))
end
let check_splitting_precondition sub1 sub2 =
@ -348,7 +350,7 @@ let check_path_errors_in_post caller_pname post post_path =
then post_path, Some path_pos
else current_path, None in (* position not found, only use the path up to the callee *)
State.set_path new_path path_pos_opt;
let exn = Exceptions.Divide_by_zero (desc, try assert false with Assert_failure x -> x) in
let exn = Exceptions.Divide_by_zero (desc, __POS__) in
let pre_opt = State.get_normalized_pre (fun te p -> p) (* Abs.abstract_no_symop *) in
Reporting.log_warning caller_pname ~pre: pre_opt exn
| _ -> () in
@ -481,7 +483,7 @@ let sigma_star_fld (sigma1 : Sil.hpred list) (sigma2 : Sil.hpred list) : Sil.hpr
L.d_str "cannot star ";
Prop.d_sigma sigma1; L.d_str " and "; Prop.d_sigma sigma2;
L.d_ln ();
raise (Prop.Cannot_star (try assert false with Assert_failure x -> x))
raise (Prop.Cannot_star __POS__)
let hpred_typing_lhs_compare hpred1 (e2, te2) = match hpred1 with
| Sil.Hpointsto(e1, _, _) -> Sil.exp_compare e1 e2
@ -513,7 +515,7 @@ let sigma_star_typ (sigma1 : Sil.hpred list) (typings2 : (Sil.exp * Sil.exp) lis
L.d_str "cannot star ";
Prop.d_sigma sigma1; L.d_str " and "; Prover.d_typings typings2;
L.d_ln ();
raise (Prop.Cannot_star (try assert false with Assert_failure x -> x))
raise (Prop.Cannot_star __POS__)
(** [prop_footprint_add_pi_sigma_starfld_sigma prop pi sigma missing_fld] extends the footprint of [prop] with [pi,sigma] and extends the fields of |-> with [missing_fld] *)
let prop_footprint_add_pi_sigma_starfld_sigma (prop : 'a Prop.t) pi_new sigma_new missing_fld missing_typ : Prop.normal Prop.t option =
@ -556,7 +558,7 @@ let check_attr_dealloc_mismatch att_old att_new = match att_old, att_new with
Sil.Aresource ({ Sil.ra_kind = Sil.Rrelease; Sil.ra_res = Sil.Rmemory mk_new } as ra_new)
when Sil.mem_kind_compare mk_old mk_new <> 0 ->
let desc = Errdesc.explain_allocation_mismatch ra_old ra_new in
raise (Exceptions.Deallocation_mismatch (desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Deallocation_mismatch (desc, __POS__))
| _ -> ()
(** [prop_copy_footprint p1 p2] copies the footprint and pure part of [p1] into [p2] *)
@ -796,7 +798,7 @@ let mk_actual_precondition prop actual_params formal_params =
(let str = "more actual pars than formal pars in fun call (" ^ string_of_int (IList.length actual_params) ^ " vs " ^ string_of_int (IList.length formal_params) ^ ")" in
L.d_warning str; L.d_ln ());
[]
| _:: _,[] -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x)) in
| _:: _,[] -> raise (Exceptions.Wrong_argument_number __POS__) in
comb formal_params actual_params in
let mk_instantiation (formal_var, (actual_e, actual_t)) =
Prop.mk_ptsto (Sil.Lvar formal_var) (Sil.Eexp (actual_e, Sil.inst_actual_precondition)) (Sil.Sizeof (actual_t, Sil.Subtype.exact)) in
@ -893,7 +895,7 @@ let do_taint_check caller_pname callee_pname calling_pi missing_pi sub prop =
callee_pname (State.get_loc ()) in
let exn =
Exceptions.Tainted_value_reaching_sensitive_function
(err_desc, try assert false with Assert_failure x -> x) in
(err_desc, __POS__) in
Reporting.log_warning caller_pname exn in
IList.iter report_one_error taint_atoms in
Sil.ExpMap.iter report_taint_errors taint_untaint_exp_map;
@ -912,26 +914,26 @@ let do_taint_check caller_pname callee_pname calling_pi missing_pi sub prop =
taint_untaint_exp_map) in
IList.filter not_untaint_atom missing_pi_sub
let class_cast_exn pname_opt texp1 texp2 exp ml_location =
let class_cast_exn pname_opt texp1 texp2 exp ml_loc =
let desc = Errdesc.explain_class_cast_exception pname_opt texp1 texp2 exp (State.get_node ()) (State.get_loc ()) in
Exceptions.Class_cast_exception (desc, ml_location)
Exceptions.Class_cast_exception (desc, ml_loc)
let raise_cast_exception ml_location pname_opt texp1 texp2 exp =
let exn = class_cast_exn pname_opt texp1 texp2 exp ml_location in
let raise_cast_exception ml_loc pname_opt texp1 texp2 exp =
let exn = class_cast_exn pname_opt texp1 texp2 exp ml_loc in
raise exn
let get_check_exn check callee_pname loc ml_location = match check with
let get_check_exn check callee_pname loc ml_loc = match check with
| Prover.Bounds_check ->
let desc = Localise.desc_precondition_not_met (Some Localise.Pnm_bounds) callee_pname loc in
Exceptions.Precondition_not_met (desc, ml_location)
Exceptions.Precondition_not_met (desc, ml_loc)
| Prover.Class_cast_check (texp1, texp2, exp) ->
class_cast_exn (Some callee_pname) texp1 texp2 exp ml_location
class_cast_exn (Some callee_pname) texp1 texp2 exp ml_loc
let check_uninitialize_dangling_deref callee_pname actual_pre sub formal_params props =
IList.iter (fun (p, _ ) ->
match check_dereferences callee_pname actual_pre sub p formal_params with
| Some (Deref_undef_exp, desc) ->
raise (Exceptions.Dangling_pointer_dereference (Some Sil.DAuninit, desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Dangling_pointer_dereference (Some Sil.DAuninit, desc, __POS__))
| _ -> ()) props
(** Perform symbolic execution for a single spec *)
@ -952,7 +954,7 @@ let exe_spec
| Prover.ImplFail checks -> Invalid_res (Prover_checks checks)
| Prover.ImplOK (checks, sub1, sub2, frame, missing_pi, missing_sigma, frame_fld, missing_fld, frame_typ, missing_typ) ->
let log_check_exn check =
let exn = get_check_exn check callee_pname loc (try assert false with Assert_failure x -> x) in
let exn = get_check_exn check callee_pname loc __POS__ in
Reporting.log_warning caller_pname exn in
let do_split () =
let missing_pi' =
@ -1088,27 +1090,29 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname loc initial_prop r
| Dereference_error (Deref_minusone, desc, path_opt) ->
trace_call Specs.CallStats.CR_not_met;
extend_path path_opt None;
raise (Exceptions.Dangling_pointer_dereference (Some Sil.DAminusone, desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Dangling_pointer_dereference
(Some Sil.DAminusone, desc, __POS__))
| Dereference_error (Deref_undef_exp, desc, path_opt) ->
trace_call Specs.CallStats.CR_not_met;
extend_path path_opt None;
raise (Exceptions.Dangling_pointer_dereference (Some Sil.DAuninit, desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Dangling_pointer_dereference
(Some Sil.DAuninit, desc, __POS__))
| Dereference_error (Deref_null pos, desc, path_opt) ->
trace_call Specs.CallStats.CR_not_met;
extend_path path_opt (Some pos);
if Localise.is_parameter_not_null_checked_desc desc then
raise (Exceptions.Parameter_not_null_checked (desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Parameter_not_null_checked (desc, __POS__))
else if Localise.is_field_not_null_checked_desc desc then
raise (Exceptions.Field_not_null_checked (desc, try assert false with Assert_failure x -> x))
else raise (Exceptions.Null_dereference (desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Field_not_null_checked (desc, __POS__))
else raise (Exceptions.Null_dereference (desc, __POS__))
| Dereference_error (Deref_freed ra, desc, path_opt) ->
trace_call Specs.CallStats.CR_not_met;
extend_path path_opt None;
raise (Exceptions.Use_after_free (desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Use_after_free (desc, __POS__))
| Dereference_error (Deref_undef (s, loc, pos), desc, path_opt) ->
trace_call Specs.CallStats.CR_not_met;
extend_path path_opt (Some pos);
raise (Exceptions.Skip_pointer_dereference (desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Skip_pointer_dereference (desc, __POS__))
| Prover_checks _ | Cannot_combine | Missing_sigma_not_empty | Missing_fld_not_empty ->
trace_call Specs.CallStats.CR_not_met;
assert false
@ -1119,13 +1123,13 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname loc initial_prop r
else if IList.exists (function
| Prover_checks (check :: _) ->
trace_call Specs.CallStats.CR_not_met;
let exn = get_check_exn check callee_pname loc (try assert false with Assert_failure x -> x) in
let exn = get_check_exn check callee_pname loc __POS__ in
raise exn
| _ -> false) invalid_res then
call_desc (Some Localise.Pnm_bounds)
else call_desc None in
trace_call Specs.CallStats.CR_not_met;
raise (Exceptions.Precondition_not_met (desc, try assert false with Assert_failure x -> x))
raise (Exceptions.Precondition_not_met (desc, __POS__))
end
else (* combine the valid results, and store diverging states *)
let process_valid_res vr =
@ -1140,7 +1144,7 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname loc initial_prop r
else if valid_res_no_miss_pi != [] then
IList.flatten (IList.map (fun vr -> vr.vr_cons_res) valid_res_no_miss_pi)
else if valid_res_miss_pi == [] then
raise (Exceptions.Precondition_not_met (call_desc None, try assert false with Assert_failure x -> x))
raise (Exceptions.Precondition_not_met (call_desc None, __POS__))
else
begin
L.d_strln "Missing pure facts for the function call:";
@ -1148,7 +1152,7 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname loc initial_prop r
match Prover.find_minimum_pure_cover (IList.map (fun vr -> (vr.vr_pi, vr.vr_cons_res)) valid_res_miss_pi) with
| None ->
trace_call Specs.CallStats.CR_not_met;
raise (Exceptions.Precondition_not_met (call_desc None, try assert false with Assert_failure x -> x))
raise (Exceptions.Precondition_not_met (call_desc None, __POS__))
| Some cover ->
L.d_strln "Found minimum cover";
IList.iter print_pi (IList.map fst cover);

2
infer/src/backend/tabulation.mli
Unescape View File

@ -24,7 +24,7 @@ val find_dereference_without_null_check_in_sexp : Sil.strexp -> (int * Sil.path_
(** raise a cast exception *)
val raise_cast_exception :
Utils.ml_location -> Procname.t option -> Sil.exp -> Sil.exp -> Sil.exp -> 'a
Utils.ml_loc -> Procname.t option -> Sil.exp -> Sil.exp -> Sil.exp -> 'a
(** check if a prop is an exception *)
val prop_is_exn : Procname.t -> 'a Prop.t -> bool

24
infer/src/backend/utils.ml
Unescape View File

@ -237,25 +237,21 @@ let pp_elapsed_time fmt () =
let elapsed = Unix.gettimeofday () -. initial_timeofday in
Format.fprintf fmt "%f" elapsed
(** Type of location in ml source: file,line,column *)
type ml_location = string * int * int
(** Type of location in ml source: __POS__ *)
type ml_loc = string * int * int * int
(** String describing the file of an ml location *)
let ml_location_file_string ((file: string), (line: int), (column: int)) =
"file " ^ file
(** Turn an ml location into a string *)
let ml_location_string ((file: string), (line: int), (column: int)) =
"file " ^ file ^ " line " ^ string_of_int line ^ " column " ^ string_of_int column
(** Convert a ml location to a string *)
let ml_loc_to_string (file, lnum, cnum, enum) =
Printf.sprintf "%s:%d:%d-%d:" file lnum cnum enum
(** Pretty print a location of ml source *)
let pp_ml_location fmt mloc =
F.fprintf fmt "%s" (ml_location_string mloc)
let pp_ml_loc fmt ml_loc =
F.fprintf fmt "%s" (ml_loc_to_string ml_loc)
let pp_ml_location_opt fmt mloco =
if !Config.developer_mode then match mloco with
let pp_ml_loc_opt fmt ml_loc_opt =
if !Config.developer_mode then match ml_loc_opt with
| None -> ()
| Some mloc -> F.fprintf fmt "(%a)" pp_ml_location mloc
| Some ml_loc -> F.fprintf fmt "(%a)" pp_ml_loc ml_loc
(** {2 SymOp and Failures: units of symbolic execution} *)

13
infer/src/backend/utils.mli
Unescape View File

@ -68,17 +68,14 @@ module StringMap : Map.S with type key = string
(** {2 Printing} *)
(** Type of location in ml source: file,line,column *)
type ml_location = string * int * int
(** Type of location in ml source: __POS__ *)
type ml_loc = string * int * int * int
(** String describing the file of an ml location *)
val ml_location_file_string : ml_location -> string
(** Turn an ml location into a string *)
val ml_location_string : ml_location -> string
(** Convert a ml location to a string *)
val ml_loc_to_string : ml_loc -> string
(** Pretty print a location of ml source *)
val pp_ml_location_opt : Format.formatter -> ml_location option -> unit
val pp_ml_loc_opt : Format.formatter -> ml_loc option -> unit
(** Colors supported in printing *)
type color = Black | Blue | Green | Orange | Red

3
infer/src/clang/cFrontend_errors.ml
Unescape View File

@ -34,8 +34,7 @@ let log_frontend_warning pdesc warn_desc =
let err_desc =
Errdesc.explain_frontend_warning warn_desc.description warn_desc.suggestion loc in
let exn = Exceptions.Frontend_warning
(warn_desc.name, err_desc,
try assert false with Assert_failure x -> x) in
(warn_desc.name, err_desc, __POS__) in
Reporting.log_error_from_errlog errlog exn ~loc:(Some loc)
(* Call all checkers on properties of class c *)

3
infer/src/eradicate/modelTables.ml
Unescape View File

@ -234,8 +234,7 @@ let mk_table list =
IList.iter (function (v, pn_id) -> Hashtbl.replace map pn_id v) list;
map
let ml_location =
try assert false with Assert_failure x -> x
let this_file = __FILE__
let annotated_table_nullable = mk_table annotated_list_nullable
let annotated_table_present = mk_table annotated_list_present

4
infer/src/eradicate/modelTables.mli
Unescape View File

@ -11,8 +11,8 @@ open Utils
type model_table_t = (string, bool * bool list) Hashtbl.t
(** Location of this file. *)
val ml_location : ml_location
(** Name of this file. *)
val this_file : string
val annotated_table_nullable : model_table_t
val annotated_table_present : model_table_t

2
infer/src/eradicate/typeOrigin.ml
Unescape View File

@ -96,7 +96,7 @@ let get_description origin =
| None -> "" in
let modelled_in =
if Models.is_modelled_nullable po.pname
then " modelled in " ^ (Utils.ml_location_file_string ModelTables.ml_location)
then " modelled in " ^ ModelTables.this_file
else "" in
let description = Printf.sprintf
"call to %s%s%s%s"

Write Preview
Loading…
Cancel
Save