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

Incorrect Unused name warning with recent SAW #1376

Open
RyanGlScott opened this issue Jul 13, 2021 · 2 comments
Open

Incorrect Unused name warning with recent SAW #1376

RyanGlScott opened this issue Jul 13, 2021 · 2 comments
Labels
topics: error-messages Issues involving the messages SAW produces on error type: bug Issues reporting bugs or unexpected/unwanted behavior
Milestone

Comments

@RyanGlScott
Copy link
Contributor

Using a nightly build of SAW from here (at commit 235d05e), if I run the following program:

let
{{
type foo = 123
}};

prove_print z3 {{ `foo == `foo }};

I get the following warning:

$ ~/Software/saw-0.8.0.99-Linux-x86_64/bin/saw Bug.saw


[13:13:53.443] Loading file "/home/rscott/Documents/Hacking/SAW/Bug.saw"
[warning] at /home/rscott/Documents/Hacking/SAW/Bug.saw:3:6--3:9
    Unused name: <interactive>::foo

This is incorrect, since foo is used in the prove_print line. (The formatting of <interactive>::foo is also a bit strange, but that would be moot if the warning never triggered in the first place.)

This is a regression from SAW 0.8, which does not produce the same warning:

$ ~/Software/saw-0.8/bin/saw Bug.saw


[13:13:56.182] Loading file "/home/rscott/Documents/Hacking/SAW/Bug.saw"
@RyanGlScott RyanGlScott added type: bug Issues reporting bugs or unexpected/unwanted behavior topics: error-messages Issues involving the messages SAW produces on error labels Jul 13, 2021
@RyanGlScott
Copy link
Contributor Author

This was introduced in #1191.

@robdockins
Copy link
Contributor

Probably this is due to some changes in the Cryptol renamer.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
topics: error-messages Issues involving the messages SAW produces on error type: bug Issues reporting bugs or unexpected/unwanted behavior
Projects
None yet
Development

No branches or pull requests

3 participants