From a708b053390bcd88472a07b50d438fd1ec47338a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= <theophile@wallez.net>
Date: Tue, 30 May 2023 17:34:34 +0200
Subject: [PATCH] Allow '@' on fatal errors in --warn_error

---
 ocaml/fstar-lib/generated/FStar_Errors.ml | 38 +++++++++++++++++------
 src/basic/FStar.Errors.fst                |  6 +++-
 2 files changed, 33 insertions(+), 11 deletions(-)

diff --git a/ocaml/fstar-lib/generated/FStar_Errors.ml b/ocaml/fstar-lib/generated/FStar_Errors.ml
index 0826e2f5a7e..a6ad16c4f63 100644
--- a/ocaml/fstar-lib/generated/FStar_Errors.ml
+++ b/ocaml/fstar-lib/generated/FStar_Errors.ml
@@ -81,14 +81,32 @@ let (update_flags :
               FStar_Compiler_Util.format1 "cannot silence error %s" uu___2 in
             Invalid_warn_error_setting uu___1 in
           FStar_Compiler_Effect.raise uu___
-      | (uu___, FStar_Errors_Codes.CFatal) ->
-          let uu___1 =
-            let uu___2 =
-              let uu___3 = FStar_Compiler_Util.string_of_int i in
+      | (FStar_Errors_Codes.CSilent, FStar_Errors_Codes.CFatal) ->
+          let uu___ =
+            let uu___1 =
+              let uu___2 = FStar_Compiler_Util.string_of_int i in
               FStar_Compiler_Util.format1
-                "cannot change the error level of fatal error %s" uu___3 in
-            Invalid_warn_error_setting uu___2 in
-          FStar_Compiler_Effect.raise uu___1
+                "cannot change the error level of fatal error %s" uu___2 in
+            Invalid_warn_error_setting uu___1 in
+          FStar_Compiler_Effect.raise uu___
+      | (FStar_Errors_Codes.CWarning, FStar_Errors_Codes.CFatal) ->
+          let uu___ =
+            let uu___1 =
+              let uu___2 = FStar_Compiler_Util.string_of_int i in
+              FStar_Compiler_Util.format1
+                "cannot change the error level of fatal error %s" uu___2 in
+            Invalid_warn_error_setting uu___1 in
+          FStar_Compiler_Effect.raise uu___
+      | (FStar_Errors_Codes.CError, FStar_Errors_Codes.CFatal) ->
+          let uu___ =
+            let uu___1 =
+              let uu___2 = FStar_Compiler_Util.string_of_int i in
+              FStar_Compiler_Util.format1
+                "cannot change the error level of fatal error %s" uu___2 in
+            Invalid_warn_error_setting uu___1 in
+          FStar_Compiler_Effect.raise uu___
+      | (FStar_Errors_Codes.CAlwaysError, FStar_Errors_Codes.CFatal) ->
+          FStar_Errors_Codes.CFatal
       | uu___ -> flag in
     let set_flag_for_range uu___ =
       match uu___ with
@@ -529,7 +547,7 @@ let (set_option_warning_callback_range :
   FStar_Compiler_Range_Type.range FStar_Pervasives_Native.option -> unit) =
   fun ropt ->
     FStar_Options.set_option_warning_callback (warn_unsafe_options ropt)
-let (uu___290 :
+let (uu___299 :
   (((Prims.string -> FStar_Errors_Codes.error_setting Prims.list) -> unit) *
     (unit -> FStar_Errors_Codes.error_setting Prims.list)))
   =
@@ -575,10 +593,10 @@ let (uu___290 :
   (set_callbacks, get_error_flags)
 let (t_set_parse_warn_error :
   (Prims.string -> FStar_Errors_Codes.error_setting Prims.list) -> unit) =
-  match uu___290 with
+  match uu___299 with
   | (t_set_parse_warn_error1, error_flags) -> t_set_parse_warn_error1
 let (error_flags : unit -> FStar_Errors_Codes.error_setting Prims.list) =
-  match uu___290 with
+  match uu___299 with
   | (t_set_parse_warn_error1, error_flags1) -> error_flags1
 let (set_parse_warn_error :
   (Prims.string -> FStar_Errors_Codes.error_setting Prims.list) -> unit) =
diff --git a/src/basic/FStar.Errors.fst b/src/basic/FStar.Errors.fst
index 060418fa332..726dfa11138 100644
--- a/src/basic/FStar.Errors.fst
+++ b/src/basic/FStar.Errors.fst
@@ -72,10 +72,14 @@ let update_flags (l:list (error_flag * string))
         raise (Invalid_warn_error_setting
                  (BU.format1 "cannot silence error %s"
                              (BU.string_of_int i)))
-      | (_, CFatal) ->
+      | (CSilent, CFatal)
+      | (CWarning, CFatal)
+      | (CError, CFatal) ->
         raise (Invalid_warn_error_setting
                  (BU.format1 "cannot change the error level of fatal error %s"
                              (BU.string_of_int i)))
+      | (CAlwaysError, CFatal) ->
+        CFatal
       | _ -> flag
    in
    let set_flag_for_range (flag, range) =