From a7b2b63cb15bebc218cfc9f6ca255d7ac42ef9e6 Mon Sep 17 00:00:00 2001 From: Canitas Date: Fri, 30 Oct 2026 15:40:44 -0700 Subject: [PATCH] fix: fail on //@ annotations that lsc does not read A //@ comment that lsc didn't read was dropped without a word, so a false postcondition that was misspelled or misplaced passed with "0 verified, 0 errors" (#238). Extraction now records where each contract annotation's value is used and ends with one check over the file's comments: a malformed or unknown //@ comment, or a contract annotation that nothing used, is an error naming the file, line and text. Declarations left out on purpose (unselected, extern or skip) are exempt from the placement check, and TypeScript's //@ts- comments are left alone. Option lines are recognized by config's own grammar. Four example lines that were never read are removed; the generated Dafny and Lean files are unchanged. --- SPEC.md | 2 + examples/nullableArray.ts | 2 - examples/readonlyArray.ts | 1 - examples/toposort.ts | 1 - tools/src/config.ts | 43 +++++--- tools/src/extract.ts | 137 +++++++++++++++++++------ tools/tests/unread-annotations.test.ts | 57 ++++++++++ 7 files changed, 190 insertions(+), 53 deletions(-) create mode 100644 tools/tests/unread-annotations.test.ts diff --git a/SPEC.md b/SPEC.md index e800a8d5..564178ee 100644 --- a/SPEC.md +++ b/SPEC.md @@ -51,6 +51,8 @@ Annotations are TypeScript comments of the form `//@ `. | `autohavoc` | File-level, or before a `//@ verify` function | Abstract every unmodellable expression to a nondeterministic value, so verification rests only on declared contracts (see §2.12). Dafny only. | | `skip` | Before a statement or top-level value declaration | Omit it from the verification model (for side-effect-only code or an intentionally unsupported declaration). | +`lsc` rejects a `//@` comment it does not read: a malformed one, an unknown keyword, or a `requires`, `ensures`, `contract`, `invariant`, `decreases`, `done_with` or `type` placed where nothing takes it. Placement is not checked inside declarations left out on purpose (unselected, `extern` or `skip`), and TypeScript's own `//@ts-…` comments are left alone. + ### 2.2 Spec Expression Grammar At top level, `//@ skip` may precede a function, class, or `const` declaration; diff --git a/examples/nullableArray.ts b/examples/nullableArray.ts index 0e0c6395..161da26b 100644 --- a/examples/nullableArray.ts +++ b/examples/nullableArray.ts @@ -67,7 +67,6 @@ export function dropOrphans(messages: Message[]): Message[] { let i = 0; while (i < messages.length) { - //@ type i nat //@ invariant i <= messages.length //@ invariant filteredContents.length === messages.length const cur = filteredContents[i]; @@ -80,7 +79,6 @@ export function dropOrphans(messages: Message[]): Message[] { const result: Message[] = []; let j = 0; while (j < messages.length) { - //@ type j nat //@ invariant j <= messages.length //@ invariant result.length <= j const f = filteredContents[j]; diff --git a/examples/readonlyArray.ts b/examples/readonlyArray.ts index bf339a56..395d47e2 100644 --- a/examples/readonlyArray.ts +++ b/examples/readonlyArray.ts @@ -14,6 +14,5 @@ export function firstOrZero(xs: readonly number[]): number { export function lengthOf(xs: ReadonlyArray): number { //@ ensures \result === xs.length - //@ type T return xs.length; } diff --git a/examples/toposort.ts b/examples/toposort.ts index 32916e47..c65078e5 100644 --- a/examples/toposort.ts +++ b/examples/toposort.ts @@ -72,7 +72,6 @@ export function topologicalSort( let sorted: string[] = []; let qHead = 0; while (qHead < queue.length) { - //@ type qHead nat //@ invariant qHead <= queue.length //@ invariant sorted.length === qHead //@ invariant sorted.length <= nodeIds.length diff --git a/tools/src/config.ts b/tools/src/config.ts index c76da256..85270943 100644 --- a/tools/src/config.ts +++ b/tools/src/config.ts @@ -130,13 +130,14 @@ function parseDirectiveValue(key: keyof OptionSpecs, text: string, source: strin } /** - * Find comment lines, marking those that occur before any code. + * Find comment lines and the comment on each, marking those that occur before + * any code. * * Use the parsed syntax tree to skip strings, regexes, and template text. * Without those boundaries, the scanner can read /[/*]/ as a block comment * or treat a template's closing backtick as the start of another template. */ -function* fileCommentLines(sourceText: string): Generator<{ text: string; index: number; inLeadingRegion: boolean }> { +export function* fileCommentLines(sourceText: string): Generator<{ text: string; comment: string; index: number; inLeadingRegion: boolean }> { // Normalize once so a leading BOM also works before a shebang. sourceText = sourceText.replace(/^\uFEFF/, ""); const lines = sourceText.split(/\r\n|[\n\r\u2028\u2029]/); @@ -163,8 +164,9 @@ function* fileCommentLines(sourceText: string): Generator<{ text: string; index: if (token === ts.SyntaxKind.SingleLineCommentTrivia || token === ts.SyntaxKind.MultiLineCommentTrivia) { const firstLine = sourceFile.getLineAndCharacterOfPosition(scanner.getTokenStart()).line; const lastLine = sourceFile.getLineAndCharacterOfPosition(scanner.getTokenEnd() - 1).line; + const comment = scanner.getTokenText(); for (let index = firstLine; index <= lastLine; index++) { - yield { text: lines[index], index, inLeadingRegion }; + yield { text: lines[index], comment, index, inLeadingRegion }; } } else if (token !== ts.SyntaxKind.WhitespaceTrivia && token !== ts.SyntaxKind.NewLineTrivia && token !== ts.SyntaxKind.ShebangTrivia) { @@ -175,6 +177,22 @@ function* fileCommentLines(sourceText: string): Generator<{ text: string; index: } } +const OPTION_DIRECTIVE = /^[ \t]*\/\/@[ \t]+option(?:[ \t]+(.*?))?[ \t]*$/; +const ALIAS_DIRECTIVE = /^[ \t]*\/\/@[ \t]+([A-Za-z][A-Za-z0-9-]*)[ \t]*$/; + +/** The option a legacy alias such as `//@ safe-slice` sets, if `line` is one. */ +function aliasedOption(line: string): keyof OptionSpecs | undefined { + const alias = line.match(ALIAS_DIRECTIVE)?.[1]; + if (alias === undefined) return undefined; + return KNOWN_KEYS.find(key => "directiveAliases" in OPTION_SPECS[key] && + (OPTION_SPECS[key].directiveAliases as readonly string[]).includes(alias)); +} + +/** Whether `parseFileOptions` reads `line` as an option directive or a legacy alias. */ +export function isOptionDirective(line: string): boolean { + return OPTION_DIRECTIVE.test(line) || aliasedOption(line) !== undefined; +} + /** Parse top-of-file `//@ option key value` directives and legacy aliases. */ export function parseFileOptions(sourceText: string, source: string): ExplicitOptions { const seen = new Map(); @@ -191,7 +209,7 @@ export function parseFileOptions(sourceText: string, source: string): ExplicitOp const parseLine = (lineText: string, index: number, inLeadingRegion: boolean): void => { const line = index + 1; - const optionMatch = lineText.match(/^[ \t]*\/\/@[ \t]+option(?:[ \t]+(.*?))?[ \t]*$/); + const optionMatch = lineText.match(OPTION_DIRECTIVE); if (optionMatch) { if (!inLeadingRegion) fail(`${source}:${line}`, "//@ option directives must appear before the first source statement"); const parts = (optionMatch[1] ?? "").trim().split(/\s+/).filter(Boolean); @@ -206,19 +224,10 @@ export function parseFileOptions(sourceText: string, source: string): ExplicitOp return; } - const aliasMatch = lineText.match(/^[ \t]*\/\/@[ \t]+([A-Za-z][A-Za-z0-9-]*)[ \t]*$/); - if (!aliasMatch) return; - const alias = aliasMatch[1]; - for (const key of KNOWN_KEYS) { - const aliases = "directiveAliases" in OPTION_SPECS[key] - ? OPTION_SPECS[key].directiveAliases as readonly string[] - : []; - if (!aliases.includes(alias)) continue; - // Legacy aliases retain their pre-config placement behavior. New generic - // option directives are deliberately restricted to the file preamble. - setOption(key, true as LscOptions[typeof key], line); - return; - } + // Legacy aliases retain their pre-config placement behavior. New generic + // option directives are deliberately restricted to the file preamble. + const key = aliasedOption(lineText); + if (key) setOption(key, true as LscOptions[typeof key], line); }; for (const { text, index, inLeadingRegion } of fileCommentLines(sourceText)) { diff --git a/tools/src/extract.ts b/tools/src/extract.ts index 795cd28c..341cc599 100644 --- a/tools/src/extract.ts +++ b/tools/src/extract.ts @@ -11,7 +11,7 @@ import { initTypeParser } from "./types.js"; import type { RawExpr, RawStmt, RawFunction, RawModule, RawClass, RawConst, RawGhostLet, RawGhostAssign } from "./rawir.js"; import { normalizeBigIntLiteral } from "./rawir.js"; import { setUserNames, freshName } from "./names.js"; -import { DEFAULT_OPTIONS, type LscOptions } from "./config.js"; +import { DEFAULT_OPTIONS, fileCommentLines, isOptionDirective, type LscOptions } from "./config.js"; // ── Expression extraction ──────────────────────────────────── @@ -737,24 +737,82 @@ function extractExpr(node: Expression): RawExpr { const PREFIX = "//@ "; const KEYWORDS = ["requires", "ensures", "contract", "invariant", "decreases", "done_with", "type"] as const; +/** The other directives (SPEC §2.1) besides options, read by keyword elsewhere. */ +const DIRECTIVES = ["verify", "pure", "impure", "skip", "extern", "havoc", "autohavoc", "assert", "assume", + "ghost", "declare-type", "backend", "lean-module"]; export type AnnotKind = (typeof KEYWORDS)[number]; -interface Annotation { kind: AnnotKind; expr: string } +/** `line` is set only for annotations in the file being extracted. */ +interface Annotation { kind: AnnotKind; expr: string; line?: number } + +function parseAnnotation(text: string): Annotation | null { + if (!text.startsWith(PREFIX)) return null; + const content = text.slice(PREFIX.length); + const sp = content.indexOf(" "); + if (sp === -1) return null; + const kw = content.slice(0, sp); + if (!(KEYWORDS as readonly string[]).includes(kw)) return null; + return { kind: kw as AnnotKind, expr: content.slice(sp + 1).trim() }; +} function parseAnnotations(node: Node): Annotation[] { const result: Annotation[] = []; for (const range of node.getLeadingCommentRanges()) { - const text = range.getText().trim(); - if (!text.startsWith(PREFIX)) continue; - const content = text.slice(PREFIX.length); - const sp = content.indexOf(" "); - if (sp === -1) continue; - const kw = content.slice(0, sp); - if (!(KEYWORDS as readonly string[]).includes(kw)) continue; - result.push({ kind: kw as AnnotKind, expr: content.slice(sp + 1).trim() }); + const a = parseAnnotation(range.getText().trim()); + if (!a) continue; + a.line = currentFileLine(node, range.getPos()); + result.push(a); } return result; } +/** The line of `pos` in `node`'s file, when that is the file being extracted. */ +function currentFileLine(node: Node, pos: number): number | undefined { + const sourceFile = node.getSourceFile(); + return sourceFile === _currentSourceFile ? sourceFile.getLineAndColumnAtPos(pos).line : undefined; +} + +/** Lines of the annotations whose value reached the Raw IR. */ +const _readLines = new Set(); +/** Line spans the extractor leaves out on purpose: `//@ skip`, unselected and extern functions. */ +const _skippedSpans: [number, number][] = []; + +/** The annotation's expression, recording that it was read. */ +function readExpr(a: Annotation): string { + if (a.line !== undefined) _readLines.add(a.line); + return a.expr; +} +function annotExprs(annots: Annotation[], kind: AnnotKind): string[] { + return annots.filter(a => a.kind === kind).map(readExpr); +} +/** Only the first is read; a repeated one is reported as unread. */ +function firstAnnotExpr(annots: Annotation[], kind: AnnotKind): string | null { + const a = annots.find(a => a.kind === kind); + return a ? readExpr(a) : null; +} +function skipSpan(node: Node): void { + const first = node.getLeadingCommentRanges()[0]; + const from = first ? node.getSourceFile().getLineAndColumnAtPos(first.getPos()).line : node.getStartLineNumber(); + _skippedSpans.push([from, node.getEndLineNumber()]); +} + +/** Fail on `//@` comments lsc ignores: a malformed or unknown one, or a + * contract annotation where no reader looks. Other directives are checked + * by keyword only. TypeScript's `//@ts-…` comments are not ours. */ +function checkAnnotationsRead(sourceFile: SourceFile): void { + const errors: string[] = []; + for (const { comment, index } of fileCommentLines(sourceFile.getFullText())) { + const text = comment.trim(); + if (!text.startsWith("//@") || text.startsWith("//@ts-")) continue; + const line = index + 1; + const keyword = text.match(/^\/\/@ (\S+)(?: |$)/)?.[1]; + const read = parseAnnotation(text) + ? _readLines.has(line) || _skippedSpans.some(([from, to]) => from <= line && line <= to) + : DIRECTIVES.includes(keyword ?? "") || isOptionDirective(text); + if (!read) errors.push(`${sourceFile.getBaseName()}:${line}: lsc does not read this annotation: ${text}`); + } + if (errors.length > 0) throw new Error(errors.join("\n")); +} + function collectAnnotations(node: Node, body?: Node[]): Annotation[] { const own = parseAnnotations(node); if (body && body.length > 0) return [...own, ...parseAnnotations(body[0])]; @@ -881,8 +939,8 @@ function extractTypeDecl(decl: TypeAliasDeclaration, extraDecls?: TypeDeclInfo[] // Leading `//@ type ` overrides extraction — the declared TS type is // replaced by the annotated backend type. Used to coerce literal unions // (`5 | 15 | 30` → `nat`) and other types LS can't model precisely. - const override = parseAnnotations(decl).find(a => a.kind === "type"); - if (override) return { name, typeParams: tpField, kind: "alias", aliasOf: override.expr }; + const override = firstAnnotExpr(parseAnnotations(decl), "type"); + if (override) return { name, typeParams: tpField, kind: "alias", aliasOf: override }; if (type.isUnion()) { const members = type.getUnionTypes(); @@ -979,7 +1037,9 @@ function extractInterface(decl: InterfaceDeclaration, extraDecls?: TypeDeclInfo[ if (Node.isPropertySignature(member)) { const text = member.getTrailingCommentRanges().map(r => r.getText()).join(" "); const match = text.match(/\/\/@ type (\w+)/); - if (match) overrides.set(member.getName(), match[1]); + if (match) { + overrides.set(member.getName(), readExpr({ kind: "type", expr: match[1], line: currentFileLine(member, member.getEnd()) })); + } } } return extractRecord(decl.getName(), decl.getType(), decl, overrides, extraDecls); @@ -1400,6 +1460,7 @@ function extractStmts(stmts: Node[]): RawStmt[] { // //@ skip — omit this statement from the verification model if (leadingComments.some(r => r.getText().trim() === "//@ skip")) { + skipSpan(s); continue; } @@ -1606,9 +1667,9 @@ function extractStmts(stmts: Node[]): RawStmt[] { result.push({ kind: "while", cond: extractExpr(s.getExpression()), - invariants: annots.filter(a => a.kind === "invariant").map(a => a.expr), - decreases: annots.find(a => a.kind === "decreases")?.expr ?? null, - doneWith: annots.find(a => a.kind === "done_with")?.expr ?? null, + invariants: annotExprs(annots, "invariant"), + decreases: firstAnnotExpr(annots, "decreases"), + doneWith: firstAnnotExpr(annots, "done_with"), body: extractStmts(bodyStmts), line, }); @@ -1656,8 +1717,8 @@ function extractStmts(stmts: Node[]): RawStmt[] { kind: "forof", names, iterable: extractExpr(iterableExpr), - invariants: annots.filter(a => a.kind === "invariant").map(a => a.expr), - doneWith: annots.find(a => a.kind === "done_with")?.expr ?? null, + invariants: annotExprs(annots, "invariant"), + doneWith: firstAnnotExpr(annots, "done_with"), body: extractStmts(bodyStmts), line, }); @@ -1717,9 +1778,9 @@ function extractStmts(stmts: Node[]): RawStmt[] { } let condExpr: RawExpr = cond ? extractExpr(cond) : { kind: "bool", value: true }; - let invariants = annots.filter(a => a.kind === "invariant").map(a => a.expr); - let decreases = annots.find(a => a.kind === "decreases")?.expr ?? null; - let doneWith = annots.find(a => a.kind === "done_with")?.expr ?? null; + let invariants = annotExprs(annots, "invariant"); + let decreases = firstAnnotExpr(annots, "decreases"); + let doneWith = firstAnnotExpr(annots, "done_with"); for (const [from, to] of renames) { for (let k = 0; k < hoisted.length; k++) hoisted[k] = renameRawStmt(hoisted[k], from, to); condExpr = renameRawExpr(condExpr, from, to); @@ -1756,8 +1817,8 @@ function extractStmts(stmts: Node[]): RawStmt[] { kind: "forof", names: [name], iterable: extractExpr(s.getExpression()), - invariants: annots.filter(a => a.kind === "invariant").map(a => a.expr), - doneWith: annots.find(a => a.kind === "done_with")?.expr ?? null, + invariants: annotExprs(annots, "invariant"), + doneWith: firstAnnotExpr(annots, "done_with"), body: extractStmts(bodyStmts), line, }); @@ -1976,7 +2037,9 @@ function extractFunctionInner(fn: FunctionDeclaration, parentAnnotations?: Annot for (const a of annots) { if (a.kind === "type") { const parts = a.expr.split(/\s+/); - if (parts.length === 2) typeAnnotations.push({ name: parts[0], type: parts[1] }); + if (parts.length !== 2) continue; + readExpr(a); + typeAnnotations.push({ name: parts[0], type: parts[1] }); } } @@ -2065,10 +2128,10 @@ function extractFunctionInner(fn: FunctionDeclaration, parentAnnotations?: Annot if (inferred.isAny()) return "unknown"; return _eraseGenerics(typeToString(inferred)); })(), - requires: annots.filter(a => a.kind === "requires").map(a => a.expr), - ensures: annots.filter(a => a.kind === "ensures").map(a => a.expr), - contract: annots.filter(a => a.kind === "contract").map(a => a.expr), - decreases: annots.find(a => a.kind === "decreases")?.expr ?? null, + requires: annotExprs(annots, "requires"), + ensures: annotExprs(annots, "ensures"), + contract: annotExprs(annots, "contract"), + decreases: firstAnnotExpr(annots, "decreases"), pure: hasPureAnnotation(fn, body && Node.isBlock(body) ? body.getStatements() as Node[] : undefined), autohavoc: false, // set in extractModule (file-level directive or per-function) typeAnnotations, @@ -2094,6 +2157,8 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA // here), deduped by qualified name. _externs.clear(); _externSigTypes.length = 0; + _readLines.clear(); + _skippedSpans.length = 0; // Match a `//@ ` directive only as the first non-whitespace on a line, // so prose mentioning an annotation does not activate it. @@ -2204,7 +2269,7 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA const constants: RawConst[] = []; for (const stmt of sourceFile.getStatements()) { if (Node.isVariableStatement(stmt)) { - if (hasLeadingDirective(stmt, "skip")) continue; + if (hasLeadingDirective(stmt, "skip")) { skipSpan(stmt); continue; } for (const decl of stmt.getDeclarationList().getDeclarations()) { if (stmt.getDeclarationList().getFlags() & 2 /* const */) { const init = decl.getInitializer(); @@ -2361,6 +2426,12 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA ); const hasVerifyDirective = nonExternFns.some(hasVerify) || hasVerifiedClassMethod; const fnsToExtract = hasVerifyDirective ? nonExternFns.filter(hasVerify) : nonExternFns; + // A statement holding a selected function keeps its comments checked. + for (const f of allFns) { + if (fnsToExtract.includes(f)) continue; + const wholeStmt = f.parentStmt && !fnsToExtract.some(s => s.parentStmt === f.parentStmt); + skipSpan(wholeStmt ? f.parentStmt! : f.node); + } // `//@ autohavoc` — enable the auto-havoc abstraction (see autohavoc.ts). // File-level: a directive at column 0 (top of file) enables it for every @@ -2739,11 +2810,11 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA // Extract classes with //@ verify methods const classes: RawClass[] = []; for (const cls of sourceFile.getClasses()) { - if (hasLeadingDirective(cls, "skip")) continue; + if (hasLeadingDirective(cls, "skip")) { skipSpan(cls); continue; } const methods: RawFunction[] = []; for (const method of cls.getMethods()) { - if (hasLeadingDirective(method, "skip")) continue; - if (!method.getFullText().includes('//@ verify')) continue; + if (hasLeadingDirective(method, "skip")) { skipSpan(method); continue; } + if (!method.getFullText().includes('//@ verify')) { skipSpan(method); continue; } methods.push(extractFunction(method as any)); } if (methods.length === 0) continue; @@ -2758,6 +2829,8 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA // union stringification outside of an extractModule call. _synthArrayUnions = null; + checkAnnotationsRead(sourceFile); + return { file: sourceFile.getFilePath(), typeDecls, diff --git a/tools/tests/unread-annotations.test.ts b/tools/tests/unread-annotations.test.ts new file mode 100644 index 00000000..4b97479e --- /dev/null +++ b/tools/tests/unread-annotations.test.ts @@ -0,0 +1,57 @@ +import { test } from "node:test"; +import assert from "node:assert/strict"; +import { Project, ScriptTarget } from "ts-morph"; +import { extractModule } from "../src/extract.ts"; + +function extract(text: string) { + const project = new Project({ compilerOptions: { strict: true, + target: ScriptTarget.ESNext, lib: ["lib.esnext.d.ts"], types: [], skipLibCheck: true } }); + return extractModule(project.createSourceFile("f.ts", text)); +} + +const inBody = (annotation: string) => + `export function f(x: number): number {\n ${annotation}\n return x;\n}\n`; +const g = "export function g(x: number): number {\n //@ verify\n return x;\n}\n"; + +for (const [name, text, line] of [ + ["a missing space", inBody(String.raw`//@ensures \result > x`), 2], + ["extra spaces", inBody(String.raw`//@ ensures \result > x`), 2], + ["a tab after the keyword", inBody(String.raw`//@ ensures` + "\t" + String.raw`\result > x`), 2], + ["a missing expression", inBody("//@ ensures"), 2], + ["a misspelled keyword", inBody(String.raw`//@ ensure \result > x`), 2], + ["a block-body arrow", String.raw`//@ ensures \result > x` + "\nexport const f = (x: number): number => { return x; };\n", 1], + ["a statement before the function", String.raw`//@ ensures \result > x` + "\nconst unrelated = 1;\n" + inBody(""), 1], + ["a loop body requires", "export function f(n: number): number {\n let i = 0;\n while (i < n) {\n" + + " //@ invariant i <= n\n //@ requires false\n i = i + 1;\n }\n return i;\n}\n", 5], + ["a second decreases", "export function f(n: number): number {\n //@ decreases n\n //@ decreases n + 1\n" + + " return n <= 0 ? 0 : f(n - 1);\n}\n", 3], + ["a misspelled verify outside the selected functions", g + inBody("//@verify"), 6], + ["a tab after a directive", inBody("//@ assert\tfalse"), 2], + ["a selected arrow beside an unselected one", "export const a = (x: number): number => x,\n" + + " b = (x: number): number => {\n //@ verify\n const y = x;\n //@ ensures false\n return y;\n };\n", 5], +] as const) { + test(`an unread annotation with ${name} fails extraction`, () => { + assert.throws(() => extract(text), new RegExp(`^Error: f\\.ts:${line}: lsc does not read this annotation`)); + }); +} + +for (const [name, text] of [ + ["a contract above a function", String.raw`//@ ensures \result > x` + "\nexport function f(x: number): number {\n return x;\n}\n"], + ["a contract above an expression-body arrow", String.raw`//@ ensures \result > x` + "\nexport const f = (x: number): number => x;\n"], +] as const) { + test(`${name} is read`, () => { + assert.deepEqual(extract(text).functions[0].ensures, [String.raw`\result > x`]); + }); +} + +for (const [name, text] of [ + ["a contract in a function outside the selected ones", g + inBody(String.raw`//@ ensures \result > x`)], + ["a skipped statement", "export function f(n: number): number {\n //@ skip\n while (n > 0) {\n //@ requires false\n n = n - 1;\n }\n return n;\n}\n"], + ["a TypeScript directive", inBody("//@ts-ignore")], + ["an option with extra spaces", "//@ option safe-slice true\n" + inBody("")], + ["an option alias after a tab", "//@\tsafe-slice\n" + inBody("")], +] as const) { + test(`${name} still extracts`, () => { + assert.doesNotThrow(() => extract(text)); + }); +}