link to compcert

[web.git] / ralf / _posts / 2017-07-17-types-as-contracts.md

diff --git a/ralf/_posts/2017-07-17-types-as-contracts.md b/ralf/_posts/2017-07-17-types-as-contracts.md
index bb867e78bcd9060690bafd94b568d903a397ce3a..d7b1b71a54c6dfbdc236bb1a5bf7fe2978f002ce 100644 (file)
--- a/ralf/_posts/2017-07-17-types-as-contracts.md
+++ b/ralf/_posts/2017-07-17-types-as-contracts.md
@@ -305,7 +305,7 @@ This grants the functions write access to memory that we are explicitly passing
 Suspend validation occurs before taking a reference, using the lifetime of the new reference.
 This encodes the fact that when the lifetime ends (and hence the lock is being reacquired), we are the exclusive owner of this memory again.
 
-**Update**: It has been pointed out to me that another way for values to flow back into a function is through mutable references. Good catch! I will need to extend the validation machinery to also perform acquire validation when a write lock is reacquired. **/Update**
+**Update:** It has been pointed out to me that another way for values to flow back into a function is through mutable references. Good catch! I will need to extend the validation machinery to also perform acquire validation when a write lock is reacquired. **/Update**
 
 To summarize, validation statements are emitted during MIR construction in the following places:
 - At the beginning of the function, we perform acquire validation of the arguments.