You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
sanjit-bhat
changed the title
Update det vals parser once new overall CBMC output parser is merged in
Det playback: Update det vals parser to use serde structs
Aug 11, 2022
sanjit-bhat
changed the title
Det playback: Update det vals parser to use serde structs
Update concrete values parser to use serde structs
Aug 19, 2022
The current deterministic values parser in
kani-driver/src/exe_trace.rs
works on arbitraryserde::Value
types. This means that if we expect certainValue
blobs to be arrays, we have to test for that and handle errors. With this change, we would complete the serde struct for traces inkani-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.The text was updated successfully, but these errors were encountered: