Changes between Version 52 and Version 53 of Language

Timestamp:

05/23/23 11:09:41 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -121 +121 @@
 
 An atomic function must have a definition; in particular, neither a system function nor an abstract function may be declared using `$atomic_f`.
+
+The guard of an atomic function is taken to be the guard of the function's body.  For example, if `f` is defined
+{{{
+$atomic_f int f(int x) {
+  $when (x>0);
+  ...
+}
+}}}
+then a call to `f` will block if the argument used in the call is not positive—no activation frame is pushed onto the stack unless the guard is true.
 
 === System functions: `$system` #system
@@ -732 +741 @@
 Note that `malloc` is implemented as `$malloc($root, size)`.
 
-Function `$free` deallocates the object pointed to by `p`, which should be a pointer that was returned
-by an earlier call to `$malloc`. 
+Function `$free` deallocates the object pointed to by `p`, which should be a pointer that was returned by an earlier call to `$malloc`. 
 An error is generated if the pointer is not one that was returned by $malloc, or if it was already freed.
 
@@ -824 +832 @@
 This clause has syntax
   `executes_when` ''expr'' `;`
-It may be used with an [#atomic_f atomic] or [#system system] function.
+It may be used with a [#system system function].
+(For all other functions, this clause is ignored.)
 This clause specifies a guard that applies whenever the function is called.
 The ''expr'' is an ACSL expression and may use the formal parameters of the function as well as any other variables that are in scope.
@@ -833 +842 @@
 {{{
 \*@ executes_when \true; */
-void f() {...}
+$system void f(int x);
 }}}