History for tests - MattCCC/cppl

fix: Refuse by name an element of a vector, a string or a span read in a contract, whose model keeps only the length, and point to the array forms a contract reads

MattCCC

committed

f0479a6

test: Refuse a contract whose parenthesized propositions beside && nest past the depth a proposition is read to

MattCCC

committed

6cd178d

feat: Read an implication or an equivalence in a loop invariant, and a parenthesized implication beside && or || in a contract, keeping a parenthesized member access the C++ it is

MattCCC

committed

c88fea6

feat: Compose a function's path proofs through a select its returned value holds beneath another operation, as !both for a local both = p && q, so the route split on the local lines up

MattCCC

committed

4417675

fix: Refuse by name an element of a std::array a pointer designates selected at a term, and make the value-initialization mutations compile

MattCCC

committed

db3723d

feat: Lower a statement whose ?:, && or || reads an element on one arm as a call's argument or an operand once on each route, the route's arm in place of the selection

MattCCC

committed

2b63e64

feat: Value-initialize the members an aggregate initializer leaves out, as C++ does, refusing a default member initializer, a constructor and a designated element by name

MattCCC

committed

ef2aac8

feat: Follow a member array of the implicit object, std::array or built in, and an object a reference parameter designates member by member, so a stack class and its callers verify

MattCCC

committed

edc0837

build: Delete the oversized.txt exemption and the code that reads it, now that every C++ file is within the file-length limit

MattCCC

committed

10440af

test: Split the projection tests into the projection's properties and what erasure removes

MattCCC

committed

87ff340

feat: Lower a declaration or assignment whose ?:, && or || reads an element on one arm once on each route, the route's arm in place of the selection

MattCCC

committed

fe884a5

feat: Use an implication in scope whose premise automation proves rather than finds as stated, as a caller relies on a callee's conditional postcondition

MattCCC

committed

08c55d6

feat: Lower && and || in a pure definition and a contract's term as the conditional value C++ evaluates, each operand owing its conditions unguarded

MattCCC

committed

9d42e11

feat: Verify && and || as the values C++ evaluates, each arm of a returned ?:, && or || on its own route, and element reads in if and loop conditions where they are evaluated

MattCCC

committed

d6f12cb

test: Split the adversarial kernel tests into attacks on the rules, on structure and limits, and on falsity

MattCCC

committed

512ce0e

test: Split the kernel's checking tests by rule: reflexivity and well-formedness, quantifiers, implication, transport, and the connectives

MattCCC

committed

d183c7e

test: Split the recognizer tests by what they recognize: declarations and words, proofs, contracts and loops, claims and splits, and unsafe and ghost code

MattCCC

committed

e435dc9

feat: Take cases on a disjunction inside a premise, on a first side's order, and on a selection in a disjunctive goal or a premise, and split a selection local where a condition reads it

MattCCC

committed

e5d7e52

test: Split the formatter tests by what they format: the engine's contract, clauses, proofs, ranges, and style and idempotency

MattCCC

committed

9f2f0bf

test: Split the arithmetic evidence tests by what they test: types and normalization, reasoning, the kernel's authority, and realistic obligations

MattCCC

committed

ebefa3a

feat: State a loop invariant's && and || as the conjunction and disjunction of its operands, each specified on its own, as a contract does

MattCCC

committed

00cada9

refactor: Split the kernel derivation generator by the rules it draws: terms and definitions, structural rules, eliminations and arithmetic

MattCCC

committed

e89cc74

test: Refuse a call to a function with unsafe code made by a default argument a call relies on, which would read the temporary it writes as kept, and break the check that sees it

MattCCC

committed

e1ad843

test: Refuse a struct member rebound out of order, a reference beside a written member, a refined member assigned whole and a converting constructor, and require each refusal to come from its own case

MattCCC

committed

a6954ac

test: Verify and run whole struct values flowing through copies, calls, returns and assignments, and refuse each flow whose claim is false or whose copy runs user code

MattCCC

committed

89550fd

feat: Pass, return, copy and assign whole struct values in verified bodies, reading a C++-defined memberwise copy as its operand and a struct handed to a reference as the group of members it may write

MattCCC

committed

ee75a3f

fix: Refuse a call to a function whose unsafe code may write what it is handed anywhere but as a statement, initializer or assignment of its own, since only there is that write followed

MattCCC

committed

50f5bf6

build: Enforce a 1000-line limit on every C++ file with ci_filelength, recording each file over it whose split is pending

MattCCC

committed

1df696c

test: Refuse a range-based for whose unseen initialization or measured shrinking would otherwise be proven, and drop two range checks no input reaches

MattCCC

committed

a955cb6

