enabling #pragma disable "pointer-primitive"

[remi-delmas-3000]

Fixes #6239.

This PR enables #pragma disable "pointer-primitive" by adding "pointer-primitive" to the list of named checks accepted by the ansi-c lexer, to allow users to disable pointer primitive checks using pragmas embedded in C code. This addresses issue #6239. The goto_check function already handles "disable:pointer-primitive-check" so only a lexer modification was needed.

• Each commit message has a non-empty body, explaining why the change was made.
• Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[SaswatPadhi]

A minor comment below

[SaswatPadhi]

This pattern seems a bit fragile -- the 2 checks come from malloc but if the library implementation changes, that number could be different in the future.

I think just checking VERIFICATION SUCCESSFUL, as you are already doing below, should suffice?

[jimgrundy]

We need this to unblock some of the loop-contracts work. Can someone take a look?

[martin-cs]

Looks good. If you really want to gold plate it you could have something that fails the --pointer-primitive-check outside of the area covered by the #pragma.

[martin-cs]

@jimgrundy HTH but note that there are currently regression failures of this PR and it cannot be merged until those are resolved.

[kroening]

I had hoped to get some clarification on the use-case.
The _CPROVER-prefixed pointer primitives are not really meant to be used in user-code, so why would one want to have checks for them?

[remi-delmas-3000]

Looks good. If you really want to gold plate it you could have something that fails the --pointer-primitive-check outside of the area covered by the #pragma.

will do

[jimgrundy]

Should have been more specific. I was hoping one of "us" would be prompted to take a look at it, at least to get those build fails fixed so we can talk about merging.

[jimgrundy]

@kroening "The _CPROVER-prefixed pointer primitives are not really meant to be used in user-code, so why would one want to have checks for them?". Well, yes, sure. But in a way we're agreeing with you here by asking for a way to shut them off for selected code.

Why do we turn them on globally in the first place though I guess would be a reasonable question. If we never turned them on globally with a command-line flag we wouldn't need a pragma to turn them off locally. One might ask more generally why these checks were implemented in the first place.

I think the answer is that we find that these checks can point out misunderstandings in the instrumentation code that we generate and so we've grown to like them. However, there are times when in local sections we feel like we know what we are doing and would be better served by turning them off.

More generally, there are a number of checks that can be enabled globally via a command-line flag and disabled locally with a pragma. This one has been the odd one out in that you can enable it globally but not disable it locally. It just seems that for consistency they should all work the same.

[codecov]

Codecov Report

Merging #6395 (8f1620d) into develop (af94148) will increase coverage by 0.00%.
The diff coverage is n/a.

❗ Current head 8f1620d differs from pull request most recent head 9c875f2. Consider uploading reports for the commit 9c875f2 to get more accurate results

@@           Coverage Diff            @@
##           develop    #6395   +/-   ##
========================================
  Coverage    75.97%   75.97%           
========================================
  Files         1523     1523           
  Lines       164191   164191           
========================================
+ Hits        124748   124752    +4     
+ Misses       39443    39439    -4     

Impacted Files	Coverage Δ
src/ansi-c/scanner.l	61.75% <ø> (ø)
src/goto-analyzer/taint_analysis.cpp	78.21% <0.00%> (-0.22%)	⬇️
src/goto-instrument/dot.cpp	0.00% <0.00%> (ø)
src/goto-symex/symex_main.cpp	86.00% <0.00%> (+0.03%)	⬆️
src/goto-programs/remove_virtual_functions.cpp	92.85% <0.00%> (+0.04%)	⬆️
src/goto-instrument/goto_program2code.cpp	69.33% <0.00%> (+0.12%)	⬆️
src/goto-programs/goto_program.h	90.49% <0.00%> (+0.21%)	⬆️
src/analyses/goto_check.cpp	88.74% <0.00%> (+0.30%)	⬆️

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 038a53b...9c875f2. Read the comment docs.

[SaswatPadhi]

LGTM; thanks!

[TGWDB]

@kroening Has your question been answered? Also are you the one that approval is now waiting on?