mutliple enable/disable now cause a hard PARSING_ERROR in the C frontend.

Author: Remi Delmas

doc/cprover-manual/properties.md

@@ -142,7 +142,7 @@ CPROVER pragmas are handled using a stack:
 - `#pragma CPROVER check disable "<name_of_check>"` adds a disable pragma at the top of the stack
 - `#pragma CPROVER check enable "<name_of_check>"` adds a enable pragma at the top of the stack
 - an `enable` or `disable` pragma for a given check present at the top level of the stack shadows other pragmas for the same in lower levels of the stack
-- adding both `enable` and `disable` pragmas for a same check in a same level of the stack creates a warning, the most recent pragma takes precedence
+- adding both `enable` and `disable` pragmas for a same check in a same level of the stack creates a PARSING_ERROR.
 - `#pragma CPROVER check pop` pops a level in the stack and restores the state of pragmas at the sub level  
 
 For example, for unsigned overflow checks, use
@@ -183,12 +183,12 @@ unsigned foo(unsigned x)
 #pragma CPROVER check push
 #pragma CPROVER check disable "unsigned-overflow"
 #pragma CPROVER check enable "unsigned-overflow" 
-  // warning: both enable and disable for unsigned-overflow (last one takes precedence)
-  x = x + 2; // unsigned and signed overflow check apply here
+  // PARSING_ERROR ... Found enable and disable pragmas for unsigned-overflow-check
+  x = x + 2;
 #pragma CPROVER check pop
-  x = x + 3; // unsigned and signed overflow check apply here
+  x = x + 3;
 #pragma CPROVER check pop
-  x = x + 2; // unsigned overflow checks do not apply here
+  x = x + 2;
 ```
 
 

regression/cbmc/pragma_cprover_enable_disable_multiple/test.desc

@@ -2,8 +2,8 @@ CORE
 main.c
 
 ^file main.c line \d+ function main: Found enable and disable pragmas for pointer-primitive-check
-^VERIFICATION SUCCESSFUL$
-^EXIT=0$
+^PARSING ERROR$
+^EXIT=6$
 ^SIGNAL=0$
 --
 ^file main.c line \d+ function main: Found enable and disable pragmas for pointer-overflow-check

src/analyses/goto_check.cpp

@@ -10,7 +10,6 @@ Author: Daniel Kroening, [email protected]
 /// GOTO Programs
 
 #include "goto_check.h"
-#include<iostream>
 
 #include <algorithm>
 

src/ansi-c/ansi_c_parser.cpp

@@ -197,12 +197,14 @@ void ansi_c_parsert::pragma_cprover_add_check(irep_idt name, bool enabled)
   if(pragma_cprover_stack.empty())
     pragma_cprover_push();
 
+  pragma_cprover_stack.back()[name] = enabled;
+}
+
+bool ansi_c_parsert::pragma_cprover_clash(irep_idt name, bool enabled)
+{
   auto top = pragma_cprover_stack.back();
   auto found = top.find(name);
-  if(found != top.end() && found->second!=enabled)
-    yyansi_cerror("Found enable and disable pragmas for " + id2string(name));
-  
-  pragma_cprover_stack.back()[name] = enabled;
+  return found != top.end() && found->second != enabled;
 }
 
 void ansi_c_parsert::set_pragma_cprover()

src/ansi-c/ansi_c_parser.h

@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/parser.h>
 #include <util/config.h>
-#include <iostream>
+
 #include "ansi_c_parse_tree.h"
 #include "ansi_c_scope.h"
 
@@ -154,12 +154,12 @@ class ansi_c_parsert:public parsert
   void pragma_cprover_pop();
 
   /// \brief Adds a check to the CPROVER pragma stack
-  /// 
-  /// Reports a yyansi_cerror if 
-  /// the same check with different polarity
-  /// is already present in at top of the stack
   void pragma_cprover_add_check(irep_idt name, bool enabled);
 
+  /// Returns true the same check with different polarity
+  /// is already present at top of the stack
+  bool pragma_cprover_clash(irep_idt name, bool enabled);
+
   /// \brief Tags \ref source_location with 
   /// the current CPROVER pragma stack
   void set_pragma_cprover();

src/ansi-c/scanner.l

@@ -416,10 +416,18 @@ void ansi_c_scanner_init()
                   std::string tmp(yytext);
                   bool enable = tmp.find("enable")!=std::string::npos;
                   std::string::size_type p = tmp.find('"') + 1;
-                  std::string value =
+                  std::string check_name =
                     std::string(tmp, p, tmp.size() - p - 1) +
                     std::string("-check");
-                  PARSER.pragma_cprover_add_check(value, enable);
+                  bool clash = PARSER.pragma_cprover_clash(check_name, enable);
+                  if(clash)
+                  {
+                    yyansi_cerror(
+                      "Found enable and disable pragmas for " +
+                      id2string(check_name));
+                    return TOK_SCANNER_ERROR;
+                  }
+                  PARSER.pragma_cprover_add_check(check_name, enable);
                   PARSER.set_pragma_cprover();
                 }
 <CPROVER_PRAGMA>. {