GaloisInc / saw-script

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

Lack of checking of typedefs #2077

Open sauclovian-g opened 4 months ago

sauclovian-g commented 4 months ago

saw lets me write this: typedef x = { foo: Int, bar: x }; and it seems like it probably shouldn't.

Also, you can introduce fresh universally-quantified type variables just by mentioning them: typedef x = a;, and that doesn't seem entirely desirable either.

I haven't been able to get it to do anything unsound with either of these even after prodding it for a while, but it's definitely possible I just haven't tried hard enough.