Skip to content

Fix typo#2

Merged
buger merged 1 commit intobuger:masterfrom
adrianblynch:patch-1
Mar 21, 2016
Merged

Fix typo#2
buger merged 1 commit intobuger:masterfrom
adrianblynch:patch-1

Conversation

@adrianblynch
Copy link
Copy Markdown

No description provided.

buger added a commit that referenced this pull request Mar 21, 2016
@buger buger merged commit d1e4798 into buger:master Mar 21, 2016
@buger
Copy link
Copy Markdown
Owner

buger commented Mar 21, 2016

Thank you!

buger added a commit that referenced this pull request May 3, 2026
Re-sweep after reqproof translator fixes shipped on
feat/translator-gap-fixes (HEAD 02a8cb94): char literals (Fix #3),
type conversions (Fix #4), package-level const references (Fix #6),
multi-lemma per host (Fix #7).

Coverage went from 18/18 (100%) to 25/25 (100%). Lemma corpus 11 -> 23
(9 -> 21 PROVED via cached path; 22 PROVED + 1 expected COUNTEREXAMPLE
via fresh-translation --coverage path).

- 4 new lemmas via Fix #3 (char literals): h2I_decimal_digit,
  h2I_uppercase_hex, h2I_lowercase_hex, h2I_nondigit_is_badhex.
  All exercise '0'..'9' / 'A'..'F' / 'a'..'f' on h2I.
- Fix #4 (type conversions) is on the same h2I host — its body uses
  int(c-48) etc., which previously made the host untranslatable.
  Without Fix #4 the four char-literal lemmas above would translation-
  error on the host.
- 3 new lemmas via Fix #6 (package consts): h2I_nondigit_is_badhex
  (uses const badHex), isUTF16EncodedRune_const_high_bound (uses const
  highSurrogateOffset), isUTF16EncodedRune_const_bmp_bound (uses const
  basicMultilingualPlaneReservedOffset).
- 6 additional :lemma directives on existing hosts via Fix #7
  (multi-lemma per host): tokenEnd_nonneg, tokenEnd_empty_zero,
  tokenStart_nonneg, tokenStart_empty_zero, nextToken_signed_disjoint,
  lastToken_signed_disjoint. Pre-fix the scanner dropped any second
  :lemma on a host silently.

Tried-and-rejected (still blocked by other deferred translator gaps):
- combineUTF16Surrogates: Fix #6 resolves the package-const refs in
  the body, but `<<` shift op is unsupported (separate gap, not
  one of #1/#2/#5).
- findTokenStart: still blocked by #1 (early-return / __early_val
  scoping bug in switch + return body shape).
- unescapeToUTF8: still blocked by #2 (switch).

No new production bugs surfaced. The single COUNTEREXAMPLE
(deleteCleanupBuggy_prevTok_nonneg_falsifiable) is the existing
documented OSS-Fuzz Delete demo from a6c5ed3 — counterexample
prevTok=-1, remainedTok=0 matches the documented falsifying witness.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants