Skip to content

Update concrete values parser to use serde structs #1477

@sanjit-bhat

Description

@sanjit-bhat

The current deterministic values parser in kani-driver/src/exe_trace.rs works on arbitrary serde::Value types. This means that if we expect certain Value blobs to be arrays, we have to test for that and handle errors. With this change, we would complete the serde struct for traces in kani-driver/src/cbmc_output_parser.rs and use those objects directly. We would still have to walk down this structure to extract deterministic values, but we wouldn't need as much error handling since the blob would be automatically serialized into the right type.

Metadata

Metadata

Labels

No labels
No labels

Type

No type

Projects

Relationships

None yet

Development

No branches or pull requests

Issue actions