@@ -195,6 +195,8 @@ where
195
195
// C: Entry state
196
196
self.bg = Background::Light;
197
197
self.results.seek_to_block_start(block);
198
+ let block_entry_state = self.results.get().clone();
199
+
198
200
self.write_row_with_full_state(w, "", "(on entry)")?;
199
201
200
202
// D: Statement transfer functions
@@ -213,29 +215,42 @@ where
213
215
self.write_row_for_location(w, "T", &terminator_str, terminator_loc)?;
214
216
215
217
// F: Exit state
218
+
219
+ // Write the full dataflow state immediately after the terminator if it differs from the
220
+ // state at block entry.
216
221
self.results.seek_after(terminator_loc);
217
- if let mir::TerminatorKind::Call { destination: Some(_), .. } = &terminator.kind {
218
- self.write_row_with_full_state(w, "", "(on unwind)")?;
219
-
220
- let num_state_columns = self.num_state_columns();
221
- self.write_row(w, "", "(on successful return)", |this, w, fmt| {
222
- write!(
223
- w,
224
- r#"<td balign="left" colspan="{colspan}" {fmt} align="left">"#,
225
- colspan = num_state_columns,
226
- fmt = fmt,
227
- )?;
228
-
229
- let state_on_unwind = this.results.get().clone();
230
- this.results.seek_after_assume_call_returns(terminator_loc);
231
- write_diff(w, this.results.analysis(), &state_on_unwind, this.results.get())?;
232
-
233
- write!(w, "</td>")
234
- })?;
235
- } else {
236
- self.write_row_with_full_state(w, "", "(on exit)")?;
222
+ if self.results.get() != &block_entry_state {
223
+ let after_terminator_name = match terminator.kind {
224
+ mir::TerminatorKind::Call { destination: Some(_), .. } => "(on unwind)",
225
+ _ => "(on exit)",
226
+ };
227
+
228
+ self.write_row_with_full_state(w, "", after_terminator_name)?;
237
229
}
238
230
231
+ // Write any changes caused by terminator-specific effects
232
+ match terminator.kind {
233
+ mir::TerminatorKind::Call { destination: Some(_), .. } => {
234
+ let num_state_columns = self.num_state_columns();
235
+ self.write_row(w, "", "(on successful return)", |this, w, fmt| {
236
+ write!(
237
+ w,
238
+ r#"<td balign="left" colspan="{colspan}" {fmt} align="left">"#,
239
+ colspan = num_state_columns,
240
+ fmt = fmt,
241
+ )?;
242
+
243
+ let state_on_unwind = this.results.get().clone();
244
+ this.results.seek_after_assume_call_returns(terminator_loc);
245
+ write_diff(w, this.results.analysis(), &state_on_unwind, this.results.get())?;
246
+
247
+ write!(w, "</td>")
248
+ })?;
249
+ }
250
+
251
+ _ => {}
252
+ };
253
+
239
254
write!(w, "</table>")
240
255
}
241
256
0 commit comments