Merge branch 'ks/dialyzer-R14-fixes' into dev

* ks/dialyzer-R14-fixes:
  Various changes to dialyzer-related files for R14.

OTP-8699 ks/dialyzer-R14-fixes

Various changes to dialyzer-related files for R14.

- Dialyzer properly supports the new attribute -export_type and checks that
remote types only refer to exported types. A warning is produced if some
files/applications refer to types defined in modules which are neither in
the PLT nor in the analyzed applications.

- Support for detecting data races involving whereis/1 and unregister/1.

- More precise identification of the reason(s) why a record construction
violates the types declared for its fields.

- Fixed bug in the handling of the 'or' guard.

- Better handling of the erlang:element/2 BIF.

- Complete handling of Erlang BIFs.

18 files changed, 773 insertions, 635 deletions

diff --git a/lib/dialyzer/RELEASE_NOTES b/lib/dialyzer/RELEASE_NOTES
index b668142327..62b0c92f97 100644
--- a/lib/dialyzer/RELEASE_NOTES
+++ b/lib/dialyzer/RELEASE_NOTES
@@ -3,6 +3,19 @@
 		(in reversed chronological order)
 ==============================================================================
 
+Version 2.3.0 (in Erlang/OTP R14)
+---------------------------------
+ - Dialyzer properly supports the new attribute -export_type and checks
+   that remote types only refer to exported types. A warning is produced
+   if some files/applications refer to types defined in modules which are
+   neither in the PLT nor in the analyzed applications.
+ - Support for detecting data races involving whereis/1 and unregister/1.
+ - More precise identification of the reason(s) why a record construction
+   violates the types declared for its fields.
+ - Fixed bug in the handling of the 'or' guard.
+ - Better handling of the erlang:element/2 BIF.
+ - Complete handling of Erlang BIFs.
+
 Version 2.2.0 (in Erlang/OTP R13B04)
 ------------------------------------
  - Much better support for opaque types (thanks to Manouk Manoukian).
diff --git a/lib/dialyzer/src/dialyzer.erl b/lib/dialyzer/src/dialyzer.erl
index 3b7b68e8c4..d8fd073ca6 100644
--- a/lib/dialyzer/src/dialyzer.erl
+++ b/lib/dialyzer/src/dialyzer.erl
@@ -33,8 +33,8 @@
 %% NOTE: Only functions exported by this module are available to
 %%       other applications.
 %%--------------------------------------------------------------------
