Skip to content

[CN-Testing] Support C-typed ghost arguments in input generators #530

Open
Feature
Open
[CN-Testing] Support C-typed ghost arguments in input generators#530
Feature
Assignees
ZippeyKeys12
Labels
BennetRelated to input generation via random backtracking search. Available via `cn test`CN spec testingRelated to Bennet, Darcy, or the shared infrastructure for running spec-based random testing.DarcyRelated to input generation via constraint solving. Available via `cn test --symbolic`enhancementNew feature or request

Description

@ZippeyKeys12
ZippeyKeys12
opened on Apr 11, 2026

Support ghost arguments of C types (bitvectors, pointers, and structs).
Doesn't require new primitives, so not too hard to do.

Metadata

Metadata

Assignees

Labels

BennetRelated to input generation via random backtracking search. Available via `cn test`CN spec testingRelated to Bennet, Darcy, or the shared infrastructure for running spec-based random testing.DarcyRelated to input generation via constraint solving. Available via `cn test --symbolic`enhancementNew feature or request

Type

Feature

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions