Allow '@' on fatal errors in --warn_error

[TWal]

Currently, F* has the following behavior:

$ fstar.exe Test.fst --warn_error '@20'
Invalid --warn_error setting: cannot change the error level of fatal error 20

It makes it difficult to have a -Werror-like flag, which we could hope simulate via something like --warn_error '@0..1000', only to stumble on the same error message as above.

This PR allows using @ in --warn_error for fatal errors, hence allowing to easily simulate a -Werror-like flag.

For example with this file, which has two warnings (bad SMT pattern, top-level binding with effects):

module Test

let l (n:int) (m:int) : Lemma (n+m == m+n) [SMTPat (n)] = ()
let rec f (): Dv False = f ()
let g: False = f ()

We can choose to only allow the bad SMT pattern warning, but disallow any other warning (such as top-level binding with effects)

$ fstar.exe Test.fst --warn_error '[email protected]'
Test.fst(3,52-3,53): (Warning 271) SMT pattern misses at least one bound variable: m#215 (see also Test.fst(3,7-3,8))
Test.fst(3,52-3,53): (Warning 271) SMT pattern misses at least one bound variable: m#308 (see also Test.fst(3,7-3,8))
Test.fst(5,0-5,19): (Error 272) Top-level let-bindings must be total; this term may have effects
Verified module: Test
2 errors were reported (see above)

[mtzguido]

Hi Théophile, thanks! This looks good to me.

One minor comment, independent of this PR, is that I'm surprised with the order of --warn_error [email protected], I expected the @0..1000 on the right to override the +271, but I see the logic is backwards. It seems easy enough to change.. any thoughts?

[TWal]

Thanks! I don't have a strong opinion on this, but I agree I also expected it to be the other way when I tried it.