scilla icon indicating copy to clipboard operation
scilla copied to clipboard

SanityChecker: Check that map value is unboxed before use

Open jubnzv opened this issue 2 years ago • 0 comments

Closes #1097

This is unfinished work, because I need to switch to another task at the moment. It is not ready for merging, but we could use it to find some issues in the production code.

Here's a list of things that must be done before merging it:

  • [ ] #1144 must be reviewed and merged first. Then we need rebase this PR to the master branch.
  • [ ] We should handle re-definitions of the map values, for example:
v <- m[k];
v1 = v; (* check if v1 is actually matched*)
  • [ ] Check the behavior on type functions and applications. I haven't look at this at the moment.
  • [ ] If the optional value is called in the standard function (one of rlibs), we should consider it as matched. Otherwise, the analysis of the whole standard library could be slow.
  • [ ] We should check how the value from the map is used. If it is assigned to the field with an optional type, we should not emit warnings. At the moment CI will fail because of this.

jubnzv avatar Aug 17 '22 10:08 jubnzv