Changes between Version 3 and Version 4 of Function_Contracts

Timestamp:

01/11/16 16:56:58 (10 years ago)

Author:

zmanchun

Comment:

--

Function_Contracts

@@ -57 +57 @@
  * `Assigns e0, e1, ...;`: side-effects, `e0, e1, ...` have `Mem` type
   * absence of `Assigns` clause does NOT mean that the function has no side-effects
-  * `Assigns \nothing`: means that the function has no side-effects
+  * `Assigns nothing`: means that the function has no side-effects
  * `Allocates e0, e1, ...;`: memory units allocated by the function, `e0, e1, ...` have `Mem` type
  * `Frees e0, e1, ...;`: memory units deallocated by the function, `e0, e1, ...` have `Mem` type
@@ -64 +64 @@
   * similar to `Assigns`
   * absence of `Reads` clause does NOT mean that the function does NOT read anything
-  * `Reads \nothing`: means that the function does NOT read the memory
+  * `Reads nothing`: means that the function does NOT read the memory
  * `Depends e0, e1, ...;`: dependency relation, where `e0, e1, ...` have `Mem` type
  * Note: `Guards`, `Depends` and `Reads` are CIVL extension for ACSL