T2: differential execution of verdicts, nightly in CI

.github/workflows/cppverify-differential.yml

@@ -0,0 +1,81 @@
+name: CppVerify differential execution
+
+# Every night, each differential case (clang/utils/cppverify-differential) is
+# verified in every configuration it lists and run natively under UBSan on its
+# inputs. The job fails when a verdict and the execution disagree.
+
+on:
+  schedule:
+    - cron: "43 2 * * *"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+env:
+  CVC5_VERSION: "1.4.2"
+
+jobs:
+  differential:
+    name: Differential execution
+    runs-on: ubuntu-24.04
+    timeout-minutes: 355
+    env:
+      CCACHE_DIR: ${{ github.workspace }}/.ccache
+      CCACHE_MAXSIZE: 4G
+      CCACHE_COMPRESS: "1"
+    steps:
+      - name: Free disk space
+        run: |
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /opt/hostedtoolcache/CodeQL
+          df -h /
+
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install build tools and cvc5
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y ninja-build ccache
+          curl -sSfL -o "$RUNNER_TEMP/cvc5.zip" \
+            "https://github.com/cvc5/cvc5/releases/download/cvc5-$CVC5_VERSION/cvc5-Linux-x86_64-static.zip"
+          unzip -q "$RUNNER_TEMP/cvc5.zip" -d "$RUNNER_TEMP/cvc5"
+          dirname "$(find "$RUNNER_TEMP/cvc5" -name cvc5 -type f)" >> "$GITHUB_PATH"
+
+      - uses: actions/cache/restore@v4
+        with:
+          path: .ccache
+          key: ccache-linux-release-${{ github.sha }}
+          restore-keys: ccache-linux-release-
+
+      - name: Configure
+        run: |
+          cmake -S llvm -B build -G Ninja \
+            -DCMAKE_BUILD_TYPE=Release \
+            -DLLVM_ENABLE_PROJECTS=clang \
+            -DLLVM_TARGETS_TO_BUILD=Native \
+            -DCPPVERIFY_VENDOR_Z3=ON \
+            -DCPPVERIFY_PREFER_SYSTEM_Z3=OFF \
+            -DLLVM_ENABLE_ASSERTIONS=OFF \
+            -DLLVM_CCACHE_BUILD=ON
+
+      - name: Build
+        run: ninja -C build clang cpp-verify
+
+      - name: Report the versions
+        run: |
+          build/bin/cpp-verify --version
+          cvc5 --version | head -1
+
+      - name: Run the differential cases
+        run: |
+          python3 clang/utils/cppverify-differential/run.py \
+            --cpp-verify build/bin/cpp-verify --jobs "$(nproc)" \
+            --work "$RUNNER_TEMP/differential" --report differential.json
+
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: differential-report
+          path: differential.json

clang/test/Verify/differential.test

@@ -0,0 +1,28 @@
+# The differential tool (clang/utils/cppverify-differential), which runs nightly
+# over every case, on its own cases: verdicts that execution confirms pass, and
+# a verdict that disagrees with execution is reported. Two of the cases state
+# their contract wrongly in Python on purpose, so a right verdict reads as
+# UNSOUND and a right counterexample as BADCEX. A read past a buffer traps on
+# the page after it, and a contract undefined at an input is no failure of the
+# body.
+#
+# UNSUPPORTED: system-windows
+# RUN: rm -rf %t
+# RUN: not %python %S/../../utils/cppverify-differential/run.py --suite selftest \
+# RUN:   --cpp-verify %cpp-verify --clang %clang --work %t --jobs 1 --report %t.json \
+# RUN:   | FileCheck %s
+# RUN: %python -c "import json, sys; r = {c['case']: c for c in json.load(open(sys.argv[1]))}; \
+# RUN:   print(sorted(r), r['self_overflow']['counterexamples'])" %t.json | FileCheck %s --check-prefix=REPORT
+
+# CHECK-DAG: {{^}}self_add {{ *}}z3=verified admitted=65536 violations=0{{$}}
+# CHECK-DAG: {{^}}self_overflow {{ *}}z3=failed:overflow admitted=20188 violations=21 counterexamples: z3 confirmed: undefined behavior at (2147483647,){{$}}
+# CHECK-DAG: {{^}}self_sum {{ *}}z3=verified admitted=25 violations=0{{$}}
+# CHECK-DAG: {{^}}self_read_past {{ *}}z3=failed:bounds admitted=4 violations=4 counterexamples: z3 no input values{{$}}
+# CHECK-DAG: {{^}}self_contract_div {{ *}}z3=failed:division-by-zero admitted=256 violations=0 counterexamples: z3 the contract is undefined there (division-by-zero){{$}}
+# CHECK-DAG: {{^}}self_bound {{ *}}z3=verified admitted=32768 violations=1{{$}}
+# CHECK-DAG: {{^}}  problem: UNSOUND[z3]: verified, yet 1 admitted inputs misbehave, such as [((0,), 'POST', 0)]{{$}}
+# CHECK-DAG: {{^}}self_wrong_at_5 {{ *}}z3=failed:postcondition admitted=256 violations=0{{$}}
+# CHECK-DAG: {{^}}  problem: BADCEX[z3]: (5,) returns 6 and meets the contract (verification failed: self_wrong_at_5
+# CHECK: {{^}}7 cases, 2 problems{{$}}
+
+# REPORT: ['self_add', 'self_bound', 'self_contract_div', 'self_overflow', 'self_read_past', 'self_sum', 'self_wrong_at_5'] {'z3': 'confirmed: undefined behavior at (2147483647,)'}

