Skip to content

vera test: ADT parameter input generation #440

@aallan

Description

@aallan

Currently vera test skips functions with ADT parameters (e.g. @Color, @Option<Int>) because the Z3 input generation pipeline only supports primitive types. String and Float64 are being added in #169, but ADTs require constructor synthesis — generating a valid Color means picking one of Red, Green, Blue and synthesising the right WASM value.

Scope: Extend the test runner to generate inputs for simple ADTs (enums with no fields, and ADTs whose constructor fields are all in _Z3_SUPPORTED). Complex cases (ADTs with recursive fields, generic ADTs) may remain out of scope.

Depends on: #169 (String/Float64 support, which establishes the heterogeneous-input infrastructure)

SKIPPED (cannot generate Color inputs)   ← current
TESTED  (5/5 passed)                     ← goal

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions