[SwayamInSync]

A quantifier in executable code compiled without a diagnostic, to poison:

bool all_nonneg(int n) { return cppverify::forall(k, 0, n, k >= 0); }

define dso_local noundef zeroext i1 @_Z10all_nonnegi(i32 noundef %n) {
entry:
  ret i1 poison
}

CodeGen returns poison for every contract expression as a safety net, since contract expressions should never reach it, and Sema rejects cppverify::choose in executable code (err_choose_in_executable_code) but not cppverify::forall or cppverify::exists. The verifier reads the quantifier as a quantifier, so a function could verify and compile to undefined behavior.

ExecutableSpecUseFinder, which already rejects spec functions, ghost variables, collections, and choose in executable code, now rejects the quantifiers too, with the error that named choose and now names the construct (cppverify::forall exists only for verification and cannot be used in executable code; use it in a contract, ghost block, or spec or proof function). A construct is reported once, with what it contains, rather than once for each nested quantifier, choice, or spec call inside it. Contracts, ghost code, cppverify::check, and unevaluated operands (sizeof, decltype, noexcept) are unaffected.

Testing: Verify/errors_quantifier_in_executable.cpp checks a quantifier returned, used as an initializer, nested in another, in a global initializer, and in two templates (one never instantiated, one instantiated twice, each reported once), and that quantifiers in a contract, a check, a ghost block, and sizeof compile with no poison in the IR. It fails on main. Each of six mutations fails it or errors_choose.cpp: not checking forall, exists, or choose; reporting a nested quantifier again; reporting one in ghost code; and reporting one again for each instantiation of its template.

errors_namespaced.cpp wrote a bare forall (under using namespace cppverify) in a return statement. The parser recovers it as cppverify::forall, which now also draws the new error, so the test writes it in a cppverify::check, where a quantifier belongs, and still checks its one error.

Checked on main together with the change of #37, for Clang's analyses, whose files are disjoint from these: in a build with assertions every Clang test passes (48,612), as does the Verify suite; in a release build the Verify suite gives 417 passed, 1 unsupported. A verdict differential against main over the Verify sources changes only the new test and decode_uleb128_canonical (llvm_uleb128.cpp, with roundtrip_uleb128 after it), which timed out in main's run and verified here, as in another differential against main the same day; that file has no quantifier in executable code. No time changed.

Rebased onto main after #28, after which a quantifier whose body depends on a template parameter compiles, as in the template cases: Verify suite 421 passed, 1 unsupported.