From 3eb4c3e80460eee318e423e1eb7bd1dfb8f3b37b Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 22 Oct 2019 10:56:45 -0700 Subject: [PATCH] Update CHANGES.md about fix for #30 --- CHANGES.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/CHANGES.md b/CHANGES.md index b666038282..c78de35986 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -5,7 +5,13 @@ function that neglected to mention an effect that the function in fact caused could be successfully verified. When verifying a caller of that function, only the effects mentioned in the specification would be - used. + used. The fix for this issue may break some proof scripts: any pointer + mentioned using `crucible_points_to` in the initial state of a + specification but not in the final state will be assigned a final + value of "invalid", and any subsequent reads from the pointer will + fail. To fix this issue, make sure that every specification you use + provides a final value for every pointer it touches (which in many + cases will be the same as its initial value). * Added an experimental command, `llvm_boilerplate`, that emits skeleton function specifications for every function defined in an LLVM module.