Skip to content

Commit

Permalink
[textual] make type error better localized
Browse files Browse the repository at this point in the history
Summary: when possible we give a location error that is closer to the problem.

Reviewed By: geralt-encore

Differential Revision: D46845506

fbshipit-source-id: 97d94ade358934534e315c1efc249ffb7475bf0c
  • Loading branch information
davidpichardie authored and facebook-github-bot committed Jun 21, 2023
1 parent 887e59b commit bcacaf3
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 9 deletions.
25 changes: 23 additions & 2 deletions infer/src/textual/TextualTypeVerification.ml
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,28 @@ let pp_error sourcefile fmt error =
F.fprintf fmt "variable %a has not been declared" VarName.pp var


let mk_type_mismatch_error expected loc exp typ : error = TypeMismatch {exp; typ; expected; loc}
let rec loc_of_exp exp =
match (exp : Exp.t) with
| Var _ ->
None
| Lvar {loc} ->
Some loc
| Field {exp} ->
loc_of_exp exp
| Index (exp, _) ->
loc_of_exp exp
| Const _ ->
None
| Call {proc} ->
Some proc.name.loc
| Typ _ ->
None


let mk_type_mismatch_error expected loc exp typ : error =
let loc = loc_of_exp exp |> Option.value ~default:loc in
TypeMismatch {exp; typ; expected; loc}


(** state + error monad *)
type state =
Expand Down Expand Up @@ -208,7 +229,7 @@ let typeof_var var : Typ.t monad =
let optional_typ = VarName.Map.find_opt var state.vars in
option_value_map optional_typ state
~none:
(let* loc = get_location in
(let loc = var.VarName.loc in
let* () = add_error (VarTypeNotDeclared {var; loc}) in
abort )
~some:ret
Expand Down
14 changes: 7 additions & 7 deletions infer/tests/codetoanalyze/sil/verif/issues.exp
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
annotated.sil, line 21, column 4: textual type error: expression &y has type *float, while a subtype of *int was expected
annotated.sil, line 22, column 4: textual type error: expression &n has type **node, while a pointer of array type was expected
basic.sil, line 17, column 4: textual type error: expression &y has type *float, while a subtype of *int was expected
basic.sil, line 18, column 4: textual type error: expression &n has type **node, while a pointer of array type was expected
annotated.sil, line 21, column 19: textual type error: expression &y has type *float, while a subtype of *int was expected
annotated.sil, line 22, column 19: textual type error: expression &n has type **node, while a pointer of array type was expected
basic.sil, line 17, column 19: textual type error: expression &y has type *float, while a subtype of *int was expected
basic.sil, line 18, column 19: textual type error: expression &n has type **node, while a pointer of array type was expected
basic.sil, line 20, column 4: textual type error: expression n1 has type int, while a subtype of *node was expected
basic.sil, line 35, column 4: textual type error: variable u has not been declared
basic.sil, line 35, column 11: textual type error: variable u has not been declared
basic.sil, line 36, column 4: textual type error: ident n0 is given the type float, but it has already been given the type int at line 17
basic.sil, line 24, column 4: textual type error: expression n0 has type int, while a subtype of float was expected
basic.sil, line 24, column 4: textual type error: expression &x has type *int, while a supertype of *float was expected
basic.sil, line 24, column 11: textual type error: expression &x has type *int, while a supertype of *float was expected
basic.sil, line 25, column 4: textual type error: expression n1 has type int, while a subtype of float was expected
basic.sil, line 25, column 4: textual type error: expression &x has type *int, while a pointer of array type was expected
basic.sil, line 25, column 11: textual type error: expression &x has type *int, while a pointer of array type was expected
basic.sil, line 29, column 4: textual type error: expression n3 has type *int[], while a pointer of struct type was expected
basic.sil, line 49, column 4: textual type error: ident n1 is read before being written
basic.sil, line 60, column 4: textual type error: builtin __sil_allocate is called with 2 arguments while it expects 1
Expand Down

0 comments on commit bcacaf3

Please sign in to comment.