Skip to content

Commit 2608484

Browse files
authored
feat: Implement JingleDisplay for SmtValuationState (#157)
1 parent 716b9db commit 2608484

File tree

1 file changed

+18
-0
lines changed
  • jingle/src/analysis/valuation

1 file changed

+18
-0
lines changed

jingle/src/analysis/valuation/smt.rs

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -535,6 +535,24 @@ impl Display for SmtValuationState {
535535
}
536536
}
537537

538+
impl JingleDisplay for SmtValuationState {
539+
fn fmt_jingle(&self, f: &mut Formatter<'_>, info: &SleighArchInfo) -> std::fmt::Result {
540+
// Render the written locations in a concise form using the Sleigh arch display context.
541+
write!(f, "SmtValuationState {{")?;
542+
let mut first = true;
543+
for (vn, val) in self.written_locations.iter() {
544+
if !first {
545+
write!(f, ", ")?;
546+
}
547+
first = false;
548+
// Use the JingleDisplay implementations for VarNode and SmtVal
549+
write!(f, "{} = {}", vn.display(info), val.display(info))?;
550+
}
551+
write!(f, "}}")?;
552+
Ok(())
553+
}
554+
}
555+
538556
pub struct SmtValuationAnalysis {
539557
arch_info: SleighArchInfo,
540558
/// Default merge behavior for states produced by this analysis.

0 commit comments

Comments
 (0)