Merge pull request #7565 from remi-delmas-3000/checked-pragma-fix

Fix handling of "enable:named-check" pragmas

Author: tautschnig

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