[SwayamInSync]

Member functions were not verified: contracts written in a class were skipped with a warning (contracts on member functions are not yet supported and are ignored), and a contracted member function defined outside its class was an error (member function verification is unsupported). Now a member function of a class without bases or virtual functions is a function of this:

struct Counter {
  void bump()
    cv::pre(n < limit)
    cv::modifies(n)
    cv::post(n == cv::old(n) + 1 && limit == cv::old(limit))
  {
    n = n + 1;
  }

  int get() const
    cv::post(cv::result == n)
  {
    return n;
  }

  void reset()
    cv::post(n == 0 && limit == 10)
  {
    n = 0;
    limit = 10;
  }

  void copy_from(const Counter &o)
    cv::modifies(n)
    cv::post(n == o.n)
  {
    n = o.n;
  }

  int n;
  int limit;
};

int counted()
  cv::post(cv::result == 11)
{
  Counter c;
  c.n = 0;
  c.limit = 5;
  c.bump();
  int k = c.get();
  c.reset();
  return k + c.limit;
}

void reset_count(Counter &c)
  cv::modifies(c.n)
{
  c.reset();
}

void self_copy(Counter &c)
  cv::modifies(c.n)
{
  c.copy_from(c);
}

Verified: Counter::bump [backend=z3]
Verified: Counter::get [backend=z3]
Verified: Counter::reset [backend=z3]
Verified: Counter::copy_from [backend=z3]
Verified: counted [backend=z3]
counter.cpp:49:5: error: verification failed: reset_count [...::frame@49:5] (counterexample: c [ssa=c_0] [type=pointer] = 1; trace: call.reset@49:5 arg0=1) [backend=z3] [reason=counterexample]
counter.cpp:55:5: error: verification failed: self_copy [...::aliasing@55:5] (counterexample: c [ssa=c_0] [type=pointer] = 1; trace: call.copy_from@55:5 arg0=1 arg1=1) [backend=z3] [reason=counterexample]

Stacked on #72 (B3-1 of plan item B3: member functions; constructors, class invariants, and member operators follow).

Design

Plan B3's design, from Dafny's this with modifies this, Verus's &self/&mut self, and C++26's contracts, on top of B3a:

• this is a parameter. A non-static member function's first parameter is this, a pointer to getFunctionObjectParameterType() (to const in a const member function), with the generated validity of a reference (non-null, valid, initialized at entry). CXXThisExpr converts to it, so this->n and an implicit n are places through a pointer exactly as p->n (3b), and modifies(*this) is its object's region. It joins the default separation (AddressEntry); cppverify::aliases(this, o) names it (aliasesListed). Its class is a RecordParams entry, so a local object is lent to a member function under verify: Lend local records and addresses to callees that keep no address of them #71's rules.
• Frame, decision Q8 (decided 2026-10-20): a verified non-const member function without modifies may write *this; a const one only its own storage, mutable fields only when listed; an explicit modifies replaces the default; a trusted or bodiless one keeps the trusted-contract rule.
• Calls pass the object's address first (convertExecCallArgs): p->m() passes p, this->m() and m() pass this, and obj.m() binds obj as a reference argument (address discovery promotes the local). A static member function is a free function. A member call inside an expression is unsupported as a free call is.
• Clauses in the complete-class context. C++26 makes a function contract specifier of a member function a complete-class context. The parser now keeps an in-class member function's clause tokens with its late-parsed declaration, as Clang keeps an exception specification's, and parses them in ParseLexedMethodDeclaration with the parameters and this in scope, before the late-parsed body (ParseFunctionContractClauseList is ParseFunctionContractClauses after the declarator's scopes). An out-of-line definition's clauses enter its class's scope and this, as its trailing requires-clause does.
• Fail closed (unsupportedMemberFunction), each an error of its function when it is contracted: virtual functions, member functions of a class with bases (or polymorphic), constructors and destructors (next), conversion functions, explicit object parameters, rvalue- and volatile-qualified ones, lambdas. A member of a class template keeps the template warning, now naming the class template.

Tests

suite/member_functions.cpp (Z3, BMC, a Lean export): bump, a const get, reset without modifies (the default frame), twice through implicit this calls, copy_from and aliases(this, o), a store outside modifies (frame), a const member function writing a mutable field without and with modifies, a static member function, a declaration's contract with an out-of-line definition, a member call inside an expression (the free-call error); callers on a local object, through a pointer, through a reference, on a member of an object; a caller frame narrower than the default (frame); this and a parameter one object (aliasing, and with aliases); a const member function sharing its object with a read-only parameter; the located errors of a virtual function, a derived class, a constructor, a destructor, and a conversion function.

member_function_contracts.cpp (-verify): in-class clauses name later members and this, an undeclared name is an error there, an out-of-line definition's clauses name members and this, and a contract on two declarations is an error.

located_errors.cpp now locates a virtual function's error; template_contracts.cpp expects the class template's warning on its member.

The warning for contracts on member functions is gone, since it is no longer issued.

Mutants, each built and run on member_functions.cpp, member_function_contracts.cpp, template_contracts.cpp, located_errors.cpp, and local_record_arguments.cpp: 15 of 15 killed.

Mutant	Killed by
member functions rejected (the base)	member_functions
no validity of this	member_functions
this not in the separation	member_functions
this mutable in a const member function	member_functions (self_plus)
no default frame (Q8)	member_functions
the default frame for const member functions too	member_functions (peek_bad)
the object not passed	member_functions
a called local not promoted	member_functions
virtual functions accepted	member_functions, located_errors
classes with bases accepted	member_functions
aliases cannot name this	member_functions
in-class clauses dropped	member_functions, member_function_contracts, template_contracts
out-of-line clauses outside the class's scope	member_functions, member_function_contracts
a class template's member named as a function template	template_contracts
no this in out-of-line clauses	member_functions, member_function_contracts

Docs

• structs.rst: "Member functions", a checked example (five verified, the narrow frame and the self-copy fail).
• functions-loops.rst, limitations.rst: member functions supported; what is not.
• Release notes: "Member functions".
• DESIGN.md: 3f. ARCHITECTURE.md: member functions, the late parse.

Checked

• The Verify suite on a release build: 457 passed (the exhaustive decoder filtered out), 1199 s with 40 workers.
• After removing the warning and formatting: the 8 member-function, reference, extent, located-error, template, and docs tests pass.
• The doc pages' examples (structs, functions-loops, DESIGN): 42 checked, 0 failed.