Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

The static analyzer either reports too many or too few errors #177

Open
bugarela opened this issue Aug 30, 2022 · 1 comment
Open

The static analyzer either reports too many or too few errors #177

bugarela opened this issue Aug 30, 2022 · 1 comment
Assignees
Labels
effect system Quint effects checker effort-hard Takes >= 5 days (probably requires issue refactor) impact-high High impact typechecker Type checker for Quint

Comments

@bugarela
Copy link
Collaborator

Imagine this scenario

def a = 1 + true // error 1
def b = 2 + false // error 2
def c = a // error 3

Error 3 is consequence of error 1, so we should not report the two of them. But errors 1 and 2 are completely independent, so we should report both.

This is the scenario I'm stumbling upon in error reporting, but there might be other ways of chaining errors where we want to report only the root cause.

In the current implementation, is easy to do:

  1. report only error 1
  2. report all 3 errors

But the ideal is to report only error 1 and 2.

@bugarela bugarela added typechecker Type checker for Quint effect system Quint effects checker labels Aug 30, 2022
@bugarela bugarela self-assigned this Aug 30, 2022
@bugarela bugarela added this to the T1.3.2 Type System milestone Aug 30, 2022
@bugarela bugarela changed the title tntc either reports too many or too little errors tntc either reports too many or too few errors Aug 30, 2022
@konnov
Copy link
Contributor

konnov commented Sep 1, 2022

I guess, the idea here is that a gets assigned some special type that indicates a type error, right? If you do that, then you don't have to report c, as it is tainted by this special type.

@bugarela bugarela added impact-high High impact effort-hard Takes >= 5 days (probably requires issue refactor) labels Nov 30, 2022
@bugarela bugarela changed the title tntc either reports too many or too few errors quint either reports too many or too few errors Jan 27, 2023
@bugarela bugarela changed the title quint either reports too many or too few errors The static analyzer either reports too many or too few errors Jan 27, 2023
@shonfeder shonfeder removed this from the T1.3.2 Type System milestone Jan 9, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
effect system Quint effects checker effort-hard Takes >= 5 days (probably requires issue refactor) impact-high High impact typechecker Type checker for Quint
Projects
None yet
Development

No branches or pull requests

3 participants