--export([plain_cl/0, 
-	 run/1, 
+-export([plain_cl/0,
+	 run/1,
 	 gui/0,
 	 gui/1,
 	 plt_info/1,
@@ -55,7 +55,7 @@
 
 plain_cl() ->
   case dialyzer_cl_parse:start() of
-    {check_init, Opts} -> 
+    {check_init, Opts} ->
       cl_halt(cl_check_init(Opts), Opts);
     {plt_info, Opts} ->
       cl_halt(cl_print_plt_info(Opts), Opts);
@@ -72,7 +72,7 @@ plain_cl() ->
 	false ->
 	  gui_halt(internal_gui(Type, Opts), Opts)
       end;
-    {cl, Opts} -> 
+    {cl, Opts} ->
       case Opts#options.check_plt of
 	true ->
 	  case cl_check_init(Opts#options{get_warnings = false}) of
@@ -82,7 +82,7 @@ plain_cl() ->
 	false ->
 	  cl_halt(cl(Opts), Opts)
       end;
-    {error, Msg} -> 
+    {error, Msg} ->
       cl_error(Msg)
   end.
 
@@ -146,7 +146,7 @@ cl(Opts) ->
 -spec run(dial_options()) -> [dial_warning()].
 
 run(Opts) ->
-  try dialyzer_options:build([{report_mode, quiet}, 
+  try dialyzer_options:build([{report_mode, quiet},
 			      {erlang_mode, true}|Opts]) of
     {error, Msg} ->
       throw({dialyzer_error, Msg});
@@ -161,7 +161,7 @@ run(Opts) ->
 	  throw({dialyzer_error, ErrorMsg1})
       end
   catch
-    throw:{dialyzer_error, ErrorMsg} -> 
+    throw:{dialyzer_error, ErrorMsg} ->
       erlang:error({dialyzer_error, lists:flatten(ErrorMsg)})
   end.
 
@@ -226,7 +226,7 @@ plt_info(Plt) ->
 %%-----------
 
 doit(F) ->
-  try 
+  try
     {ok, F()}
   catch
     throw:{dialyzer_error, Msg} ->
@@ -241,9 +241,9 @@ gui_halt(R, Opts) ->
 
 -spec cl_halt({'ok',dial_ret()} | {'error',string()}, #options{}) -> no_return().
 
-cl_halt({ok, R = ?RET_NOTHING_SUSPICIOUS}, #options{report_mode = quiet}) -> 
+cl_halt({ok, R = ?RET_NOTHING_SUSPICIOUS}, #options{report_mode = quiet}) ->
   halt(R);
-cl_halt({ok, R = ?RET_DISCREPANCIES}, #options{report_mode = quiet}) -> 
+cl_halt({ok, R = ?RET_DISCREPANCIES}, #options{report_mode = quiet}) ->
   halt(R);
 cl_halt({ok, R = ?RET_NOTHING_SUSPICIOUS}, #options{}) ->
   io:put_chars("done (passed successfully)\n"),
@@ -267,7 +267,7 @@ cl_check_log(Output) ->
 
 -spec format_warning(dial_warning()) -> string().
 
-format_warning({_Tag, {File, Line}, Msg}) when is_list(File), 
+format_warning({_Tag, {File, Line}, Msg}) when is_list(File),
 					       is_integer(Line) ->
   BaseName = filename:basename(File),
   String = lists:flatten(message_to_string(Msg)),
@@ -290,7 +290,7 @@ message_to_string({app_call, [M, F, Args, Culprit, ExpectedType, FoundType]}) ->
 message_to_string({bin_construction, [Culprit, Size, Seg, Type]}) ->
   io_lib:format("Binary construction will fail since the ~s field ~s in"
 		" segment ~s has type ~s\n", [Culprit, Size, Seg, Type]);
-message_to_string({call, [M, F, Args, ArgNs, FailReason, 
+message_to_string({call, [M, F, Args, ArgNs, FailReason,
 			  SigArgs, SigRet, Contract]}) ->
   io_lib:format("The call ~w:~w~s ", [M, F, Args]) ++
     call_or_apply_to_string(ArgNs, FailReason, SigArgs, SigRet, Contract);
@@ -329,9 +329,9 @@ message_to_string({no_return, [Type|Name]}) ->
     only_normal -> NameString ++ "has no local return\n";
     both -> NameString ++ "has no local return\n"
   end;
-message_to_string({record_constr, [Types, Name]}) ->
+message_to_string({record_constr, [RecConstr, FieldDiffs]}) ->
   io_lib:format("Record construction ~s violates the"
-		" declared type for #~w{}\n", [Types, Name]);
+		" declared type of field ~s\n", [RecConstr, FieldDiffs]);
 message_to_string({record_constr, [Name, Field, Type]}) ->
   io_lib:format("Record construction violates the declared type for #~w{}"
 		" since ~s cannot be of type ~s\n", [Name, Field, Type]);
@@ -358,7 +358,7 @@ message_to_string({contract_diff, [M, F, _A, Contract, Sig]}) ->
 		[M, F, Contract, M, F, Sig]);
 message_to_string({contract_subtype, [M, F, _A, Contract, Sig]}) ->
   io_lib:format("Type specification ~w:~w~s"
-		" is a subtype of the success typing: ~w:~w~s\n", 
+		" is a subtype of the success typing: ~w:~w~s\n",
 		[M, F, Contract, M, F, Sig]);
 message_to_string({contract_supertype, [M, F, _A, Contract, Sig]}) ->
   io_lib:format("Type specification ~w:~w~s"
@@ -427,7 +427,7 @@ message_to_string({spec_missing, [B, F, A]}) ->
 %% Auxiliary functions below
 %%-----------------------------------------------------------------------------
 
-call_or_apply_to_string(ArgNs, FailReason, SigArgs, SigRet, 
+call_or_apply_to_string(ArgNs, FailReason, SigArgs, SigRet,
 			{IsOverloaded, Contract}) ->
   PositionString = form_position_string(ArgNs),
   case FailReason of
@@ -442,7 +442,7 @@ call_or_apply_to_string(ArgNs, FailReason, SigArgs, SigRet,
 			" from the success typing arguments: ~s\n",
 			[PositionString, SigArgs])
       end;
-    only_contract -> 
+    only_contract ->
       case (ArgNs =:= []) orelse IsOverloaded of
 	true ->
 	  %% We do not know which arguments caused the failure
@@ -494,7 +494,7 @@ form_position_string(ArgNs) ->
   case ArgNs of
     [] -> "";
     [N1] -> ordinal(N1);
-    [_,_|_] -> 
+    [_,_|_] ->
       [Last|Prevs] = lists:reverse(ArgNs),
       ", " ++ Head = lists:flatten([io_lib:format(", ~s",[ordinal(N)]) ||
 				     N <- lists:reverse(Prevs)]),
diff --git a/lib/dialyzer/src/dialyzer_analysis_callgraph.erl b/lib/dialyzer/src/dialyzer_analysis_callgraph.erl
index e3dd690470..3438cc8c7e 100644
--- a/lib/dialyzer/src/dialyzer_analysis_callgraph.erl
+++ b/lib/dialyzer/src/dialyzer_analysis_callgraph.erl
@@ -398,7 +398,7 @@ store_core(Mod, Core, NoWarn, Callgraph, CServer) ->
   store_code_and_build_callgraph(Mod, LabeledCore, Callgraph, CServer3, NoWarn).
 
 abs_get_nowarn(Abs, M) ->
-  [{M, F, A} 
+  [{M, F, A}
    || {attribute, _, compile, {nowarn_unused_function, {F, A}}} <- Abs].
 
 get_exported_types_from_core(Core) ->
@@ -421,7 +421,7 @@ label_core(Core, CServer) ->
   NextLabel = dialyzer_codeserver:get_next_core_label(CServer),
   CoreTree = cerl:from_records(Core),
   {LabeledTree, NewNextLabel} = cerl_trees:label(CoreTree, NextLabel),
-  {cerl:to_records(LabeledTree), 
+  {cerl:to_records(LabeledTree),
    dialyzer_codeserver:set_next_core_label(NewNextLabel, CServer)}.
 
 store_code_and_build_callgraph(Mod, Core, Callgraph, CServer, NoWarn) ->
@@ -489,7 +489,8 @@ rcv_and_send_ext_types(Parent) ->
   Self = self(),
   Self ! {Self, done},
   ExtTypes = rcv_ext_types(Self, []),
-  Parent ! {Self, ext_types, ExtTypes}.
+  Parent ! {Self, ext_types, ExtTypes},
+  ok.
 
 rcv_ext_types(Self, ExtTypes) ->
   receive
@@ -515,7 +516,7 @@ filter_warnings(LegalWarnings, Warnings) ->
 send_analysis_done(Parent, Plt, DocPlt) ->
   Parent ! {self(), done, Plt, DocPlt},
   ok.
-  
+
 send_ext_calls(Parent, ExtCalls) ->
   Parent ! {self(), ext_calls, ExtCalls},
   ok.
@@ -539,7 +540,7 @@ send_mod_deps(Parent, ModuleDeps) ->
   Parent ! {self(), mod_deps, ModuleDeps},
   ok.
 
-format_bad_calls([{{_, _, _}, {_, module_info, A}}|Left], CodeServer, Acc) 
+format_bad_calls([{{_, _, _}, {_, module_info, A}}|Left], CodeServer, Acc)
   when A =:= 0; A =:= 1 ->
   format_bad_calls(Left, CodeServer, Acc);
 format_bad_calls([{FromMFA, {M, F, A} = To}|Left], CodeServer, Acc) ->
@@ -552,7 +553,7 @@ format_bad_calls([], _CodeServer, Acc) ->
   Acc.
 
 find_call_file_and_line(Tree, MFA) ->
-  Fun = 
+  Fun =
     fun(SubTree, Acc) ->
 	case cerl:is_c_call(SubTree) of
 	  true ->
diff --git a/lib/dialyzer/src/dialyzer_behaviours.erl b/lib/dialyzer/src/dialyzer_behaviours.erl
index 3fae816cfe..47ce9ba6eb 100644
--- a/lib/dialyzer/src/dialyzer_behaviours.erl
+++ b/lib/dialyzer/src/dialyzer_behaviours.erl
@@ -34,19 +34,25 @@
 	 translate_behaviour_api_call/5, translatable_behaviours/1,
 	 translate_callgraph/3]).
 
+-export_type([behaviour/0, behaviour_api_dict/0]).
+
 %%--------------------------------------------------------------------
 
 -include("dialyzer.hrl").
 
 %%--------------------------------------------------------------------
 
+-type behaviour() :: atom().
+
 -record(state, {plt        :: dialyzer_plt:plt(),
 		codeserver :: dialyzer_codeserver:codeserver(),
-		filename   :: string(),
-		behlines   :: [{atom(), number()}]}).
+		filename   :: file:filename(),
+		behlines   :: [{behaviour(), non_neg_integer()}]}).
+
+%%--------------------------------------------------------------------
 
 -spec get_behaviours([module()], dialyzer_codeserver:codeserver()) ->
-  {[atom()], [atom()]}.
+  {[behaviour()], [behaviour()]}.
 
 get_behaviours(Modules, Codeserver) ->
   get_behaviours(Modules, Codeserver, [], []).
@@ -59,29 +65,37 @@ check_callbacks(Module, Attrs, Plt, Codeserver) ->
   {Behaviours, BehLines} = get_behaviours(Attrs),
   case Behaviours of
     [] -> [];
-     _ -> {_Var,Code} =
-	    dialyzer_codeserver:lookup_mfa_code({Module,module_info,0},
-						Codeserver),
-	  File = get_file(cerl:get_ann(Code)),
-	  State = #state{plt = Plt, codeserver = Codeserver, filename = File,
-			 behlines = BehLines},
-	  Warnings = get_warnings(Module, Behaviours, State),
-	  [add_tag_file_line(Module, W, State) || W <- Warnings]
+    _ ->
+      MFA = {Module,module_info,0},
+      {_Var,Code} = dialyzer_codeserver:lookup_mfa_code(MFA, Codeserver),
+      File = get_file(cerl:get_ann(Code)),
+      State = #state{plt = Plt, codeserver = Codeserver, filename = File,
+		     behlines = BehLines},
+      Warnings = get_warnings(Module, Behaviours, State),
+      [add_tag_file_line(Module, W, State) || W <- Warnings]
   end.
 
--spec translatable_behaviours(cerl:c_module()) -> [{atom(),[_]}].
+-spec translatable_behaviours(cerl:c_module()) -> behaviour_api_dict().
 
 translatable_behaviours(Tree) ->
   Attrs = cerl:module_attrs(Tree),
   {Behaviours, _BehLines} = get_behaviours(Attrs),
   [{B, Calls} || B <- Behaviours, (Calls = behaviour_api_calls(B)) =/= []].
 
--spec get_behaviour_apis([atom()]) -> [mfa()].
+-spec get_behaviour_apis([behaviour()]) -> [mfa()].
 
 get_behaviour_apis(Behaviours) ->
   get_behaviour_apis(Behaviours, []).
 
--spec translate_behaviour_api_call(_, _, _, _, _) -> _.
+-spec translate_behaviour_api_call(dialyzer_races:mfa_or_funlbl(),
+				   [erl_types:erl_type()],
+				   [dialyzer_races:core_vars()],
+				   module(),
+				   behaviour_api_dict()) ->
+				      {dialyzer_races:mfa_or_funlbl(),
+				       [erl_types:erl_type()],
+				       [dialyzer_races:core_vars()]}
+					| 'plain_call'.
 
 translate_behaviour_api_call(_Fun, _ArgTypes, _Args, _Module, []) ->
   plain_call;
@@ -101,8 +115,9 @@ translate_behaviour_api_call({Module, Fun, Arity}, ArgTypes, Args,
 translate_behaviour_api_call(_Fun, _ArgTypes, _Args, _Module, _BehApiInfo) ->
   plain_call.
 
--spec translate_callgraph([{atom(), _}], atom(), dialyzer_callgraph:callgraph())
-			  -> dialyzer_callgraph:callgraph().
+-spec translate_callgraph(behaviour_api_dict(), atom(),
+			  dialyzer_callgraph:callgraph()) ->
+			     dialyzer_callgraph:callgraph().
 
 translate_callgraph([{Behaviour,_}|Behaviours], Module, Callgraph) ->
   UsedCalls = [Call || {_From, {M, _F, _A}} = Call <-
@@ -263,7 +278,7 @@ get_line([]) -> -1.
 get_file([{file, File}|_]) -> File;
 get_file([_|Tail]) -> get_file(Tail).
 
-%%------------------------------------------------------------------------------
+%%-----------------------------------------------------------------------------
 
 get_behaviours([], _Codeserver, KnownAcc, UnknownAcc) ->
   {KnownAcc, UnknownAcc};
@@ -292,7 +307,7 @@ call_behaviours([Behaviour|Rest], KnownAcc, UnknownAcc) ->
     _:_ -> call_behaviours(Rest, KnownAcc, [Behaviour | UnknownAcc])
   end.
 
-%-------------------------------------------------------------------------------
+%------------------------------------------------------------------------------
 
 get_behaviour_apis([], Acc) ->
   Acc;
@@ -301,14 +316,22 @@ get_behaviour_apis([Behaviour | Rest], Acc) ->
 	   {{Fun, Arity}, _} <- behaviour_api_calls(Behaviour)],
   get_behaviour_apis(Rest, MFAs ++ Acc).
 
-%-------------------------------------------------------------------------------
+%------------------------------------------------------------------------------
 
 nth_or_0(0, _List, Zero) ->
   Zero;
 nth_or_0(N, List, _Zero) ->
   lists:nth(N, List).
 
-%-------------------------------------------------------------------------------
+%------------------------------------------------------------------------------
+
+-type behaviour_api_dict()::[{behaviour(), behaviour_api_info()}].
+-type behaviour_api_info()::[{original_fun(), replacement_fun()}].
+-type original_fun()::{atom(), arity()}.
+-type replacement_fun()::{atom(), arity(), arg_list()}.
+-type arg_list()::[byte()].
+
+-spec behaviour_api_calls(behaviour()) -> behaviour_api_info().
 
 behaviour_api_calls(gen_server) ->
   [{{start_link, 3}, {init, 1, [2]}},
diff --git a/lib/dialyzer/src/dialyzer_cl.erl b/lib/dialyzer/src/dialyzer_cl.erl
index 1d02c4f0dc..57f0d6e736 100644
--- a/lib/dialyzer/src/dialyzer_cl.erl
+++ b/lib/dialyzer/src/dialyzer_cl.erl
@@ -48,7 +48,7 @@
 	 report_mode     = normal         :: rep_mode(),
 	 return_status= ?RET_NOTHING_SUSPICIOUS	:: dial_ret(),
 	 stored_warnings = []             :: [dial_warning()],
-	 unknown_behaviours = []          :: [atom()]
+	 unknown_behaviours = []          :: [dialyzer_behaviours:behaviour()]
 	}).
 
 %%--------------------------------------------------------------------
@@ -577,7 +577,7 @@ format_log_cache(LogCache) ->
 store_warnings(#cl_state{stored_warnings = StoredWarnings} = St, Warnings) ->
   St#cl_state{stored_warnings = StoredWarnings ++ Warnings}.
 
--spec store_unknown_behaviours(#cl_state{}, [_]) -> #cl_state{}.
+-spec store_unknown_behaviours(#cl_state{}, [dialyzer_behaviours:behaviour()]) -> #cl_state{}.
 
 store_unknown_behaviours(#cl_state{unknown_behaviours = Behs} = St, Beh) ->
   St#cl_state{unknown_behaviours = Beh ++ Behs}.
diff --git a/lib/dialyzer/src/dialyzer_codeserver.erl b/lib/dialyzer/src/dialyzer_codeserver.erl
index 3cf090712c..b2097f7e53 100644
--- a/lib/dialyzer/src/dialyzer_codeserver.erl
+++ b/lib/dialyzer/src/dialyzer_codeserver.erl
@@ -21,7 +21,7 @@
 %%%-------------------------------------------------------------------
 %%% File    : dialyzer_codeserver.erl
 %%% Author  : Tobias Lindahl <[email protected]>
-%%% Description : 
+%%% Description :
 %%%
 %%% Created :  4 Apr 2005 by Tobias Lindahl <[email protected]>
 %%%-------------------------------------------------------------------
@@ -33,7 +33,7 @@
 	 finalize_records/2,
 	 get_contracts/1,
          get_exported_types/1,
-	 get_exports/1, 
+	 get_exports/1,
 	 get_records/1,
 	 get_next_core_label/1,
 	 get_temp_contracts/1,
@@ -86,7 +86,7 @@ new() ->
 delete(#codeserver{table_pid = TablePid}) ->
   table__delete(TablePid).
 
--spec insert(module(), cerl:c_module(), codeserver()) -> codeserver().
+-spec insert(atom(), cerl:c_module(), codeserver()) -> codeserver().
 
 insert(Mod, ModCode, CS) ->
   NewTablePid = table__insert(CS#codeserver.table_pid, Mod, ModCode),
@@ -129,7 +129,7 @@ get_exports(#codeserver{exports = Exports}) ->
 finalize_exported_types(Set, CS) ->
   CS#codeserver{exported_types = Set, temp_exported_types = sets:new()}.
 
--spec lookup_mod_code(module(), codeserver()) -> cerl:c_module().
+-spec lookup_mod_code(atom(), codeserver()) -> cerl:c_module().
 
 lookup_mod_code(Mod, CS) when is_atom(Mod) ->
   table__lookup(CS#codeserver.table_pid, Mod).
@@ -149,7 +149,7 @@ get_next_core_label(#codeserver{next_core_label = NCL}) ->
 set_next_core_label(NCL, CS) ->
   CS#codeserver{next_core_label = NCL}.
 
--spec store_records(module(), dict(), codeserver()) -> codeserver().
+-spec store_records(atom(), dict(), codeserver()) -> codeserver().
 
 store_records(Mod, Dict, #codeserver{records = RecDict} = CS)
   when is_atom(Mod) ->
@@ -158,7 +158,7 @@ store_records(Mod, Dict, #codeserver{records = RecDict} = CS)
     false -> CS#codeserver{records = dict:store(Mod, Dict, RecDict)}
   end.
 
--spec lookup_mod_records(module(), codeserver()) -> dict(). 
+-spec lookup_mod_records(atom(), codeserver()) -> dict().
 
 lookup_mod_records(Mod, #codeserver{records = RecDict})
   when is_atom(Mod) ->
@@ -167,12 +167,12 @@ lookup_mod_records(Mod, #codeserver{records = RecDict})
     {ok, Dict} -> Dict
   end.
 
--spec get_records(codeserver()) -> dict(). 
+-spec get_records(codeserver()) -> dict().
 
 get_records(#codeserver{records = RecDict}) ->
   RecDict.
 
--spec store_temp_records(module(), dict(), codeserver()) -> codeserver().
+-spec store_temp_records(atom(), dict(), codeserver()) -> codeserver().
 
 store_temp_records(Mod, Dict, #codeserver{temp_records = TempRecDict} = CS)
   when is_atom(Mod) ->
@@ -181,7 +181,7 @@ store_temp_records(Mod, Dict, #codeserver{temp_records = TempRecDict} = CS)
     false -> CS#codeserver{temp_records = dict:store(Mod, Dict, TempRecDict)}
   end.
 
--spec get_temp_records(codeserver()) -> dict(). 
+-spec get_temp_records(codeserver()) -> dict().
 
 get_temp_records(#codeserver{temp_records = TempRecDict}) ->
   TempRecDict.
@@ -191,12 +191,12 @@ get_temp_records(#codeserver{temp_records = TempRecDict}) ->
 set_temp_records(Dict, CS) ->
   CS#codeserver{temp_records = Dict}.
 
--spec finalize_records(dict(), codeserver()) -> codeserver(). 
+-spec finalize_records(dict(), codeserver()) -> codeserver().
 
 finalize_records(Dict, CS) ->
   CS#codeserver{records = Dict, temp_records = dict:new()}.
 
--spec store_contracts(module(), dict(), codeserver()) -> codeserver(). 
+-spec store_contracts(atom(), dict(), codeserver()) -> codeserver().
 
 store_contracts(Mod, Dict, #codeserver{contracts = C} = CS) when is_atom(Mod) ->
   case dict:size(Dict) =:= 0 of
@@ -204,7 +204,7 @@ store_contracts(Mod, Dict, #codeserver{contracts = C} = CS) when is_atom(Mod) ->
     false -> CS#codeserver{contracts = dict:store(Mod, Dict, C)}
   end.
 
--spec lookup_mod_contracts(module(), codeserver()) -> dict().
+-spec lookup_mod_contracts(atom(), codeserver()) -> dict().
 
 lookup_mod_contracts(Mod, #codeserver{contracts = ContDict})
   when is_atom(Mod) ->
@@ -213,7 +213,7 @@ lookup_mod_contracts(Mod, #codeserver{contracts = ContDict})
     {ok, Dict} -> Dict
   end.
 
--spec lookup_mfa_contract(mfa(), codeserver()) -> 
+-spec lookup_mfa_contract(mfa(), codeserver()) ->
          'error' | {'ok', dialyzer_contracts:file_contract()}.
 
 lookup_mfa_contract({M,_F,_A} = MFA, #codeserver{contracts = ContDict}) ->
@@ -222,12 +222,12 @@ lookup_mfa_contract({M,_F,_A} = MFA, #codeserver{contracts = ContDict}) ->
     {ok, Dict} -> dict:find(MFA, Dict)
   end.
 
--spec get_contracts(codeserver()) -> dict(). 
+-spec get_contracts(codeserver()) -> dict().
 
 get_contracts(#codeserver{contracts = ContDict}) ->
   ContDict.
 
--spec store_temp_contracts(module(), dict(), codeserver()) -> codeserver(). 
+-spec store_temp_contracts(atom(), dict(), codeserver()) -> codeserver().
 
 store_temp_contracts(Mod, Dict, #codeserver{temp_contracts = C} = CS)
   when is_atom(Mod) ->
@@ -291,7 +291,7 @@ table__loop(Cached, Map) ->
       Pid ! {self(), Mod, Ans},
       table__loop({Mod, Ans}, Map);
     {insert, List} ->
-      NewMap = lists:foldl(fun({Key, Val}, AccMap) -> 
+      NewMap = lists:foldl(fun({Key, Val}, AccMap) ->
 			       dict:store(Key, Val, AccMap)
 			   end, Map, List),
       table__loop(Cached, NewMap)
diff --git a/lib/dialyzer/src/dialyzer_contracts.erl b/lib/dialyzer/src/dialyzer_contracts.erl
index 2bedf99e42..bf80c6f470 100644
--- a/lib/dialyzer/src/dialyzer_contracts.erl
+++ b/lib/dialyzer/src/dialyzer_contracts.erl
@@ -21,7 +21,7 @@
 -module(dialyzer_contracts).
 
 -export([check_contract/2,
-	 check_contracts/3, 
+	 check_contracts/3,
 	 contracts_without_fun/3,
 	 contract_to_string/1,
 	 get_invalid_contract_warnings/3,
@@ -106,13 +106,13 @@ contract_to_string(#contract{forms = Forms}) ->
 contract_to_string_1([{Contract, []}]) ->
   strip_fun(erl_types:t_form_to_string(Contract));
 contract_to_string_1([{Contract, []}|Rest]) ->
-  strip_fun(erl_types:t_form_to_string(Contract)) ++ "\n    ; " 
+  strip_fun(erl_types:t_form_to_string(Contract)) ++ "\n    ; "
     ++ contract_to_string_1(Rest);
 contract_to_string_1([{Contract, Constraints}]) ->
-  strip_fun(erl_types:t_form_to_string(Contract)) ++ " when " 
+  strip_fun(erl_types:t_form_to_string(Contract)) ++ " when "
     ++ constraints_to_string(Constraints);
 contract_to_string_1([{Contract, Constraints}|Rest]) ->
-  strip_fun(erl_types:t_form_to_string(Contract)) ++ " when " 
+  strip_fun(erl_types:t_form_to_string(Contract)) ++ " when "
     ++ constraints_to_string(Constraints) ++ ";" ++
     contract_to_string_1(Rest).
 
@@ -130,7 +130,7 @@ constraints_to_string([{type, _, constraint, [{atom, _, What}, Types]}]) ->
     sequence([erl_types:t_form_to_string(T) || T <- Types], ",") ++ ")";
 constraints_to_string([{type, _, constraint, [{atom, _, What}, Types]}|Rest]) ->
   atom_to_list(What) ++ "(" ++
-    sequence([erl_types:t_form_to_string(T) || T <- Types], ",") 
+    sequence([erl_types:t_form_to_string(T) || T <- Types], ",")
     ++ "), " ++ constraints_to_string(Rest).
 
 sequence([], _Delimiter) -> "";
@@ -156,21 +156,21 @@ process_contract_remote_types(CodeServer) ->
     end,
   NewContractDict = dict:map(ModuleFun, TmpContractDict),
   dialyzer_codeserver:finalize_contracts(NewContractDict, CodeServer).
-  
+
 -spec check_contracts([{mfa(), file_contract()}],
 		      dialyzer_callgraph:callgraph(), dict()) -> plt_contracts().
 
 check_contracts(Contracts, Callgraph, FunTypes) ->
   FoldFun =
-    fun(Label, Type, NewContracts) -> 
+    fun(Label, Type, NewContracts) ->
 	{ok, {M,F,A} = MFA} = dialyzer_callgraph:lookup_name(Label, Callgraph),
 	case orddict:find(MFA, Contracts) of
-	  {ok, {_FileLine, Contract}} -> 
+	  {ok, {_FileLine, Contract}} ->
 	    case check_contract(Contract, Type) of
 	      ok ->
 		case erl_bif_types:is_known(M, F, A) of
 		  true ->
-		    %% Disregard the contracts since 
+		    %% Disregard the contracts since
 		    %% this is a known function.
 		    NewContracts;
 		  false ->
@@ -187,8 +187,8 @@ check_contracts(Contracts, Callgraph, FunTypes) ->
 -spec check_contract(#contract{}, erl_types:erl_type()) -> 'ok' | {'error', term()}.
 
 check_contract(#contract{contracts = Contracts}, SuccType) ->
-  try 
-    Contracts1 = [{Contract, insert_constraints(Constraints, dict:new())} 
+  try
+    Contracts1 = [{Contract, insert_constraints(Constraints, dict:new())}
 		  || {Contract, Constraints} <- Contracts],
     Contracts2 = [erl_types:t_subst(Contract, Dict)
 		  || {Contract, Dict} <- Contracts1],
@@ -197,7 +197,7 @@ check_contract(#contract{contracts = Contracts}, SuccType) ->
       error ->
 	{error, {overlapping_contract, []}};
       ok ->
-	InfList = [erl_types:t_inf(Contract, SuccType, opaque) 
+	InfList = [erl_types:t_inf(Contract, SuccType, opaque)
 		   || Contract <- Contracts2],
 	case check_contract_inf_list(InfList, SuccType) of
 	  {error, _} = Invalid -> Invalid;
@@ -229,7 +229,7 @@ check_contract_inf_list([FunType|Left], SuccType) ->
       STRange = erl_types:t_fun_range(SuccType),
       case erl_types:t_is_none_or_unit(STRange) of
 	true -> ok;
-	false -> 
+	false ->
 	  Range = erl_types:t_fun_range(FunType),
 	  case erl_types:t_is_none(erl_types:t_inf(STRange, Range, opaque)) of
 	    true -> check_contract_inf_list(Left, SuccType);
@@ -261,9 +261,9 @@ check_extraneous_1(Contract, SuccType) ->
 
 process_contracts(OverContracts, Args) ->
   process_contracts(OverContracts, Args, erl_types:t_none()).
-  
+
 process_contracts([OverContract|Left], Args, AccRange) ->
-  NewAccRange = 
+  NewAccRange =
     case process_contract(OverContract, Args) of
       error -> AccRange;
       {ok, Range} -> erl_types:t_sup(AccRange, Range)
@@ -276,12 +276,12 @@ process_contracts([], _Args, AccRange) ->
 
 process_contract({Contract, Constraints}, CallTypes0) ->
   CallTypesFun = erl_types:t_fun(CallTypes0, erl_types:t_any()),
-  ContArgsFun = erl_types:t_fun(erl_types:t_fun_args(Contract), 
+  ContArgsFun = erl_types:t_fun(erl_types:t_fun_args(Contract),
 				erl_types:t_any()),
   ?debug("Instance: Contract:  ~s\n          Arguments: ~s\n",
-	 [erl_types:t_to_string(ContArgsFun), 
+	 [erl_types:t_to_string(ContArgsFun),
 	  erl_types:t_to_string(CallTypesFun)]),
-  case solve_constraints(ContArgsFun, CallTypesFun, Constraints) of 
+  case solve_constraints(ContArgsFun, CallTypesFun, Constraints) of
     {ok, VarDict} ->
       {ok, erl_types:t_subst(erl_types:t_fun_range(Contract), VarDict)};
     error -> error
@@ -291,7 +291,7 @@ solve_constraints(Contract, Call, Constraints) ->
   %% First make sure the call follows the constraints
   CDict = insert_constraints(Constraints, dict:new()),
   Contract1 = erl_types:t_subst(Contract, CDict),
-  %% Just a safe over-approximation. 
+  %% Just a safe over-approximation.
   %% TODO: Find the types for type variables properly
   ContrArgs = erl_types:t_fun_args(Contract1),
   CallArgs = erl_types:t_fun_args(Call),
@@ -312,7 +312,7 @@ solve_constraints(Contract, Call, Constraints) ->
 -spec contracts_without_fun(dict(), [_], dialyzer_callgraph:callgraph()) -> [dial_warning()].
 
 contracts_without_fun(Contracts, AllFuns0, Callgraph) ->
-  AllFuns1 = [{dialyzer_callgraph:lookup_name(Label, Callgraph), Arity} 
+  AllFuns1 = [{dialyzer_callgraph:lookup_name(Label, Callgraph), Arity}
 	      || {Label, Arity} <- AllFuns0],
   AllFuns2 = [{M, F, A} || {{ok, {M, F, _}}, A} <- AllFuns1],
   AllContractMFAs = dict:fetch_keys(Contracts),
@@ -354,9 +354,9 @@ contract_from_form(Forms, RecDict) ->
   {CFuns, Forms1} = contract_from_form(Forms, RecDict, [], []),
   #tmp_contract{contract_funs = CFuns, forms = Forms1}.
 
-contract_from_form([{type, _, 'fun', [_, _]} = Form | Left], RecDict, 
+contract_from_form([{type, _, 'fun', [_, _]} = Form | Left], RecDict,
 		   TypeAcc, FormAcc) ->
-  TypeFun = 
+  TypeFun =
     fun(ExpTypes, AllRecords) ->
 	Type = erl_types:t_from_form(Form, RecDict),
 	NewType = erl_types:t_solve_remote(Type, ExpTypes, AllRecords),
@@ -365,10 +365,10 @@ contract_from_form([{type, _, 'fun', [_, _]} = Form | Left], RecDict,
   NewTypeAcc = [TypeFun | TypeAcc],
   NewFormAcc = [{Form, []} | FormAcc],
   contract_from_form(Left, RecDict, NewTypeAcc, NewFormAcc);
-contract_from_form([{type, _L1, bounded_fun, 
+contract_from_form([{type, _L1, bounded_fun,
 		     [{type, _L2, 'fun', [_, _]} = Form, Constr]}| Left],
 		   RecDict, TypeAcc, FormAcc) ->
-  TypeFun = 
+  TypeFun =
     fun(ExpTypes, AllRecords) ->
 	Constr1 = [constraint_from_form(C, RecDict, ExpTypes, AllRecords)
                    || C <- Constr],
@@ -376,14 +376,14 @@ contract_from_form([{type, _L1, bounded_fun,
 	Type = erl_types:t_from_form(Form, RecDict, VarDict),
 	NewType = erl_types:t_solve_remote(Type, ExpTypes, AllRecords),
 	{NewType, Constr1}
-    end,  
+    end,
   NewTypeAcc = [TypeFun | TypeAcc],
   NewFormAcc = [{Form, Constr} | FormAcc],
   contract_from_form(Left, RecDict, NewTypeAcc, NewFormAcc);
-contract_from_form([], _RecDict, TypeAcc, FormAcc) -> 
+contract_from_form([], _RecDict, TypeAcc, FormAcc) ->
   {lists:reverse(TypeAcc), lists:reverse(FormAcc)}.
 
-constraint_from_form({type, _, constraint, [{atom, _, is_subtype}, 
+constraint_from_form({type, _, constraint, [{atom, _, is_subtype},
 					    [Type1, Type2]]}, RecDict,
                      ExpTypes, AllRecords) ->
   T1 = erl_types:t_from_form(Type1, RecDict),
@@ -396,7 +396,7 @@ constraint_from_form({type, _, constraint, [{atom,_,Name}, List]}, _RecDict,
   N = length(List),
   throw({error, io_lib:format("Unsupported type guard ~w/~w\n", [Name, N])}).
 
-%% Gets the most general domain of a list of domains of all 
+%% Gets the most general domain of a list of domains of all
 %% the overloaded contracts
 
 general_domain(List) ->
@@ -425,7 +425,7 @@ get_invalid_contract_warnings_modules([Mod|Mods], CodeServer, Plt, Acc) ->
 get_invalid_contract_warnings_modules([], _CodeServer, _Plt, Acc) ->
   Acc.
 
-get_invalid_contract_warnings_funs([{MFA, {FileLine, Contract}}|Left], 
+get_invalid_contract_warnings_funs([{MFA, {FileLine, Contract}}|Left],
 				   Plt, RecDict, Acc) ->
   case dialyzer_plt:lookup(Plt, MFA) of
     none ->
@@ -453,15 +453,15 @@ get_invalid_contract_warnings_funs([{MFA, {FileLine, Contract}}|Left],
 		BifRet = erl_bif_types:type(M, F, A),
 		BifSig = erl_types:t_fun(BifArgs, BifRet),
 		case check_contract(Contract, BifSig) of
-		  {error, _} -> 
+		  {error, _} ->
 		    [invalid_contract_warning(MFA, FileLine, BifSig, RecDict)
 		     |Acc];
 		  ok ->
-		    picky_contract_check(CSig, BifSig, MFA, FileLine, 
+		    picky_contract_check(CSig, BifSig, MFA, FileLine,
 					 Contract, RecDict, Acc)
 		end;
 	      false ->
-		picky_contract_check(CSig, Sig, MFA, FileLine, Contract, 
+		picky_contract_check(CSig, Sig, MFA, FileLine, Contract,
 				     RecDict, Acc)
 	    end
 	end,
@@ -485,12 +485,12 @@ picky_contract_check(CSig0, Sig0, MFA, FileLine, Contract, RecDict, Acc) ->
   Sig = erl_types:t_abstract_records(Sig0, RecDict),
   case erl_types:t_is_equal(CSig, Sig) of
     true -> Acc;
-    false -> 
+    false ->
       case (erl_types:t_is_none(erl_types:t_fun_range(Sig)) andalso
 	    erl_types:t_is_unit(erl_types:t_fun_range(CSig))) of
 	true -> Acc;
 	false ->
-	  case extra_contract_warning(MFA, FileLine, Contract, 
+	  case extra_contract_warning(MFA, FileLine, Contract,
 				      CSig, Sig, RecDict) of
 	    no_warning -> Acc;
 	    {warning, Warning} -> [Warning|Acc]
@@ -509,16 +509,16 @@ extra_contract_warning({M, F, A}, FileLine, Contract, CSig, Sig, RecDict) ->
       ContractString = contract_to_string(Contract),
       {Tag, Msg} =
 	case erl_types:t_is_subtype(CSig, Sig) of
-	  true -> 
-	    {?WARN_CONTRACT_SUBTYPE, 
+	  true ->
+	    {?WARN_CONTRACT_SUBTYPE,
 	     {contract_subtype, [M, F, A, ContractString, SigString]}};
 	  false ->
 	    case erl_types:t_is_subtype(Sig, CSig) of
 	      true ->
-		{?WARN_CONTRACT_SUPERTYPE, 
+		{?WARN_CONTRACT_SUPERTYPE,
 		 {contract_supertype, [M, F, A, ContractString, SigString]}};
 	      false ->
-		{?WARN_CONTRACT_NOT_EQUAL, 
+		{?WARN_CONTRACT_NOT_EQUAL,
 		 {contract_diff, [M, F, A, ContractString, SigString]}}
 	    end
 	end,
diff --git a/lib/dialyzer/src/dialyzer_dataflow.erl b/lib/dialyzer/src/dialyzer_dataflow.erl
index a3c7114ee1..b80c7efc1a 100644
--- a/lib/dialyzer/src/dialyzer_dataflow.erl
+++ b/lib/dialyzer/src/dialyzer_dataflow.erl
@@ -21,7 +21,7 @@
 %%%-------------------------------------------------------------------
 %%% File    : dialyzer_dataflow.erl
 %%% Author  : Tobias Lindahl <[email protected]>
-%%% Description : 
+%%% Description :
 %%%
 %%% Created : 19 Apr 2005 by Tobias Lindahl <[email protected]>
 %%%-------------------------------------------------------------------
@@ -30,6 +30,7 @@
 
 -export([get_fun_types/4, get_warnings/5, format_args/3]).
 
+%% Data structure interfaces.
 -export([state__add_warning/2, state__cleanup/1,
          state__get_callgraph/1, state__get_races/1,
          state__get_records/1, state__put_callgraph/2,
@@ -42,7 +43,7 @@
 
 -include("dialyzer.hrl").
 
--import(erl_types, 
+-import(erl_types,
 	[any_none/1, t_any/0, t_atom/0, t_atom/1, t_atom_vals/1,
 	 t_binary/0, t_boolean/0,
 	 t_bitstr/0, t_bitstr/2, t_bitstr_concat/1, t_bitstr_match/2,
@@ -90,14 +91,15 @@
 		fun_tab		     :: dict(),
 		plt		     :: dialyzer_plt:plt(),
 		opaques              :: [erl_types:erl_type()],
-		races                :: dialyzer_races:races(),
-		records              :: dict(),
+		races = dialyzer_races:new() :: dialyzer_races:races(),
+		records = dict:new() :: dict(),
 		tree_map	     :: dict(),
 		warning_mode = false :: boolean(),
 		warnings = []        :: [dial_warning()],
 		work                 :: {[_], [_], set()},
 		module               :: module(),
-		behaviour_api_info = [] :: [{atom(),[_]}]}).
+		behaviour_api_dict = [] ::
+		  dialyzer_behaviours:behaviour_api_dict()}).
 
 %% Exported Types
 
@@ -165,20 +167,20 @@ get_top_level_signatures(Code, Records) ->
 				error ->
 				  Arity = cerl:fname_arity(V),
 				  Type = t_fun(lists:duplicate(Arity,
-							       t_none()), 
+							       t_none()),
 					       t_none()),
 				  dict:store(Label, Type, Acc);
 				{ok, _} -> Acc
 			      end
 			  end, FunTypes, cerl:module_defs(Tree)),
   dialyzer_callgraph:delete(Callgraph),
-  Sigs = [{{cerl:fname_id(V), cerl:fname_arity(V)}, 
-	   dict:fetch(get_label(F), FunTypes1)} 
+  Sigs = [{{cerl:fname_id(V), cerl:fname_arity(V)},
+	   dict:fetch(get_label(F), FunTypes1)}
 	  || {V, F} <- cerl:module_defs(Tree)],
   ordsets:from_list(Sigs).
 
 get_def_plt() ->
-  try 
+  try
     dialyzer_plt:from_file(dialyzer_plt:get_default_plt())
   catch
     throw:{dialyzer_error, _} -> dialyzer_plt:new()
@@ -204,7 +206,7 @@ annotate_module(Code, Plt) ->
 annotate(Tree, State) ->
   case cerl:subtrees(Tree) of
     [] -> set_type(Tree, State);
-    List -> 
+    List ->
       NewSubTrees = [[annotate(Subtree, State) || Subtree <- Group]
 		     || Group <- List],
       NewTree = cerl:update_tree(Tree, NewSubTrees),
@@ -216,9 +218,9 @@ set_type(Tree, State) ->
     'fun' ->
       Type = state__fun_type(Tree, State),
       case t_is_any(Type) of
-	true -> 
+	true ->
 	  cerl:set_ann(Tree, delete_ann(typesig, cerl:get_ann(Tree)));
-	false -> 
+	false ->
 	  cerl:set_ann(Tree, append_ann(typesig, Type, cerl:get_ann(Tree)))
       end;
     apply ->
@@ -226,10 +228,10 @@ set_type(Tree, State) ->
 	unknown -> Tree;
 	ReturnType ->
 	  case t_is_any(ReturnType) of
-	    true -> 
+	    true ->
 	      cerl:set_ann(Tree, delete_ann(type, cerl:get_ann(Tree)));
-	    false -> 
-	      cerl:set_ann(Tree, append_ann(type, ReturnType, 
+	    false ->
+	      cerl:set_ann(Tree, append_ann(type, ReturnType,
 					    cerl:get_ann(Tree)))
 	  end
       end;
@@ -238,7 +240,7 @@ set_type(Tree, State) ->
   end.
 
 append_ann(Tag, Val, [X | Xs]) ->
-  if tuple_size(X) >= 1, element(1, X) =:= Tag -> 
+  if tuple_size(X) >= 1, element(1, X) =:= Tag ->
       append_ann(Tag, Val, Xs);
      true ->
       [X | append_ann(Tag, Val, Xs)]
@@ -247,7 +249,7 @@ append_ann(Tag, Val, []) ->
   [{Tag, Val}].
 
 delete_ann(Tag, [X | Xs]) ->
-  if tuple_size(X) >= 1, element(1, X) =:= Tag -> 
+  if tuple_size(X) >= 1, element(1, X) =:= Tag ->
       delete_ann(Tag, Xs);
      true ->
       [X | delete_ann(Tag, Xs)]
@@ -316,21 +318,21 @@ analyze_loop(#state{callgraph = Callgraph, races = Races} = State) ->
     {Fun, NewState} ->
       ArgTypes = state__get_args(Fun, NewState),
       case any_none(ArgTypes) of
-	true -> 
-	  ?debug("Not handling1 ~w: ~s\n", 
-		 [state__lookup_name(get_label(Fun), State), 
+	true ->
+	  ?debug("Not handling1 ~w: ~s\n",
+		 [state__lookup_name(get_label(Fun), State),
 		  t_to_string(t_product(ArgTypes))]),
 	  analyze_loop(NewState);
-	false -> 
+	false ->
 	  case state__fun_env(Fun, NewState) of
-	    none -> 
-	      ?debug("Not handling2 ~w: ~s\n", 
-		     [state__lookup_name(get_label(Fun), State), 
+	    none ->
+	      ?debug("Not handling2 ~w: ~s\n",
+		     [state__lookup_name(get_label(Fun), State),
 		      t_to_string(t_product(ArgTypes))]),
 	      analyze_loop(NewState);
 	    Map ->
-	      ?debug("Handling fun ~p: ~s\n", 
-		     [state__lookup_name(get_label(Fun), State), 
+	      ?debug("Handling fun ~p: ~s\n",
+		     [state__lookup_name(get_label(Fun), State),
 		      t_to_string(state__fun_type(Fun, NewState))]),
 	      NewState1 = state__mark_fun_as_handled(NewState, Fun),
 	      Vars = cerl:fun_vars(Fun),
@@ -341,19 +343,19 @@ analyze_loop(#state{callgraph = Callgraph, races = Races} = State) ->
               RaceAnalysis = dialyzer_races:get_race_analysis(Races),
               NewState3 =
                 case RaceDetection andalso RaceAnalysis of
-                  true ->             
+                  true ->
                     NewState2 = state__renew_curr_fun(
                       state__lookup_name(FunLabel, NewState1), FunLabel,
                       NewState1),
                     state__renew_race_list([], 0, NewState2);
 		  false -> NewState1
                 end,
-	      {NewState4, _Map2, BodyType} = 
+	      {NewState4, _Map2, BodyType} =
 		traverse(Body, Map1, NewState3),
-	      ?debug("Done analyzing: ~w:~s\n", 
+	      ?debug("Done analyzing: ~w:~s\n",
 		     [state__lookup_name(get_label(Fun), State),
 		      t_to_string(t_fun(ArgTypes, BodyType))]),
-              NewState5 = 
+              NewState5 =
                 case RaceDetection andalso RaceAnalysis of
                   true ->
 		    Races1 = NewState4#state.races,
@@ -384,7 +386,7 @@ traverse(Tree, Map, State) ->
       %% This only happens when checking for illegal record patterns
       %% so the handling is a bit rudimentary.
       traverse(cerl:alias_pat(Tree), Map, State);
-    apply -> 
+    apply ->
       handle_apply(Tree, Map, State);
     binary ->
       Segs = cerl:binary_segments(Tree),
@@ -418,7 +420,7 @@ traverse(Tree, Map, State) ->
       %% By not including the variables in scope we can assure that we
       %% will get the current function type when using the variables.
       FoldFun = fun({Var, Fun}, {AccState, AccMap}) ->
-		    {NewAccState, NewAccMap0, FunType} = 
+		    {NewAccState, NewAccMap0, FunType} =
 		      traverse(Fun, AccMap, AccState),
 		    NewAccMap = enter_type(Var, FunType, NewAccMap0),
 		    {NewAccState, NewAccMap}
@@ -430,7 +432,7 @@ traverse(Tree, Map, State) ->
       case cerl:unfold_literal(Tree) of
 	Tree ->
 	  Type = literal_type(Tree),
-	  NewType = 
+	  NewType =
 	    case erl_types:t_opaque_match_atom(Type, State#state.opaques) of
 	      [Opaque] -> Opaque;
 	      _ -> Type
@@ -448,8 +450,8 @@ traverse(Tree, Map, State) ->
 	  bs_init_writable -> t_from_term(<<>>);
 	  Other -> erlang:error({'Unsupported primop', Other})
 	end,
-      {State, Map, Type};      
-    'receive' -> 
+      {State, Map, Type};
+    'receive' ->
       handle_receive(Tree, Map, State);
     seq ->
       Arg = cerl:seq_arg(Tree),
@@ -459,13 +461,13 @@ traverse(Tree, Map, State) ->
 	true ->
 	  SMA;
 	false ->
-	  State2 = 
+	  State2 =
 	    case (t_is_any(ArgType) orelse t_is_simple(ArgType)
 		                    orelse is_call_to_send(Arg)) of
 	      true -> % do not warn in these cases
 		State1;
 	      false ->
-		state__add_warning(State1, ?WARN_UNMATCHED_RETURN, Arg, 
+		state__add_warning(State1, ?WARN_UNMATCHED_RETURN, Arg,
 				   {unmatched_return,
 				    [format_type(ArgType, State1)]})
 	    end,
@@ -483,12 +485,12 @@ traverse(Tree, Map, State) ->
     var ->
       ?debug("Looking up unknown variable: ~p\n", [Tree]),
       case state__lookup_type_for_rec_var(Tree, State) of
-	error -> 
+	error ->
 	  LType = lookup_type(Tree, Map),
 	  Opaques = State#state.opaques,
 	  case t_opaque_match_record(LType, Opaques) of
 	    [Opaque] -> {State, Map, Opaque};
-	    _ -> 
+	    _ ->
 	      case t_opaque_match_atom(LType, Opaques) of
 		[Opaque] -> {State, Map, Opaque};
 		_ -> {State, Map, LType}
@@ -508,7 +510,7 @@ traverse_list([Tree|Tail], Map, State, Acc) ->
   traverse_list(Tail, Map1, State1, [Type|Acc]);
 traverse_list([], Map, State, Acc) ->
   {State, Map, lists:reverse(Acc)}.
-  
+
 %%________________________________________
 %%
 %% Special instructions
@@ -520,7 +522,7 @@ handle_apply(Tree, Map, State) ->
   {State1, Map1, ArgTypes} = traverse_list(Args, Map, State),
   {State2, Map2, OpType} = traverse(Op, Map1, State1),
   case any_none(ArgTypes) of
-    true -> 
+    true ->
       {State2, Map2, t_none()};
     false ->
       {CallSitesKnown, FunList} =
@@ -535,7 +537,7 @@ handle_apply(Tree, Map, State) ->
 	  OpType1 = t_inf(OpType, t_fun(Arity, t_any())),
 	  case t_is_none(OpType1) of
 	    true ->
-	      Msg = {fun_app_no_fun, 
+	      Msg = {fun_app_no_fun,
 		     [format_cerl(Op), format_type(OpType, State2), Arity]},
 	      State3 = state__add_warning(State2, ?WARN_FAILING_CALL,
 					  Tree, Msg),
@@ -543,7 +545,7 @@ handle_apply(Tree, Map, State) ->
 	    false ->
 	      NewArgs = t_inf_lists(ArgTypes, t_fun_args(OpType1)),
 	      case any_none(NewArgs) of
-		true -> 
+		true ->
 		  Msg = {fun_app_args,
 			 [format_args(Args, ArgTypes, State),
 			  format_type(OpType, State)]},
@@ -556,7 +558,7 @@ handle_apply(Tree, Map, State) ->
 	      end
 	  end;
 	true ->
-	  FunInfoList = [{local, state__fun_info(Fun, State)} 
+	  FunInfoList = [{local, state__fun_info(Fun, State)}
 			 || Fun <- FunList],
 	  handle_apply_or_call(FunInfoList, Args, ArgTypes, Map2, Tree, State1)
       end
@@ -564,7 +566,7 @@ handle_apply(Tree, Map, State) ->
 
 handle_apply_or_call(FunInfoList, Args, ArgTypes, Map, Tree, State) ->
   None = t_none(),
-  handle_apply_or_call(FunInfoList, Args, ArgTypes, Map, Tree, State, 
+  handle_apply_or_call(FunInfoList, Args, ArgTypes, Map, Tree, State,
 		       [None || _ <- ArgTypes], None).
 
 handle_apply_or_call([{local, external}|Left], Args, ArgTypes, Map, Tree, State,
@@ -579,7 +581,7 @@ handle_apply_or_call([{TypeOfApply, {Fun, Sig, Contr, LocalRet}}|Left],
   Any = t_any(),
   AnyArgs = [Any || _ <- Args],
   GenSig = {AnyArgs, fun(_) -> t_any() end},
-  {CArgs, CRange} = 
+  {CArgs, CRange} =
     case Contr of
       {value, #contract{args = As} = C} ->
 	{As, fun(FunArgs) ->
@@ -629,9 +631,9 @@ handle_apply_or_call([{TypeOfApply, {Fun, Sig, Contr, LocalRet}}|Left],
 	end
     end,
   ArgModeMask = [case lists:member(Arg, Opaques) of
-	       true -> opaque;
-	       false -> structured
-	     end || Arg <- ArgTypes],
+                   true -> opaque;
+                   false -> structured
+                 end || Arg <- ArgTypes],
   NewArgsSig = t_inf_lists_masked(SigArgs, ArgTypes, ArgModeMask),
   NewArgsContract = t_inf_lists_masked(CArgs, ArgTypes, ArgModeMask),
   NewArgsBif = t_inf_lists_masked(BifArgs, ArgTypes, ArgModeMask),
@@ -639,7 +641,7 @@ handle_apply_or_call([{TypeOfApply, {Fun, Sig, Contr, LocalRet}}|Left],
   NewArgTypes = t_inf_lists_masked(NewArgTypes0, NewArgsBif, ArgModeMask),
   BifRet = BifRange(NewArgTypes),
   {TmpArgTypes, TmpArgsContract} =
-    case (TypeOfApply == remote) andalso (not IsBIF) of
+    case (TypeOfApply =:= remote) andalso (not IsBIF) of
       true ->
 	List1 = lists:zip(CArgs, NewArgTypes),
 	List2 = lists:zip(CArgs, NewArgsContract),
@@ -650,16 +652,17 @@ handle_apply_or_call([{TypeOfApply, {Fun, Sig, Contr, LocalRet}}|Left],
       false  -> {NewArgTypes, NewArgsContract}
     end,
   ContrRet = CRange(TmpArgTypes),
-  RetMode = case t_contains_opaque(ContrRet) orelse t_contains_opaque(BifRet) of
-	   true  -> opaque;
-	   false -> structured
-	 end,
+  RetMode =
+    case t_contains_opaque(ContrRet) orelse t_contains_opaque(BifRet) of
+      true  -> opaque;
+      false -> structured
+    end,
   RetWithoutLocal = t_inf(t_inf(ContrRet, BifRet, RetMode), SigRange, RetMode),
   ?debug("--------------------------------------------------------\n", []),
   ?debug("Fun: ~p\n", [Fun]),
   ?debug("Args: ~s\n", [erl_types:t_to_string(t_product(ArgTypes))]),
   ?debug("NewArgsSig: ~s\n", [erl_types:t_to_string(t_product(NewArgsSig))]),
-  ?debug("NewArgsContract: ~s\n", 
+  ?debug("NewArgsContract: ~s\n",
 	 [erl_types:t_to_string(t_product(NewArgsContract))]),
   ?debug("NewArgsBif: ~s\n", [erl_types:t_to_string(t_product(NewArgsBif))]),
   ?debug("NewArgTypes: ~s\n", [erl_types:t_to_string(t_product(NewArgTypes))]),
@@ -679,11 +682,11 @@ handle_apply_or_call([{TypeOfApply, {Fun, Sig, Contr, LocalRet}}|Left],
 	%%               respective callback module's function.
 
 	Module = State#state.module,
-	BehApiInfo = State#state.behaviour_api_info,
+	BehApiDict = State#state.behaviour_api_dict,
 	{RealFun, RealArgTypes, RealArgs} =
 	  case dialyzer_behaviours:translate_behaviour_api_call(Fun, ArgTypes,
 								Args, Module,
-								BehApiInfo) of
+								BehApiDict) of
 	    plain_call    -> {Fun, ArgTypes, Args};
 	    BehaviourAPI  -> BehaviourAPI
 	  end,
@@ -700,10 +703,10 @@ handle_apply_or_call([{TypeOfApply, {Fun, Sig, Contr, LocalRet}}|Left],
 	FailedSig = any_none(NewArgsSig),
 	FailedContract = any_none([CRange(TmpArgsContract)|NewArgsContract]),
 	FailedBif = any_none([BifRange(NewArgsBif)|NewArgsBif]),
-	InfSig = t_inf(t_fun(SigArgs, SigRange), 
+	InfSig = t_inf(t_fun(SigArgs, SigRange),
 		       t_fun(BifArgs, BifRange(BifArgs))),
 	FailReason = apply_fail_reason(FailedSig, FailedBif, FailedContract),
-        Msg = get_apply_fail_msg(Fun, Args, ArgTypes, NewArgTypes, InfSig, 
+        Msg = get_apply_fail_msg(Fun, Args, ArgTypes, NewArgTypes, InfSig,
 				 Contr, CArgs, State1, FailReason),
 	WarnType = case Msg of
 		     {call, _} -> ?WARN_FAILING_CALL;
@@ -727,15 +730,15 @@ handle_apply_or_call([{TypeOfApply, {Fun, Sig, Contr, LocalRet}}|Left],
       remote ->
         add_bif_warnings(Fun, NewArgTypes, Tree, State2)
     end,
-  NewAccArgTypes = 
+  NewAccArgTypes =
     case FailedConj of
       true -> AccArgTypes;
       false -> [t_sup(X, Y) || {X, Y} <- lists:zip(NewArgTypes, AccArgTypes)]
     end,
   NewAccRet = t_sup(AccRet, t_inf(RetWithoutLocal, LocalRet, opaque)),
-  handle_apply_or_call(Left, Args, ArgTypes, Map, Tree, 
+  handle_apply_or_call(Left, Args, ArgTypes, Map, Tree,
 		       State3, NewAccArgTypes, NewAccRet);
-handle_apply_or_call([], Args, _ArgTypes, Map, _Tree, State, 
+handle_apply_or_call([], Args, _ArgTypes, Map, _Tree, State,
 		     AccArgTypes, AccRet) ->
   NewMap = enter_type_lists(Args, AccArgTypes, Map),
   {State, NewMap, AccRet}.
@@ -747,13 +750,13 @@ apply_fail_reason(FailedSig, FailedBif, FailedContract) ->
     true                                                      -> both
   end.
 
-get_apply_fail_msg(Fun, Args, ArgTypes, NewArgTypes, 
+get_apply_fail_msg(Fun, Args, ArgTypes, NewArgTypes,
 		   Sig, Contract, ContrArgs, State, FailReason) ->
   ArgStrings = format_args(Args, ArgTypes, State),
   ContractInfo =
     case Contract of
       {value, #contract{} = C} ->
-	{dialyzer_contracts:is_overloaded(C), 
+	{dialyzer_contracts:is_overloaded(C),
 	 dialyzer_contracts:contract_to_string(C)};
       none -> {false, none}
     end,
@@ -767,7 +770,7 @@ get_apply_fail_msg(Fun, Args, ArgTypes, NewArgTypes,
     {M, F, _A} ->
       case is_opaque_type_test_problem(Fun, NewArgTypes, State) of
 	true ->
-	  [Opaque] = NewArgTypes, 
+	  [Opaque] = NewArgTypes,
 	  {opaque_type_test, [atom_to_list(F), erl_types:t_to_string(Opaque)]};
 	false ->
 	  SigArgs = t_fun_args(Sig),
@@ -791,7 +794,7 @@ get_apply_fail_msg(Fun, Args, ArgTypes, NewArgTypes,
 		  {call_without_opaque, [M, F, ArgStrings, ExpectedTriples]};
 		false -> %% there is a structured term clash in some argument
 		  {call, [M, F, ArgStrings,
-			  ArgNs, FailReason, 
+			  ArgNs, FailReason,
 			  format_sig_args(Sig, State),
 			  format_type(t_fun_range(Sig), State),
 			  ContractInfo]}
@@ -799,8 +802,8 @@ get_apply_fail_msg(Fun, Args, ArgTypes, NewArgTypes,
 	  end
       end;
     Label when is_integer(Label) ->
-      {apply, [ArgStrings, 
-	       ArgNs, FailReason, 
+      {apply, [ArgStrings,
+	       ArgNs, FailReason,
 	       format_sig_args(Sig, State),
 	       format_type(t_fun_range(Sig), State),
 	       ContractInfo]}
@@ -828,7 +831,7 @@ is_opaque_type_test_problem(Fun, ArgTypes, State) ->
 			 FN =:= is_number;    FN =:= is_pid; FN =:= is_port;
 			 FN =:= is_reference; FN =:= is_tuple ->
       [Type] = ArgTypes,
-      erl_types:t_is_opaque(Type) andalso 
+      erl_types:t_is_opaque(Type) andalso
 	not lists:member(Type, State#state.opaques);
     _ -> false
   end.
@@ -1045,7 +1048,7 @@ handle_cons(Tree, Map, State) ->
   Tl = cerl:cons_tl(Tree),
   {State1, Map1, HdType} = traverse(Hd, Map, State),
   {State2, Map2, TlType} = traverse(Tl, Map1, State1),
-  State3 = 
+  State3 =
     case t_is_none(t_inf(TlType, t_list())) of
       true ->
 	Msg = {improper_list_constr, [format_type(TlType, State2)]},
@@ -1090,7 +1093,7 @@ handle_let(Tree, Map, #state{callgraph = Callgraph, races = Races} = State) ->
         case cerl:is_literal(Mod) andalso
              cerl:concrete(Mod) =:= ets andalso
              cerl:is_literal(Name) andalso
-             cerl:concrete(Name) =:= new of            
+             cerl:concrete(Name) =:= new of
           true ->
             NewTable = dialyzer_races:get_new_table(State1#state.races),
             renew_public_tables(Vars, NewTable,
@@ -1114,7 +1117,7 @@ handle_module(Tree, Map, State) ->
   %% By not including the variables in scope we can assure that we
   %% will get the current function type when using the variables.
   Defs = cerl:module_defs(Tree),
-  PartFun = fun({_Var, Fun}) -> 
+  PartFun = fun({_Var, Fun}) ->
 		state__is_escaping(get_label(Fun), State)
 	    end,
   {Defs1, Defs2} = lists:partition(PartFun, Defs),
@@ -1145,12 +1148,12 @@ handle_receive(Tree, Map,
                                RaceListSize + 1, State);
       false -> State
     end,
-  {MapList, State2, ReceiveType} = 
+  {MapList, State2, ReceiveType} =
     handle_clauses(Clauses, ?no_arg, t_any(), t_any(), State1, [], Map,
                    [], []),
   Map1 = join_maps(MapList, Map),
   {State3, Map2, TimeoutType} = traverse(Timeout, Map1, State2),
-  case (t_is_atom(TimeoutType) andalso 
+  case (t_is_atom(TimeoutType) andalso
 	(t_atom_vals(TimeoutType) =:= ['infinity'])) of
     true ->
       {State3, Map2, ReceiveType};
@@ -1170,17 +1173,17 @@ handle_try(Tree, Map, State) ->
   Vars = cerl:try_vars(Tree),
   Body = cerl:try_body(Tree),
   Handler = cerl:try_handler(Tree),
-  {State1, Map1, ArgType} = traverse(Arg, Map, State),      
+  {State1, Map1, ArgType} = traverse(Arg, Map, State),
   Map2 = mark_as_fresh(Vars, Map1),
   {SuccState, SuccMap, SuccType} =
     case bind_pat_vars(Vars, t_to_tlist(ArgType), [], Map2, State1) of
       {error, _, _, _, _} ->
 	{State1, map__new(), t_none()};
       {SuccMap1, VarTypes} ->
-	%% Try to bind the argument. Will only succeed if 
+	%% Try to bind the argument. Will only succeed if
 	%% it is a simple structured term.
 	SuccMap2 =
-	  case bind_pat_vars_reverse([Arg], [t_product(VarTypes)], [], 
+	  case bind_pat_vars_reverse([Arg], [t_product(VarTypes)], [],
 				     SuccMap1, State1) of
 	    {error, _, _, _, _} -> SuccMap1;
 	    {SM, _} -> SM
@@ -1214,10 +1217,10 @@ handle_tuple(Tree, Map, State) ->
 		  RecFields = t_tuple_args(RecStruct),
 		  case bind_pat_vars(Elements, RecFields, [], Map1, State1) of
 		    {error, _, ErrorPat, ErrorType, _} ->
-		      Msg = {record_constr, 
+		      Msg = {record_constr,
 			     [TagVal, format_patterns(ErrorPat),
 			      format_type(ErrorType, State1)]},
-		      State2 = state__add_warning(State1, ?WARN_MATCHING, 
+		      State2 = state__add_warning(State1, ?WARN_MATCHING,
 						  Tree, Msg),
 		      {State2, Map1, t_none()};
 		    {Map2, _ETypes} ->
@@ -1226,26 +1229,24 @@ handle_tuple(Tree, Map, State) ->
 		_ ->
 		  case state__lookup_record(TagVal, length(Left), State1) of
 		    error -> {State1, Map1, TupleType};
-		    {ok, Prototype} ->
-		      %% io:format("In handle_tuple:\n  Prototype = ~p\n", [Prototype]),
-		      InfTupleType = t_inf(Prototype, TupleType),
-		      %% io:format("  TupleType = ~p,\n  Inf = ~p\n", [TupleType, InfTupleType]),
+		    {ok, RecType} ->
+		      InfTupleType = t_inf(RecType, TupleType),
 		      case t_is_none(InfTupleType) of
 			true ->
-			  Msg = {record_constr, 
-				 [format_type(TupleType, State1), TagVal]},
-			  State2 = state__add_warning(State1, ?WARN_MATCHING, 
+			  RecC = format_type(TupleType, State1),
+			  FieldDiffs = format_field_diffs(TupleType, State1),
+			  Msg = {record_constr, [RecC, FieldDiffs]},
+			  State2 = state__add_warning(State1, ?WARN_MATCHING,
 						      Tree, Msg),
 			  {State2, Map1, t_none()};
 			false ->
-			  case bind_pat_vars(Elements, t_tuple_args(Prototype),
+			  case bind_pat_vars(Elements, t_tuple_args(RecType),
 					     [], Map1, State1) of
 			    {error, bind, ErrorPat, ErrorType, _} ->
-			      %% io:format("error\n", []),
-			      Msg = {record_constr, 
+			      Msg = {record_constr,
 				     [TagVal, format_patterns(ErrorPat),
 				      format_type(ErrorType, State1)]},
-			      State2 = state__add_warning(State1, ?WARN_MATCHING, 
+			      State2 = state__add_warning(State1, ?WARN_MATCHING,
 							  Tree, Msg),
 			      {State2, Map1, t_none()};
 			    {Map2, ETypes} ->
@@ -1307,7 +1308,7 @@ handle_clauses([C|Left], Arg, ArgType, OrigArgType,
 handle_clauses([], _Arg, _ArgType, _OrigArgType,
 	       #state{callgraph = Callgraph, races = Races} = State,
                CaseTypes, _MapIn, Acc, ClauseAcc) ->
-  State1 = 
+  State1 =
     case dialyzer_callgraph:get_race_detection(Callgraph) andalso
          dialyzer_races:get_race_analysis(Races) of
       true ->
@@ -1315,7 +1316,7 @@ handle_clauses([], _Arg, _ArgType, _OrigArgType,
           [dialyzer_races:end_case_new(ClauseAcc)|
            dialyzer_races:get_race_list(Races)],
           dialyzer_races:get_race_list_size(Races) + 1, State);
-      false -> State 
+      false -> State
     end,
   {lists:reverse(Acc), State1, t_sup(CaseTypes)}.
 
@@ -1326,7 +1327,7 @@ do_clause(C, Arg, ArgType0, OrigArgType, Map,
   Body = cerl:clause_body(C),
   RaceDetection = dialyzer_callgraph:get_race_detection(Callgraph),
   RaceAnalysis = dialyzer_races:get_race_analysis(Races),
-  State1 = 
+  State1 =
     case RaceDetection andalso RaceAnalysis of
       true ->
         state__renew_fun_args(Pats, State);
@@ -1341,7 +1342,7 @@ do_clause(C, Arg, ArgType0, OrigArgType, Map,
       true ->
 	{error, bind, Pats, ArgType0, ArgType0};
       false ->
-	ArgTypes = 
+	ArgTypes =
 	  case t_is_any(ArgType0) of
 	    true -> [ArgType0 || _ <- Pats];
 	    false -> t_to_tlist(ArgType0)
@@ -1350,7 +1351,7 @@ do_clause(C, Arg, ArgType0, OrigArgType, Map,
     end,
   case BindRes of
     {error, BindOrOpaque, NewPats, Type, OpaqueTerm} ->
-      ?debug("Failed binding pattern: ~s\nto ~s\n", 
+      ?debug("Failed binding pattern: ~s\nto ~s\n",
 	     [cerl_prettypr:format(C), format_type(ArgType0, State1)]),
       case state__warning_mode(State1) of
         false ->
@@ -1361,7 +1362,7 @@ do_clause(C, Arg, ArgType0, OrigArgType, Map,
 	      bind   -> format_patterns(Pats);
 	      opaque -> format_patterns(NewPats)
 	    end,
-	  {Msg, Force} = 
+	  {Msg, Force} =
 	    case t_is_none(ArgType0) of
 	      true ->
 		PatTypes = [PatString, format_type(OrigArgType, State1)],
@@ -1377,13 +1378,13 @@ do_clause(C, Arg, ArgType0, OrigArgType, Map,
 		  {_, _} -> {{pattern_match_cov, PatTypes}, false}
 		end;
 	      false ->
-		%% Try to find out if this is a default clause in a list 
+		%% Try to find out if this is a default clause in a list
 		%% comprehension and supress this. A real Hack(tm)
 		Force0 =
 		  case is_compiler_generated(cerl:get_ann(C)) of
 		    true ->
 		      case Pats of
-			[Pat] -> 
+			[Pat] ->
 			  case cerl:is_c_cons(Pat) of
 			    true ->
 			      not (cerl:is_c_var(cerl:cons_hd(Pat)) andalso
@@ -1400,9 +1401,9 @@ do_clause(C, Arg, ArgType0, OrigArgType, Map,
 		  end,
 		PatTypes = case BindOrOpaque of
 			     bind -> [PatString, format_type(ArgType0, State1)];
-			     opaque -> [PatString, format_type(Type, State1), 
+			     opaque -> [PatString, format_type(Type, State1),
 					format_type(OpaqueTerm, State1)]
-			      end,					
+			      end,
 		FailedMsg = case BindOrOpaque of
 			      bind  -> {pattern_match, PatTypes};
 			      opaque -> {opaque_match, PatTypes}
@@ -1422,9 +1423,9 @@ do_clause(C, Arg, ArgType0, OrigArgType, Map,
 	case Arg =:= ?no_arg of
 	  true -> Map2;
 	  false ->
-	    %% Try to bind the argument. Will only succeed if 
+	    %% Try to bind the argument. Will only succeed if
 	    %% it is a simple structured term.
-	    case bind_pat_vars_reverse([Arg], [t_product(PatTypes)], 
+	    case bind_pat_vars_reverse([Arg], [t_product(PatTypes)],
 				       [], Map2, State1) of
 	      {error, _, _, _, _} -> Map2;
 	      {NewMap, _} -> NewMap
@@ -1438,11 +1439,11 @@ do_clause(C, Arg, ArgType0, OrigArgType, Map,
 	    t_subtract(t_product(t_to_tlist(ArgType0)), GenType)
 	end,
       case bind_guard(Guard, Map3, State1) of
-	{error, Reason} -> 
-	  ?debug("Failed guard: ~s\n", 
+	{error, Reason} ->
+	  ?debug("Failed guard: ~s\n",
 		 [cerl_prettypr:format(C, [{hook, cerl_typean:pp_hook()}])]),
 	  PatString = format_patterns(Pats),
-	  DefaultMsg = 
+	  DefaultMsg =
 	    case Pats =:= [] of
 	      true -> {guard_fail, []};
 	      false ->
@@ -1472,7 +1473,7 @@ do_clause(C, Arg, ArgType0, OrigArgType, Map,
 
 bind_subst(Arg, Pats, Map) ->
   case cerl:type(Arg) of
-    values -> 
+    values ->
       bind_subst_list(cerl:values_es(Arg), Pats, Map);
     var ->
       [Pat] = Pats,
@@ -1501,16 +1502,16 @@ bind_subst_list([], [], Map) ->
 %%
 
 bind_pat_vars(Pats, Types, Acc, Map, State) ->
-  try 
+  try
     bind_pat_vars(Pats, Types, Acc, Map, State, false)
-  catch 
+  catch
     throw:Error -> Error % Error = {error, bind | opaque, ErrorPats, ErrorType}
   end.
 
 bind_pat_vars_reverse(Pats, Types, Acc, Map, State) ->
-  try 
+  try
     bind_pat_vars(Pats, Types, Acc, Map, State, true)
-  catch 
+  catch
     throw:Error -> Error % Error = {error, bind | opaque, ErrorPats, ErrorType}
   end.
 
@@ -1522,7 +1523,7 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
 	AliasPat = cerl:alias_pat(Pat),
 	Var = cerl:alias_var(Pat),
 	Map1 = enter_subst(Var, AliasPat, Map),
-	{Map2, [PatType]} = bind_pat_vars([AliasPat], [Type], [], 
+	{Map2, [PatType]} = bind_pat_vars([AliasPat], [Type], [],
 					  Map1, State, Rev),
 	{enter_type(Var, PatType, Map2), PatType};
       binary ->
@@ -1543,18 +1544,18 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
       cons ->
 	Cons = t_inf(Type, t_cons()),
 	case t_is_none(Cons) of
-	  true -> 
+	  true ->
 	    bind_opaque_pats(t_cons(), Type, Pat, Map, State, Rev);
 	  false ->
-	    {Map1, [HdType, TlType]} = 
+	    {Map1, [HdType, TlType]} =
 	      bind_pat_vars([cerl:cons_hd(Pat), cerl:cons_tl(Pat)],
-			    [t_cons_hd(Cons), t_cons_tl(Cons)], 
+			    [t_cons_hd(Cons), t_cons_tl(Cons)],
 			    [], Map, State, Rev),
 	    {Map1, t_cons(HdType, TlType)}
 	end;
       literal ->
 	Literal = literal_type(Pat),
-	LiteralOrOpaque = 
+	LiteralOrOpaque =
 	  case t_opaque_match_atom(Literal, State#state.opaques) of
 	    [Opaque] -> Opaque;
 	    _ -> Literal
@@ -1566,7 +1567,7 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
 	end;
       tuple ->
 	Es = cerl:tuple_es(Pat),
-	Prototype = 
+	Prototype =
 	  case Es of
 	    [] -> t_tuple([]);
 	    [Tag|Left] ->
@@ -1587,10 +1588,10 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
 	  false ->
 	    SubTuples = t_tuple_subtypes(Tuple),
 	    %% Need to call the top function to get the try-catch wrapper
-	    Results = 
+	    Results =
 	      case Rev of
 		true ->
-		  [bind_pat_vars_reverse(Es, t_tuple_args(SubTuple), [], 
+		  [bind_pat_vars_reverse(Es, t_tuple_args(SubTuple), [],
 					 Map, State)
 		   || SubTuple <- SubTuples];
 		false ->
@@ -1634,12 +1635,12 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
 	  end,
 	%% Must do inf when binding args to pats. Vars in pats are fresh.
 	VarType2 = t_inf(VarType1, Type),
-	VarType3 = 
+	VarType3 =
 	  case Opaques =/= [] of
 	    true ->
 	      case t_opaque_match_record(VarType2, Opaques) of
 		[OpaqueRec] -> OpaqueRec;
-		_ -> 
+		_ ->
 		  case t_opaque_match_atom(VarType2, Opaques) of
 		    [OpaqueAtom] -> OpaqueAtom;
 		    _ -> VarType2
@@ -1650,9 +1651,9 @@ bind_pat_vars([Pat|PatLeft], [Type|TypeLeft], Acc, Map, State, Rev) ->
 	case t_is_none(VarType3) of
 	  true ->
 	    case t_find_opaque_mismatch(VarType1, Type) of
-	      {ok, T1, T2}  -> 
+	      {ok, T1, T2}  ->
 		bind_error([Pat], T1, T2, opaque);
-	      error -> 
+	      error ->
 		bind_error([Pat], Type, t_none(), bind)
 	    end;
 	  false ->
@@ -1754,10 +1755,10 @@ bind_guard(Guard, Map, State) ->
   end.
 
 bind_guard(Guard, Map, Env, Eval, State) ->
-  ?debug("Handling ~w guard: ~s\n", 
+  ?debug("Handling ~w guard: ~s\n",
 	 [Eval, cerl_prettypr:format(Guard, [{noann, true}])]),
   case cerl:type(Guard) of
-    binary -> 
+    binary ->
       {Map, t_binary()};
     'case' ->
       Arg = cerl:case_arg(Guard),
@@ -1795,10 +1796,10 @@ bind_guard(Guard, Map, Env, Eval, State) ->
     var ->
       ?debug("Looking for var(~w)...", [cerl_trees:get_label(Guard)]),
       case dict:find(get_label(Guard), Env) of
-	error -> 
+	error ->
 	  ?debug("Did not find it\n", []),
 	  Type = lookup_type(Guard, Map),
-	  Constr = 
+	  Constr =
 	    case Eval of
 	      pos -> t_atom(true);
 	      neg -> t_atom(false);
@@ -1806,7 +1807,7 @@ bind_guard(Guard, Map, Env, Eval, State) ->
 	    end,
 	  Inf = t_inf(Constr, Type),
 	  {enter_type(Guard, Inf, Map), Inf};
-	{ok, Tree} -> 
+	{ok, Tree} ->
 	  ?debug("Found it\n", []),
 	  {Map1, Type} = bind_guard(Tree, Map, Env, Eval, State),
 	  {enter_type(Guard, Type, Map1), Type}
@@ -1829,7 +1830,7 @@ handle_guard_call(Guard, Map, Env, Eval, State) ->
       handle_guard_type_test(Guard, F, Map, Env, Eval, State);
     {erlang, is_function, 2} ->
       handle_guard_is_function(Guard, Map, Env, Eval, State);
-    MFA when (MFA =:= {erlang, internal_is_record, 3}) or 
+    MFA when (MFA =:= {erlang, internal_is_record, 3}) or
 	     (MFA =:= {erlang, is_record, 3}) ->
       handle_guard_is_record(Guard, Map, Env, Eval, State);
     {erlang, '=:=', 2} ->
@@ -1842,7 +1843,7 @@ handle_guard_call(Guard, Map, Env, Eval, State) ->
       handle_guard_or(Guard, Map, Env, Eval, State);
     {erlang, 'not', 1} ->
       handle_guard_not(Guard, Map, Env, Eval, State);
-    {erlang, Comp, 2} when Comp =:= '<'; Comp =:= '=<'; 
+    {erlang, Comp, 2} when Comp =:= '<'; Comp =:= '=<';
                            Comp =:= '>'; Comp =:= '>=' ->
       handle_guard_comp(Guard, Comp, Map, Env, Eval, State);
     _ ->
@@ -1877,7 +1878,7 @@ handle_guard_gen_fun({M, F, A}, Guard, Map, Env, Eval, State) ->
 		  List -> List
 		end,
       Map2 = enter_type_lists(Args, t_inf_lists(BifArgs, As0, Mode), Map1),
-      Ret = 
+      Ret =
 	case Eval of
 	  pos -> t_inf(t_atom(true), BifRet);
 	  neg -> t_inf(t_atom(false), BifRet);
@@ -1894,14 +1895,14 @@ handle_guard_gen_fun({M, F, A}, Guard, Map, Env, Eval, State) ->
   end.
 
 handle_guard_type_test(Guard, F, Map, Env, Eval, State) ->
-  [Arg] = cerl:call_args(Guard),      
+  [Arg] = cerl:call_args(Guard),
   {Map1, ArgType} = bind_guard(Arg, Map, Env, dont_know, State),
   case bind_type_test(Eval, F, ArgType, State) of
-    error -> 
+    error ->
       ?debug("Type test: ~w failed\n", [F]),
       signal_guard_fail(Guard, [ArgType], State);
-    {ok, NewArgType, Ret} -> 
-      ?debug("Type test: ~w succeeded, NewType: ~s, Ret: ~s\n", 
+    {ok, NewArgType, Ret} ->
+      ?debug("Type test: ~w succeeded, NewType: ~s, Ret: ~s\n",
 	     [F, t_to_string(NewArgType), t_to_string(Ret)]),
       {enter_type(Arg, NewArgType, Map1), Ret}
   end.
@@ -1932,13 +1933,13 @@ bind_type_test(Eval, TypeTest, ArgType, State) ->
       end;
     neg ->
       case Mode of
-	opaque -> 
+	opaque ->
 	  Struct = erl_types:t_opaque_structure(ArgType),
 	  case t_is_none(t_subtract(Struct, Type)) of
 	    true -> error;
 	    false  -> {ok, ArgType, t_atom(false)}
 	  end;
-	structured ->  
+	structured ->
 	  Sub = t_subtract(ArgType, Type),
 	  case t_is_none(Sub) of
 	    true -> error;
@@ -1976,7 +1977,7 @@ handle_guard_comp(Guard, Comp, Map, Env, Eval, State) ->
 	error -> signal_guard_fail(Guard, ArgTypes, State);
 	{ok, NewMap} -> {NewMap, t_atom(true)}
       end;
-    {_, _} -> 
+    {_, _} ->
       handle_guard_gen_fun({erlang, Comp, 2}, Guard, Map, Env, Eval, State)
   end.
 
@@ -2023,7 +2024,7 @@ handle_guard_is_function(Guard, Map, Env, Eval, State) ->
 	end,
       FunType = t_inf(FunType0, FunTypeConstr),
       case t_is_none(FunType) of
-	true -> 
+	true ->
 	  case Eval of
 	    pos -> signal_guard_fail(Guard, ArgTypes0, State);
 	    neg -> {Map1, t_atom(false)};
@@ -2059,16 +2060,16 @@ handle_guard_is_record(Guard, Map, Env, Eval, State) ->
     end,
   Type = t_inf(NewTupleType, RecType, Mode),
   case t_is_none(Type) of
-    true -> 
+    true ->
       case Eval of
-	pos -> signal_guard_fail(Guard, 
-				 [RecType, t_from_term(Tag), 
+	pos -> signal_guard_fail(Guard,
+				 [RecType, t_from_term(Tag),
 				  t_from_term(Arity)],
 				 State);
 	neg -> {Map1, t_atom(false)};
 	dont_know -> {Map1, t_atom(false)}
       end;
-    false -> 
+    false ->
       case Eval of
 	pos -> {enter_type(Rec, Type, Map1), t_atom(true)};
 	neg -> {Map1, t_atom(false)};
@@ -2081,17 +2082,17 @@ handle_guard_eq(Guard, Map, Env, Eval, State) ->
   case {cerl:type(Arg1), cerl:type(Arg2)} of
     {literal, literal} ->
       case cerl:concrete(Arg1) =:= cerl:concrete(Arg2) of
-	true -> 
-	  if 
+	true ->
+	  if
 	    Eval =:= pos -> {Map, t_atom(true)};
 	    Eval =:= neg -> throw({fail, none});
 	    Eval =:= dont_know -> {Map, t_atom(true)}
 	  end;
 	false ->
-	  if 
+	  if
 	    Eval =:= neg -> {Map, t_atom(false)};
 	    Eval =:= dont_know -> {Map, t_atom(false)};
-	    Eval =:= pos -> 
+	    Eval =:= pos ->
 	      ArgTypes = [t_from_term(cerl:concrete(Arg1)),
 			  t_from_term(cerl:concrete(Arg2))],
 	      signal_guard_fail(Guard, ArgTypes, State)
@@ -2146,7 +2147,7 @@ handle_guard_eqeq(Guard, Map, Env, Eval, State) ->
 	false ->
 	  if Eval =:= neg -> {Map, t_atom(false)};
 	     Eval =:= dont_know -> {Map, t_atom(false)};
-	     Eval =:= pos -> 
+	     Eval =:= pos ->
 	      ArgTypes = [t_from_term(cerl:concrete(Arg1)),
 			  t_from_term(cerl:concrete(Arg2))],
 	      signal_guard_fail(Guard, ArgTypes, State)
@@ -2163,7 +2164,7 @@ handle_guard_eqeq(Guard, Map, Env, Eval, State) ->
 bind_eqeq_guard(Guard, Arg1, Arg2, Map, Env, Eval, State) ->
   {Map1, Type1} = bind_guard(Arg1, Map, Env, dont_know, State),
   {Map2, Type2} = bind_guard(Arg2, Map1, Env, dont_know, State),
-  ?debug("Types are:~s =:= ~s\n", [t_to_string(Type1), 
+  ?debug("Types are:~s =:= ~s\n", [t_to_string(Type1),
 				   t_to_string(Type2)]),
   Inf = t_inf(Type1, Type2),
   case t_is_none(Inf) of
@@ -2204,15 +2205,15 @@ bind_eqeq_guard_lit_other(Guard, Arg1, Arg2, Map, Env, State) ->
       {_, Type} = MT = bind_guard(Arg2, Map, Env, pos, State),
       case t_is_atom(true, Type) of
 	true -> MT;
-	false -> 
+	false ->
 	  {_, Type0} = bind_guard(Arg2, Map, Env, dont_know, State),
 	  signal_guard_fail(Guard, [Type0, t_atom(true)], State)
       end;
-    false -> 
+    false ->
       {Map1, Type} = bind_guard(Arg2, Map, Env, neg, State),
       case t_is_atom(false, Type) of
 	true -> {Map1, t_atom(true)};
-	false -> 
+	false ->
 	  {_, Type0} = bind_guard(Arg2, Map, Env, dont_know, State),
 	  signal_guard_fail(Guard, [Type0, t_atom(true)], State)
       end;
@@ -2244,11 +2245,11 @@ handle_guard_and(Guard, Map, Env, Eval, State) ->
 	  end
       end;
     neg ->
-      {Map1, Type1} = 
+      {Map1, Type1} =
 	try bind_guard(Arg1, Map, Env, neg, State)
 	catch throw:{fail, _} -> bind_guard(Arg2, Map, Env, pos, State)
 	end,
-      {Map2, Type2} = 
+      {Map2, Type2} =
 	try bind_guard(Arg1, Map, Env, neg, State)
 	catch throw:{fail, _} -> bind_guard(Arg2, Map, Env, pos, State)
 	end,
@@ -2274,18 +2275,18 @@ handle_guard_or(Guard, Map, Env, Eval, State) ->
   [Arg1, Arg2] = cerl:call_args(Guard),
   case Eval of
 	pos ->
-      {Map1, Bool1} = 
+      {Map1, Bool1} =
 	try bind_guard(Arg1, Map, Env, pos, State)
-	catch 
+	catch
 	  throw:{fail,_} -> bind_guard(Arg1, Map, Env, dont_know, State)
 	end,
-      {Map2, Bool2} = 
+      {Map2, Bool2} =
 	try bind_guard(Arg2, Map, Env, pos, State)
-	catch 
+	catch
 	  throw:{fail,_} -> bind_guard(Arg2, Map, Env, dont_know, State)
 	end,
       case ((t_is_atom(true, Bool1) andalso t_is_boolean(Bool2))
-	    orelse 
+	    orelse
 	    (t_is_atom(true, Bool2) andalso t_is_boolean(Bool1))) of
 	true -> {join_maps([Map1, Map2], Map), t_atom(true)};
 	false -> throw({fail, none})
@@ -2313,19 +2314,19 @@ handle_guard_or(Guard, Map, Env, Eval, State) ->
 handle_guard_not(Guard, Map, Env, Eval, State) ->
   [Arg] = cerl:call_args(Guard),
   case Eval of
-    neg -> 
+    neg ->
       {Map1, Type} = bind_guard(Arg, Map, Env, pos, State),
       case t_is_atom(true, Type) of
 	true -> {Map1, t_atom(false)};
 	false -> throw({fail, none})
       end;
-    pos -> 
+    pos ->
       {Map1, Type} = bind_guard(Arg, Map, Env, neg, State),
       case t_is_atom(false, Type) of
 	true -> {Map1, t_atom(true)};
 	false -> throw({fail, none})
       end;
-    dont_know -> 
+    dont_know ->
       {Map1, Type} = bind_guard(Arg, Map, Env, dont_know, State),
       Bool = t_inf(Type, t_boolean()),
       case t_is_none(Bool) of
@@ -2357,10 +2358,10 @@ signal_guard_fail(Guard, ArgTypes, State) ->
   MFA = {cerl:atom_val(cerl:call_module(Guard)), F, length(Args)},
   Msg =
     case is_infix_op(MFA) of
-      true -> 
+      true ->
 	[ArgType1, ArgType2] = ArgTypes,
 	[Arg1, Arg2] = Args,
-	{guard_fail, [format_args_1([Arg1], [ArgType1], State), 
+	{guard_fail, [format_args_1([Arg1], [ArgType1], State),
 		      atom_to_list(F),
 		      format_args_1([Arg2], [ArgType2], State)]};
       false ->
@@ -2383,7 +2384,7 @@ is_infix_op({M, F, A}) when is_atom(M), is_atom(F),
         no_return().
 
 signal_guard_fatal_fail(Guard, ArgTypes, State) ->
-  Args = cerl:call_args(Guard),      
+  Args = cerl:call_args(Guard),
   F = cerl:atom_val(cerl:call_name(Guard)),
   Msg = mk_guard_msg(F, Args, ArgTypes, State),
   throw({fatal_fail, {Guard, Msg}}).
@@ -2394,11 +2395,11 @@ mk_guard_msg(F, Args, ArgTypes, State) ->
     true -> {opaque_guard, FArgs};
     false -> {guard_fail, FArgs}
   end.
-  
+
 bind_guard_case_clauses(Arg, Clauses, Map, Env, Eval, State) ->
   Clauses1 = filter_fail_clauses(Clauses),
   {GenMap, GenArgType} = bind_guard(Arg, Map, Env, dont_know, State),
-  bind_guard_case_clauses(GenArgType, GenMap, Arg, Clauses1, Map, Env, Eval, 
+  bind_guard_case_clauses(GenArgType, GenMap, Arg, Clauses1, Map, Env, Eval,
 			  t_none(), [], State).
 
 filter_fail_clauses([Clause|Left]) ->
@@ -2415,7 +2416,7 @@ filter_fail_clauses([Clause|Left]) ->
 filter_fail_clauses([]) ->
   [].
 
-bind_guard_case_clauses(GenArgType, GenMap, ArgExpr, [Clause|Left], 
+bind_guard_case_clauses(GenArgType, GenMap, ArgExpr, [Clause|Left],
 			Map, Env, Eval, AccType, AccMaps, State) ->
   Pats = cerl:clause_pats(Clause),
   {NewMap0, ArgType} =
@@ -2429,7 +2430,7 @@ bind_guard_case_clauses(GenArgType, GenMap, ArgExpr, [Clause|Left],
 		false -> bind_guard(ArgExpr, Map, Env, neg, State);
 		_ -> {GenMap, GenArgType}
 	      end
-	    catch 
+	    catch
 	      throw:{fail, _} -> {none, GenArgType}
 	    end;
 	  false ->
@@ -2459,7 +2460,7 @@ bind_guard_case_clauses(GenArgType, GenMap, ArgExpr, [Clause|Left],
   NewGenArgType = t_subtract(GenArgType, GenPatType),
   case (NewMap1 =:= none) orelse t_is_none(GenArgType) of
     true ->
-      bind_guard_case_clauses(NewGenArgType, GenMap, ArgExpr, Left, Map, Env, 
+      bind_guard_case_clauses(NewGenArgType, GenMap, ArgExpr, Left, Map, Env,
 			      Eval, AccType, AccMaps, State);
     false ->
       {NewAccType, NewAccMaps} =
@@ -2469,15 +2470,15 @@ bind_guard_case_clauses(GenArgType, GenMap, ArgExpr, [Clause|Left],
 	    true -> throw({fail, none});
 	    false -> ok
 	  end,
-	  {NewMap3, CType} = bind_guard(cerl:clause_body(Clause), NewMap2, 
+	  {NewMap3, CType} = bind_guard(cerl:clause_body(Clause), NewMap2,
 					Env, Eval, State),
 	  case Eval of
-	    pos -> 
+	    pos ->
 	      case t_is_atom(true, CType) of
 		true -> ok;
 		false -> throw({fail, none})
 	      end;
-	    neg -> 
+	    neg ->
 	      case t_is_atom(false, CType) of
 		true -> ok;
 		false -> throw({fail, none})
@@ -2489,10 +2490,10 @@ bind_guard_case_clauses(GenArgType, GenMap, ArgExpr, [Clause|Left],
 	catch
 	  throw:{fail, _What} -> {AccType, AccMaps}
 	end,
-      bind_guard_case_clauses(NewGenArgType, GenMap, ArgExpr, Left, Map, Env, 
+      bind_guard_case_clauses(NewGenArgType, GenMap, ArgExpr, Left, Map, Env,
 			      Eval, NewAccType, NewAccMaps, State)
   end;
-bind_guard_case_clauses(_GenArgType, _GenMap, _ArgExpr, [], Map, _Env, _Eval, 
+bind_guard_case_clauses(_GenArgType, _GenMap, _ArgExpr, [], Map, _Env, _Eval,
 			AccType, AccMaps, _State) ->
   case t_is_none(AccType) of
     true -> throw({fail, none});
@@ -2578,7 +2579,7 @@ enter_type(Key, Val, {Map, Subst} = MS) ->
 enter_subst(Key, Val, {Map, Subst} = MS) ->
   KeyLabel = get_label(Key),
   case cerl:is_literal(Val) of
-    true -> 
+    true ->
       NewMap = dict:store(KeyLabel, literal_type(Val), Map),
       {NewMap, Subst};
     false ->
@@ -2600,13 +2601,13 @@ enter_subst(Key, Val, {Map, Subst} = MS) ->
       end
   end.
 
-lookup_type(Key, {Map, Subst}) -> 
+lookup_type(Key, {Map, Subst}) ->
   lookup(Key, Map, Subst, t_none()).
 
 lookup(Key, Map, Subst, AnyNone) ->
   case cerl:is_literal(Key) of
     true -> literal_type(Key);
-    false -> 
+    false ->
       Label = get_label(Key),
       case dict:find(Label, Subst) of
 	{ok, NewKey} -> lookup(NewKey, Map, Subst, AnyNone);
@@ -2671,7 +2672,7 @@ get_label(T) ->
 
 t_is_simple(ArgType) ->
   t_is_atom(ArgType) orelse t_is_number(ArgType) orelse t_is_port(ArgType)
-    orelse t_is_pid(ArgType) orelse t_is_reference(ArgType) 
+    orelse t_is_pid(ArgType) orelse t_is_reference(ArgType)
     orelse t_is_nil(ArgType).
 
 %% t_is_structured(ArgType) ->
@@ -2689,8 +2690,8 @@ is_call_to_send(Tree) ->
       Mod = cerl:call_module(Tree),
       Name = cerl:call_name(Tree),
       Arity = cerl:call_arity(Tree),
-      cerl:is_c_atom(Mod) 
-	andalso cerl:is_c_atom(Name) 
+      cerl:is_c_atom(Mod)
+	andalso cerl:is_c_atom(Name)
 	andalso (cerl:atom_val(Name) =:= '!')
 	andalso (cerl:atom_val(Mod) =:= erlang)
 	andalso (Arity =:= 2)
@@ -2716,7 +2717,7 @@ filter_match_fail([Clause] = Cls) ->
 filter_match_fail([H|T]) ->
   [H|filter_match_fail(T)];
 filter_match_fail([]) ->
-  %% This can actually happen, for example in 
+  %% This can actually happen, for example in
   %%      receive after 1 -> ok end
   [].
 
@@ -2733,9 +2734,11 @@ determine_mode(Type, Opaques) ->
 %%% ===========================================================================
 
 state__new(Callgraph, Tree, Plt, Module, Records, BehaviourTranslations) ->
+  Opaques = erl_types:module_builtin_opaques(Module) ++
+    erl_types:t_opaque_from_records(Records),
   TreeMap = build_tree_map(Tree),
   Funs = dict:fetch_keys(TreeMap),
-  FunTab = init_fun_tab(Funs, dict:new(), TreeMap, Callgraph, Plt),
+  FunTab = init_fun_tab(Funs, dict:new(), TreeMap, Callgraph, Plt, Opaques),
   Work = init_work([get_label(Tree)]),
   Env = dict:store(top, map__new(), dict:new()),
   Opaques = erl_types:module_builtin_opaques(Module) ++
@@ -2743,12 +2746,12 @@ state__new(Callgraph, Tree, Plt, Module, Records, BehaviourTranslations) ->
   #state{callgraph = Callgraph, envs = Env, fun_tab = FunTab, opaques = Opaques,
 	 plt = Plt, races = dialyzer_races:new(), records = Records,
 	 warning_mode = false, warnings = [], work = Work, tree_map = TreeMap,
-	 module = Module, behaviour_api_info = BehaviourTranslations}.
+	 module = Module, behaviour_api_dict = BehaviourTranslations}.
 
 state__mark_fun_as_handled(#state{fun_tab = FunTab} = State, Fun0) ->
   Fun = get_label(Fun0),
   case dict:find(Fun, FunTab) of
-    {ok, {not_handled, Entry}} -> 
+    {ok, {not_handled, Entry}} ->
       State#state{fun_tab = dict:store(Fun, Entry, FunTab)};
     {ok, {_, _}} ->
       State
@@ -2802,7 +2805,7 @@ state__add_warning(State, Tag, Tree, Msg) ->
 
 state__add_warning(#state{warning_mode = false} = State, _, _, _, _) ->
   State;
-state__add_warning(#state{warnings = Warnings, warning_mode = true} = State, 
+state__add_warning(#state{warnings = Warnings, warning_mode = true} = State,
 		   Tag, Tree, Msg, Force) ->
   Ann = cerl:get_ann(Tree),
   case Force of
@@ -2850,7 +2853,7 @@ state__get_warnings(#state{tree_map = TreeMap, fun_tab = FunTab,
 	    {Name, Contract} =
 	      case dialyzer_callgraph:lookup_name(FunLbl, Callgraph) of
 		error -> {[], none};
-		{ok, {_M, F, A} = MFA} -> 
+		{ok, {_M, F, A} = MFA} ->
 		  {[F, A], dialyzer_plt:lookup_contract(Plt, MFA)}
 	      end,
 	    case t_is_none(Ret) of
@@ -2868,19 +2871,19 @@ state__get_warnings(#state{tree_map = TreeMap, fun_tab = FunTab,
 		    case classify_returns(Fun) of
 		      no_match ->
 			Msg = {no_return, [no_match|Name]},
-			state__add_warning(AccState, ?WARN_RETURN_NO_RETURN, 
+			state__add_warning(AccState, ?WARN_RETURN_NO_RETURN,
 					   Fun, Msg);
 		      only_explicit ->
 			Msg = {no_return, [only_explicit|Name]},
-			state__add_warning(AccState, ?WARN_RETURN_ONLY_EXIT, 
+			state__add_warning(AccState, ?WARN_RETURN_ONLY_EXIT,
 					   Fun, Msg);
 		      only_normal ->
 			Msg = {no_return, [only_normal|Name]},
-			state__add_warning(AccState, ?WARN_RETURN_NO_RETURN, 
+			state__add_warning(AccState, ?WARN_RETURN_NO_RETURN,
 					   Fun, Msg);
 		      both ->
 			Msg = {no_return, [both|Name]},
-			state__add_warning(AccState, ?WARN_RETURN_NO_RETURN, 
+			state__add_warning(AccState, ?WARN_RETURN_NO_RETURN,
 					   Fun, Msg)
 		    end;
 		  false ->
@@ -2918,10 +2921,10 @@ state__lookup_name(Fun, #state{callgraph = Callgraph}) ->
 
 state__lookup_record(Tag, Arity, #state{records = Records}) ->
   case erl_types:lookup_record(Tag, Arity, Records) of
-    {ok, Fields} -> 
+    {ok, Fields} ->
       {ok, t_tuple([t_atom(Tag)|
 		    [FieldType || {_FieldName, FieldType} <- Fields]])};
-    error -> 
+    error ->
       error
   end.
 
@@ -2944,15 +2947,15 @@ build_tree_map(Tree) ->
     end,
   cerl_trees:fold(Fun, dict:new(), Tree).
 
-init_fun_tab([top|Left], Dict, TreeMap, Callgraph, Plt) ->
+init_fun_tab([top|Left], Dict, TreeMap, Callgraph, Plt, Opaques) ->
   NewDict = dict:store(top, {not_handled, {[], t_none()}}, Dict),
-  init_fun_tab(Left, NewDict, TreeMap, Callgraph, Plt);
-init_fun_tab([Fun|Left], Dict, TreeMap, Callgraph, Plt) ->
+  init_fun_tab(Left, NewDict, TreeMap, Callgraph, Plt, Opaques);
+init_fun_tab([Fun|Left], Dict, TreeMap, Callgraph, Plt, Opaques) ->
   Arity = cerl:fun_arity(dict:fetch(Fun, TreeMap)),
   FunEntry =
     case dialyzer_callgraph:is_escaping(Fun, Callgraph) of
       true ->
-	Args = lists:duplicate(Arity, t_any()),
+        Args = lists:duplicate(Arity, t_any()),
 	case lookup_fun_sig(Fun, Callgraph, Plt) of
 	  none -> {Args, t_unit()};
 	  {value, {RetType, _}} ->
@@ -2964,8 +2967,8 @@ init_fun_tab([Fun|Left], Dict, TreeMap, Callgraph, Plt) ->
       false -> {lists:duplicate(Arity, t_none()), t_unit()}
     end,
   NewDict = dict:store(Fun, {not_handled, FunEntry}, Dict),
-  init_fun_tab(Left, NewDict, TreeMap, Callgraph, Plt);
-init_fun_tab([], Dict, _TreeMap, _Callgraph, _Plt) ->
+  init_fun_tab(Left, NewDict, TreeMap, Callgraph, Plt, Opaques);
+init_fun_tab([], Dict, _TreeMap, _Callgraph, _Plt, _Opaques) ->
   Dict.
 
 state__update_fun_env(Tree, Map, #state{envs = Envs} = State) ->
@@ -2992,7 +2995,7 @@ state__all_fun_types(#state{fun_tab = FunTab}) ->
   dict:map(fun(_Fun, {Args, Ret}) -> t_fun(Args, Ret)end, Tab1).
 
 state__fun_type(Fun, #state{fun_tab = FunTab}) ->
-  Label = 
+  Label =
     if is_integer(Fun) -> Fun;
        true -> get_label(Fun)
     end,
@@ -3003,10 +3006,10 @@ state__fun_type(Fun, #state{fun_tab = FunTab}) ->
       t_fun(A, R)
   end.
 
-state__update_fun_entry(Tree, ArgTypes, Out0, 
+state__update_fun_entry(Tree, ArgTypes, Out0,
 			#state{fun_tab=FunTab, callgraph=CG, plt=Plt} = State)->
   Fun = get_label(Tree),
-  Out1 = 
+  Out1 =
     if Fun =:= top -> Out0;
        true ->
 	case lookup_fun_sig(Fun, CG, Plt) of
@@ -3018,15 +3021,15 @@ state__update_fun_entry(Tree, ArgTypes, Out0,
   case dict:find(Fun, FunTab) of
     {ok, {ArgTypes, OldOut}} ->
       case t_is_equal(OldOut, Out) of
-	true -> 
-	  ?debug("Fixpoint for ~w: ~s\n", 
-		 [state__lookup_name(Fun, State), 
+	true ->
+	  ?debug("Fixpoint for ~w: ~s\n",
+		 [state__lookup_name(Fun, State),
 		  t_to_string(t_fun(ArgTypes, Out))]),
 	  State;
 	false ->
 	  NewEntry = {ArgTypes, Out},
-	  ?debug("New Entry for ~w: ~s\n", 
-		 [state__lookup_name(Fun, State), 
+	  ?debug("New Entry for ~w: ~s\n",
+		 [state__lookup_name(Fun, State),
 		  t_to_string(t_fun(ArgTypes, Out))]),
 	  NewFunTab = dict:store(Fun, NewEntry, FunTab),
 	  State1 = State#state{fun_tab = NewFunTab},
@@ -3035,8 +3038,8 @@ state__update_fun_entry(Tree, ArgTypes, Out0,
     {ok, {NewArgTypes, _OldOut}} ->
       %% Can only happen in self-recursive functions. Only update the out type.
       NewEntry = {NewArgTypes, Out},
-      ?debug("New Entry for ~w: ~s\n", 
-	     [state__lookup_name(Fun, State), 
+      ?debug("New Entry for ~w: ~s\n",
+	     [state__lookup_name(Fun, State),
 	      t_to_string(t_fun(NewArgTypes, Out))]),
       NewFunTab = dict:store(Fun, NewEntry, FunTab),
       State1 = State#state{fun_tab = NewFunTab},
@@ -3055,9 +3058,9 @@ state__add_work_from_fun(Tree, #state{callgraph = Callgraph,
 	MFAList ->
 	  LabelList = [dialyzer_callgraph:lookup_label(MFA, Callgraph)
 		       || MFA <- MFAList],
-	  %% Must filter the result for results in this module.	  
+	  %% Must filter the result for results in this module.
 	  FilteredList = [L || {ok, L} <- LabelList, dict:is_key(L, TreeMap)],
-	  ?debug("~w: Will try to add:~w\n", 
+	  ?debug("~w: Will try to add:~w\n",
 		 [state__lookup_name(get_label(Tree), State), MFAList]),
 	  lists:foldl(fun(L, AccState) ->
 			  state__add_work(L, AccState)
@@ -3088,15 +3091,15 @@ state__fun_info(external, #state{}) ->
   external;
 state__fun_info({_, _, _} = MFA, #state{plt = PLT}) ->
   {MFA,
-   dialyzer_plt:lookup(PLT, MFA), 
+   dialyzer_plt:lookup(PLT, MFA),
    dialyzer_plt:lookup_contract(PLT, MFA),
    t_any()};
 state__fun_info(Fun, #state{callgraph = CG, fun_tab = FunTab, plt = PLT}) ->
   {Sig, Contract} =
     case dialyzer_callgraph:lookup_name(Fun, CG) of
-      error -> 
+      error ->
 	{dialyzer_plt:lookup(PLT, Fun), none};
-      {ok, MFA} -> 
+      {ok, MFA} ->
 	{dialyzer_plt:lookup(PLT, MFA), dialyzer_plt:lookup_contract(PLT, MFA)}
     end,
   LocalRet =
@@ -3124,18 +3127,18 @@ state__find_apply_return(Tree, #state{callgraph = Callgraph} = State) ->
 forward_args(Fun, ArgTypes, #state{work = Work, fun_tab = FunTab} = State) ->
   {OldArgTypes, OldOut, Fixpoint} =
     case dict:find(Fun, FunTab) of
-      {ok, {not_handled, {OldArgTypes0, OldOut0}}} -> 
+      {ok, {not_handled, {OldArgTypes0, OldOut0}}} ->
 	{OldArgTypes0, OldOut0, false};
       {ok, {OldArgTypes0, OldOut0}} ->
-	{OldArgTypes0, OldOut0, 
+	{OldArgTypes0, OldOut0,
 	 t_is_subtype(t_product(ArgTypes), t_product(OldArgTypes0))}
     end,
   case Fixpoint of
     true -> State;
-    false -> 
+    false ->
       NewArgTypes = [t_sup(X, Y) || {X, Y} <- lists:zip(ArgTypes, OldArgTypes)],
       NewWork = add_work(Fun, Work),
-      ?debug("~w: forwarding args ~s\n", 
+      ?debug("~w: forwarding args ~s\n",
 	     [state__lookup_name(Fun, State),
 	      t_to_string(t_product(NewArgTypes))]),
       NewFunTab = dict:store(Fun, {NewArgTypes, OldOut}, FunTab),
@@ -3250,7 +3253,7 @@ get_file([_|Tail]) -> get_file(Tail).
 is_compiler_generated(Ann) ->
   lists:member(compiler_generated, Ann) orelse (get_line(Ann) < 1).
 
--spec format_args([term()], [erl_types:erl_type()], state()) ->
+-spec format_args([cerl:cerl()], [erl_types:erl_type()], state()) ->
   nonempty_string().
 
 format_args([], [], _State) ->
@@ -3258,9 +3261,6 @@ format_args([], [], _State) ->
 format_args(ArgList, TypeList, State) ->
   "(" ++ format_args_1(ArgList, TypeList, State) ++ ")".
 
--spec format_args_1([term(),...], [erl_types:erl_type(),...], state()) ->
-  string().
-
 format_args_1([Arg], [Type], State) ->
   format_arg(Arg) ++ format_type(Type, State);
 format_args_1([Arg|Args], [Type|Types], State) ->
@@ -3293,6 +3293,11 @@ format_arg(Arg) ->
 format_type(Type, #state{records = R}) ->
   t_to_string(Type, R).
 
+-spec format_field_diffs(erl_types:erl_type(), state()) -> string().
+
+format_field_diffs(RecConstruction, #state{records = R}) ->
+  erl_types:record_field_diffs_to_string(RecConstruction, R).
+
 -spec format_sig_args(erl_types:erl_type(), state()) -> string().
 
 format_sig_args(Type, #state{records = R}) ->
@@ -3300,12 +3305,12 @@ format_sig_args(Type, #state{records = R}) ->
   case SigArgs of
     [] -> "()";
     [SArg|SArgs] ->
-      lists:flatten("(" ++ t_to_string(SArg, R) 
+      lists:flatten("(" ++ t_to_string(SArg, R)
 		        ++ ["," ++ t_to_string(T, R) || T <- SArgs] ++ ")")
     end.
 
 format_cerl(Tree) ->
-  cerl_prettypr:format(cerl:set_ann(Tree, []), 
+  cerl_prettypr:format(cerl:set_ann(Tree, []),
 		       [{hook, dialyzer_utils:pp_hook()},
 			{noann, true},
 			{paper, 100000}, %% These guys strip
@@ -3368,7 +3373,7 @@ find_terminals(Tree) ->
 	true ->
 	  M = cerl:concrete(M0),
 	  F = cerl:concrete(F0),
-	  case (erl_bif_types:is_known(M, F, A) 
+	  case (erl_bif_types:is_known(M, F, A)
 		andalso t_is_none(erl_bif_types:type(M, F, A))) of
 	    true -> {true, false};
 	    false -> {false, true}
@@ -3383,12 +3388,12 @@ find_terminals(Tree) ->
     letrec -> find_terminals(cerl:letrec_body(Tree));
     literal -> {false, true};
     primop -> {false, false}; %% match_fail, etc. are not explicit exits.
-    'receive' -> 
+    'receive' ->
       Timeout = cerl:receive_timeout(Tree),
       Clauses = cerl:receive_clauses(Tree),
       case (cerl:is_literal(Timeout) andalso
 	    (cerl:concrete(Timeout) =:= infinity)) of
-	true -> 
+	true ->
 	  if Clauses =:= [] -> {false, true}; %% A never ending receive.
 	     true -> find_terminals_list(Clauses)
 	  end;
@@ -3456,11 +3461,11 @@ find_rec_warnings_tuple(Tree, State) ->
 	      TagVal = cerl:atom_val(Tag),
 	      case state__lookup_record(TagVal, length(Left), State) of
 		error -> State;
-		{ok, Prototype} -> 
+		{ok, Prototype} ->
 		  InfTupleType = t_inf(Prototype, TupleType),
 		  case t_is_none(InfTupleType) of
 		    true ->
-		      Msg = {record_matching, 
+		      Msg = {record_matching,
 			     [format_patterns([Tree]), TagVal]},
 		      state__add_warning(State, ?WARN_MATCHING, Tree, Msg);
 		    false ->
@@ -3478,7 +3483,7 @@ find_rec_warnings_tuple(Tree, State) ->
 %%----------------------------------------------------------------------------
 
 -ifdef(DEBUG_PP).
-debug_pp(Tree, true) -> 
+debug_pp(Tree, true) ->
   io:put_chars(cerl_prettypr:format(Tree, [{hook, cerl_typean:pp_hook()}])),
   io:nl(),
   ok;
diff --git a/lib/dialyzer/src/dialyzer_options.erl b/lib/dialyzer/src/dialyzer_options.erl
index da0e1f9aaf..010625b7bd 100644
--- a/lib/dialyzer/src/dialyzer_options.erl
+++ b/lib/dialyzer/src/dialyzer_options.erl
@@ -184,7 +184,7 @@ build_options([], Options) ->
 assert_filenames(Term, [FileName|Left]) when length(FileName) >= 0 ->
   case filelib:is_file(FileName) orelse filelib:is_dir(FileName) of
     true -> ok;
-    false -> bad_option("No such file or directory", FileName)
+    false -> bad_option("No such file, directory or application", FileName)
   end,
   assert_filenames(Term, Left);
 assert_filenames(_Term, []) ->
diff --git a/lib/dialyzer/src/dialyzer_plt.erl b/lib/dialyzer/src/dialyzer_plt.erl
index c10375eea2..268ec4a5f0 100644
--- a/lib/dialyzer/src/dialyzer_plt.erl
+++ b/lib/dialyzer/src/dialyzer_plt.erl
@@ -21,7 +21,7 @@
 %%%-------------------------------------------------------------------
 %%% File    : dialyzer_plt.erl
 %%% Author  : Tobias Lindahl <[email protected]>
-%%% Description : Interface to display information in the persistent 
+%%% Description : Interface to display information in the persistent
 %%%               lookup tables.
 %%%
 %%% Created : 23 Jul 2004 by Tobias Lindahl <[email protected]>
@@ -101,7 +101,7 @@
 new() ->
   #plt{}.
 
--spec delete_module(plt(), module()) -> plt().
+-spec delete_module(plt(), atom()) -> plt().
 
 delete_module(#plt{info = Info, types = Types, contracts = Contracts,
                    exported_types = ExpTypes}, Mod) ->
@@ -136,7 +136,7 @@ delete_contract_list(#plt{contracts = Contracts} = PLT, List) ->
   PLT#plt{contracts = table_delete_list(Contracts, List)}.
 
 %% -spec insert(plt(), mfa() | integer(), {_, _}) -> plt().
-%% 
+%%
 %% insert(#plt{info = Info} = PLT, Id, Types) ->
 %%   PLT#plt{info = table_insert(Info, Id, Types)}.
 
@@ -177,12 +177,12 @@ get_exported_types(#plt{exported_types = ExpTypes}) ->
 
 -type mfa_types() :: {mfa(), erl_types:erl_type(), [erl_types:erl_type()]}.
 
--spec lookup_module(plt(), module()) -> 'none' | {'value', [mfa_types()]}.
+-spec lookup_module(plt(), atom()) -> 'none' | {'value', [mfa_types()]}.
 
 lookup_module(#plt{info = Info}, M) when is_atom(M) ->
   table_lookup_module(Info, M).
 
--spec contains_module(plt(), module()) -> boolean().
+-spec contains_module(plt(), atom()) -> boolean().
 
 contains_module(#plt{info = Info, contracts = Cs}, M) when is_atom(M) ->
   table_contains_module(Info, M) orelse table_contains_module(Cs, M).
@@ -190,7 +190,7 @@ contains_module(#plt{info = Info, contracts = Cs}, M) when is_atom(M) ->
 -spec contains_mfa(plt(), mfa()) -> boolean().
 
 contains_mfa(#plt{info = Info, contracts = Contracts}, MFA) ->
-  (table_lookup(Info, MFA) =/= none) 
+  (table_lookup(Info, MFA) =/= none)
     orelse (table_lookup(Contracts, MFA) =/= none).
 
 -spec get_default_plt() -> file:filename().
@@ -221,10 +221,10 @@ from_file(FileName, ReturnInfo) ->
   case get_record_from_file(FileName) of
     {ok, Rec} ->
       case check_version(Rec) of
-	error -> 
+	error ->
 	  Msg = io_lib:format("Old PLT file ~s\n", [FileName]),
 	  error(Msg);
-	ok -> 
+	ok ->
 	  Plt = #plt{info = Rec#file_plt.info,
 		     types = Rec#file_plt.types,
 		     contracts = Rec#file_plt.contracts,
@@ -238,12 +238,12 @@ from_file(FileName, ReturnInfo) ->
 	  end
       end;
     {error, Reason} ->
-      error(io_lib:format("Could not read PLT file ~s: ~p\n", 
+      error(io_lib:format("Could not read PLT file ~s: ~p\n",
 			  [FileName, Reason]))
   end.
 
 -type inc_file_err_rsn() :: 'no_such_file' | 'read_error'.
--spec included_files(file:filename()) -> {'ok', [file:filename()]} 
+-spec included_files(file:filename()) -> {'ok', [file:filename()]}
 				      |  {'error', inc_file_err_rsn()}.
 
 included_files(FileName) ->
@@ -268,12 +268,12 @@ get_record_from_file(FileName) ->
       try binary_to_term(Bin) of
 	  #file_plt{} = FilePLT -> {ok, FilePLT};
 	  _ -> {error, not_valid}
-      catch 
+      catch
 	_:_ -> {error, not_valid}
       end;
     {error, enoent} ->
       {error, no_such_file};
-    {error, _} -> 
+    {error, _} ->
       {error, read_error}
   end.
 
@@ -295,9 +295,9 @@ to_file(FileName,
 	#plt{info = Info, types = Types, contracts = Contracts,
              exported_types = ExpTypes},
 	ModDeps, {MD5, OldModDeps}) ->
-  NewModDeps = dict:merge(fun(_Key, OldVal, NewVal) -> 
+  NewModDeps = dict:merge(fun(_Key, OldVal, NewVal) ->
 			      ordsets:union(OldVal, NewVal)
-			  end, 
+			  end,
 			  OldModDeps, ModDeps),
   ImplMd5 = compute_implementation_md5(),
   Record = #file_plt{version = ?VSN,
@@ -312,7 +312,7 @@ to_file(FileName,
   case file:write_file(FileName, Bin) of
     ok -> ok;
     {error, Reason} ->
-      Msg = io_lib:format("Could not write PLT file ~s: ~w\n", 
+      Msg = io_lib:format("Could not write PLT file ~s: ~w\n",
 			  [FileName, Reason]),
       throw({dialyzer_error, Msg})
   end.
@@ -320,8 +320,8 @@ to_file(FileName,
 -type md5_diff()    :: [{'differ', atom()} | {'removed', atom()}].
 -type check_error() :: 'not_valid' | 'no_such_file' | 'read_error'
                      | {'no_file_to_remove', file:filename()}.
-      
--spec check_plt(file:filename(), [file:filename()], [file:filename()]) -> 
+
+-spec check_plt(file:filename(), [file:filename()], [file:filename()]) ->
 	 'ok'
        | {'error', check_error()}
        | {'differ', [file_md5()], md5_diff(), mod_deps()}
@@ -331,7 +331,7 @@ check_plt(FileName, RemoveFiles, AddFiles) ->
   case get_record_from_file(FileName) of
     {ok, #file_plt{file_md5_list = Md5, mod_deps = ModDeps} = Rec} ->
       case check_version(Rec) of
-	ok -> 
+	ok ->
 	  case compute_new_md5(Md5, RemoveFiles, AddFiles) of
 	    ok -> ok;
 	    {differ, NewMd5, DiffMd5} -> {differ, NewMd5, DiffMd5, ModDeps};
@@ -388,7 +388,7 @@ compute_md5_from_files(Files) ->
 
 compute_md5_from_file(File) ->
   case filelib:is_regular(File) of
-    false -> 
+    false ->
       Msg = io_lib:format("Not a regular file: ~s\n", [File]),
       throw({dialyzer_error, Msg});
     true ->
@@ -419,7 +419,7 @@ init_md5_list_1([{File, _Md5}|Md5Left], [{remove, File}|DiffLeft], Acc) ->
   init_md5_list_1(Md5Left, DiffLeft, Acc);
 init_md5_list_1([{File, _Md5} = Entry|Md5Left], [{add, File}|DiffLeft], Acc) ->
   init_md5_list_1(Md5Left, DiffLeft, [Entry|Acc]);
-init_md5_list_1([{File1, _Md5} = Entry|Md5Left] = Md5List, 
+init_md5_list_1([{File1, _Md5} = Entry|Md5Left] = Md5List,
 		[{Tag, File2}|DiffLeft] = DiffList, Acc) ->
   case File1 < File2 of
     true -> init_md5_list_1(Md5Left, DiffList, [Entry|Acc]);
@@ -450,7 +450,7 @@ get_specs(#plt{info = Info}) ->
 beam_file_to_module(Filename) ->
   list_to_atom(filename:basename(Filename, ".beam")).
 
--spec get_specs(plt(), module(), atom(), arity_patt()) -> 'none' | string().
+-spec get_specs(plt(), atom(), atom(), arity_patt()) -> 'none' | string().
 
 get_specs(#plt{info = Info}, M, F, A) when is_atom(M), is_atom(F) ->
   MFA = {M, F, A},
@@ -460,7 +460,7 @@ get_specs(#plt{info = Info}, M, F, A) when is_atom(M), is_atom(F) ->
   end.
 
 create_specs([{{M, F, _A}, {Ret, Args}}|Left], M) ->
-  [io_lib:format("-spec ~w(~s) -> ~s\n", 
+  [io_lib:format("-spec ~w(~s) -> ~s\n",
 		 [F, expand_args(Args), erl_types:t_to_string(Ret)])
    | create_specs(Left, M)];
 create_specs(List = [{{M, _F, _A}, {_Ret, _Args}}| _], _M) ->
@@ -516,7 +516,7 @@ table_insert_list(Plt, [{Key, Val}|Left]) ->
 table_insert_list(Plt, []) ->
   Plt.
 
-table_insert(Plt, Key, {_Ret, _Arg} = Obj) -> 
+table_insert(Plt, Key, {_Ret, _Arg} = Obj) ->
   dict:store(Key, Obj, Plt);
 table_insert(Plt, Key, #contract{} = C) ->
   dict:store(Key, C, Plt).
@@ -592,7 +592,7 @@ pp_non_returning() ->
 			      [M, F, dialyzer_utils:format_sig(Type)])
 		end, lists:sort(None)).
 
--spec pp_mod(module()) -> 'ok'.
+-spec pp_mod(atom()) -> 'ok'.
 
 pp_mod(Mod) when is_atom(Mod) ->
   PltFile = get_default_plt(),
diff --git a/lib/dialyzer/src/dialyzer_races.erl b/lib/dialyzer/src/dialyzer_races.erl
index fb16e6a75f..ec8d613b96 100644
--- a/lib/dialyzer/src/dialyzer_races.erl
+++ b/lib/dialyzer/src/dialyzer_races.erl
@@ -21,7 +21,7 @@
 %%%----------------------------------------------------------------------
 %%% File    : dialyzer_races.erl
 %%% Author  : Maria Christakis <[email protected]>
-%%% Description : Utility functions for race condition detection 
+%%% Description : Utility functions for race condition detection
 %%%
 %%% Created : 21 Nov 2008 by Maria Christakis <[email protected]>
 %%%----------------------------------------------------------------------
@@ -39,7 +39,7 @@
          let_tag_new/2, new/0, put_curr_fun/3, put_fun_args/2,
          put_race_analysis/2, put_race_list/3]).
 
--export_type([races/0]).
+-export_type([races/0, mfa_or_funlbl/0, core_vars/0]).
 
 -include("dialyzer.hrl").
 
@@ -82,7 +82,7 @@
 -type call()       :: 'whereis' | 'register' | 'unregister' | 'ets_new'
                     | 'ets_lookup' | 'ets_insert' | 'mnesia_dirty_read1'
                     | 'mnesia_dirty_read2' | 'mnesia_dirty_write1'
-                    | 'mnesia_dirty_write2' | 'function_call'. 
+                    | 'mnesia_dirty_write2' | 'function_call'.
 -type race_tag()   :: 'whereis_register' | 'whereis_unregister'
                     | 'ets_lookup_insert' | 'mnesia_dirty_read_write'.
 
@@ -159,7 +159,7 @@
 %%% ===========================================================================
 
 -spec store_race_call(mfa_or_funlbl(), [erl_types:erl_type()], [core_vars()],
-                      file_line(), dialyzer_dataflow:state()) -> 
+                      file_line(), dialyzer_dataflow:state()) ->
   dialyzer_dataflow:state().
 
 store_race_call(Fun, ArgTypes, Args, FileLine, State) ->
@@ -168,7 +168,7 @@ store_race_call(Fun, ArgTypes, Args, FileLine, State) ->
   CurrFunLabel = Races#races.curr_fun_label,
   RaceTags = Races#races.race_tags,
   CleanState = dialyzer_dataflow:state__records_only(State),
-  {NewRaceList, NewRaceListSize, NewRaceTags, NewTable} = 
+  {NewRaceList, NewRaceListSize, NewRaceTags, NewTable} =
     case CurrFun of
       {_Module, module_info, A} when A =:= 0 orelse A =:= 1 ->
         {[], 0, RaceTags, no_t};
@@ -424,7 +424,7 @@ fixup_race_forward_pullout(CurrFun, CurrFunLabel, Calls, Code, RaceList,
                 Races = dialyzer_dataflow:state__get_races(State),
                 {RetCurrFun, RetCurrFunLabel, RetCalls, RetCode,
                  RetRaceList, RetRaceVarMap, RetFunDefVars, RetFunCallVars,
-                 RetFunArgTypes, RetNestingLevel} = 
+                 RetFunArgTypes, RetNestingLevel} =
                   fixup_race_forward_helper(NewCurrFun,
                       NewCurrFunLabel, Fun, Int, NewCalls, NewCalls,
                       [#curr_fun{status = out, mfa = NewCurrFun,
@@ -578,7 +578,7 @@ fixup_race_forward(CurrFun, CurrFunLabel, Calls, Code, RaceList,
           RaceTag ->
             PublicTables = dialyzer_callgraph:get_public_tables(Callgraph),
             NamedTables = dialyzer_callgraph:get_named_tables(Callgraph),
-            WarnVarArgs1 = 
+            WarnVarArgs1 =
               var_type_analysis(FunDefVars, FunArgTypes, WarnVarArgs,
                                 RaceWarnTag, RaceVarMap,
                                 dialyzer_dataflow:state__records_only(State)),
@@ -600,7 +600,7 @@ fixup_race_forward(CurrFun, CurrFunLabel, Calls, Code, RaceList,
                     [#warn_call{call_name = ets_insert, args = WarnVarArgs,
                                 var_map = RaceVarMap}],
                   [Tab, Names, _, _] = WarnVarArgs,
-                  case IsPublic orelse 
+                  case IsPublic orelse
                     compare_var_list(Tab, PublicTables, RaceVarMap)
                     orelse
                     length(Names -- NamedTables) < length(Names) of
@@ -638,7 +638,7 @@ fixup_race_forward(CurrFun, CurrFunLabel, Calls, Code, RaceList,
                  #curr_fun{mfa = CurrFun2, label = CurrFunLabel2,
                            var_map = RaceVarMap2, def_vars = FunDefVars2,
                            call_vars = FunCallVars2, arg_types = FunArgTypes2},
-                 Code2, NestingLevel2} = 
+                 Code2, NestingLevel2} =
                   remove_clause(NewRL,
                                 #curr_fun{mfa = CurrFun, label = CurrFunLabel,
                                           var_map = RaceVarMap1,
@@ -650,7 +650,7 @@ fixup_race_forward(CurrFun, CurrFunLabel, Calls, Code, RaceList,
                  RaceVarMap2, FunDefVars2, FunCallVars2, FunArgTypes2,
                  NestingLevel2, false};
               false ->
-                {CurrFun, CurrFunLabel, Tail, NewRL, RaceVarMap1, 
+                {CurrFun, CurrFunLabel, Tail, NewRL, RaceVarMap1,
                  FunDefVars, FunCallVars, FunArgTypes, NewNL, false}
             end;
           #end_clause{arg = Arg, pats = Pats, guard = Guard} ->
@@ -895,7 +895,7 @@ do_clause(RaceList, WarnVarArgs, RaceWarnTag, RaceVarMap, CurrLevel,
           PublicTables, NamedTables) ->
   {DepList, IsPublic, Continue} =
     get_deplist_paths(fixup_case_path(RaceList, 0), WarnVarArgs,
-		      RaceWarnTag, RaceVarMap, CurrLevel, 
+		      RaceWarnTag, RaceVarMap, CurrLevel,
                       PublicTables, NamedTables),
   {fixup_case_rest_paths(RaceList, 0), DepList, IsPublic, Continue}.
 
@@ -965,7 +965,7 @@ fixup_race_forward_helper(CurrFun, CurrFunLabel, Fun, FunLabel,
        #curr_fun{mfa = NewCurrFun, label = NewCurrFunLabel,
                  var_map = NewRaceVarMap, def_vars = NewFunDefVars,
                  call_vars = NewFunCallVars, arg_types = NewFunArgTypes},
-       NewCode, NewNestingLevel} = 
+       NewCode, NewNestingLevel} =
         remove_clause(RaceList,
         #curr_fun{mfa = CurrFun, label = CurrFunLabel, var_map = RaceVarMap,
                   def_vars = FunDefVars, call_vars = FunCallVars,
@@ -997,7 +997,7 @@ fixup_race_forward_helper(CurrFun, CurrFunLabel, Fun, FunLabel,
                        arg_types = NewFunTypes}],
             [#curr_fun{status = in, mfa = Fun,
                        label = FunLabel, var_map = NewRaceVarMap,
-                       def_vars = Args, call_vars = NewFunArgs, 
+                       def_vars = Args, call_vars = NewFunArgs,
                        arg_types = NewFunTypes}|
             lists:reverse(StateRaceList)] ++
             RetC, NewRaceVarMap),
@@ -1062,7 +1062,7 @@ fixup_race_backward(CurrFun, Calls, CallsToAnalyze, Parents, Height) ->
   case Height =:= 0 of
     true -> Parents;
     false ->
-      case Calls of 
+      case Calls of
         [] ->
           case is_integer(CurrFun) orelse lists:member(CurrFun, Parents) of
             true -> Parents;
@@ -1221,7 +1221,7 @@ are_bound_vars(Vars1, Vars2, RaceVarMap) ->
 callgraph__renew_tables(Table, Callgraph) ->
   case Table of
     {named, NameLabel, Names} ->
-      PTablesToAdd = 
+      PTablesToAdd =
         case NameLabel of
           ?no_label -> [];
           _Other -> [NameLabel]
@@ -1440,7 +1440,7 @@ lists_key_members_lists_helper(Elem, List, N) when is_integer(Elem) ->
   end;
 lists_key_members_lists_helper(_Elem, _List, _N) ->
   [0].
-          
+
 lists_key_replace(N, List, NewMember) ->
   {Before, [_|After]} = lists:split(N - 1, List),
   Before ++ [NewMember|After].
@@ -1490,7 +1490,7 @@ refine_race_helper(RaceCall, VarArgs, WarnVarArgs, RaceWarnTag, DependencyList,
     false -> DependencyList
   end.
 
-remove_clause(RaceList, CurrTuple, Code, NestingLevel) -> 
+remove_clause(RaceList, CurrTuple, Code, NestingLevel) ->
   NewRaceList = fixup_case_rest_paths(RaceList, 0),
   {NewCurrTuple, NewCode} =
     cleanup_clause_code(CurrTuple, Code, 0, NestingLevel),
@@ -1623,7 +1623,7 @@ compare_ets_insert(OldWarnVarArgs, NewWarnVarArgs, RaceVarMap) ->
         end
     end,
   case Bool of
-    true -> 
+    true ->
       case any_args(Old4) of
         true ->
           case compare_list_vars(Old3, ets_list_args(New3), [], RaceVarMap) of
@@ -1692,7 +1692,6 @@ compare_types(VarArgs, WarnVarArgs, RaceWarnTag, RaceVarMap) ->
             false ->
               compare_var_list(VA1, WVA1, RaceVarMap) orelse
                 compare_argtypes(VA2, WVA2)
-                
           end
       end;
     ?WARN_WHEREIS_UNREGISTER ->
@@ -1717,12 +1716,12 @@ compare_types(VarArgs, WarnVarArgs, RaceWarnTag, RaceVarMap) ->
           false ->
             case any_args(WVA2) of
               true -> compare_var_list(VA1, WVA1, RaceVarMap);
-              false -> 
+              false ->
                 compare_var_list(VA1, WVA1, RaceVarMap) orelse
                   compare_argtypes(VA2, WVA2)
             end
         end,
-      Bool andalso  
+      Bool andalso
         (case any_args(VA4) of
            true ->
              compare_var_list(VA3, WVA3, RaceVarMap);
@@ -2159,7 +2158,7 @@ race_var_map_guard_helper1(Arg, Pats, RaceVarMap, Op) ->
                     _Else -> {RaceVarMap, false}
                   end;
                 false -> {RaceVarMap, false}
-              end;                   
+              end;
             _Other -> {RaceVarMap, false}
           end;
         _Other -> {RaceVarMap, false}
@@ -2242,7 +2241,7 @@ var_analysis(FunDefArgs, FunCallArgs, WarnVarArgs, RaceWarnTag) ->
       [WVA1, WVA2|T] = WarnVarArgs,
       ArgNos = lists_key_members_lists(WVA1, FunDefArgs),
       [[lists_get(N, FunCallArgs) || N <- ArgNos], WVA2|T]
-  end.     
+  end.
 
 var_type_analysis(FunDefArgs, FunCallTypes, WarnVarArgs, RaceWarnTag,
                   RaceVarMap, CleanState) ->
@@ -2287,7 +2286,7 @@ var_type_analysis(FunDefArgs, FunCallTypes, WarnVarArgs, RaceWarnTag,
             ets_tuple_argtypes1(lists:nth(N2 + 1, FunVarArgs), [], [], 0),
             []),
           FirstVarArg ++ [Vars2, NewWVA4]
-          
+
       end;
     ?WARN_MNESIA_DIRTY_READ_WRITE ->
       [WVA1, WVA2|T] = WarnVarArgs,
@@ -2331,7 +2330,7 @@ get_race_warn(Fun, Args, ArgTypes, DepList, State) ->
 
 -spec get_race_warnings(races(), dialyzer_dataflow:state()) ->
   {races(), dialyzer_dataflow:state()}.
-  
+
 get_race_warnings(#races{race_warnings = RaceWarnings}, State) ->
   get_race_warnings_helper(RaceWarnings, State).
 
@@ -2431,12 +2430,12 @@ end_clause_new(Arg, Pats, Guard) ->
   #end_clause{arg = Arg, pats = Pats, guard = Guard}.
 
 -spec get_curr_fun(races()) -> mfa_or_funlbl().
-  
+
 get_curr_fun(#races{curr_fun = CurrFun}) ->
   CurrFun.
 
 -spec get_curr_fun_args(races()) -> core_args().
-  
+
 get_curr_fun_args(#races{curr_fun_args = CurrFunArgs}) ->
   CurrFunArgs.
 
@@ -2446,17 +2445,17 @@ get_new_table(#races{new_table = Table}) ->
   Table.
 
 -spec get_race_analysis(races()) -> boolean().
-  
+
 get_race_analysis(#races{race_analysis = RaceAnalysis}) ->
   RaceAnalysis.
 
 -spec get_race_list(races()) -> code().
-  
+
 get_race_list(#races{race_list = RaceList}) ->
   RaceList.
 
 -spec get_race_list_size(races()) -> non_neg_integer().
-  
+
 get_race_list_size(#races{race_list_size = RaceListSize}) ->
   RaceListSize.
 
@@ -2484,10 +2483,10 @@ put_fun_args(Args, #races{curr_fun_args = CurrFunArgs} = Races) ->
     empty -> Races#races{curr_fun_args = Args};
     _Other -> Races
   end.
-  
+
 -spec put_race_analysis(boolean(), races()) ->
   races().
-  
+
 put_race_analysis(Analysis, Races) ->
   Races#races{race_analysis = Analysis}.
 
diff --git a/lib/dialyzer/src/dialyzer_succ_typings.erl b/lib/dialyzer/src/dialyzer_succ_typings.erl
index 1ff4783852..8bfc66fc39 100644
--- a/lib/dialyzer/src/dialyzer_succ_typings.erl
+++ b/lib/dialyzer/src/dialyzer_succ_typings.erl
@@ -435,7 +435,7 @@ format_scc(SCC) ->
 %%
 %% ============================================================================
 
--spec doit(module() | string()) -> 'ok'.
+-spec doit(atom() | file:filename()) -> 'ok'.
 
 doit(Module) ->
   {ok, AbstrCode} = dialyzer_utils:get_abstract_code_from_src(Module),
diff --git a/lib/dialyzer/src/dialyzer_typesig.erl b/lib/dialyzer/src/dialyzer_typesig.erl
index 35b283a00a..3effb1c2e6 100644
--- a/lib/dialyzer/src/dialyzer_typesig.erl
+++ b/lib/dialyzer/src/dialyzer_typesig.erl
@@ -21,7 +21,7 @@
 %%%-------------------------------------------------------------------
 %%% File    : dialyzer_typesig.erl
 %%% Author  : Tobias Lindahl <[email protected]>
-%%% Description : 
+%%% Description :
 %%%
 %%% Created : 25 Apr 2005 by Tobias Lindahl <[email protected]>
 %%%-------------------------------------------------------------------
@@ -31,12 +31,12 @@
 -export([analyze_scc/5]).
 -export([get_safe_underapprox/2]).
 
--import(erl_types, 
+-import(erl_types,
 	[t_any/0, t_atom/0, t_atom_vals/1,
 	 t_binary/0, t_bitstr/0, t_bitstr/2, t_bitstr_concat/1, t_boolean/0,
 	 t_collect_vars/1, t_cons/2, t_cons_hd/1, t_cons_tl/1,
 	 t_float/0, t_from_range/2, t_from_term/1,
-	 t_fun/0, t_fun/2, t_fun_args/1, t_fun_range/1, 
+	 t_fun/0, t_fun/2, t_fun_args/1, t_fun_range/1,
 	 t_has_var/1,
 	 t_inf/2, t_inf/3, t_integer/0,
 	 t_is_any/1, t_is_atom/1, t_is_atom/2, t_is_cons/1, t_is_equal/2,
@@ -44,7 +44,7 @@
 	 t_is_integer/1, t_non_neg_integer/0,
 	 t_is_list/1, t_is_nil/1, t_is_none/1, t_is_number/1,
 
-	 t_is_subtype/2, t_limit/2, t_list/0, t_list/1, 
+	 t_is_subtype/2, t_limit/2, t_list/0, t_list/1,
 	 t_list_elements/1, t_nonempty_list/1, t_maybe_improper_list/0,
 	 t_module/0, t_number/0, t_number_vals/1,
 	 t_opaque_match_record/2, t_opaque_matching_structure/2,
@@ -101,7 +101,7 @@
 		name_map      = dict:new() :: dict(),
 		next_label                 :: label(),
 		non_self_recs = []         :: [label()],
-		plt                        :: dialyzer_plt:plt(), 
+		plt                        :: dialyzer_plt:plt(),
 		prop_types    = dict:new() :: dict(),
 		records       = dict:new() :: dict(),
 		opaques       = []         :: [erl_types:erl_type()],
@@ -140,8 +140,8 @@
 %%             where Def = {Var, Fun} as in the Core Erlang module definitions.
 %%                   Records = dict(RecName, {Arity, [{FieldName, FieldType}]})
 %% NextLabel - An integer that is higher than any label in the code.
-%% CallGraph - A callgraph as produced by dialyzer_callgraph.erl 
-%%             Note: The callgraph must have been built with all the 
+%% CallGraph - A callgraph as produced by dialyzer_callgraph.erl
+%%             Note: The callgraph must have been built with all the
 %%                   code that the SCC is a part of.
 %% PLT       - A dialyzer PLT. This PLT should contain available information
 %%             about functions that can be called by this SCC.
@@ -150,7 +150,7 @@
 %%-----------------------------------------------------------------------------
 
 -spec analyze_scc(typesig_scc(), label(),
-		  dialyzer_callgraph:callgraph(), 
+		  dialyzer_callgraph:callgraph(),
 		  dialyzer_plt:plt(), dict()) -> dict().
 
 analyze_scc(SCC, NextLabel, CallGraph, Plt, PropTypes) ->
@@ -202,7 +202,7 @@ traverse(Tree, DefinedVars, State) ->
       {State1, OpType} = traverse(Op, DefinedVars, State0),
       {State2, FunType} = state__get_fun_prototype(OpType, Arity, State1),
       State3 = state__store_conj(FunType, eq, OpType, State2),
-      State4 = state__store_conj(mk_var(Tree), sub, t_fun_range(FunType), 
+      State4 = state__store_conj(mk_var(Tree), sub, t_fun_range(FunType),
 				 State3),
       State5 = state__store_conj_lists(ArgTypes, sub, t_fun_args(FunType),
 				       State4),
@@ -216,7 +216,7 @@ traverse(Tree, DefinedVars, State) ->
 	  end
       end;
     binary ->
-      {State1, SegTypes} = traverse_list(cerl:binary_segments(Tree), 
+      {State1, SegTypes} = traverse_list(cerl:binary_segments(Tree),
 					 DefinedVars, State),
       Type = mk_fun_var(fun(Map) ->
 			    TmpSegTypes = lookup_type_list(SegTypes, Map),
@@ -227,7 +227,7 @@ traverse(Tree, DefinedVars, State) ->
       Size = cerl:bitstr_size(Tree),
       UnitVal = cerl:int_val(cerl:bitstr_unit(Tree)),
       Val = cerl:bitstr_val(Tree),
-      {State1, [SizeType, ValType]} = 
+      {State1, [SizeType, ValType]} =
 	traverse_list([Size, Val], DefinedVars, State),
       {State2, TypeConstr} =
 	case cerl:bitstr_bitsize(Tree) of
@@ -250,7 +250,7 @@ traverse(Tree, DefinedVars, State) ->
 	    case state__is_in_match(State1) of
 	      true ->
 		Flags = cerl:concrete(cerl:bitstr_flags(Tree)),
-		mk_fun_var(bitstr_val_constr(SizeType, UnitVal, Flags), 
+		mk_fun_var(bitstr_val_constr(SizeType, UnitVal, Flags),
 			   [SizeType]);
 	      false -> t_integer()
 	    end;
@@ -282,7 +282,7 @@ traverse(Tree, DefinedVars, State) ->
 	false ->
 	  ConsVar = mk_var(Tree),
 	  ConsType = mk_fun_var(fun(Map) ->
-				    t_cons(lookup_type(HdVar, Map), 
+				    t_cons(lookup_type(HdVar, Map),
 					   lookup_type(TlVar, Map))
 				end, [HdVar, TlVar]),
 	  HdType = mk_fun_var(fun(Map) ->
@@ -299,8 +299,8 @@ traverse(Tree, DefinedVars, State) ->
 				    true -> t_cons_tl(Cons)
 				  end
 			      end, [ConsVar]),
-	  State2 = state__store_conj_lists([HdVar, TlVar, ConsVar], sub, 
-					   [HdType, TlType, ConsType], 
+	  State2 = state__store_conj_lists([HdVar, TlVar, ConsVar], sub,
+					   [HdType, TlType, ConsType],
 					   State1),
 	  {State2, ConsVar}
       end;
@@ -314,14 +314,14 @@ traverse(Tree, DefinedVars, State) ->
 	  error -> t_fun(length(Vars), t_none());
 	  {ok, Dom} -> t_fun(Dom, t_none())
 	end,
-      State2 = 
+      State2 =
 	try
 	  State1 = case state__add_prop_constrs(Tree, State0) of
 		     not_called -> State0;
 		     PropState -> PropState
 		   end,
 	  {BodyState, BodyVar} = traverse(Body, DefinedVars1, State1),
-	  state__store_conj(mk_var(Tree), eq, 
+	  state__store_conj(mk_var(Tree), eq,
 			    t_fun(mk_var_list(Vars), BodyVar), BodyState)
 	catch
 	  throw:error ->
@@ -340,7 +340,7 @@ traverse(Tree, DefinedVars, State) ->
       Arg = cerl:let_arg(Tree),
       Body = cerl:let_body(Tree),
       {State1, ArgVars} = traverse(Arg, DefinedVars, State),
-      State2 = state__store_conj(t_product(mk_var_list(Vars)), eq, 
+      State2 = state__store_conj(t_product(mk_var_list(Vars)), eq,
 				 ArgVars, State1),
       DefinedVars1 = add_def_list(Vars, DefinedVars),
       traverse(Body, DefinedVars1, State2);
@@ -353,12 +353,12 @@ traverse(Tree, DefinedVars, State) ->
       DefinedVars1 = add_def_list(Vars, DefinedVars),
       {State2, _} = traverse_list(Funs, DefinedVars1, State1),
       traverse(Body, DefinedVars1, State2);
-    literal ->      
+    literal ->
       %% This is needed for finding records
       case cerl:unfold_literal(Tree) of
-	Tree -> 
+	Tree ->
 	  Type = t_from_term(cerl:concrete(Tree)),
-	  NewType = 
+	  NewType =
 	    case erl_types:t_opaque_match_atom(Type, State#state.opaques) of
 	      [Opaque] -> Opaque;
 	      _ -> Type
@@ -370,7 +370,7 @@ traverse(Tree, DefinedVars, State) ->
       Defs = cerl:module_defs(Tree),
       Funs = [Fun || {_Var, Fun} <- Defs],
       Vars = [Var || {Var, _Fun} <- Defs],
-      DefinedVars1 = add_def_list(Vars, DefinedVars),      
+      DefinedVars1 = add_def_list(Vars, DefinedVars),
       State1 = state__store_funs(Vars, Funs, State),
       FoldFun = fun(Fun, AccState) ->
 		    {S, _} = traverse(Fun, DefinedVars1,
@@ -388,7 +388,7 @@ traverse(Tree, DefinedVars, State) ->
     'receive' ->
       Clauses = filter_match_fail(cerl:receive_clauses(Tree)),
       Timeout = cerl:receive_timeout(Tree),
-      case (cerl:is_c_atom(Timeout) andalso 
+      case (cerl:is_c_atom(Timeout) andalso
 	    (cerl:atom_val(Timeout) =:= infinity)) of
 	true ->
 	  handle_clauses(Clauses, mk_var(Tree), [], DefinedVars, State);
@@ -421,7 +421,7 @@ traverse(Tree, DefinedVars, State) ->
 		      case t_has_var(Var) of
 			true ->
 			  {AccState1, NewVar} = state__mk_var(AccState),
-			  {NewVar, 
+			  {NewVar,
 			   state__store_conj(Var, eq, NewVar, AccState1)};
 			false ->
 			  {Var, AccState}
@@ -431,7 +431,7 @@ traverse(Tree, DefinedVars, State) ->
 	    {TmpState, t_tuple(NewEvars)}
 	end,
       case Elements of
-	[Tag|Fields] -> 
+	[Tag|Fields] ->
 	  case cerl:is_c_atom(Tag) of
 	    true ->
 	      %% Check if an opaque term is constructed.
@@ -534,7 +534,7 @@ handle_try(Tree, DefinedVars, State) ->
   Handler = cerl:try_handler(Tree),
   State1 = state__new_constraint_context(State),
   {ArgBodyState, BodyVar} =
-    try 
+    try
       {State2, ArgVar} = traverse(Arg, DefinedVars, State1),
       DefinedVars1 = add_def_list(Vars, DefinedVars),
       {State3, BodyVar1} = traverse(Body, DefinedVars1, State2),
@@ -542,17 +542,17 @@ handle_try(Tree, DefinedVars, State) ->
 				 State3),
       {State4, BodyVar1}
     catch
-      throw:error -> 
+      throw:error ->
 	{State1, t_none()}
     end,
   State6 = state__new_constraint_context(ArgBodyState),
   {HandlerState, HandlerVar} =
     try
-      DefinedVars2 = add_def_list([X || X <- EVars, cerl:is_c_var(X)], 
+      DefinedVars2 = add_def_list([X || X <- EVars, cerl:is_c_var(X)],
 				  DefinedVars),
       traverse(Handler, DefinedVars2, State6)
     catch
-      throw:error -> 
+      throw:error ->
 	{State6, t_none()}
     end,
   ArgBodyCs = state__cs(ArgBodyState),
@@ -561,7 +561,7 @@ handle_try(Tree, DefinedVars, State) ->
   OldCs = state__cs(State),
   case state__is_in_guard(State) of
     true ->
-      Conj1 = mk_conj_constraint_list([ArgBodyCs, 
+      Conj1 = mk_conj_constraint_list([ArgBodyCs,
 				       mk_constraint(BodyVar, eq, TreeVar)]),
       Disj = mk_disj_constraint_list([Conj1,
 				      mk_constraint(HandlerVar, eq, TreeVar)]),
@@ -573,10 +573,10 @@ handle_try(Tree, DefinedVars, State) ->
       {NewCs, ReturnVar} =
 	case {t_is_none(BodyVar), t_is_none(HandlerVar)} of
 	  {false, false} ->
-	    Conj1 = 
+	    Conj1 =
 	      mk_conj_constraint_list([ArgBodyCs,
 				       mk_constraint(TreeVar, eq, BodyVar)]),
-	    Conj2 = 
+	    Conj2 =
 	      mk_conj_constraint_list([HandlerCs,
 				       mk_constraint(TreeVar, eq, HandlerVar)]),
 	    Disj = mk_disj_constraint_list([Conj1, Conj2]),
@@ -603,7 +603,7 @@ handle_try(Tree, DefinedVars, State) ->
 %% Call
 %%
 
-handle_call(Call, DefinedVars, State) ->      
+handle_call(Call, DefinedVars, State) ->
   Args = cerl:call_args(Call),
   Mod = cerl:call_module(Call),
   Fun = cerl:call_name(Call),
@@ -618,7 +618,7 @@ handle_call(Call, DefinedVars, State) ->
       case state__lookup_rec_var_in_scope(MFA, State) of
 	error ->
 	  case get_bif_constr(MFA, Dst, ArgVars, State1) of
-	    none -> 
+	    none ->
 	      {get_plt_constr(MFA, Dst, ArgVars, State1), Dst};
 	    C ->
 	      {state__store_conj(C, State1), Dst}
@@ -647,7 +647,7 @@ get_plt_constr(MFA, Dst, ArgVars, State) ->
       case PltRes of
 	none -> State;
 	{value, {PltRetType, PltArgTypes}} ->
-	  state__store_conj_lists([Dst|ArgVars], sub, 
+	  state__store_conj_lists([Dst|ArgVars], sub,
 				  [PltRetType|PltArgTypes], State)
       end;
     {value, #contract{args = GenArgs} = C} ->
@@ -655,7 +655,7 @@ get_plt_constr(MFA, Dst, ArgVars, State) ->
 	case PltRes of
 	  none ->
 	    {mk_fun_var(fun(Map) ->
-			    ArgTypes = lookup_type_list(ArgVars, Map), 
+			    ArgTypes = lookup_type_list(ArgVars, Map),
 			    dialyzer_contracts:get_contract_return(C, ArgTypes)
 			end, ArgVars), GenArgs};
 	  {value, {PltRetType, PltArgTypes}} ->
@@ -692,7 +692,7 @@ filter_match_fail([Clause] = Cls) ->
 filter_match_fail([H|T]) ->
   [H|filter_match_fail(T)];
 filter_match_fail([]) ->
-  %% This can actually happen, for example in 
+  %% This can actually happen, for example in
   %%      receive after 1 -> ok end
   [].
 
@@ -714,16 +714,16 @@ handle_clauses(Clauses, TopVar, Arg, Action, DefinedVars, State) ->
     if length(Clauses) > ?MAX_NOF_CLAUSES -> overflow;
        true -> []
     end,
-  {State1, CList} = handle_clauses_1(Clauses, TopVar, Arg, DefinedVars, 
+  {State1, CList} = handle_clauses_1(Clauses, TopVar, Arg, DefinedVars,
 				     State, SubtrTypeList, []),
   {NewCs, NewState} =
     case Action of
-      none -> 
+      none ->
 	if CList =:= [] -> throw(error);
 	   true -> {CList, State1}
 	end;
-      _ -> 
-	try 
+      _ ->
+	try
 	  {State2, ActionVar} = traverse(Action, DefinedVars, State1),
 	  TmpC = mk_constraint(TopVar, eq, ActionVar),
 	  ActionCs = mk_conj_constraint_list([state__cs(State2),TmpC]),
@@ -740,7 +740,7 @@ handle_clauses(Clauses, TopVar, Arg, Action, DefinedVars, State) ->
   FinalState = state__new_constraint_context(NewState),
   {state__store_conj_list([OldCs, NewCList], FinalState), TopVar}.
 
-handle_clauses_1([Clause|Tail], TopVar, Arg, DefinedVars, 
+handle_clauses_1([Clause|Tail], TopVar, Arg, DefinedVars,
 		 State, SubtrTypes, Acc) ->
   State0 = state__new_constraint_context(State),
   Pats = cerl:clause_pats(Clause),
@@ -749,22 +749,22 @@ handle_clauses_1([Clause|Tail], TopVar, Arg, DefinedVars,
   NewSubtrTypes =
     case SubtrTypes =:= overflow of
       true -> overflow;
-      false -> 
+      false ->
 	ordsets:add_element(get_safe_underapprox(Pats, Guard), SubtrTypes)
     end,
-  try 
+  try
     DefinedVars1 = add_def_from_tree_list(Pats, DefinedVars),
     State1 = state__set_in_match(State0, true),
     {State2, PatVars} = traverse_list(Pats, DefinedVars1, State1),
     State3 =
       case Arg =:= [] of
 	true -> State2;
-        false -> 
+        false ->
 	  S = state__store_conj(Arg, eq, t_product(PatVars), State2),
 	  case SubtrTypes =:= overflow of
 	    true -> S;
 	    false ->
-	      SubtrPatVar = mk_fun_var(fun(Map) -> 
+	      SubtrPatVar = mk_fun_var(fun(Map) ->
 					   TmpType = lookup_type(Arg, Map),
 					   t_subtract_list(TmpType, SubtrTypes)
 				       end, [Arg]),
@@ -772,15 +772,15 @@ handle_clauses_1([Clause|Tail], TopVar, Arg, DefinedVars,
 	  end
       end,
     State4 = handle_guard(Guard, DefinedVars1, State3),
-    {State5, BodyVar} = traverse(Body, DefinedVars1, 
+    {State5, BodyVar} = traverse(Body, DefinedVars1,
 				 state__set_in_match(State4, false)),
     State6 = state__store_conj(TopVar, eq, BodyVar, State5),
     Cs = state__cs(State6),
-    handle_clauses_1(Tail, TopVar, Arg, DefinedVars, State6, 
+    handle_clauses_1(Tail, TopVar, Arg, DefinedVars, State6,
 		     NewSubtrTypes, [Cs|Acc])
   catch
-    throw:error -> 
-      handle_clauses_1(Tail, TopVar, Arg, DefinedVars, 
+    throw:error ->
+      handle_clauses_1(Tail, TopVar, Arg, DefinedVars,
 		       State, NewSubtrTypes, Acc)
   end;
 handle_clauses_1([], _TopVar, _Arg, _DefinedVars, State, _SubtrType, Acc) ->
@@ -792,7 +792,7 @@ get_safe_underapprox(Pats, Guard) ->
   try
     Map1 = cerl_trees:fold(fun(X, Acc) ->
 			       case cerl:is_c_var(X) of
-				 true -> 
+				 true ->
 				   dict:store(cerl_trees:get_label(X), t_any(),
 					      Acc);
 				 false -> Acc
@@ -804,8 +804,8 @@ get_safe_underapprox(Pats, Guard) ->
 	     false ->
 	       case cerl:is_c_var(Guard) of
 		 false -> Map2;
-		 true -> 
-		   dict:store(cerl_trees:get_label(Guard), 
+		 true ->
+		   dict:store(cerl_trees:get_label(Guard),
 			      t_from_term(true), Map2)
 	       end
 	   end,
@@ -819,8 +819,8 @@ get_underapprox_from_guard(Tree, Map) ->
   True = t_from_term(true),
   case cerl:type(Tree) of
     call ->
-      case {cerl:concrete(cerl:call_module(Tree)), 
-	    cerl:concrete(cerl:call_name(Tree)), 
+      case {cerl:concrete(cerl:call_module(Tree)),
+	    cerl:concrete(cerl:call_name(Tree)),
 	    length(cerl:call_args(Tree))} of
 	{erlang, is_function, 2} ->
 	  [Fun, Arity] = cerl:call_args(Tree),
@@ -856,15 +856,15 @@ get_underapprox_from_guard(Tree, Map) ->
 		{erlang, '==', 2} -> throw(dont_know);
 		{erlang, 'and', 2} ->
 		  [Arg1, Arg2] = cerl:call_args(Tree),
-		  case ((cerl:is_c_var(Arg1) orelse cerl:is_literal(Arg1)) 
+		  case ((cerl:is_c_var(Arg1) orelse cerl:is_literal(Arg1))
 			andalso
 			(cerl:is_c_var(Arg2) orelse cerl:is_literal(Arg2))) of
 		    true ->
 		      {Arg1Type, _} = get_underapprox_from_guard(Arg1, Map),
 		      {Arg2Type, _} = get_underapprox_from_guard(Arg2, Map),
-		      case (t_is_equal(True, Arg1Type) andalso 
+		      case (t_is_equal(True, Arg1Type) andalso
 			    t_is_equal(True, Arg2Type)) of
-			true -> {True, Map}; 
+			true -> {True, Map};
 			false -> throw(dont_know)
 		      end;
 		    false ->
@@ -876,7 +876,7 @@ get_underapprox_from_guard(Tree, Map) ->
 	  end
       end;
     var ->
-      Type = 
+      Type =
 	case dict:find(cerl_trees:get_label(Tree), Map) of
 	  error -> throw(dont_know);
 	  {ok, T} -> T
@@ -931,7 +931,7 @@ bitstr_constr(SizeType, UnitVal) ->
 	      MinSize = erl_types:number_min(TmpSizeType),
 	      t_bitstr(UnitVal, MinSize * UnitVal)
 	  end;
-	false -> 
+	false ->
 	  t_bitstr(UnitVal, 0)
       end
   end.
@@ -975,9 +975,9 @@ get_safe_underapprox_1([Pat|Left], Acc, Map) ->
       end;
     binary ->
       %% TODO: Can maybe do something here
-      throw(dont_know);      
+      throw(dont_know);
     cons ->
-      {[Hd, Tl], Map1} = 
+      {[Hd, Tl], Map1} =
 	get_safe_underapprox_1([cerl:cons_hd(Pat), cerl:cons_tl(Pat)], [], Map),
       case t_is_any(Tl) of
 	true -> get_safe_underapprox_1(Left, [t_nonempty_list(Hd)|Acc], Map1);
@@ -1020,7 +1020,7 @@ get_safe_underapprox_1([], Acc, Map) ->
 %% Guards
 %%
 
-handle_guard(Guard, DefinedVars, State) ->  
+handle_guard(Guard, DefinedVars, State) ->
   True = t_from_term(true),
   State1 = state__set_in_guard(State, true),
   State2 = state__new_constraint_context(State1),
@@ -1039,7 +1039,7 @@ handle_guard(Guard, DefinedVars, State) ->
 %%
 %%=============================================================================
 
-get_bif_constr({erlang, Op, 2}, Dst, Args = [Arg1, Arg2], _State) 
+get_bif_constr({erlang, Op, 2}, Dst, Args = [Arg1, Arg2], _State)
   when Op =:= '+'; Op =:= '-'; Op =:= '*' ->
   ReturnType = mk_fun_var(fun(Map) ->
 			      TmpArgTypes = lookup_type_list(Args, Map),
@@ -1047,14 +1047,14 @@ get_bif_constr({erlang, Op, 2}, Dst, Args = [Arg1, Arg2], _State)
 			  end, Args),
   ArgFun =
     fun(A, Pos) ->
-	F = 
+	F =
 	  fun(Map) ->
 	      DstType = lookup_type(Dst, Map),
 	      AType = lookup_type(A, Map),
 	      case t_is_integer(DstType) of
 		true ->
 		  case t_is_integer(AType) of
-		    true -> 
+		    true ->
 		      eval_inv_arith(Op, Pos, DstType, AType);
 		    false  ->
 		      %% This must be temporary.
@@ -1062,7 +1062,7 @@ get_bif_constr({erlang, Op, 2}, Dst, Args = [Arg1, Arg2], _State)
 		  end;
 		false ->
 		  case t_is_float(DstType) of
-		    true -> 
+		    true ->
 		      case t_is_integer(AType) of
 			true -> t_float();
 			false -> t_number()
@@ -1079,9 +1079,9 @@ get_bif_constr({erlang, Op, 2}, Dst, Args = [Arg1, Arg2], _State)
   mk_conj_constraint_list([mk_constraint(Dst, sub, ReturnType),
 			   mk_constraint(Arg1, sub, Arg1FunVar),
 			   mk_constraint(Arg2, sub, Arg2FunVar)]);
-get_bif_constr({erlang, Op, 2}, Dst, [Arg1, Arg2] = Args, _State) 
+get_bif_constr({erlang, Op, 2}, Dst, [Arg1, Arg2] = Args, _State)
   when Op =:= '<'; Op =:= '=<'; Op =:= '>'; Op =:= '>=' ->
-  ArgFun = 
+  ArgFun =
     fun(LocalArg1, LocalArg2, LocalOp) ->
 	fun(Map) ->
 	    DstType = lookup_type(Dst, Map),
@@ -1098,19 +1098,19 @@ get_bif_constr({erlang, Op, 2}, Dst, [Arg1, Arg2] = Args, _State)
 		    Max2 = erl_types:number_max(Arg2Type),
 		    Min2 = erl_types:number_min(Arg2Type),
 		    case LocalOp of
-		      '=<' -> 
+		      '=<' ->
 			if IsTrue  -> t_from_range(Min1, Max2);
 			   IsFalse -> t_from_range(range_inc(Min2), Max1)
 			end;
-		      '<'  -> 
+		      '<'  ->
 			if IsTrue  -> t_from_range(Min1, range_dec(Max2));
 			   IsFalse -> t_from_range(Min2, Max1)
 			end;
-		      '>=' -> 
+		      '>=' ->
 			if IsTrue  -> t_from_range(Min2, Max1);
 			   IsFalse -> t_from_range(Min1, range_dec(Max2))
 			end;
-		      '>'  -> 
+		      '>'  ->
 			if IsTrue  -> t_from_range(range_inc(Min2), Max1);
 			   IsFalse -> t_from_range(Min1, Max2)
 			end
@@ -1131,7 +1131,7 @@ get_bif_constr({erlang, Op, 2}, Dst, [Arg1, Arg2] = Args, _State)
   DstArgs = [Dst, Arg1, Arg2],
   Arg1Var = mk_fun_var(Arg1Fun, DstArgs),
   Arg2Var = mk_fun_var(Arg2Fun, DstArgs),
-  DstVar = mk_fun_var(fun(Map) -> 
+  DstVar = mk_fun_var(fun(Map) ->
 			  TmpArgTypes = lookup_type_list(Args, Map),
 			  erl_bif_types:type(erlang, Op, 2, TmpArgTypes)
 		      end, Args),
@@ -1143,9 +1143,9 @@ get_bif_constr({erlang, '++', 2}, Dst, [Hd, Tl] = Args, _State) ->
 	      DstType = lookup_type(Dst, Map),
 	      case t_is_cons(DstType) of
 		true -> t_list(t_cons_hd(DstType));
-		false -> 
+		false ->
 		  case t_is_list(DstType) of
-		    true -> 
+		    true ->
 		      case t_is_nil(DstType) of
 			true -> DstType;
 			false -> t_list(t_list_elements(DstType))
@@ -1160,7 +1160,7 @@ get_bif_constr({erlang, '++', 2}, Dst, [Hd, Tl] = Args, _State) ->
 		true -> t_sup(t_cons_tl(DstType), DstType);
 		false ->
 		  case t_is_list(DstType) of
-		    true -> 
+		    true ->
 		      case t_is_nil(DstType) of
 			true -> DstType;
 			false -> t_list(t_list_elements(DstType))
@@ -1170,10 +1170,10 @@ get_bif_constr({erlang, '++', 2}, Dst, [Hd, Tl] = Args, _State) ->
 	      end
 	  end,
   DstL = [Dst],
-  HdVar = mk_fun_var(HdFun, DstL),  
+  HdVar = mk_fun_var(HdFun, DstL),
   TlVar = mk_fun_var(TlFun, DstL),
   ArgTypes = erl_bif_types:arg_types(erlang, '++', 2),
-  ReturnType = mk_fun_var(fun(Map) -> 
+  ReturnType = mk_fun_var(fun(Map) ->
 			      TmpArgTypes = lookup_type_list(Args, Map),
 			      erl_bif_types:type(erlang, '++', 2, TmpArgTypes)
 			  end, Args),
@@ -1198,7 +1198,7 @@ get_bif_constr({erlang, is_function, 2}, Dst, [Fun, Arity], _State) ->
   ArgFun = fun(Map) ->
 	       DstType = lookup_type(Dst, Map),
 	       case t_is_atom(true, DstType) of
-		 true -> 
+		 true ->
 		   ArityType = lookup_type(Arity, Map),
 		   case t_number_vals(ArityType) of
 		     unknown -> t_fun();
@@ -1231,7 +1231,7 @@ get_bif_constr({erlang, is_record, 2}, Dst, [Var, Tag] = Args, _State) ->
 	       end
 	   end,
   ArgV = mk_fun_var(ArgFun, [Dst]),
-  DstFun = fun(Map) -> 
+  DstFun = fun(Map) ->
 	       TmpArgTypes = lookup_type_list(Args, Map),
 	       erl_bif_types:type(erlang, is_record, 2, TmpArgTypes)
 	   end,
@@ -1241,7 +1241,7 @@ get_bif_constr({erlang, is_record, 2}, Dst, [Var, Tag] = Args, _State) ->
 			   mk_constraint(Var, sub, ArgV)]);
 get_bif_constr({erlang, is_record, 3}, Dst, [Var, Tag, Arity] = Args, State) ->
   %% TODO: Revise this to make it precise for Tag and Arity.
-  ArgFun = 
+  ArgFun =
     fun(Map) ->
 	case t_is_atom(true, lookup_type(Dst, Map)) of
 	  true ->
@@ -1257,14 +1257,14 @@ get_bif_constr({erlang, is_record, 3}, Dst, [Var, Tag, Arity] = Args, State) ->
 			GenRecord = t_tuple([TagType|AnyElems]),
 			case t_atom_vals(TagType) of
 			  [TagVal] ->
-			    case state__lookup_record(State, TagVal, 
+			    case state__lookup_record(State, TagVal,
 						      ArityVal - 1) of
 			      {ok, Type} ->
 				AllOpaques = State#state.opaques,
 				case t_opaque_match_record(Type, AllOpaques) of
 				  [Opaque] -> Opaque;
 				  _ -> Type
-				end;			      
+				end;
 			      error -> GenRecord
 			    end;
 			  _ -> GenRecord
@@ -1279,9 +1279,9 @@ get_bif_constr({erlang, is_record, 3}, Dst, [Var, Tag, Arity] = Args, State) ->
 	end
     end,
   ArgV = mk_fun_var(ArgFun, [Tag, Arity, Dst]),
-  DstFun = fun(Map) -> 
+  DstFun = fun(Map) ->
 	       [TmpVar, TmpTag, TmpArity] = TmpArgTypes = lookup_type_list(Args, Map),
-	       TmpArgTypes2 = 
+	       TmpArgTypes2 =
 		 case lists:member(TmpVar, State#state.opaques) of
 		   true ->
 		     case t_is_integer(TmpArity) of
@@ -1293,7 +1293,7 @@ get_bif_constr({erlang, is_record, 3}, Dst, [Var, Tag, Arity] = Args, State) ->
 				 case t_atom_vals(TmpTag) of
 				   [TmpTagVal] ->
 				     case state__lookup_record(State, TmpTagVal, TmpArityVal - 1) of
-				       {ok, TmpType} -> 
+				       {ok, TmpType} ->
 					 case t_is_none(t_inf(TmpType, TmpVar, opaque)) of
 					   true  -> TmpArgTypes;
 					   false -> [TmpType, TmpTag, TmpArity]
@@ -1312,7 +1312,7 @@ get_bif_constr({erlang, is_record, 3}, Dst, [Var, Tag, Arity] = Args, State) ->
 		 end,
 	       erl_bif_types:type(erlang, is_record, 3, TmpArgTypes2)
 	   end,
-  DstV = mk_fun_var(DstFun, Args),  
+  DstV = mk_fun_var(DstFun, Args),
   mk_conj_constraint_list([mk_constraint(Dst, sub, DstV),
 			   mk_constraint(Arity, sub, t_integer()),
 			   mk_constraint(Tag, sub, t_atom()),
@@ -1334,7 +1334,7 @@ get_bif_constr({erlang, 'and', 2}, Dst, [Arg1, Arg2] = Args, _State) ->
 			     true -> False;
 			     false -> t_boolean()
 			   end;
-			 false -> 
+			 false ->
 			   t_boolean()
 		       end
 		   end
@@ -1349,7 +1349,7 @@ get_bif_constr({erlang, 'and', 2}, Dst, [Arg1, Arg2] = Args, _State) ->
 		   case t_is_atom(false, Arg2Type) of
 		     true -> False;
 		     false ->
-		       case (t_is_atom(true, Arg1Type) 
+		       case (t_is_atom(true, Arg1Type)
 			     andalso t_is_atom(true, Arg2Type)) of
 			 true -> True;
 			 false -> t_boolean()
@@ -1378,7 +1378,7 @@ get_bif_constr({erlang, 'or', 2}, Dst, [Arg1, Arg2] = Args, _State) ->
 			     true -> True;
 			     false -> t_boolean()
 			   end;
-			 false -> 
+			 false ->
 			   t_boolean()
 		       end
 		   end
@@ -1393,7 +1393,7 @@ get_bif_constr({erlang, 'or', 2}, Dst, [Arg1, Arg2] = Args, _State) ->
 		   case t_is_atom(true, Arg2Type) of
 		     true -> True;
 		     false ->
-		       case (t_is_atom(false, Arg1Type) 
+		       case (t_is_atom(false, Arg1Type)
 			     andalso t_is_atom(false, Arg2Type)) of
 			 true -> False;
 			 false -> t_boolean()
@@ -1414,7 +1414,7 @@ get_bif_constr({erlang, 'or', 2}, Dst, [Arg1, Arg2] = Args, _State) ->
 get_bif_constr({erlang, 'not', 1}, Dst, [Arg] = Args, _State) ->
   True = t_from_term(true),
   False = t_from_term(false),
-  Fun = fun(Var) -> 
+  Fun = fun(Var) ->
 	    fun(Map) ->
 		Type = lookup_type(Var, Map),
 		case t_is_atom(true, Type) of
@@ -1439,7 +1439,7 @@ get_bif_constr({erlang, '=:=', 2}, Dst, [Arg1, Arg2] = Args, _State) ->
 	    OtherVarType = lookup_type(OtherVar, Map),
 	    case t_is_atom(true, DstType) of
 	      true -> OtherVarType;
-	      false -> 
+	      false ->
 		case t_is_atom(false, DstType) of
 		  true ->
 		    case is_singleton_type(OtherVarType) of
@@ -1492,7 +1492,7 @@ get_bif_constr({erlang, '==', 2}, Dst, [Arg1, Arg2] = Args, _State) ->
 		  true ->
 		    case t_is_number(VarType) of
 		      true -> t_number();
-		      false -> 
+		      false ->
 			case t_is_atom(VarType) of
 			  true -> VarType;
 			  false -> t_any()
@@ -1511,7 +1511,8 @@ get_bif_constr({erlang, '==', 2}, Dst, [Arg1, Arg2] = Args, _State) ->
   mk_conj_constraint_list([mk_constraint(Dst, sub, DstV),
 			   mk_constraint(Arg1, sub, ArgV1),
 			   mk_constraint(Arg2, sub, ArgV2)]);
-get_bif_constr({erlang, element, 2} = _BIF, Dst, Args, State) ->
+get_bif_constr({erlang, element, 2} = _BIF, Dst, Args,
+               #state{cs = Constrs} = State) ->
   GenType = erl_bif_types:type(erlang, element, 2),
   case t_is_none(GenType) of
     true -> ?debug("Bif: ~w failed\n", [_BIF]), throw(error);
@@ -1525,9 +1526,14 @@ get_bif_constr({erlang, element, 2} = _BIF, Dst, Args, State) ->
 		erl_bif_types:type(erlang, element, 2, ATs2)
 	    end,
       ReturnType = mk_fun_var(Fun, Args),
-      ArgTypes = erl_bif_types:arg_types(erlang, element, 2),      
+      ArgTypes = erl_bif_types:arg_types(erlang, element, 2),
       Cs = mk_constraints(Args, sub, ArgTypes),
-      mk_conj_constraint_list([mk_constraint(Dst, sub, ReturnType)|Cs])
+      NewCs =
+        case find_element(Args, Constrs) of
+          'unknown' -> Cs;
+          Elem -> [mk_constraint(Dst, eq, Elem)|Cs]
+        end,
+      mk_conj_constraint_list([mk_constraint(Dst, sub, ReturnType)|NewCs])
   end;
 get_bif_constr({M, F, A} = _BIF, Dst, Args, State) ->
   GenType = erl_bif_types:type(M, F, A),
@@ -1541,7 +1547,7 @@ get_bif_constr({M, F, A} = _BIF, Dst, Args, State) ->
 		    false -> T
 		  end
 	end,
-      ReturnType = mk_fun_var(fun(Map) -> 
+      ReturnType = mk_fun_var(fun(Map) ->
 				  TmpArgTypes0 = lookup_type_list(Args, Map),
 				  TmpArgTypes = [UnopaqueFun(T) || T<- TmpArgTypes0],
 				  erl_bif_types:type(M, F, A, TmpArgTypes)
@@ -1561,12 +1567,12 @@ get_bif_constr({M, F, A} = _BIF, Dst, Args, State) ->
       end
   end.
 
-eval_inv_arith('+', _Pos, Dst, Arg) -> 
+eval_inv_arith('+', _Pos, Dst, Arg) ->
   erl_bif_types:type(erlang, '-', 2, [Dst, Arg]);
-eval_inv_arith('*', _Pos, Dst, Arg) -> 
+eval_inv_arith('*', _Pos, Dst, Arg) ->
   case t_number_vals(Arg) of
     [0] -> t_integer();
-    _ -> 
+    _ ->
       TmpRet = erl_bif_types:type(erlang, 'div', 2, [Dst, Arg]),
       Zero = t_from_term(0),
       %% If 0 is not part of the result, it cannot be part of the argument.
@@ -1575,9 +1581,9 @@ eval_inv_arith('*', _Pos, Dst, Arg) ->
 	true -> TmpRet
       end
   end;
-eval_inv_arith('-', 1, Dst, Arg) -> 
+eval_inv_arith('-', 1, Dst, Arg) ->
   erl_bif_types:type(erlang, '-', 2, [Arg, Dst]);
-eval_inv_arith('-', 2, Dst, Arg) -> 
+eval_inv_arith('-', 2, Dst, Arg) ->
   erl_bif_types:type(erlang, '+', 2, [Arg, Dst]).
 
 range_inc(neg_inf) -> neg_inf;
@@ -1614,7 +1620,7 @@ get_bif_test_constr(Dst, Arg, Type, State) ->
 		       end;
 		     false ->  t_from_term(false)
 		   end;
-		 false -> 
+		 false ->
 		   case t_is_subtype(ArgType, Type) of
 		     true -> t_from_term(true);
 		     false -> t_boolean()
@@ -1632,11 +1638,11 @@ get_bif_test_constr(Dst, Arg, Type, State) ->
 %%=============================================================================
 
 solve([Fun], State) ->
-  ?debug("============ Analyzing Fun: ~w ===========\n", 
+  ?debug("============ Analyzing Fun: ~w ===========\n",
 	 [debug_lookup_name(Fun)]),
   solve_fun(Fun, dict:new(), State);
 solve([_|_] = SCC, State) ->
-  ?debug("============ Analyzing SCC: ~w ===========\n", 
+  ?debug("============ Analyzing SCC: ~w ===========\n",
 	 [[debug_lookup_name(F) || F <- SCC]]),
   solve_scc(SCC, dict:new(), State, false).
 
@@ -1655,7 +1661,7 @@ solve_fun(Fun, FunMap, State) ->
 
 solve_scc(SCC, Map, State, TryingUnit) ->
   State1 = state__mark_as_non_self_rec(SCC, State),
-  Vars0 = [{Fun, state__get_rec_var(Fun, State)} || Fun <- SCC],  
+  Vars0 = [{Fun, state__get_rec_var(Fun, State)} || Fun <- SCC],
   Vars = [Var || {_, {ok, Var}} <- Vars0],
   Funs = [Fun || {Fun, {ok, _}} <- Vars0],
   Types = unsafe_lookup_type_list(Funs, Map),
@@ -1682,7 +1688,7 @@ solve_scc(SCC, Map, State, TryingUnit) ->
 	false ->
 	  Map2
       end;
-    false -> 
+    false ->
       ?debug("SCC ~w did not reach fixpoint\n", [SCC]),
       solve_scc(SCC, Map2, State, TryingUnit)
   end.
@@ -1704,29 +1710,29 @@ scc_fold_fun(F, FunMap, State) ->
 						  format_type(NewType)]),
   NewFunMap.
 
-solve_ref_or_list(#constraint_ref{id = Id, deps = Deps}, 
+solve_ref_or_list(#constraint_ref{id = Id, deps = Deps},
 		  Map, MapDict, State) ->
-  {OldLocalMap, Check} = 
+  {OldLocalMap, Check} =
     case dict:find(Id, MapDict) of
       error -> {dict:new(), false};
       {ok, M} -> {M, true}
-    end,  
+    end,
   ?debug("Checking ref to fun: ~w\n", [debug_lookup_name(Id)]),
   CheckDeps = ordsets:del_element(t_var_name(Id), Deps),
   case Check andalso maps_are_equal(OldLocalMap, Map, CheckDeps) of
-    true -> 
+    true ->
       ?debug("Equal\n", []),
       {ok, MapDict, Map};
     false ->
       ?debug("Not equal. Solving\n", []),
       Cs = state__get_cs(Id, State),
-      Res = 
+      Res =
 	case state__is_self_rec(Id, State) of
 	  true -> solve_self_recursive(Cs, Map, MapDict, Id, t_none(), State);
 	  false -> solve_ref_or_list(Cs, Map, MapDict, State)
 	end,
       case Res of
-	{error, NewMapDict} ->	  
+	{error, NewMapDict} ->
 	  ?debug("Error solving for function ~p\n", [debug_lookup_name(Id)]),
 	  Arity = state__fun_arity(Id, State),
 	  FunType =
@@ -1755,17 +1761,17 @@ solve_ref_or_list(#constraint_ref{id = Id, deps = Deps},
   end;
 solve_ref_or_list(#constraint_list{type=Type, list = Cs, deps = Deps, id = Id},
 		  Map, MapDict, State) ->
-  {OldLocalMap, Check} = 
+  {OldLocalMap, Check} =
     case dict:find(Id, MapDict) of
       error -> {dict:new(), false};
       {ok, M} -> {M, true}
     end,
   ?debug("Checking ref to list: ~w\n", [Id]),
   case Check andalso maps_are_equal(OldLocalMap, Map, Deps) of
-    true -> 
+    true ->
       ?debug("~w equal ~w\n", [Type, Id]),
       {ok, MapDict, Map};
-    false -> 
+    false ->
       ?debug("~w not equal: ~w. Solving\n", [Type, Id]),
       solve_clist(Cs, Type, Id, Deps, MapDict, Map, State)
   end.
@@ -1793,7 +1799,7 @@ solve_self_recursive(Cs, Map, MapDict, Id, RecType0, State) ->
 	     [[{X, format_type(Y)} || {X, Y} <- dict:to_list(NewMap)]]),
       NewRecType = unsafe_lookup_type(Id, NewMap),
       case t_is_equal(NewRecType, RecType0) of
-	true -> 	  
+	true ->
 	  {ok, NewMapDict, enter_type(RecVar, NewRecType, NewMap)};
 	false ->
 	  solve_self_recursive(Cs, Map, MapDict, Id, NewRecType, State)
@@ -1801,7 +1807,7 @@ solve_self_recursive(Cs, Map, MapDict, Id, RecType0, State) ->
   end.
 
 solve_clist(Cs, conj, Id, Deps, MapDict, Map, State) ->
-  case solve_cs(Cs, Map, MapDict, State) of 
+  case solve_cs(Cs, Map, MapDict, State) of
     {error, _} = Error -> Error;
     {ok, NewMapDict, NewMap} = Ret ->
       case Cs of
@@ -1821,12 +1827,12 @@ solve_clist(Cs, disj, Id, _Deps, MapDict, Map, State) ->
 	      {ok, NewDict, NewMap} -> {{ok, NewMap}, NewDict};
 	      {error, _NewDict} = Error -> Error
 	    end
-	end,  
+	end,
   {Maps, NewMapDict} = lists:mapfoldl(Fun, MapDict, Cs),
   case [X || {ok, X} <- Maps] of
     [] -> {error, NewMapDict};
-    MapList -> 
-      NewMap = join_maps(MapList),      
+    MapList ->
+      NewMap = join_maps(MapList),
       {ok, dict:store(Id, NewMap, NewMapDict), NewMap}
   end.
 
@@ -1844,13 +1850,13 @@ solve_cs([#constraint{} = C|Tail], Map, MapDict, State) ->
   case solve_one_c(C, Map, State#state.opaques) of
     error ->
       ?debug("+++++++++++\nFailed: ~s :: ~s ~w ~s :: ~s\n+++++++++++\n",
-	     [format_type(C#constraint.lhs), 
+	     [format_type(C#constraint.lhs),
 	      format_type(lookup_type(C#constraint.lhs, Map)),
 	      C#constraint.op,
-	      format_type(C#constraint.rhs), 
+	      format_type(C#constraint.rhs),
 	      format_type(lookup_type(C#constraint.rhs, Map))]),
       {error, MapDict};
-    {ok, NewMap} -> 
+    {ok, NewMap} ->
       solve_cs(Tail, NewMap, MapDict, State)
   end;
 solve_cs([], Map, MapDict, _State) ->
@@ -1863,7 +1869,7 @@ solve_one_c(#constraint{lhs = Lhs, rhs = Rhs, op = Op}, Map, Opaques) ->
   ?debug("Solving: ~s :: ~s ~w ~s :: ~s\n\tInf: ~s\n",
 	 [format_type(Lhs), format_type(LhsType), Op,
 	  format_type(Rhs), format_type(RhsType), format_type(Inf)]),
-  case t_is_none(Inf) of 
+  case t_is_none(Inf) of
     true -> error;
     false ->
       case Op of
@@ -1887,8 +1893,8 @@ solve_subtype(Type, Inf, Map, Opaques) ->
       try t_unify(Type, Inf, Opaques) of
 	{_, List} -> {ok, enter_type_list(List, Map)}
       catch
-	throw:{mismatch, _T1, _T2} -> 
-	  ?debug("Mismatch between ~s and ~s\n", 
+	throw:{mismatch, _T1, _T2} ->
+	  ?debug("Mismatch between ~s and ~s\n",
 		 [format_type(_T1), format_type(_T2)]),
 	  error
       end.
@@ -1936,9 +1942,9 @@ maps_are_equal_1(Map1, Map2, [H|Tail]) ->
   T2 = lookup_type(H, Map2),
   case t_is_equal(T1, T2) of
     true -> maps_are_equal_1(Map1, Map2, Tail);
-    false -> 
+    false ->
       ?debug("~w: ~s =/= ~s\n", [H, format_type(T1), format_type(T2)]),
-      false      
+      false
   end;
 maps_are_equal_1(_Map1, _Map2, []) ->
   true.
@@ -1953,7 +1959,7 @@ prune_keys(Map1, Map2, Deps) ->
     true ->
       Keys1 = dict:fetch_keys(Map1),
       case length(Keys1) > NofDeps of
-	true -> 
+	true ->
 	  Set1 = lists:sort(Keys1),
 	  Set2 = lists:sort(dict:fetch_keys(Map2)),
 	  ordsets:intersection(ordsets:union(Set1, Set2), Deps);
@@ -2035,7 +2041,7 @@ lookup_type(Key, Map) ->
 mk_var(Var) ->
   case cerl:is_literal(Var) of
     true -> Var;
-    false -> 
+    false ->
       case cerl:is_c_values(Var) of
 	true -> t_product(mk_var_no_lit_list(cerl:values_es(Var)));
 	false -> t_var(cerl_trees:get_label(Var))
@@ -2076,10 +2082,10 @@ state__set_opaques(#state{records = RecDict} = State, {M, _F, _A}) ->
 
 state__lookup_record(#state{records = Records}, Tag, Arity) ->
   case erl_types:lookup_record(Tag, Arity, Records) of
-    {ok, Fields} -> 
+    {ok, Fields} ->
       {ok, t_tuple([t_from_term(Tag)|
 		    [FieldType || {_FieldName, FieldType} <- Fields]])};
-    error -> 
+    error ->
       error
   end.
 
@@ -2098,12 +2104,12 @@ state__is_in_guard(#state{in_guard = Bool}) ->
 state__get_fun_prototype(Op, Arity, State) ->
   case t_is_fun(Op) of
     true -> {State, Op};
-    false -> 
+    false ->
       {State1, [Ret|Args]} = state__mk_vars(Arity+1, State),
       Fun = t_fun(Args, Ret),
       {State1, Fun}
   end.
-    
+
 state__lookup_rec_var_in_scope(MFA, #state{name_map = NameMap}) ->
   dict:find(MFA, NameMap).
 
@@ -2115,11 +2121,11 @@ state__store_fun_arity(Tree, #state{fun_arities = Map} = State) ->
 state__fun_arity(Id, #state{fun_arities = Map}) ->
   dict:fetch(Id, Map).
 
-state__lookup_undef_var(Tree, #state{callgraph = CG, plt = Plt}) ->  
+state__lookup_undef_var(Tree, #state{callgraph = CG, plt = Plt}) ->
   Label = cerl_trees:get_label(Tree),
   case dialyzer_callgraph:lookup_rec_var(Label, CG) of
     error -> error;
-    {ok, MFA} -> 
+    {ok, MFA} ->
       case dialyzer_plt:lookup(Plt, MFA) of
 	none -> error;
 	{value, {RetType, ArgTypes}} -> {ok, t_fun(ArgTypes, RetType)}
@@ -2179,7 +2185,7 @@ state__add_prop_constrs(Tree, #state{prop_types = PropTypes} = State) ->
 	  case erl_types:any_none(ArgTypes) of
 	    true -> not_called;
 	    false ->
-	      ?debug("Adding propagated constr: ~s for function ~w\n", 
+	      ?debug("Adding propagated constr: ~s for function ~w\n",
 		     [format_type(FunType), debug_lookup_name(mk_var(Tree))]),
 	      FunVar = mk_var(Tree),
 	      state__store_conj(FunVar, sub, FunType, State)
@@ -2225,7 +2231,7 @@ state__store_conj_lists_1([], _Op, [], State) ->
 
 state__mk_var(#state{next_label = NL} = State) ->
   {State#state{next_label = NL+1}, t_var(NL)}.
-  
+
 state__mk_vars(N, #state{next_label = NL} = State) ->
   NewLabel = NL + N,
   Vars = [t_var(X) || X <- lists:seq(NL, NewLabel-1)],
@@ -2235,7 +2241,7 @@ state__store_constrs(Id, Cs, #state{cmap = Dict} = State) ->
   NewDict = dict:store(Id, Cs, Dict),
   State#state{cmap = NewDict}.
 
-state__get_cs(Var, #state{cmap = Dict}) ->  
+state__get_cs(Var, #state{cmap = Dict}) ->
   dict:fetch(Var, Dict).
 
 %% The functions here will not be treated as self recursive.
@@ -2286,7 +2292,7 @@ mk_constraint(Lhs, Op, Rhs) ->
 	  %% This constraint is constant. Solve it immediately.
 	  case solve_one_c(C, dict:new(), []) of
 	    error -> throw(error);
-	    _ -> 
+	    _ ->
 	      %% This is always true, keep it anyway for logistic reasons
 	      C
 	  end;
@@ -2335,7 +2341,7 @@ mk_constraint_1(Lhs, eq, Rhs) when Lhs < Rhs ->
 mk_constraint_1(Lhs, eq, Rhs) ->
   #constraint{lhs = Rhs, op = eq, rhs = Lhs};
 mk_constraint_1(Lhs, Op, Rhs) ->
-  #constraint{lhs = Lhs, op = Op, rhs = Rhs}.  
+  #constraint{lhs = Lhs, op = Op, rhs = Rhs}.
 
 mk_constraints([Lhs|LhsTail], Op, [Rhs|RhsTail]) ->
   [mk_constraint(Lhs, Op, Rhs)|mk_constraints(LhsTail, Op, RhsTail)];
@@ -2350,7 +2356,7 @@ mk_constraint_list(Type, List) ->
   List2 = ordsets:filter(fun(X) -> get_deps(X) =/= [] end, List1),
   Deps = calculate_deps(List2),
   case Deps =:= [] of
-    true -> #constraint_list{type = conj, 
+    true -> #constraint_list{type = conj,
 			     list = [mk_constraint(t_any(), eq, t_any())],
 			     deps = []};
     false -> #constraint_list{type = Type, list = List2, deps = Deps}
@@ -2372,11 +2378,11 @@ update_constraint_list(CL, List) ->
 %% We expand guard constraints into dijunctive normal form to gain
 %% precision in simple guards. However, because of the exponential
 %% growth of this expansion in the presens of disjunctions we can even
-%% get into trouble while expanding. 
+%% get into trouble while expanding.
 %%
 %% To limit this we only expand when the number of disjunctions are
 %% below a certain limit. This limit is currently set based on the
-%% behaviour of boolean 'or'. 
+%% behaviour of boolean 'or'.
 %%
 %%         V1 = V2 or V3
 %%
@@ -2395,7 +2401,7 @@ update_constraint_list(CL, List) ->
 -define(DISJ_NORM_FORM_LIMIT, 28).
 
 mk_disj_norm_form(#constraint_list{} = CL) ->
-  try 
+  try
     List1 = expand_to_conjunctions(CL),
     mk_disj_constraint_list(List1)
   catch
@@ -2409,7 +2415,7 @@ expand_to_conjunctions(#constraint_list{type = conj, list = List}) ->
     true -> [mk_conj_constraint_list(List1)];
     false ->
       case List2 of
-	[JustOneList] -> 
+	[JustOneList] ->
 	  [mk_conj_constraint_list([L|List1]) || L <- JustOneList];
 	_ ->
 	  combine_conj_lists(List2, List1)
@@ -2422,7 +2428,7 @@ expand_to_conjunctions(#constraint_list{type = disj, list = List}) ->
   List1 = [C || C <- List, is_simple_constraint(C)],
   %% Just an assert.
   [] = [C || #constraint{} = C <- List1],
-  Expanded = lists:flatten([expand_to_conjunctions(C) 
+  Expanded = lists:flatten([expand_to_conjunctions(C)
 			    || #constraint_list{} = C <- List]),
   ReturnList = Expanded ++ List1,
   if length(ReturnList) > ?DISJ_NORM_FORM_LIMIT -> throw(too_many_disj);
@@ -2467,7 +2473,7 @@ wrap_simple_constr(#constraint_list{} = C) -> C;
 wrap_simple_constr(#constraint_ref{} = C) -> C.
 
 enumerate_constraints(State) ->
-  Cs = [mk_constraint_ref(Id, get_deps(state__get_cs(Id, State))) 
+  Cs = [mk_constraint_ref(Id, get_deps(state__get_cs(Id, State)))
 	|| Id <- state__scc(State)],
   {_, _, NewState} = enumerate_constraints(Cs, 0, [], State),
   NewState.
@@ -2475,9 +2481,9 @@ enumerate_constraints(State) ->
 enumerate_constraints([#constraint_ref{id = Id} = C|Tail], N, Acc, State) ->
   Cs = state__get_cs(Id, State),
   {[NewCs], NewN, NewState1} = enumerate_constraints([Cs], N, [], State),
-  NewState2 = state__store_constrs(Id, NewCs, NewState1),  
+  NewState2 = state__store_constrs(Id, NewCs, NewState1),
   enumerate_constraints(Tail, NewN+1, [C|Acc], NewState2);
-enumerate_constraints([#constraint_list{type = conj, list = List} = C|Tail], 
+enumerate_constraints([#constraint_list{type = conj, list = List} = C|Tail],
 		      N, Acc, State) ->
   %% Separate the flat constraints from the deep ones to make a
   %% separate fixpoint interation over the flat ones for speed.
@@ -2496,7 +2502,7 @@ enumerate_constraints([#constraint_list{type = conj, list = List} = C|Tail],
     end,
   NewAcc = [C#constraint_list{list = NewList, id = {list, N3}}|Acc],
   enumerate_constraints(Tail, N3+1, NewAcc, State2);
-enumerate_constraints([#constraint_list{list = List, type = disj} = C|Tail], 
+enumerate_constraints([#constraint_list{list = List, type = disj} = C|Tail],
 		      N, Acc, State) ->
   {NewList, NewN, NewState} = enumerate_constraints(List, N, [], State),
   NewAcc = [C#constraint_list{list = NewList, id = {list, NewN}}|Acc],
@@ -2515,7 +2521,7 @@ group_constraints_in_components(Cs, N) ->
   case find_dep_components(DepList, []) of
     [_] -> {Cs, N};
     [_|_] = Components ->
-      ConstrComp = [[C || #constraint{deps = D} = C <- Cs, 
+      ConstrComp = [[C || #constraint{deps = D} = C <- Cs,
 			  ordsets:is_subset(D, Comp)]
 		    || Comp <- Components],
       lists:mapfoldl(fun(CComp, TmpN) ->
@@ -2545,7 +2551,7 @@ find_dep_components([], AccSet, Ungrouped) ->
 %% Put the fun ref constraints last in any conjunction since we need
 %% to separate the environment from the interior of the function.
 order_fun_constraints(State) ->
-  Cs = [mk_constraint_ref(Id, get_deps(state__get_cs(Id, State))) 
+  Cs = [mk_constraint_ref(Id, get_deps(state__get_cs(Id, State)))
 	|| Id <- state__scc(State)],
   order_fun_constraints(Cs, State).
 
@@ -2565,8 +2571,8 @@ order_fun_constraints([#constraint_list{list = List, type = Type} = C|Tail],
     case Type of
       conj -> order_fun_constraints(List, [], [], State);
       disj ->
-	FoldFun = fun(X, AccState) -> 
-		      {[NewX], NewAccState} = 
+	FoldFun = fun(X, AccState) ->
+		      {[NewX], NewAccState} =
 			order_fun_constraints([X], [], [], AccState),
 		      {NewX, NewAccState}
 		  end,
@@ -2588,7 +2594,7 @@ order_fun_constraints([], Funs, Acc, State) ->
 
 is_singleton_non_number_type(Type) ->
   case t_is_number(Type) of
-    true -> false;    
+    true -> false;
     false -> is_singleton_type(Type)
   end.
 
@@ -2613,6 +2619,41 @@ is_singleton_type(Type) ->
       end
   end.
 
+find_element(Args, Cs) ->
+  [Pos, Tuple] = Args,
+  case erl_types:t_is_number(Pos) of
+    true ->
+      case erl_types:t_number_vals(Pos) of
+        'unknown' -> 'unknown';
+        [I] ->
+          case find_constraint(Tuple, Cs) of
+            'unknown' -> 'unknown';
+            #constraint{lhs = ExTuple} ->
+              case erl_types:t_is_tuple(ExTuple) of
+                true ->
+                  Elems = erl_types:t_tuple_args(ExTuple),
+                  Elem = lists:nth(I, Elems),
+                  case erl_types:t_is_var(Elem) of
+                    true -> Elem;
+                    false -> 'unknown'
+                  end;
+                false -> 'unknown'
+              end
+          end;
+        _ -> 'unknown'
+      end;
+    false -> 'unknown'
+  end.
+
+find_constraint(_Tuple, []) ->
+  'unknown';
+find_constraint(Tuple, [#constraint{op = 'eq', rhs = Tuple} = C|_]) ->
+  C;
+find_constraint(Tuple, [#constraint_list{list = List}|Cs]) ->
+  find_constraint(Tuple, List ++ Cs);
+find_constraint(Tuple, [_|Cs]) ->
+  find_constraint(Tuple, Cs).
+
 %% ============================================================================
 %%
 %%  Pretty printer and debug facilities.
@@ -2638,7 +2679,7 @@ format_type(Type) ->
 -ifdef(DEBUG_NAME_MAP).
 debug_make_name_map(Vars, Funs) ->
   Map = get(dialyzer_typesig_map),
-  NewMap = 
+  NewMap =
     if Map =:= undefined -> debug_make_name_map(Vars, Funs, dict:new());
        true              -> debug_make_name_map(Vars, Funs, Map)
     end,
@@ -2676,15 +2717,15 @@ pp_constraints(Cs, State) ->
   io:nl(),
   Res.
 
-pp_constraints([List|Tail], Separator, Level, MaxDepth, 
+pp_constraints([List|Tail], Separator, Level, MaxDepth,
 	       State) when is_list(List) ->
   pp_constraints(List++Tail, Separator, Level, MaxDepth, State);
-pp_constraints([#constraint_ref{id = Id}|Left], Separator, 
+pp_constraints([#constraint_ref{id = Id}|Left], Separator,
 	       Level, MaxDepth, State) ->
   Cs = state__get_cs(Id, State),
   io:format("%Ref ~w%", [t_var_name(Id)]),
   pp_constraints([Cs|Left], Separator, Level, MaxDepth, State);
-pp_constraints([#constraint{lhs = Lhs, op = Op, rhs = Rhs}], _Separator, 
+pp_constraints([#constraint{lhs = Lhs, op = Op, rhs = Rhs}], _Separator,
 	       Level, MaxDepth, _State) ->
   io:format("~s ~w ~s", [format_type(Lhs), Op, format_type(Rhs)]),
   erlang:max(Level, MaxDepth);
@@ -2721,7 +2762,7 @@ pp_constrs_scc(_SCC, _State) ->
 
 constraints_to_dot_scc(SCC, State) ->
   io:format("SCC: ~p\n", [SCC]),
-  Name = lists:flatten([io_lib:format("'~w'", [debug_lookup_name(Fun)]) 
+  Name = lists:flatten([io_lib:format("'~w'", [debug_lookup_name(Fun)])
 			|| Fun <- SCC]),
   Cs = [state__get_cs(Fun, State) || Fun <- SCC],
   constraints_to_dot(Cs, Name, State).
@@ -2737,22 +2778,22 @@ constraints_to_dot(Cs0, Name, State) ->
 
 constraints_to_nodes([{Name, #constraint_list{type = Type, list = List, id=Id}}
 		      |Left], N, Level, Graph, Opts, State) ->
-  N1 = N + length(List), 
+  N1 = N + length(List),
   NewList = lists:zip(lists:seq(N, N1 - 1), List),
   Names = [SubName || {SubName, _C} <- NewList],
   Edges = [{Name, SubName} || SubName <- Names],
-  ThisNode = [{Name, Opt} || Opt <- [{label, 
+  ThisNode = [{Name, Opt} || Opt <- [{label,
 				      lists:flatten(io_lib:format("~w", [Id]))},
 				     {shape, get_shape(Type)},
 				     {level, Level}]],
-  {NewGraph, NewOpts, N2} = constraints_to_nodes(NewList, N1, Level+1, 
-						 [Edges|Graph], 
+  {NewGraph, NewOpts, N2} = constraints_to_nodes(NewList, N1, Level+1,
+						 [Edges|Graph],
 						 [ThisNode|Opts], State),
   constraints_to_nodes(Left, N2, Level, NewGraph, NewOpts, State);
 constraints_to_nodes([{Name, #constraint{lhs = Lhs, op = Op, rhs = Rhs}}|Left],
 		     N, Level, Graph, Opts, State) ->
-  Label = lists:flatten(io_lib:format("~s ~w ~s", 
-				      [format_type(Lhs), Op, 
+  Label = lists:flatten(io_lib:format("~s ~w ~s",
+				      [format_type(Lhs), Op,
 				       format_type(Rhs)])),
   ThisNode = [{Name, Opt} || Opt <- [{label, Label}, {level, Level}]],
   NewOpts = [ThisNode|Opts],
@@ -2761,20 +2802,20 @@ constraints_to_nodes([{Name, #constraint_ref{id = Id0}}|Left],
 		     N, Level, Graph, Opts, State) ->
   Id = debug_lookup_name(Id0),
   CList = state__get_cs(Id0, State),
-  ThisNode = [{Name, Opt} || Opt <- [{label, 
+  ThisNode = [{Name, Opt} || Opt <- [{label,
 				      lists:flatten(io_lib:format("~w", [Id]))},
 				     {shape, ellipse},
-				     {level, Level}]],  
-  NewList = [{N, CList}],  
-  {NewGraph, NewOpts, N1} = constraints_to_nodes(NewList, N + 1, Level + 1, 
+				     {level, Level}]],
+  NewList = [{N, CList}],
+  {NewGraph, NewOpts, N1} = constraints_to_nodes(NewList, N + 1, Level + 1,
 						 [{Name, N}|Graph],
 						 [ThisNode|Opts], State),
   constraints_to_nodes(Left, N1, Level, NewGraph, NewOpts, State);
 constraints_to_nodes([], N, _Level, Graph, Opts, _State) ->
   {lists:flatten(Graph), lists:flatten(Opts), N}.
-  
+
 get_shape(conj) -> box;
-get_shape(disj) -> diamond.  
+get_shape(disj) -> diamond.
 
 -else.
 constraints_to_dot_scc(_SCC, _State) ->
diff --git a/lib/dialyzer/src/dialyzer_utils.erl b/lib/dialyzer/src/dialyzer_utils.erl
index 338027c5ab..a9da229061 100644
--- a/lib/dialyzer/src/dialyzer_utils.erl
+++ b/lib/dialyzer/src/dialyzer_utils.erl
@@ -21,7 +21,7 @@
 %%%-------------------------------------------------------------------
 %%% File    : dialyzer_utils.erl
 %%% Author  : Tobias Lindahl <[email protected]>
-%%% Description : 
+%%% Description :
 %%%
 %%% Created :  5 Dec 2006 by Tobias Lindahl <[email protected]>
 %%%-------------------------------------------------------------------
@@ -74,12 +74,11 @@ print_types1([{record, _Name} = Key|T], RecDict) ->
 -define(debug(D_), ok).
 -endif.
 
-%%
-%%  Types that need to be imported from somewhere else
-%%
+%% ----------------------------------------------------------------------------
 
--type abstract_code() :: [tuple()]. %% XXX: refine
--type comp_options()  :: [atom()].  %% XXX: a restricted set of options is used
+-type abstract_code() :: [tuple()]. %% XXX: import from somewhere
+-type comp_options()  :: [compile:option()].
+-type mod_or_fname()  :: atom() | file:filename().
 
 %% ============================================================================
 %%
@@ -87,13 +86,13 @@ print_types1([{record, _Name} = Key|T], RecDict) ->
 %%
 %% ============================================================================
 
--spec get_abstract_code_from_src(atom() | file:filename()) ->
+-spec get_abstract_code_from_src(mod_or_fname()) ->
 	{'ok', abstract_code()} | {'error', [string()]}.
 
 get_abstract_code_from_src(File) ->
   get_abstract_code_from_src(File, src_compiler_opts()).
 
--spec get_abstract_code_from_src(atom() | file:filename(), comp_options()) ->
+-spec get_abstract_code_from_src(mod_or_fname(), comp_options()) ->
 	{'ok', abstract_code()} | {'error', [string()]}.
 
 get_abstract_code_from_src(File, Opts) ->
@@ -176,7 +175,7 @@ get_record_and_type_info(AbstractCode) ->
 get_record_and_type_info(AbstractCode, Module, RecDict) ->
   get_record_and_type_info(AbstractCode, Module, [], RecDict).
 
-get_record_and_type_info([{attribute, _, record, {Name, Fields0}}|Left], 
+get_record_and_type_info([{attribute, _, record, {Name, Fields0}}|Left],
 			 Module, Records, RecDict) ->
   {ok, Fields} = get_record_fields(Fields0, RecDict),
   Arity = length(Fields),
@@ -189,7 +188,7 @@ get_record_and_type_info([{attribute, _, type, {{record, Name}, Fields0, []}}
   Arity = length(Fields),
   NewRecDict = dict:store({record, Name}, [{Arity, Fields}], RecDict),
   get_record_and_type_info(Left, Module, Records, NewRecDict);
-get_record_and_type_info([{attribute, _, Attr, {Name, TypeForm}}|Left], 
+get_record_and_type_info([{attribute, _, Attr, {Name, TypeForm}}|Left],
 			 Module, Records, RecDict) when Attr =:= 'type';
                                                         Attr =:= 'opaque' ->
   try
@@ -198,7 +197,7 @@ get_record_and_type_info([{attribute, _, Attr, {Name, TypeForm}}|Left],
   catch
     throw:{error, _} = Error -> Error
   end;
-get_record_and_type_info([{attribute, _, Attr, {Name, TypeForm, Args}}|Left], 
+get_record_and_type_info([{attribute, _, Attr, {Name, TypeForm, Args}}|Left],
 			 Module, Records, RecDict) when Attr =:= 'type';
                                                         Attr =:= 'opaque' ->
   try
@@ -220,7 +219,7 @@ get_record_and_type_info([], _Module, Records, RecDict) ->
   end.
 
 add_new_type(TypeOrOpaque, Name, TypeForm, ArgForms, Module, RecDict) ->
-  case erl_types:type_is_defined(TypeOrOpaque, Name, RecDict) of 
+  case erl_types:type_is_defined(TypeOrOpaque, Name, RecDict) of
     true ->
       throw({error, io_lib:format("Type already defined: ~w\n", [Name])});
     false ->
@@ -238,7 +237,7 @@ add_new_type(TypeOrOpaque, Name, TypeForm, ArgForms, Module, RecDict) ->
 get_record_fields(Fields, RecDict) ->
   get_record_fields(Fields, RecDict, []).
 
-get_record_fields([{typed_record_field, OrdRecField, TypeForm}|Left], 
+get_record_fields([{typed_record_field, OrdRecField, TypeForm}|Left],
 		  RecDict, Acc) ->
   Name =
     case OrdRecField of
@@ -313,19 +312,19 @@ merge_records(NewRecords, OldRecords) ->
 %%
 %% ============================================================================
 
--spec get_spec_info(module(), abstract_code(), dict()) ->
+-spec get_spec_info(atom(), abstract_code(), dict()) ->
         {'ok', dict()} | {'error', string()}.
 
 get_spec_info(ModName, AbstractCode, RecordsDict) ->
   get_spec_info(AbstractCode, dict:new(), RecordsDict, ModName, "nofile").
 
-%% TypeSpec is a list of conditional contracts for a function. 
+%% TypeSpec is a list of conditional contracts for a function.
 %% Each contract is of the form {[Argument], Range, [Constraint]} where
 %%  - Argument and Range are in erl_types:erl_type() format and
 %%  - Constraint is of the form {subtype, T1, T2} where T1 and T2
 %%    are erl_types:erl_type()
 
-get_spec_info([{attribute, Ln, spec, {Id, TypeSpec}}|Left], 
+get_spec_info([{attribute, Ln, spec, {Id, TypeSpec}}|Left],
 	      SpecDict, RecordsDict, ModName, File) when is_list(TypeSpec) ->
   MFA = case Id of
 	  {_, _, _} = T -> T;
@@ -340,7 +339,7 @@ get_spec_info([{attribute, Ln, spec, {Id, TypeSpec}}|Left],
     {ok, {{OtherFile, L},_C}} ->
       {Mod, Fun, Arity} = MFA,
       Msg = io_lib:format("  Contract for function ~w:~w/~w "
-			  "already defined in ~s:~w\n", 
+			  "already defined in ~s:~w\n",
 			  [Mod, Fun, Arity, OtherFile, L]),
       throw({error, Msg})
   catch
@@ -376,7 +375,7 @@ sets_filter([Mod|Mods], ExpTypes) ->
 %%
 %% ============================================================================
 
--spec src_compiler_opts() -> comp_options().
+-spec src_compiler_opts() -> [compile:option(),...].
 
 src_compiler_opts() ->
   [no_copt, to_core, binary, return_errors, 
@@ -401,7 +400,7 @@ cleanup_parse_transforms([]) ->
 -spec format_errors([{module(), string()}]) -> [string()].
 
 format_errors([{Mod, Errors}|Left]) ->
-  FormatedError = 
+  FormatedError =
     [io_lib:format("~s:~w: ~s\n", [Mod, Line, M:format_error(Desc)])
      || {Line, M, Desc} <- Errors],
   [lists:flatten(FormatedError) | format_errors(Left)];
@@ -476,7 +475,7 @@ pp_size(Size, Ctxt, Cont) ->
   end.
 
 pp_opts(Type, Flags) ->
-  FinalFlags = 
+  FinalFlags =
     case cerl:atom_val(Type) of
       binary -> [];
       float -> keep_endian(cerl:concrete(Flags));
diff --git a/lib/dialyzer/vsn.mk b/lib/dialyzer/vsn.mk
index e3e3f6d668..f2daf86def 100644
--- a/lib/dialyzer/vsn.mk
+++ b/lib/dialyzer/vsn.mk
@@ -1 +1 @@
-DIALYZER_VSN = 2.2.0
+DIALYZER_VSN = 2.3.0
diff --git a/lib/hipe/cerl/cerl_closurean.erl b/lib/hipe/cerl/cerl_closurean.erl
index 12771668ac..021acd5b35 100644
--- a/lib/hipe/cerl/cerl_closurean.erl
+++ b/lib/hipe/cerl/cerl_closurean.erl
@@ -1,19 +1,19 @@
 %%
 %% %CopyrightBegin%
-%% 
-%% Copyright Ericsson AB 2003-2009. All Rights Reserved.
-%% 
+%%
+%% Copyright Ericsson AB 2003-2010. All Rights Reserved.
+%%
 %% The contents of this file are subject to the Erlang Public License,
 %% Version 1.1, (the "License"); you may not use this file except in
 %% compliance with the License. You should have received a copy of the
 %% Erlang Public License along with this software. If not, it can be
 %% retrieved online at http://www.erlang.org/.
-%% 
+%%
 %% Software distributed under the License is distributed on an "AS IS"
 %% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See
 %% the License for the specific language governing rights and limitations
 %% under the License.
-%% 
+%%
 %% %CopyrightEnd%
 %%
 %% =====================================================================
@@ -808,7 +808,7 @@ take_work({Queue0, Set0}) ->
 is_escape_op(match_fail, 1) -> false; 
 is_escape_op(F, A) when is_atom(F), is_integer(A) -> true.
 
--spec is_escape_op(module(), atom(), arity()) -> boolean().
+-spec is_escape_op(atom(), atom(), arity()) -> boolean().
 
 is_escape_op(erlang, error, 1) -> false;
 is_escape_op(erlang, error, 2) -> false;
@@ -825,7 +825,7 @@ is_escape_op(M, F, A) when is_atom(M), is_atom(F), is_integer(A) -> true.
 is_literal_op(match_fail, 1) -> true;
 is_literal_op(F, A) when is_atom(F), is_integer(A) -> false.
 
--spec is_literal_op(module(), atom(), arity()) -> boolean().
+-spec is_literal_op(atom(), atom(), arity()) -> boolean().
 
 is_literal_op(erlang, '+', 2) -> true;
 is_literal_op(erlang, '-', 2) -> true;
diff --git a/lib/hipe/cerl/cerl_messagean.erl b/lib/hipe/cerl/cerl_messagean.erl
index 0753376e7d..6dd93adaa3 100644
--- a/lib/hipe/cerl/cerl_messagean.erl
+++ b/lib/hipe/cerl/cerl_messagean.erl
@@ -1,19 +1,19 @@
 %% =====================================================================
 %% %CopyrightBegin%
-%% 
-%% Copyright Ericsson AB 2004-2009. All Rights Reserved.
-%% 
+%%
+%% Copyright Ericsson AB 2004-2010. All Rights Reserved.
+%%
 %% The contents of this file are subject to the Erlang Public License,
 %% Version 1.1, (the "License"); you may not use this file except in
 %% compliance with the License. You should have received a copy of the
 %% Erlang Public License along with this software. If not, it can be
 %% retrieved online at http://www.erlang.org/.
-%% 
+%%
 %% Software distributed under the License is distributed on an "AS IS"
 %% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See
 %% the License for the specific language governing rights and limitations
 %% under the License.
-%% 
+%%
 %% %CopyrightEnd%
 %%
 %% Message analysis of Core Erlang programs.
@@ -1043,7 +1043,7 @@ get_deps(L, Dep) ->
 
 %% is_escape_op(_F, _A) -> [].
 
--spec is_escape_op(module(), atom(), arity()) -> [arity()].
+-spec is_escape_op(atom(), atom(), arity()) -> [arity()].
 
 is_escape_op(erlang, '!', 2) -> [2];
 is_escape_op(erlang, send, 2) -> [2];
@@ -1064,7 +1064,7 @@ is_escape_op(_M, _F, _A) -> [].
 is_imm_op(match_fail, 1) -> true; 
 is_imm_op(_, _) -> false.
 
--spec is_imm_op(module(), atom(), arity()) -> boolean().
+-spec is_imm_op(atom(), atom(), arity()) -> boolean().
 
 is_imm_op(erlang, self, 0) -> true;
 is_imm_op(erlang, '=:=', 2) -> true;
@@ -1102,4 +1102,4 @@ is_imm_op(erlang, throw, 1) -> true;
 is_imm_op(erlang, exit, 1) -> true;
 is_imm_op(erlang, error, 1) -> true;
 is_imm_op(erlang, error, 2) -> true;
-is_imm_op(_, _, _) -> false.
+is_imm_op(_M, _F, _A) -> false.
diff --git a/lib/hipe/cerl/erl_types.erl b/lib/hipe/cerl/erl_types.erl
index c1d80740a1..9a40be6d14 100644
--- a/lib/hipe/cerl/erl_types.erl
+++ b/lib/hipe/cerl/erl_types.erl
@@ -205,6 +205,7 @@
 	 t_var_name/1,
 	 %% t_assign_variables_to_subtype/2,
 	 type_is_defined/3,
+	 record_field_diffs_to_string/2,
 	 subst_all_vars_to_any/1,
 	 lift_list_to_pos_empty/1,
 	 is_erl_type/1
@@ -303,7 +304,7 @@
 %% Auxiliary types and convenient macros
 %%
 
--type parse_form() :: {atom(), _, _} | {atom(), _, _, _}. %% XXX: Temporarily
+-type parse_form() :: {atom(), _, _} | {atom(), _, _, _} | {'op', _, _, _, _}. %% XXX: Temporarily
 -type rng_elem()   :: 'pos_inf' | 'neg_inf' | integer().
 
 -record(int_set, {set :: [integer()]}).
@@ -653,7 +654,7 @@ module_builtin_opaques(Module) ->
 %% Remote types: these types are used for preprocessing;
 %% they should never reach the analysis stage.
 
--spec t_remote(module(), atom(), [_]) -> erl_type().
+-spec t_remote(atom(), atom(), [erl_type()]) -> erl_type().
 
 t_remote(Mod, Name, Args) ->
   ?remote(set_singleton(#remote{mod = Mod, name = Name, args = Args})).
@@ -758,9 +759,8 @@ t_solve_remote_type(#remote{mod = RemMod, name = Name, args = Args} = RemType,
               throw({error, Msg})
           end;
         false ->
-          Msg = io_lib:format("Unable to find exported type ~w:~w/~w\n",
-                              [RemMod, Name, ArgsLen]),
-          throw({error, Msg})
+          self() ! {self(), ext_types, {RemMod, Name, ArgsLen}},
+          {t_any(), []}
       end
   end.
 
@@ -1608,7 +1608,7 @@ t_set() ->
 t_tid() ->
   t_opaque(ets, tid, [], t_integer()).
 
--spec all_opaque_builtins() -> [erl_type()].
+-spec all_opaque_builtins() -> [erl_type(),...].
 
 all_opaque_builtins() ->
   [t_array(), t_dict(), t_digraph(), t_gb_set(),
@@ -3312,28 +3312,44 @@ record_to_string(Tag, [_|Fields], FieldNames, RecDict) ->
   FieldStrings = record_fields_to_string(Fields, FieldNames, RecDict, []),
   "#" ++ atom_to_list(Tag) ++ "{" ++ sequence(FieldStrings, [], ",") ++ "}".
 
-record_fields_to_string([Field|Left1], [{FieldName, DeclaredType}|Left2], 
-			RecDict, Acc) ->
-  PrintType =
-    case t_is_equal(Field, DeclaredType) of
-      true -> false;
+record_fields_to_string([F|Fs], [{FName, _DefType}|FDefs], RecDict, Acc) ->
+  NewAcc =
+    case t_is_any(F) orelse t_is_atom('undefined', F) of
+      true -> Acc;
       false ->
-	case t_is_any(DeclaredType) andalso t_is_atom(undefined, Field) of
-	  true -> false;
-	  false ->
-	    TmpType = t_subtract(DeclaredType, t_atom(undefined)),
-	    not t_is_equal(Field, TmpType)
-	end
+	StrFV = atom_to_list(FName) ++ "::" ++ t_to_string(F, RecDict),
+	%% ActualDefType = t_subtract(DefType, t_atom('undefined')),
+	%% Str = case t_is_any(ActualDefType) of
+	%% 	  true -> StrFV;
+	%% 	  false -> StrFV ++ "::" ++ t_to_string(ActualDefType, RecDict)
+	%%	end,
+	[StrFV|Acc]
     end,
-  case PrintType of
-    false -> record_fields_to_string(Left1, Left2, RecDict, Acc);
-    true ->
-      String = atom_to_list(FieldName) ++ "::" ++ t_to_string(Field, RecDict),
-      record_fields_to_string(Left1, Left2, RecDict, [String|Acc])
-  end;
+  record_fields_to_string(Fs, FDefs, RecDict, NewAcc);
 record_fields_to_string([], [], _RecDict, Acc) ->
   lists:reverse(Acc).
 
+-spec record_field_diffs_to_string(erl_type(), dict()) -> string().
+
+record_field_diffs_to_string(?tuple([_|Fs], Arity, Tag), RecDict) ->
+  [TagAtom] = t_atom_vals(Tag),
+  {ok, FieldNames} = lookup_record(TagAtom, Arity-1, RecDict),
+  %% io:format("RecCElems = ~p\nRecTypes = ~p\n", [Fs, FieldNames]),
+  FieldDiffs = field_diffs(Fs, FieldNames, RecDict, []),
+  sequence(FieldDiffs, [], " and ").
+
+field_diffs([F|Fs], [{FName, DefType}|FDefs], RecDict, Acc) ->
+  NewAcc =
+    case t_is_subtype(F, DefType) of
+      true -> Acc;
+      false ->
+	Str = atom_to_list(FName) ++ "::" ++ t_to_string(DefType, RecDict),
+	[Str|Acc]
+    end,
+  field_diffs(Fs, FDefs, RecDict, NewAcc);
+field_diffs([], [], _, Acc) ->
+  lists:reverse(Acc).
+
 comma_sequence(Types, RecDict) ->
   List = [case T =:= ?any of
 	    true -> "_";
@@ -3400,6 +3416,18 @@ t_from_form({atom, _L, Atom}, _TypeNames, _RecDict, _VarDict) ->
   {t_atom(Atom), []};
 t_from_form({integer, _L, Int}, _TypeNames, _RecDict, _VarDict) ->
   {t_integer(Int), []};
+t_from_form({op, _L, _Op, _Arg} = Op, _TypeNames, _RecDict, _VarDict) ->
+  case erl_eval:partial_eval(Op) of
+    {integer, _, Val} ->
+      {t_integer(Val), []};
+    _ -> throw({error, io_lib:format("Unable evaluate type ~w\n", [Op])})
+  end;
+t_from_form({op, _L, _Op, _Arg1, _Arg2} = Op, _TypeNames, _RecDict, _VarDict) ->
+  case erl_eval:partial_eval(Op) of
+    {integer, _, Val} ->
+      {t_integer(Val), []};
+    _ -> throw({error, io_lib:format("Unable evaluate type ~w\n", [Op])})
+  end;
 t_from_form({type, _L, any, []}, _TypeNames, _RecDict, _VarDict) ->
   {t_any(), []};
 t_from_form({type, _L, arity, []}, _TypeNames, _RecDict, _VarDict) ->
@@ -3410,9 +3438,15 @@ t_from_form({type, _L, atom, []}, _TypeNames, _RecDict, _VarDict) ->
   {t_atom(), []};
 t_from_form({type, _L, binary, []}, _TypeNames, _RecDict, _VarDict) ->
   {t_binary(), []};
-t_from_form({type, _L, binary, [{integer, _, Base}, {integer, _, Unit}]}, 
+t_from_form({type, _L, binary, [Base, Unit]} = Type,
 	    _TypeNames, _RecDict, _VarDict) ->
-  {t_bitstr(Unit, Base), []};
+  case {erl_eval:partial_eval(Base), erl_eval:partial_eval(Unit)} of
+    {{integer, _, BaseVal},
+     {integer, _, UnitVal}}
+      when BaseVal >= 0, UnitVal >= 0 ->
+      {t_bitstr(UnitVal, BaseVal), []};
+    _ -> throw({error, io_lib:format("Unable evaluate type ~w\n", [Type])})
+  end;
 t_from_form({type, _L, bitstring, []}, _TypeNames, _RecDict, _VarDict) ->
   {t_bitstr(), []};
 t_from_form({type, _L, bool, []}, _TypeNames, _RecDict, _VarDict) ->
@@ -3516,9 +3550,14 @@ t_from_form({type, _L, product, Elements}, TypeNames, RecDict, VarDict) ->
   {t_product(L), R};
 t_from_form({type, _L, queue, []}, _TypeNames, _RecDict, _VarDict) ->
   {t_queue(), []};
-t_from_form({type, _L, range, [{integer, _, From}, {integer, _, To}]}, 
+t_from_form({type, _L, range, [From, To]} = Type,
 	    _TypeNames, _RecDict, _VarDict) ->
-  {t_from_range(From, To), []};
+  case {erl_eval:partial_eval(From), erl_eval:partial_eval(To)} of
+    {{integer, _, FromVal},
+     {integer, _, ToVal}} ->
+      {t_from_range(FromVal, ToVal), []};
+    _ -> throw({error, io_lib:format("Unable evaluate type ~w\n", [Type])})
+  end;
 t_from_form({type, _L, record, [Name|Fields]}, TypeNames, RecDict, VarDict) ->
   record_from_form(Name, Fields, TypeNames, RecDict, VarDict);
 t_from_form({type, _L, reference, []}, _TypeNames, _RecDict, _VarDict) ->
@@ -3693,6 +3732,16 @@ t_form_to_string({var, _L, Name}) -> atom_to_list(Name);
 t_form_to_string({atom, _L, Atom}) -> 
   io_lib:write_string(atom_to_list(Atom), $'); % To quote or not to quote... '
 t_form_to_string({integer, _L, Int}) -> integer_to_list(Int);
+t_form_to_string({op, _L, _Op, _Arg} = Op) ->
+  case erl_eval:partial_eval(Op) of
+    {integer, _, _} = Int -> t_form_to_string(Int);
+    _ -> io_lib:format("Bad formed type ~w",[Op])
+  end;
+t_form_to_string({op, _L, _Op, _Arg1, _Arg2} = Op) ->
+  case erl_eval:partial_eval(Op) of
+    {integer, _, _} = Int -> t_form_to_string(Int);
+    _ -> io_lib:format("Bad formed type ~w",[Op])
+  end;
 t_form_to_string({ann_type, _L, [Var, Type]}) ->
   t_form_to_string(Var) ++ "::" ++ t_form_to_string(Type);
 t_form_to_string({paren_type, _L, [Type]}) ->
@@ -3719,8 +3768,12 @@ t_form_to_string({type, _L, nonempty_list, [Type]}) ->
 t_form_to_string({type, _L, nonempty_string, []}) -> "nonempty_string()";
 t_form_to_string({type, _L, product, Elements}) ->
   "<" ++ sequence(t_form_to_string_list(Elements), ",") ++ ">";
-t_form_to_string({type, _L, range, [{integer, _, From}, {integer, _, To}]}) ->
-  io_lib:format("~w..~w", [From, To]);
+t_form_to_string({type, _L, range, [From, To]} = Type) ->
+  case {erl_eval:partial_eval(From), erl_eval:partial_eval(To)} of
+    {{integer, _, FromVal}, {integer, _, ToVal}} ->
+      io_lib:format("~w..~w", [FromVal, ToVal]);
+    _ -> io_lib:format("Bad formed type ~w",[Type])
+  end;
 t_form_to_string({type, _L, record, [{atom, _, Name}]}) ->
   io_lib:format("#~w{}", [Name]);
 t_form_to_string({type, _L, record, [{atom, _, Name}|Fields]}) ->
@@ -3739,13 +3792,17 @@ t_form_to_string({type, _L, Name, []} = T) ->
   try t_to_string(t_from_form(T))
   catch throw:{error, _} -> atom_to_list(Name) ++ "()"
   end;
-t_form_to_string({type, _L, binary, [{integer, _, X}, {integer, _, Y}]}) ->
-  case Y of
-    0 ->
-      case X of
-	0 -> "<<>>";
-	_ -> io_lib:format("<<_:~w>>", [X])
-      end
+t_form_to_string({type, _L, binary, [X,Y]} = Type) ->
+  case {erl_eval:partial_eval(X), erl_eval:partial_eval(Y)} of
+    {{integer, _, XVal}, {integer, _, YVal}} ->
+      case YVal of
+	0 ->
+	  case XVal of
+	    0 -> "<<>>";
+	    _ -> io_lib:format("<<_:~w>>", [XVal])
+	  end
+      end;
+    _ -> io_lib:format("Bad formed type ~w",[Type])
   end;
 t_form_to_string({type, _L, Name, List}) -> 
   io_lib:format("~w(~s)", [Name, sequence(t_form_to_string_list(List), ",")]).