clang/utils/cppverify-differential/cases/bit_int.py

@@ -0,0 +1,83 @@
+"""_BitInt(N) (no integer promotion; rank by width)."""
+import differential as diff
+from differential import *  # noqa: F401,F403
+
+for n in (2, 3, 7, 13, 31, 33, 63, 65, 127):
+    diff.TYPES['_BitInt(%d)' % n] = (n, True)
+for n in (1, 3, 7, 13, 31, 33, 63, 65, 127):
+    diff.TYPES['unsigned _BitInt(%d)' % n] = (n, False)
+
+def wrap_n(v, n):
+    v &= (1 << n) - 1
+    return v - (1 << n) if v >= 1 << (n - 1) else v
+
+def boundary_n(n):
+    lo, hi = -(1 << (n - 1)), (1 << (n - 1)) - 1
+    return sorted(set(v for v in [lo, lo + 1, -1, 0, 1, 2, hi - 1, hi, -5, 5] if lo <= v <= hi))
+
+
+R = 'cppverify::result'
+C = []
+
+def case(*a, **k):
+    k.setdefault('vflags', ['--extra-arg=-Wno-bit-int-extension'])
+    C.append(Case(*a, **k))
+
+def M(n):
+    # 2^63 and above have no C++ literal.
+    return '%d' % (1 << n) if n < 63 else '((__int128)1 << %d)' % n
+
+for n in (3, 7, 13, 33, 65):
+    u = 'unsigned _BitInt(%d)' % n
+    s = '_BitInt(%d)' % n
+    ret = '__int128'
+    case('bi_uadd_%d' % n, [(u, 'a'), (u, 'b')], ret,
+         'cppverify::post(%s == (a + b) %% %s)' % (R, M(n)), 'return a + b;',
+         post=lambda a, b, r, n=n: r == (a + b) % (1 << n))
+    case('bi_umul_%d' % n, [(u, 'a'), (u, 'b')], ret,
+         'cppverify::post(%s == (a * b) %% %s)' % (R, M(n)), 'return a * b;',
+         post=lambda a, b, r, n=n: r == (a * b) % (1 << n))
+    case('bi_usub_%d' % n, [(u, 'a'), (u, 'b')], ret,
+         'cppverify::post(%s == (a - b + %s) %% %s)' % (R, M(n), M(n)), 'return a - b;',
+         post=lambda a, b, r, n=n: r == (a - b) % (1 << n))
+    case('bi_sadd_%d' % n, [(s, 'a'), (s, 'b')], ret,
+         'cppverify::post(%s == a + b)' % R, 'return a + b;',
+         post=lambda a, b, r: r == a + b)
+    case('bi_sadd_guard_%d' % n, [(s, 'a'), (s, 'b')], ret,
+         'cppverify::pre(a + b >= -%s && a + b < %s)\ncppverify::post(%s == a + b)' % (M(n - 1), M(n - 1), R), 'return a + b;',
+         pre=lambda a, b, n=n: -(1 << (n - 1)) <= a + b < (1 << (n - 1)), post=lambda a, b, r: r == a + b)
+    case('bi_sdiv_%d' % n, [(s, 'a'), (s, 'b')], ret,
+         'cppverify::pre(b != 0)\ncppverify::post(%s == a / b)' % R, 'return a / b;',
+         pre=lambda a, b: b != 0, post=lambda a, b, r: r == tdiv(a, b))
+    case('bi_srem_%d' % n, [(s, 'a'), (s, 'b')], ret,
+         'cppverify::pre(b != 0 && !(a == -%s && b == -1))\ncppverify::post(%s == a %% b)' % (M(n - 1), R), 'return a % b;',
+         pre=lambda a, b, n=n: b != 0 and not (a == -(1 << (n - 1)) and b == -1), post=lambda a, b, r: r == tmod(a, b))
+    case('bi_sneg_%d' % n, [(s, 'a')], ret,
+         'cppverify::post(%s == -a)' % R, 'return -a;', post=lambda a, r: r == -a)
+    case('bi_conv_from_long_%d' % n, [('long', 'x')], ret,
+         'cppverify::post(%s >= -%s && %s < %s)' % (R, M(n - 1), R, M(n - 1)), 'return (%s)x;' % s,
+         post=lambda x, r, n=n: -(1 << (n - 1)) <= r < (1 << (n - 1)))
+    case('bi_conv_val_%d' % n, [('long', 'x')], ret,
+         'cppverify::post(%s == ((x %% %s) + %s + %s) %% %s - %s)' % (R, M(n), M(n), M(n - 1), M(n), M(n - 1)), 'return (%s)x;' % s,
+         post=lambda x, r, n=n: r == wrap_n(x, n))
+    case('bi_mix_int_%d' % n, [(s, 'a'), ('int', 'b')], ret,
+         'cppverify::pre(b > -1000 && b < 1000)\ncppverify::post(%s == a + b || true)' % R, 'return a + b;',
+         pre=lambda a, b: -1000 < b < 1000, post=lambda a, b, r: True)
+    case('bi_inc_%d' % n, [(s, 'a')], ret,
+         'cppverify::post(true)', 'a++; return a;', post=lambda a, r: True)
+    case('bi_cmp_us_%d' % n, [(u, 'a'), (s, 'b')], 'bool',
+         'cppverify::post(%s == (a < (b < 0 ? b + %s : b)))' % (R, M(n)), 'return a < b;',
+         post=lambda a, b, r, n=n: r == (1 if a < b % (1 << n) else 0))
+    case('bi_shl_%d' % n, [(s, 'a'), ('int', 'k')], ret,
+         'cppverify::pre(k >= 0 && k < %d && a >= 0 && a < 2)\ncppverify::post(%s == (k == %d ? -%s : a * (((__int128)1) << k)) || a == 0)' % (n, R, n - 1, M(n - 1)),
+         'return a << k;', pre=lambda a, k, n=n: 0 <= k < n and 0 <= a < 2,
+         post=lambda a, k, r, n=n: a == 0 or r == (-(1 << (n - 1)) if k == n - 1 else a << k),
+         domain=[(a, k) for a in (-1, 0, 1) for k in range(-1, n + 2)])
+    case('bi_shr_%d' % n, [(s, 'a'), ('int', 'k')], ret,
+         'cppverify::pre(k >= 0 && k < %d)\ncppverify::post(%s * (((__int128)1) << k) <= a && a < (%s + 1) * (((__int128)1) << k))' % (n, R, R),
+         'return a >> k;', pre=lambda a, k, n=n: 0 <= k < n,
+         post=lambda a, k, r: r * 2**k <= a < (r + 1) * 2**k,
+         domain=[(a, k) for a in boundary_n(n) for k in range(-1, n + 2)])
+
+CASES = C
+CONFIGS = ('z3', 'bv', 'int', 'cvc5')

