Open
Description
CBMC version: 5.87
Operating system: Rocky red-hat
Exact command line resulting in the issue:
What behaviour did you expect:
What happened instead:
I would like to disable a specific error (deref of memory that is coming from HW), so I would like to know what the concise list of PRAGMAS exist, and a match from an error to a PRAGMA.
Example :
#pragma CPROVER check push
#pragma CPROVER check disable "conversion"
code
#pragma CPROVER check pop
This check was given to me I could not see it in any doc