search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
442 stars 63 forks source link

Incorrect `Unused name` warning with recent SAW #1376

Open RyanGlScott opened 3 years ago

RyanGlScott commented 3 years ago

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 commented 3 years ago

This was introduced in #1191.

robdockins commented 3 years ago

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