Add support for the "check disable" pragma to disable the pointer-primitive check

[jimgrundy]

CBMC version: 5.34.0
Operating system: N/A
Exact command line resulting in the issue: cbmc main.c --pointer-primitive-check
What behaviour did you expect:

Running this program, I expect the analysis to pass, exactly as it does if I don't include the "--pointer-primitive-check" on the command line.

int main()
{
  void *p = malloc(1);
  void *q;

#pragma CPROVER check push
#pragma CPROVER check disable "pointer-primitive"
  if (__CPROVER_same_object(p,q)) {
  } else {
  }
#pragma CPROVER check pop
}

What happened instead:

CBMC version 5.34.0 (cbmc-5.34.0-dirty) 64-bit x86_64 macos
Parsing main.c
file main.c line 4 function main: Unsupported #pragma CPROVER before ' '
file main.c line 4 function main: syntax error before ' '
PARSING ERROR

Note: this is the same output you get if you use a complete random string in the pragma, say "dog" instead of "pointer-primtive". However, some other check names, like "pointer" do work.

This request has 2 parts:
1/ Support pointer-primitive in this pragma so that it can be disabled for code regions.
2/ Give a better error message that includes the string that wasn't recognized instead of ''

[remi-delmas-3000]

In src/ansi-c/scanner.l we have these definitions

@Line 235 
arith_check     ("conversion"|"undefined-shift"|"nan"|"div-by-zero")
enum_check      "enum-range"
memory_check    ("bounds"|"pointer"|"memory_leak")
overflow_check  ("signed"|"unsigned"|"pointer"|"float")"-overflow"
named_check     ["]({arith_check}|{enum_check}|{memory_check}|{overflow_check})["]
...
@Line 413
<CPROVER_PRAGMA>{ws}"check"{ws}"disable"{ws}{named_check} {
                  std::string tmp(yytext);
                  std::string::size_type p = tmp.find('"') + 1;
                  std::string value =
                    std::string("disable:") +
                    std::string(tmp, p, tmp.size() - p - 1) +
                    std::string("-check");
                  if(PARSER.pragma_cprover.empty())
                    PARSER.pragma_cprover.push_back({value});
                  else
                    PARSER.pragma_cprover.back().insert(value);
                  PARSER.set_pragma_cprover();
                }

This is the set of accepted check names:

"conversion"
"undefined-shift"
"nan"
"div-by-zero"
"enum-range"
"bounds" 
"pointer"
"memory_leak"
"signed-overflow"
"unsigned-overflow"
"pointer-overflow"
"float-overflow"

it does not contain "pointer-primitive".

The named_check used in the pragme gets mapped to "disable:<named_check>-check" by the lexer and is added to the source locations enclosed in the push/pop pragmas.

void goto_checkt::goto_check in src/analyses/goto_check.cpp however does handle "disable:pointer-primitive-check"

@Line 1924
      else if(d.first == "disable:pointer-primitive-check")
        flag_resetter.set_flag(enable_pointer_primitive_check, false);

So fixing the parser should suffice.