pragma check disable does not work as expected

[danielsn]

It seems that it only applies at the statement level, but there is no warning given when compiling this with CBMC

int nondet_int();

void main() {
  int a = nondet_int();
  int b = nondet_int();
  int c = a +
  #pragma CPROVER check disable "signed-overflow"
  a + b;
  #pragma CPROVER check pop
}

╰─$ cbmc test.c --signed-overflow-check
CBMC version 5.43.0 (cbmc-5.43.0-19-g6dfd3f78d) 64-bit x86_64 macos
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.00661267s
size of program expression: 50 steps
simple slicing removed 3 assignments
Generated 2 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 3.8862e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00422007s
Running propositional reduction
Post-processing
Runtime Post-process: 0.000268633s
Solving with MiniSAT 2.2.1 with simplifier
438 variables, 1345 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.00387758s
Runtime decision procedure: 0.00834528s
Running propositional reduction
Solving with MiniSAT 2.2.1 with simplifier
438 variables, 1 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 7.3659e-05s
Runtime decision procedure: 0.000119505s

** Results:
/Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/stdio.h function __sputc
[__sputc.overflow.1] line 261 arithmetic overflow on signed - in _p->_w - 1: SUCCESS

test.c function main
[main.overflow.1] line 9 arithmetic overflow on signed + in a + a: FAILURE
[main.overflow.2] line 11 arithmetic overflow on signed + in a + a + b: FAILURE

** 2 of 3 failed (3 iterations)
VERIFICATION FAILED

[tautschnig]

Having spoken to @danielsn:

1) The actual desired solution is to have ways to specify the addition as having wrap-around semantics. Similarly other built-ins may be required where the pragmas are really workarounds. 2) There should at least be a warning that this pragma will be ignored. 3) Supporting pragmas on all expressions is possible, but costly. Hence preferring 2) over this. 1) Should be covered by a separate effort.

[tautschnig]

Further failing example from @danielsn:

#include <assert.h>

int nondet_int();

void main() {
  int a = nondet_int();
  int b = nondet_int();

#pragma CPROVER check disable "signed-overflow"
  for (int i = 0; i < 10; ++i) {
    int temp = a + b;
#pragma CPROVER check pop
    int foo = temp + a;
    assert(foo > 2);
  }
}

Edit: pragma annotations are not sensitive to scopes, so there is nothing really wrong with the above.