Elsa thinks a condition is always nil when it isn't

[DarwinAwardWinner]

I have a condition in my code here: https://github.com/DarwinAwardWinner/ido-completing-read-plus/blob/master/ido-completing-read%2B.el#L558-L564

Elsa says that this conditional always evaluates to nil, which would imply that the body of the when never runs. However, I know the body does run, because it has code coverage: https://coveralls.io/builds/25154837/source?filename=ido-completing-read%2B.el#L553 (I don't know why the line numbers are different, but it's the same code.) I'm not exactly certain how to reduce this to a test case, but you can check out the elsa branch of ido-completing-read-plus and reproduce it yourself. (After cloning, just do cask install, then case exec elsa ido-completing-read+.el.)

[DarwinAwardWinner]

Ok, I actually figured out that this is because the variable whitelisted is initially set to nil in a let, and Elsa therefore decides that it can only ever be nil. That's kind of odd.

(let ((my-lex-var nil))
  ;; Elsa thinks `my-lex-var' can only be nil
  (setq my-lex-var t)
  ;; Elsa thinks this conditional is always false because it thinks
  ;; the var is always nil.
  (when my-lex-var
    (message "hello"))
  my-lex-var)

[Fuco1]

Yes it is and I was changing this yesterday. Const assignments in let will get promoted to the "type", nil will be infered to be mixed since we don't know. I pushed the code this morning

[Fuco1]

but your example above should've at least updated it to t after the assignment. That might be a bug.

[Fuco1]

@DarwinAwardWinner Can you check on the new version if this is still the issue?

[DarwinAwardWinner]

Testing on Elsa version 20191002.2030 from MELPA on ido-cr+ commit d7d26ba (current commit on branch elsa) I am still seeing this issue.

$ cask exec elsa ido-completing-read+.el 2>/dev/null | grep always
ido-completing-read+.el:570:18:warning:Condition always evaluates to nil.
ido-completing-read+.el:673:18:warning:Condition always evaluates to non-nil.
ido-completing-read+.el:680:16:warning:Condition always evaluates to nil.
ido-completing-read+.el:730:24:warning:Condition always evaluates to nil.
ido-completing-read+.el:752:6:warning:Condition always evaluates to non-nil.
ido-completing-read+.el:960:22:warning:Condition always evaluates to nil.
ido-completing-read+.el:980:24:warning:Condition always evaluates to nil.
ido-completing-read+.el:913:8:warning:Condition always evaluates to nil.
ido-completing-read+.el:995:8:warning:Condition always evaluates to nil.
ido-completing-read+.el:1004:10:warning:Condition always evaluates to nil.
ido-completing-read+.el:1001:8:warning:Condition always evaluates to nil.
ido-completing-read+.el:1029:8:warning:Condition always evaluates to nil.
ido-completing-read+.el:1180:14:warning:Condition always evaluates to nil.
ido-completing-read+.el:1199:16:warning:Condition always evaluates to non-nil.
ido-completing-read+.el:1194:6:warning:Condition always evaluates to non-nil.

From all of the above, only 980 is potentially correct (I'm not actually sure), but I'm pretty sure it's not possible to determine through static analysis whether or not that condition always evaluates to nil, so even if Elsa is right on that one, it's for the wrong reason. In all the rest, Elsa is definitely wrong.

The full output is:

analyzer: updating variable ido-completing-read+-version, old type nil
analyzer: updating variable memoize-default-timeout, old type nil
analyzer: updating variable flx-file-cache, old type nil
analyzer: updating variable flx-strings-cache, old type nil
analyzer: updating variable flx-ido-narrowed-matches-hash, old type nil
analyzer: updating variable flx-ido-debug, old type nil
analyzer: updating variable ido-cr+-minibuffer-depth, old type nil
analyzer: updating variable ido-cr+-assume-static-collection, old type nil
analyzer: updating variable ido-cr+-current-command, old type nil
analyzer: updating variable ido-cr+-dynamic-collection, old type nil
analyzer: updating variable ido-cr+-last-dynamic-update-text, old type nil
analyzer: updating variable ido-cr+-dynamic-update-idle-time, old type nil
analyzer: updating variable ido-cr+-dynamic-update-timer, old type nil
analyzer: updating variable ido-cr+-exhibit-pending, old type nil
analyzer: updating variable ido-cr+-orig-completing-read-args, old type nil
analyzer: updating variable ido-cr+-all-completions-memoized, old type nil
analyzer: updating variable ido-cr+-all-prefix-completions-memoized, old type nil
analyzer: updating variable ido-cr+-active-restrictions, old type nil
ido-completing-read+.el:101:19:error:Reference to free variable `ido-cr+-debug-mode'.
ido-completing-read+.el:111:8:error:Reference to free variable `ido-cr+-debug-mode'.
ido-completing-read+.el:112:13:error:Reference to free variable `message'.
ido-completing-read+.el:110:1:error:Function is expected to return String but returns Mixed.
ido-completing-read+.el:120:10:error:Reference to free variable `define-ido-internal-var'.
ido-completing-read+.el:120:42:error:Reference to free variable `&optional'.
ido-completing-read+.el:120:52:error:Reference to free variable `initvalue'.
ido-completing-read+.el:120:62:error:Reference to free variable `docstring'.
ido-completing-read+.el:143:25:error:Reference to free variable `ido-context-switch-command'.
ido-completing-read+.el:145:25:error:Reference to free variable `ido-cur-list'.
ido-completing-read+.el:149:25:error:Reference to free variable `ido-require-match'.
ido-completing-read+.el:151:25:error:Reference to free variable `ido-process-ignore-lists'.
ido-completing-read+.el:156:18:error:Reference to free variable `flx-ido-reset'.
ido-completing-read+.el:422:8:error:Reference to free variable `ido-cr+-debug-mode'.
ido-completing-read+.el:428:7:error:Argument 2 accepts type Mixed but received Unbound
ido-completing-read+.el:434:3:error:Argument 2 accepts type Number | Marker but received Mixed
ido-completing-read+.el:441:10:error:Reference to free variable `ido-cr+-function-is-in-list'.
ido-completing-read+.el:441:43:error:Reference to free variable `fun-list'.
ido-completing-read+.el:441:52:error:Reference to free variable `&optional'.
ido-completing-read+.el:441:62:error:Reference to free variable `list-name'.
ido-completing-read+.el:451:14:error:Reference to free variable `list-name'.
ido-completing-read+.el:451:9:error:Argument 1 accepts type Mixed but received Unbound
ido-completing-read+.el:452:17:error:Reference to free variable `fun-list'.
ido-completing-read+.el:452:9:error:Argument 1 accepts type Mixed but received Unbound
ido-completing-read+.el:453:37:error:Reference to free variable `fun-list'.
ido-completing-read+.el:453:25:error:Argument 1 accepts type Symbol? but received Unbound
ido-completing-read+.el:453:14:warning:Assigning to free variable list-name
ido-completing-read+.el:454:12:warning:Assigning to free variable list-name
ido-completing-read+.el:570:18:warning:Condition always evaluates to nil.
ido-completing-read+.el:596:25:error:Argument 1 accepts type Sequence? but received Mixed
ido-completing-read+.el:601:25:error:Argument 1 accepts type Sequence? but received Mixed
ido-completing-read+.el:613:13:error:Reference to free variable `for'.
ido-completing-read+.el:613:17:error:Reference to free variable `cmd'.
ido-completing-read+.el:613:21:error:Reference to free variable `in'.
ido-completing-read+.el:613:25:error:Argument 1 accepts type Mixed but received Unbound
ido-completing-read+.el:615:13:error:Reference to free variable `if'.
ido-completing-read+.el:615:49:error:Reference to free variable `cmd'.
ido-completing-read+.el:615:17:error:Argument 1 accepts type Mixed but received Unbound
ido-completing-read+.el:616:13:error:Reference to free variable `do'.
ido-completing-read+.el:617:68:error:Reference to free variable `cmd'.
ido-completing-read+.el:617:25:error:Argument 2 accepts type Mixed but received Unbound
ido-completing-read+.el:619:13:error:Reference to free variable `if'.
ido-completing-read+.el:620:54:error:Reference to free variable `cmd'.
ido-completing-read+.el:620:22:error:Argument 1 accepts type Mixed but received Unbound
ido-completing-read+.el:621:13:error:Reference to free variable `do'.
ido-completing-read+.el:622:72:error:Reference to free variable `cmd'.
ido-completing-read+.el:622:19:error:Argument 2 accepts type Mixed but received Unbound
ido-completing-read+.el:625:13:error:Reference to free variable `if'.
ido-completing-read+.el:628:18:error:Reference to free variable `cmd'.
ido-completing-read+.el:629:13:error:Reference to free variable `do'.
ido-completing-read+.el:631:71:error:Reference to free variable `cmd'.
ido-completing-read+.el:630:19:error:Argument 2 accepts type Mixed but received Unbound
ido-completing-read+.el:641:21:error:Reference to free variable `for'.
ido-completing-read+.el:641:25:error:Reference to free variable `i'.
ido-completing-read+.el:641:27:error:Reference to free variable `upfrom'.
ido-completing-read+.el:642:21:error:Reference to free variable `for'.
ido-completing-read+.el:642:25:error:Reference to free variable `caller'.
ido-completing-read+.el:642:32:error:Reference to free variable `='.
ido-completing-read+.el:642:57:error:Reference to free variable `i'.
ido-completing-read+.el:643:21:error:Reference to free variable `while'.
ido-completing-read+.el:643:27:error:Reference to free variable `caller'.
ido-completing-read+.el:644:21:error:Reference to free variable `while'.
ido-completing-read+.el:644:57:error:Reference to free variable `caller'.
ido-completing-read+.el:648:21:error:Reference to free variable `if'.
ido-completing-read+.el:648:57:error:Reference to free variable `caller'.
ido-completing-read+.el:648:25:error:Argument 1 accepts type Mixed but received Unbound
ido-completing-read+.el:649:21:error:Reference to free variable `do'.
ido-completing-read+.el:650:51:error:Reference to free variable `caller'.
ido-completing-read+.el:650:43:error:Argument 1 accepts type Mixed but received Unbound
ido-completing-read+.el:651:89:error:Reference to free variable `caller'.
ido-completing-read+.el:651:43:error:Argument 2 accepts type Mixed but received Unbound
ido-completing-read+.el:654:21:error:Reference to free variable `if'.
ido-completing-read+.el:655:62:error:Reference to free variable `caller'.
ido-completing-read+.el:655:30:error:Argument 1 accepts type Mixed but received Unbound
ido-completing-read+.el:656:21:error:Reference to free variable `do'.
ido-completing-read+.el:658:40:error:Reference to free variable `caller'.
ido-completing-read+.el:658:32:error:Argument 1 accepts type Mixed but received Unbound
ido-completing-read+.el:659:78:error:Reference to free variable `caller'.
ido-completing-read+.el:659:32:error:Argument 2 accepts type Mixed but received Unbound
ido-completing-read+.el:663:21:error:Reference to free variable `if'.
ido-completing-read+.el:665:30:error:Reference to free variable `caller'.
ido-completing-read+.el:666:21:error:Reference to free variable `do'.
ido-completing-read+.el:668:40:error:Reference to free variable `caller'.
ido-completing-read+.el:668:32:error:Argument 1 accepts type Mixed but received Unbound
ido-completing-read+.el:669:100:error:Reference to free variable `caller'.
ido-completing-read+.el:669:32:error:Argument 2 accepts type Mixed but received Unbound
ido-completing-read+.el:673:18:warning:Condition always evaluates to non-nil.
ido-completing-read+.el:680:16:warning:Condition always evaluates to nil.
ido-completing-read+.el:695:18:error:Variable def expects Mixed \ [Mixed], got [Mixed]
ido-completing-read+.el:698:49:error:Reference to free variable `format'.
ido-completing-read+.el:698:18:error:Variable def expects Mixed \ Nil, got Mixed
ido-completing-read+.el:700:43:error:Argument 1 accepts type Sequence but received Mixed
ido-completing-read+.el:700:43:error:Argument 2 accepts type Sequence but received Mixed
ido-completing-read+.el:704:21:error:Reference to free variable `ido-enable-dot-prefix'.
ido-completing-read+.el:716:13:error:Argument 1 accepts type Number but received Mixed
ido-completing-read+.el:720:47:error:Argument 1 accepts type Number | Marker but received Mixed
ido-completing-read+.el:732:26:error:Variable ido-cr+-dynamic-update-timer expects (), got Nil
ido-completing-read+.el:730:24:warning:Condition always evaluates to nil.
ido-completing-read+.el:735:22:error:Reference to free variable `ido-exit'.
ido-completing-read+.el:735:19:error:Argument 1 accepts type Mixed but received Unbound
ido-completing-read+.el:758:13:error:Reference to free variable `ido-completing-read+'.
ido-completing-read+.el:752:6:warning:Condition always evaluates to non-nil.
ido-completing-read+.el:761:14:error:Reference to free variable `ido-completing-read@ido-cr+-replace'.
ido-completing-read+.el:773:14:error:Reference to free variable `call-interactively@ido-cr+-record-current-command'.
ido-completing-read+.el:781:39:error:Reference to free variable `ido-fallback-command'.
ido-completing-read+.el:781:10:warning:Assigning to free variable ido-context-switch-command
ido-completing-read+.el:783:14:error:Reference to free variable `ido-magic-forward-char@ido-cr+-fallback'.
ido-completing-read+.el:790:39:error:Reference to free variable `ido-fallback-command'.
ido-completing-read+.el:790:10:warning:Assigning to free variable ido-context-switch-command
ido-completing-read+.el:792:14:error:Reference to free variable `ido-magic-backward-char@ido-cr+-fallback'.
ido-completing-read+.el:810:7:error:Reference to free variable `ido-require-match'.
ido-completing-read+.el:813:20:error:Reference to free variable `ido-text'.
ido-completing-read+.el:813:29:error:Reference to free variable `ido-cur-list'.
ido-completing-read+.el:817:28:error:Reference to free variable `ido-text'.
ido-completing-read+.el:817:11:warning:Unreachable expression
ido-completing-read+.el:825:14:error:Reference to free variable `ido-select-text@ido-cr+-fix-require-match'.
ido-completing-read+.el:827:1:notice:Public functions should have a docstring.
ido-completing-read+.el:832:8:error:Variable ido-cr+-exhibit-pending expects T, got Nil
ido-completing-read+.el:831:1:notice:Public functions should have a docstring.
ido-completing-read+.el:855:5:error:Reference to free variable `for'.
ido-completing-read+.el:855:9:error:Reference to free variable `i'.
ido-completing-read+.el:855:11:error:Reference to free variable `from'.
ido-completing-read+.el:855:18:error:Reference to free variable `upto'.
ido-completing-read+.el:855:24:error:Argument 1 accepts type Sequence? but received Mixed
ido-completing-read+.el:856:5:error:Reference to free variable `append'.
ido-completing-read+.el:858:33:error:Reference to free variable `i'.
ido-completing-read+.el:858:14:error:Argument 1 accepts type String but received Mixed
ido-completing-read+.el:858:14:error:Argument 3 accepts type Int? but received Unbound
ido-completing-read+.el:861:5:error:Reference to free variable `into'.
ido-completing-read+.el:861:10:error:Reference to free variable `completion-list'.
ido-completing-read+.el:862:5:error:Reference to free variable `finally'.
ido-completing-read+.el:862:13:error:Reference to free variable `return'.
ido-completing-read+.el:862:33:error:Reference to free variable `completion-list'.
ido-completing-read+.el:883:3:error:Reference to free variable `with'.
ido-completing-read+.el:883:8:error:Reference to free variable `filtered-collection'.
ido-completing-read+.el:883:28:error:Reference to free variable `='.
ido-completing-read+.el:884:3:error:Reference to free variable `with'.
ido-completing-read+.el:884:8:error:Reference to free variable `need-reverse'.
ido-completing-read+.el:884:21:error:Reference to free variable `='.
ido-completing-read+.el:885:3:error:Reference to free variable `for'.
ido-completing-read+.el:885:24:error:Reference to free variable `in'.
ido-completing-read+.el:886:3:error:Reference to free variable `for'.
ido-completing-read+.el:886:7:error:Reference to free variable `restriction-matches'.
ido-completing-read+.el:886:27:error:Reference to free variable `='.
ido-completing-read+.el:887:19:error:Reference to free variable `text'.
ido-completing-read+.el:889:24:error:Reference to free variable `filtered-collection'.
ido-completing-read+.el:890:3:error:Reference to free variable `do'.
ido-completing-read+.el:891:16:error:Reference to free variable `removep'.
ido-completing-read+.el:892:32:error:Reference to free variable `filtered-collection'.
ido-completing-read+.el:892:52:error:Reference to free variable `restriction-matches'.
ido-completing-read+.el:893:38:error:Reference to free variable `need-reverse'.
ido-completing-read+.el:893:34:error:Argument 1 accepts type Mixed but received Unbound
ido-completing-read+.el:893:20:warning:Assigning to free variable need-reverse
ido-completing-read+.el:894:14:error:Reference to free variable `restriction-matches'.
ido-completing-read+.el:890:12:warning:Assigning to free variable filtered-collection
ido-completing-read+.el:895:3:error:Reference to free variable `finally'.
ido-completing-read+.el:897:11:error:Reference to free variable `return'.
ido-completing-read+.el:905:3:error:Reference to free variable `for'.
ido-completing-read+.el:905:7:error:Reference to free variable `tortoise'.
ido-completing-read+.el:905:16:error:Reference to free variable `on'.
ido-completing-read+.el:906:3:error:Reference to free variable `for'.
ido-completing-read+.el:906:7:error:Reference to free variable `hare'.
ido-completing-read+.el:906:12:error:Reference to free variable `on'.
ido-completing-read+.el:906:16:error:Argument 1 accepts type (Cons Mixed Mixed)? but received Mixed
ido-completing-read+.el:906:23:error:Reference to free variable `by'.
ido-completing-read+.el:906:28:error:Reference to free variable `cddr'.
ido-completing-read+.el:907:3:error:Reference to free variable `thereis'.
ido-completing-read+.el:907:15:error:Reference to free variable `tortoise'.
ido-completing-read+.el:907:24:error:Reference to free variable `hare'.
ido-completing-read+.el:907:12:error:Argument 1 accepts type Mixed but received Unbound
ido-completing-read+.el:907:12:error:Argument 2 accepts type Mixed but received Unbound
ido-completing-read+.el:916:29:error:Reference to free variable `ido-cur-list'.
ido-completing-read+.el:919:43:error:Reference to free variable `ido-eoinput'.
ido-completing-read+.el:918:12:error:Argument 1 accepts type Int but received Mixed
ido-completing-read+.el:918:12:error:Argument 2 accepts type Int but received Unbound
ido-completing-read+.el:927:37:error:Reference to free variable `err'.
ido-completing-read+.el:929:37:error:Reference to free variable `ido-matches'.
ido-completing-read+.el:929:33:error:Argument 1 accepts type (Cons Mixed Mixed)? but received Unbound
ido-completing-read+.el:945:21:error:Reference to free variable `for'.
ido-completing-read+.el:945:25:error:Reference to free variable `string'.
ido-completing-read+.el:945:32:error:Reference to free variable `in'.
ido-completing-read+.el:946:21:error:Reference to free variable `append'.
ido-completing-read+.el:949:22:error:Reference to free variable `string'.
ido-completing-read+.el:950:21:error:Reference to free variable `into'.
ido-completing-read+.el:950:26:error:Reference to free variable `result'.
ido-completing-read+.el:951:21:error:Reference to free variable `finally'.
ido-completing-read+.el:951:29:error:Reference to free variable `return'.
ido-completing-read+.el:951:36:error:Reference to free variable `result'.
ido-completing-read+.el:953:41:error:Reference to free variable `ido-cur-list'.
ido-completing-read+.el:956:40:error:Reference to free variable `flx-ido-reset'.
ido-completing-read+.el:958:29:error:Reference to free variable `flx-ido-reset'.
ido-completing-read+.el:959:56:error:Reference to free variable `ido-cur-list'.
ido-completing-read+.el:959:49:error:Argument 1 accepts type Sequence but received Unbound
ido-completing-read+.el:959:49:error:Argument 2 accepts type Sequence but received Mixed
ido-completing-read+.el:959:22:warning:Assigning to free variable ido-cur-list
ido-completing-read+.el:960:22:warning:Condition always evaluates to nil.
ido-completing-read+.el:966:27:error:Argument 1 accepts type Sequence? but received Mixed
ido-completing-read+.el:970:22:warning:Assigning to free variable ido-rescan
ido-completing-read+.el:974:56:error:Reference to free variable `ido-matches'.
ido-completing-read+.el:974:52:error:Argument 1 accepts type (Cons Mixed Mixed)? but received Unbound
ido-completing-read+.el:975:47:error:Reference to free variable `ido-matches'.
ido-completing-read+.el:977:46:error:Reference to free variable `ido-matches'.
ido-completing-read+.el:977:24:warning:Assigning to free variable ido-matches
ido-completing-read+.el:980:24:warning:Condition always evaluates to nil.
ido-completing-read+.el:988:29:error:Reference to free variable `err'.
ido-completing-read+.el:986:29:error:Argument 2 accepts type Mixed but received Unbound
ido-completing-read+.el:991:17:error:Variable ido-cur-list expects Mixed, got Unbound
ido-completing-read+.el:993:17:error:Variable ido-cr+-dynamic-collection expects (), got Nil
ido-completing-read+.el:913:8:warning:Condition always evaluates to nil.
ido-completing-read+.el:997:10:error:Variable ido-cr+-dynamic-update-timer expects (), got Nil
ido-completing-read+.el:995:8:warning:Condition always evaluates to nil.
ido-completing-read+.el:1006:12:error:Variable ido-cr+-dynamic-update-timer expects (), got Nil
ido-completing-read+.el:1004:10:warning:Condition always evaluates to nil.
ido-completing-read+.el:1008:20:error:Reference to free variable `ido-matches'.
ido-completing-read+.el:1008:13:error:Argument 1 accepts type Sequence? but received Unbound
ido-completing-read+.el:1015:35:error:Reference to free variable `ido-cr+-update-dynamic-collection'.
ido-completing-read+.el:1001:8:warning:Condition always evaluates to nil.
ido-completing-read+.el:1035:10:warning:Assigning to free variable ido-eoinput
ido-completing-read+.el:1029:8:warning:Condition always evaluates to nil.
ido-completing-read+.el:1052:40:error:Reference to free variable `ido-text'.
ido-completing-read+.el:1052:27:error:Argument 2 accepts type Mixed but received Unbound
ido-completing-read+.el:1053:58:error:Reference to free variable `ido-text'.
ido-completing-read+.el:1053:45:error:Argument 2 accepts type Mixed but received Unbound
ido-completing-read+.el:1064:33:error:Argument 1 accepts type (Cons Mixed Mixed)? but received Mixed
ido-completing-read+.el:1065:32:error:Reference to free variable `ido-text'.
ido-completing-read+.el:1067:14:error:Variable minibuf-eldef-showing-default-in-prompt expects Bool, got Bool
ido-completing-read+.el:1069:21:error:Reference to free variable `minibuf-eldef-overlay'.
ido-completing-read+.el:1073:14:error:Reference to free variable `minibuf-eldef-update-minibuffer@ido-cr+-compat'.
ido-completing-read+.el:1076:19:error:Reference to free variable `ido-ubiquitous-mode'.
ido-completing-read+.el:1088:12:error:Reference to free variable `ido-ubiquitous-mode'.
ido-completing-read+.el:1089:14:error:Reference to free variable `ido-completing-read+'.
ido-completing-read+.el:1087:8:warning:Assigning to free variable completing-read-function
ido-completing-read+.el:1152:24:error:Argument 1 accepts type (Cons Mixed Mixed)? but received Mixed
ido-completing-read+.el:1153:31:error:Argument 1 accepts type Sequence but received Mixed
ido-completing-read+.el:1154:63:error:Reference to free variable `equal'.
ido-completing-read+.el:1162:13:error:Variable ido-cr+-function-blacklist expects [Mixed], got Mixed
ido-completing-read+.el:1180:14:warning:Condition always evaluates to nil.
ido-completing-read+.el:1187:28:error:Reference to free variable `identity'.
ido-completing-read+.el:1187:16:error:Argument 1 accepts type Mixed -> String but received Mixed
ido-completing-read+.el:1187:16:error:Argument 2 accepts type [Mixed] but received Mixed
ido-completing-read+.el:1196:28:error:Argument 1 accepts type (Cons Mixed Mixed)? but received Mixed
ido-completing-read+.el:1197:67:error:Reference to free variable `equal'.
ido-completing-read+.el:1200:224:error:Argument 1 accepts type Sequence? but received Mixed \ Nil
ido-completing-read+.el:1199:16:warning:Condition always evaluates to non-nil.
ido-completing-read+.el:1194:6:warning:Condition always evaluates to non-nil.