clang/utils/cppverify-differential/cases/calls.py

@@ -0,0 +1,165 @@
+"""Modular calls, argument/result conversions, recursion."""
+from differential import *  # noqa: F401,F403
+
+R = 'cppverify::result'
+C = []
+
+def case(*a, **k):
+    C.append(Case(*a, **k))
+
+INC8 = '''int8_t inc8(int8_t x)
+  cppverify::pre(x < 127)
+  cppverify::post(cppverify::result == x + 1)
+{ return x + 1; }'''
+case('m_conv_arg_ok', [('int', 'y')], 'int',
+     'cppverify::pre(y == 200)\ncppverify::post(%s == -55)' % R, 'return inc8(y);',
+     prelude=INC8, pre=lambda y: y == 200, post=lambda y, r: r == -55, domain=[(200,), (199,), (201,)])
+case('m_conv_arg_wrong', [('int', 'y')], 'int',
+     'cppverify::pre(y == 200)\ncppverify::post(%s == 201)' % R, 'return inc8(y);',
+     prelude=INC8, pre=lambda y: y == 200, post=lambda y, r: r == 201, domain=[(200,)])
+case('m_conv_arg_range', [('int', 'y')], 'int',
+     'cppverify::pre(y >= 0 && y < 1000 && y %% 256 != 127)\ncppverify::post(%s == ((y + 128) %% 256) - 128 + 1)' % R,
+     'return inc8(y);', prelude=INC8, pre=lambda y: 0 <= y < 1000 and y % 256 != 127,
+     post=lambda y, r: r == wrap(y, 'int8_t') + 1, domain=[(y,) for y in range(-5, 1005)])
+case('m_conv_arg_pre_violated', [('int', 'y')], 'int',
+     'cppverify::pre(y == 383)\ncppverify::post(true)', 'return inc8(y);',
+     prelude=INC8, pre=lambda y: y == 383, post=lambda y, r: True, domain=[(383,)])
+TW = '''unsigned twice(unsigned x)
+  cppverify::pre(x < 1000)
+  cppverify::post(cppverify::result == 2 * x)
+{ return 2 * x; }'''
+case('m_unsigned_arg_neg', [('int', 'y')], 'unsigned',
+     'cppverify::pre(y > -5 && y < 5)\ncppverify::post(%s < 10)' % R, 'return twice(y);',
+     prelude=TW, pre=lambda y: -5 < y < 5, post=lambda y, r: r < 10, domain=[(y,) for y in range(-10, 10)])
+LONGRET = '''long big(int x)
+  cppverify::post(cppverify::result == x * 1000L)
+{ return x * 1000L; }'''
+case('m_ret_narrow', [('int', 'x')], 'int8_t',
+     'cppverify::pre(x >= 0 && x < 100)\ncppverify::post(%s == x * 1000)' % R, 'int8_t r = big(x); return r;',
+     prelude=LONGRET, pre=lambda x: 0 <= x < 100, post=lambda x, r: r == x * 1000, domain=[(x,) for x in range(-2, 102)])
+case('m_ret_narrow_ok', [('int', 'x')], 'int8_t',
+     'cppverify::pre(x >= 0 && x < 100)\ncppverify::post(%s == ((x * 1000 + 128) %% 256) - 128)' % R, 'int8_t r = big(x); return r;',
+     prelude=LONGRET, pre=lambda x: 0 <= x < 100, post=lambda x, r: r == wrap(x * 1000, 'int8_t'), domain=[(x,) for x in range(-2, 102)])
+BOOLP = '''int b2i(bool b)
+  cppverify::post(cppverify::result == (b ? 1 : 0))
+{ return b ? 1 : 0; }'''
+case('m_bool_arg', [('int', 'x')], 'int',
+     'cppverify::post(%s == (x != 0 ? 1 : 0))' % R, 'return b2i(x);',
+     prelude=BOOLP, post=lambda x, r: r == (1 if x != 0 else 0))
+case('m_bool_arg_wrong', [('int', 'x')], 'int',
+     'cppverify::post(%s == x %% 2)' % R, 'return b2i(x);',
+     prelude=BOOLP, post=lambda x, r: r == tmod(x, 2), domain=[(x,) for x in range(-3, 300)])
+REASSIGN = '''int bump(int x)
+  cppverify::pre(x < 1000 && x > -1000)
+  cppverify::post(cppverify::result == x + 1)
+{ x = x + 1; return x; }'''
+case('m_callee_reassigns', [('int', 'y')], 'int',
+     'cppverify::pre(y > -100 && y < 100)\ncppverify::post(%s == y + 2)' % R, 'return bump(bump(y));',
+     prelude=REASSIGN, pre=lambda y: -100 < y < 100, post=lambda y, r: r == y + 2, domain=[(y,) for y in range(-105, 105)])
+case('m_callee_reassigns_wrong', [('int', 'y')], 'int',
+     'cppverify::pre(y > -100 && y < 100)\ncppverify::post(%s == y + 3)' % R, 'return bump(bump(y));',
+     prelude=REASSIGN, pre=lambda y: -100 < y < 100, post=lambda y, r: r == y + 3, domain=[(y,) for y in range(-105, 105)])
+case('m_nested_pre', [('int', 'y')], 'int',
+     'cppverify::pre(y == 998)\ncppverify::post(true)', 'return bump(bump(y));',
+     prelude=REASSIGN, pre=lambda y: y == 998, post=lambda y, r: True, domain=[(998,)])
+HELPER = '''int helper(int x) { return x * 2; }'''
+case('m_uncontracted_callee', [('int', 'x')], 'int',
+     'cppverify::post(%s == 2 * x)' % R, 'return helper(x);',
+     prelude=HELPER, post=lambda x, r: r == 2 * x)
+case('m_uncontracted_callee_guard', [('int', 'x')], 'int',
+     'cppverify::pre(x > -1000 && x < 1000)\ncppverify::post(%s == 2 * x)' % R, 'return helper(x);',
+     prelude=HELPER, pre=lambda x: -1000 < x < 1000, post=lambda x, r: r == 2 * x)
+case('m_uncontracted_callee_wrong', [('int', 'x')], 'int',
+     'cppverify::pre(x > -1000 && x < 1000)\ncppverify::post(%s == 3 * x)' % R, 'return helper(x);',
+     prelude=HELPER, pre=lambda x: -1000 < x < 1000, post=lambda x, r: r == 3 * x)
+CEX = '''constexpr int cx(int x) { return x * 2; }'''
+case('m_constexpr_callee_exec', [('int', 'x')], 'int',
+     'cppverify::post(%s == 2 * x)' % R, 'return cx(x);',
+     prelude=CEX, post=lambda x, r: r == 2 * x)
+case('m_constexpr_callee_exec_wrong', [('int', 'x')], 'int',
+     'cppverify::pre(x > -1000 && x < 1000)\ncppverify::post(%s == 3 * x)' % R, 'return cx(x);',
+     prelude=CEX, pre=lambda x: -1000 < x < 1000, post=lambda x, r: r == 3 * x)
+FACT = '''int fact(int n)
+  cppverify::pre(n >= 0 && n <= 12)
+  cppverify::decreases(n)
+  cppverify::post(cppverify::result >= 1)
+{ if (n == 0) return 1; int r = fact(n - 1); return n * r; }'''
+case('m_rec_fact', [('int', 'n')], 'int',
+     'cppverify::pre(n >= 0 && n <= 12)\ncppverify::post(%s >= 1)' % R, 'return fact(n);',
+     prelude=FACT, pre=lambda n: 0 <= n <= 12, post=lambda n, r: r >= 1, domain=[(n,) for n in range(-2, 15)])
+FACT13 = '''int fact13(int n)
+  cppverify::pre(n >= 0 && n <= 13)
+  cppverify::decreases(n)
+  cppverify::post(cppverify::result >= 1)
+{ if (n == 0) return 1; int r = fact13(n - 1); return n * r; }'''
+case('m_rec_fact13', [('int', 'n')], 'int',
+     'cppverify::pre(n >= 0 && n <= 13)\ncppverify::post(%s >= 1)' % R, 'return fact13(n);',
+     prelude=FACT13, pre=lambda n: 0 <= n <= 13, post=lambda n, r: r >= 1, domain=[(n,) for n in range(-2, 15)])
+EVENODD = '''bool is_odd(int n);
+bool is_even(int n)
+  cppverify::pre(n >= 0)
+  cppverify::decreases(n)
+  cppverify::post(cppverify::result == (n % 2 == 0))
+{ if (n == 0) return true; return is_odd(n - 1); }
+bool is_odd(int n)
+  cppverify::pre(n >= 0)
+  cppverify::decreases(n)
+  cppverify::post(cppverify::result == (n % 2 == 1))
+{ if (n == 0) return false; return is_even(n - 1); }'''
+case('m_mutual_rec', [('int', 'n')], 'bool',
+     'cppverify::pre(n >= 0 && n <= 1000)\ncppverify::post(%s == (n %% 2 == 0))' % R, 'return is_even(n);',
+     prelude=EVENODD,
+     pre=lambda n: 0 <= n <= 1000, post=lambda n, r: r == (1 if n % 2 == 0 else 0), domain=[(n,) for n in range(0, 1001)])
+DEFARG = '''int addd(int x, int y = 5)
+  cppverify::pre(x < 1000 && x > -1000)
+  cppverify::post(cppverify::result == x + y)
+{ return x + y; }'''
+case('m_default_arg', [('int', 'x')], 'int',
+     'cppverify::pre(x < 1000 && x > -1000)\ncppverify::post(%s == x + 5)' % R, 'return addd(x);',
+     prelude=DEFARG,
+     pre=lambda x: -1000 < x < 1000, post=lambda x, r: r == x + 5)
+case('m_default_arg_ub', [('int', 'x')], 'int',
+     'cppverify::post(true)', 'return addd(1, x);',
+     prelude=DEFARG,
+     post=lambda x, r: True)
+OVL = '''int ov(int x) cppverify::post(cppverify::result == 1) { return 1; }
+int ov(long x) cppverify::post(cppverify::result == 2) { return 2; }
+int ov(unsigned x) cppverify::post(cppverify::result == 3) { return 3; }'''
+case('m_overload', [('int8_t', 'x')], 'int',
+     'cppverify::post(%s == 1)' % R, 'return ov(x);', prelude=OVL, post=lambda x, r: r == 1)
+case('m_overload_u8', [('uint8_t', 'x')], 'int',
+     'cppverify::post(%s == 1)' % R, 'return ov(x);', prelude=OVL, post=lambda x, r: r == 1)
+case('m_overload_long', [('long', 'x')], 'int',
+     'cppverify::post(%s == 2)' % R, 'return ov(x);', prelude=OVL, post=lambda x, r: r == 2)
+case('m_overload_u', [('uint16_t', 'x')], 'int',
+     'cppverify::post(%s == 3)' % R, 'return ov(x + 0u);', prelude=OVL, post=lambda x, r: r == 3)
+SDIV = '''int sdiv(int x, int y)
+  cppverify::pre(y != 0 && !(x == -2147483647 - 1 && y == -1))
+  cppverify::post(cppverify::result == x / y)
+{ return x / y; }'''
+case('m_short_circuit_call', [('int', 'x'), ('int', 'y')], 'bool',
+     'cppverify::post(true)', 'return y != 0 && y != -1 && sdiv(x, y) > 0;',
+     prelude=SDIV, post=lambda x, y, r: True)
+case('m_short_circuit_call_bad', [('int', 'x'), ('int', 'y')], 'bool',
+     'cppverify::post(true)', 'return y != 0 && sdiv(x, y) > 0;',
+     prelude=SDIV, post=lambda x, y, r: True)
+case('m_ternary_call', [('int', 'x'), ('int', 'y')], 'int',
+     'cppverify::post(y == 0 || y == -1 || %s == x / y)' % R, 'return (y == 0 || y == -1) ? 0 : sdiv(x, y);',
+     prelude=SDIV, post=lambda x, y, r: y == 0 or y == -1 or r == tdiv(x, y))
+WEAK = '''int weak(int x)
+  cppverify::post(cppverify::result >= x)
+{ return x < 100 ? 100 : x; }'''
+case('m_weak_post', [('int', 'x')], 'int',
+     'cppverify::post(%s >= 100)' % R, 'return weak(x);',
+     prelude=WEAK, post=lambda x, r: r >= 100)
+case('m_arg_eval_conv', [('uint8_t', 'a'), ('uint8_t', 'b')], 'int',
+     'cppverify::post(%s == a + b)' % R, 'return sum16(a + b);',
+     prelude='int sum16(int16_t v) cppverify::post(cppverify::result == v) { return v; }',
+     post=lambda a, b, r: r == a + b)
+case('m_arg_conv_u16', [('int', 'x')], 'int',
+     'cppverify::pre(x >= 65530 && x <= 65540)\ncppverify::post(%s == x)' % R, 'return idu16(x);',
+     prelude='int idu16(uint16_t v) cppverify::post(cppverify::result == v) { return v; }',
+     pre=lambda x: 65530 <= x <= 65540, post=lambda x, r: r == x, domain=[(x,) for x in range(65525, 65545)])
+
+CASES = C
+CONFIGS = ('z3', 'bv', 'int', 'cvc5')