Clarify influence of slicing on completeness of trace

peterschrammel · peterschrammel · commit 03291918bf81 · 2019-03-10T11:02:08.000Z
Slicing may prevent you from getting a full trace until
the end of __CPROVER_start despite calling build_full_trace.
diff --git a/src/goto-checker/goto_trace_provider.h b/src/goto-checker/goto_trace_provider.h
@@ -23,6 +23,8 @@ class goto_trace_providert
 {
 public:
   /// Builds and returns the complete trace
+  /// \note If slicing is used then the trace will not be complete.
+  ///   E.g. with simple-slice it will end at the last assertion.
   virtual goto_tracet build_full_trace() const = 0;
 
   /// Builds and returns the trace up to the first failed property

Original file line number	Diff line number	Diff line change
`@@ -23,6 +23,8 @@ class goto_trace_providert`
`23`	`23`	`{`
`24`	`24`	`public:`
`25`	`25`	`/// Builds and returns the complete trace`
	`26`	`+ /// \note If slicing is used then the trace will not be complete.`
	`27`	`+ /// E.g. with simple-slice it will end at the last assertion.`
`26`	`28`	`virtual goto_tracet build_full_trace() const = 0;`
`27`	`29`
`28`	`30`	`/// Builds and returns the trace up to the first failed property`