Fix handling of enable pragmas

Check instructions generated by goto_check received a "disable"
pragma to prevent them being instrumented by later passes of
goto-instrument or cbmc.

When the source instruction carried an "enable" pragma, the check
instruction would receive both "enable" and "disable" pragmas
which is considered erroneous.

For the generated check instructions, we replace the "disable" pragmas
with "checked" pragmas which is compatible with the "enable" pragma of
their source, while still inhibiting the generation of secondary check
instructions from theses check instructions.

Author: Remi Delmas

regression/goto-instrument/enable-pragmas/main.c

@@ -0,0 +1,10 @@
+void main()
+{
+  int a[2];
+#pragma CPROVER check push
+#pragma CPROVER check enable "bounds"
+  a[0] = 1;
+  a[1] = 2;
+  a[2] = 3;
+#pragma CPROVER check pop
+}

regression/goto-instrument/enable-pragmas/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^\[main.array_bounds.\d+\] line \d+ array 'a' upper bound in a\[\(signed .* int\)2\]: FAILURE
+^VERIFICATION FAILED
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Checks that enable pragmas do not cause invariant failures when running goto-instrument
+and cbmc in sequence.

src/ansi-c/goto_check_c.cpp

@@ -308,10 +308,10 @@ class goto_check_ct
   /// on the given source location.
   void add_active_named_check_pragmas(source_locationt &source_location) const;
 
-  /// \brief Adds "disable" pragmas for all named checks
-  /// on the given source location.
+  /// \brief Adds "checked" pragmas for all named checks on the given source
+  /// location (prevents any the instanciation of any ulterior check).
   void
-  add_all_disable_named_check_pragmas(source_locationt &source_location) const;
+  add_all_checked_named_check_pragmas(source_locationt &source_location) const;
 
   /// activation statuses for named checks
   typedef enum
@@ -1726,7 +1726,7 @@ void goto_check_ct::add_guarded_property(
     annotated_location.set_comment(comment + " in " + source_expr_string);
     annotated_location.set_property_class(property_class);
 
-    add_all_disable_named_check_pragmas(annotated_location);
+    add_all_checked_named_check_pragmas(annotated_location);
 
     if(enable_assert_to_assume)
     {
@@ -2477,11 +2477,11 @@ void goto_check_ct::add_active_named_check_pragmas(
       source_location.add_pragma("checked:" + id2string(entry.first));
 }
 
-void goto_check_ct::add_all_disable_named_check_pragmas(
+void goto_check_ct::add_all_checked_named_check_pragmas(
   source_locationt &source_location) const
 {
   for(const auto &entry : name_to_flag)
-    source_location.add_pragma("disable:" + id2string(entry.first));
+    source_location.add_pragma("checked:" + id2string(entry.first));
 }
 
 goto_check_ct::named_check_statust