fix issue 3787

carolynzech · Feb 13, 2025 · 3e33eea · 3e33eea
1 parent 475ea5e
commit 3e33eea
Show file tree

Hide file tree

Showing 2 changed files with 349 additions and 84 deletions.
diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs
@@ -296,12 +296,20 @@ pub struct TraceItem {
 /// Struct that represents a trace value.
 ///
 /// Note: this struct can have a lot of different fields depending on the value type.
-/// The fields included right now are relevant to primitive types.
+/// The fields included right now are relevant to primitive types and arrays.
 #[derive(Clone, Debug, Deserialize)]
 pub struct TraceValue {
     pub binary: Option<String>,
     pub data: Option<TraceData>,
     pub width: Option<u32>,
+    // Invariant: elements is Some iff binary, data, and width are None.
+    pub elements: Option<Vec<TraceArrayValue>>,
+}
+
+/// Struct that represents an element of an array in a trace.
+#[derive(Clone, Debug, Deserialize)]
+pub struct TraceArrayValue {
+    pub value: TraceValue,
 }
 
 /// Enum that represents a trace data item.