test: Verify range-based fors over every modeled range with their erasure, refuse each unmodeled or undefined use by name, and name an aggregate element where a range-based for will not bind it

MattCCC

committed

be1d386

Navigation Menu

Repository navigation

Commits

Commits on Oct 7, 2026

fix: Ask a compound update of an array element whether the element's type is promoted, not the array's, so a[i] += 1u of a built-in or std::array element verifies

test: Sweep every V1 mechanism together in a three-unit trading desk that verifies, runs and erases in each standard, beside forty refused twins each one change from it

fix: Rest a claim whose body writes a std::array element through operator[] on the std::array model, never counting it assumption-free

release: Cut C++L 1.0.0, freezing the specification, the grammar and the kernel calculus at it, with its changelog and release claims

fix: Owe a signed subscript index that it is not negative as well as below the extent, so a[-1] no longer verifies

Commits on Oct 6, 2026

fix: Refuse by name an element of a vector, a string or a span read in a contract, whose model keeps only the length, and point to the array forms a contract reads

test: Refuse a contract whose parenthesized propositions beside && nest past the depth a proposition is read to

feat: Read an implication or an equivalence in a loop invariant, and a parenthesized implication beside && or || in a contract, keeping a parenthesized member access the C++ it is

feat: Compose a function's path proofs through a select its returned value holds beneath another operation, as !both for a local both = p && q, so the route split on the local lines up

fix: Refuse by name an element of a std::array a pointer designates selected at a term, and make the value-initialization mutations compile

feat: Lower a statement whose ?:, && or || reads an element on one arm as a call's argument or an operand once on each route, the route's arm in place of the selection

feat: Value-initialize the members an aggregate initializer leaves out, as C++ does, refusing a default member initializer, a constructor and a designated element by name

feat: Follow a member array of the implicit object, std::array or built in, and an object a reference parameter designates member by member, so a stack class and its callers verify

build: Delete the oversized.txt exemption and the code that reads it, now that every C++ file is within the file-length limit

test: Split the projection tests into the projection's properties and what erasure removes

feat: Lower a declaration or assignment whose ?:, && or || reads an element on one arm once on each route, the route's arm in place of the selection

feat: Use an implication in scope whose premise automation proves rather than finds as stated, as a caller relies on a callee's conditional postcondition

feat: Lower && and || in a pure definition and a contract's term as the conditional value C++ evaluates, each operand owing its conditions unguarded

feat: Verify && and || as the values C++ evaluates, each arm of a returned ?:, && or || on its own route, and element reads in if and loop conditions where they are evaluated

test: Split the adversarial kernel tests into attacks on the rules, on structure and limits, and on falsity

test: Split the kernel's checking tests by rule: reflexivity and well-formedness, quantifiers, implication, transport, and the connectives

test: Split the recognizer tests by what they recognize: declarations and words, proofs, contracts and loops, claims and splits, and unsafe and ghost code

feat: Take cases on a disjunction inside a premise, on a first side's order, and on a selection in a disjunctive goal or a premise, and split a selection local where a condition reads it

test: Split the formatter tests by what they format: the engine's contract, clauses, proofs, ranges, and style and idempotency

test: Split the arithmetic evidence tests by what they test: types and normalization, reasoning, the kernel's authority, and realistic obligations

feat: State a loop invariant's && and || as the conjunction and disjunction of its operands, each specified on its own, as a contract does

refactor: Split the kernel derivation generator by the rules it draws: terms and definitions, structural rules, eliminations and arithmetic

test: Refuse a call to a function with unsafe code made by a default argument a call relies on, which would read the temporary it writes as kept, and break the check that sees it

test: Refuse a struct member rebound out of order, a reference beside a written member, a refined member assigned whole and a converting constructor, and require each refusal to come from its own case

test: Verify and run whole struct values flowing through copies, calls, returns and assignments, and refuse each flow whose claim is false or whose copy runs user code

feat: Pass, return, copy and assign whole struct values in verified bodies, reading a C++-defined memberwise copy as its operand and a struct handed to a reference as the group of members it may write

fix: Refuse a call to a function whose unsafe code may write what it is handed anywhere but as a statement, initializer or assignment of its own, since only there is that write followed

build: Enforce a 1000-line limit on every C++ file with ci_filelength, recording each file over it whose split is pending

test: Refuse a range-based for whose unseen initialization or measured shrinking would otherwise be proven, and drop two range checks no input reaches

test: Verify range-based fors over every modeled range with their erasure, refuse each unmodeled or undefined use by name, and name an aggregate element where a range-based for will not bind it

Breadcrumbs

User selector

Datepicker

Commit history

Commits on Oct 7, 2026

Commits on Oct 6, 2026