[claude-experiments] Add verification tests for nullable type operations#60
Open
[claude-experiments] Add verification tests for nullable type operations#60
Conversation
The API declaration file was not regenerated after the addition of InvariantBuilder.triggers() and the @Manual annotation, causing apiCheck to fail on a clean build. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
7 new verification tests covering: - Elvis operator with null input (proves default value is returned) - Elvis operator with non-null input (proves passthrough) - Nullable passthrough (proves identity preservation) - Null literal return (proves result is null) - Null comparison on null value (proves true) - Non-null comparison on null value (proves false) - Smart cast in if-else branch (proves type narrowing) All tests pass Viper verification with z3. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Move tests from nullability_operations.kt into the existing verification/nullability.kt file. Use file-level ALWAYS_VALIDATE instead of per-function @AlwaysVerify to match the existing convention. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Keep only tests that exercise genuinely different mechanisms: - return_null: null literal - nullablePassthrough: nullable parameter identity - elvisWithNonNull: elvis operator passthrough - smartcastInBranch: smart cast after null check Remove redundant tests (returnNullLiteral duplicates return_null, null comparisons are trivial, elvisDefaultOnNull is simpler case of elvis already covered). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
jesyspa
force-pushed
the
botspace/nullability-verification-tests
branch
from
bbdc14a to
5adacfb
Compare
jesyspa
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds verification tests for nullability operations to the existing
verification/nullability.ktfile. Each test exercises a distinct code path:return xwherex: Int?)The existing
return_nulltest (null literal return) is preserved.Context
Part of the design accuracy audit for nullability encoding. These tests verify that the RuntimeTypeDomain-based nullable encoding produces correct results, not just valid Viper.
Test plan
🤖 Generated with Claude Code