Documentation fixes for checkedc issues #451 and #437. (#468)

CONTRIBUTING.md

@@ -3,8 +3,8 @@
 We welcome contributions to the Checked C Project.  Contributions can take many forms depending
 on your level of interest:
 
-* Participating in [mailing lists](https://github.com/Microsoft/CheckedC/blob/master/MAILING-LISTS.md) and discussions
-  of proposed changes to the specification.
+* Participating in [discussions](https://github.com/microsoft/checkedc/discussions)
+  on the specification and reviewing proposed changes to it.
 * Helping out with the [Checked C clang compiler implementation](https://github.com/Microsoft/checkedc-clang). We could
  particularly use code reviewers for compiler changes.  There are also a number of self-contained small features that 
  you could implement.

MAILING-LISTS.md

@@ -1,48 +0,0 @@
-# Mailing Lists
-
-There are two mailing lists for the Checked C project:
-
-* checkedc-announce: this is a low-traffic mailing list for announcements about the
-project, such as the availability of new versions of specifications  and  implementations.
-* checkedc-discussion: this is for discussing the design and
-implementation of Checked C and for questions about Checked C.  Weekly status
-updates are sent to this list.
-
-The email lists are open to anyone involved in the project.  They are not confidential, so
-please do not include confidential or proprietary information in emails sent to the lists.
-
-## Joining
-
-To join the mailing lists, send an email to listserv@lists.research.microsoft.com with a 
-message body containing the word SUBSCRIBE followed by the name of the mailing list
-(either CHECKEDC-ANNOUNCE or CHECKEDC-DISCUSSION).
-
-To leave a mailing list, send an email to listserv@lists.research.microsoft.com with a 
-message body containing the word UNSUBSCRIBE followed by the name of the mailing list.
-
-## Using the lists
-
-To email a list, send email to NAME@lists.research.microsoft.com, where NAME is either
-checkedc-announce or checkedc-discussion.
-
-These email lists are for anyone involved in or interested in the Checked C project.
-For specific issues about a specification or implementation, you can open an issue using 
-the Github issue tracking system.  If in doubt, feel free to send an email to the discussion
-list.   If we think something should be tracked using an issue, we'll ask you to open one
-or open one ourselves.
-
-## Archives
-
-The mailing lists are archived and available to members of the list.  To access
-the archive, go to https://lists.research.microsoft.com.  
-
-You will need to create a password that is associated with your email address.
-To create a password, go to the archive site, click on Get Password under the
-options section on the right-hand side.  Once you have created a password,
-you can log into the archive site.
-
-## Privacy policy
-
-Usage of these email lists is subject to the following privacy policy:
-https://go.microsoft.com/fwlink/?LinkId=521839
-

README.md

@@ -57,8 +57,8 @@ expressions for equivalence.
 # Participating
 We're happy to have the help! You can contribute by trying out Checked C, 
 reporting bugs, and giving us feedback. There are other ways to [contribute](CONTRIBUTING.md) too.
-You can join the [mailing lists](https://github.com/Microsoft/CheckedC/blob/master/MAILING-LISTS.md) for
-announcements about the project.
+You can watch the [announcement page](https://github.com/microsoft/checkedc/discussions/categories/announcements)
+for announcements about the project.
 
 # Licensing
 The software in this repository is covered by the MIT license.  See the file LICENSE.TXT for the license.   The

spec/bounds_safety/core-extensions.tex

@@ -1568,3 +1568,17 @@ out-of-bounds pointers.'' These assumptions can be turned into formal
 statements about program behavior at runtime. Given those assumptions,
 we might then prove that at runtime checked code never reads or writes
 through out-of-bounds pointers.
+
+\section{Notes on temporal memory safety}
+\label{section:notes-on-temporal-memory-safety}
+
+Checked C does not protect against temporal memory safety violations like
+use-after-free.
+
+The usage of the C standard library function $realloc$ illustrates a subtle
+way which creates a temporal memory safety violation that Checked C will not
+detect. Consider a reallocation of memory like $q = realloc(p, ...)$.
+According to the POSIX manpages, $realloc$ should always be considered to
+free the memory associated with its argument. By that interpretation,
+any dereference of $p$ after the call $realloc(p,...)$ is a temporal safety
+violation.