More faithful semantics for volatile reads and writes.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1346 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 7 insertions, 0 deletions

diff --git a/Changelog b/Changelog
index 81b2ff1..7a49998 100644
--- a/Changelog
+++ b/Changelog
@@ -1,6 +1,13 @@
 Release 1.8
 ===========
 
+- More faithful semantics for volatile accesses: 
+  . volatile reads and writes from a volatile global variable are treated
+    like input and output system calls (respectively), bypassing
+    the memory model entirely;
+  . volatile reads and writes from other locations are treated like
+    regular loads and stores.
+
 - Added "fabs" (floating-point absolute value) unary operator to Clight;
   map __builtin_fabs() to this operator.