Changes between Version 49 and Version 50 of Language

Timestamp:

05/22/23 21:27:03 (3 years ago)

Author:

siegel

Comment:

--

Language

@@ -826 +826 @@
 It may be used with an [#atomic_f atomic] or [#system system] function.
 This clause specifies a guard that applies whenever the function is called.
-The ''expr'' may use the formal parameters of the function as well as any other variables that are in scope.
+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.
 Whenever control in a process is at a call to the function, the call will be enabled only if the guard evaluates to ''true''.
 To evaluate the guard, the actual arguments used in the call are substituted for the formal parameters in the guard expression.
+
+Note that `\true` should be used for the Boolean constant ''true'' in the ACSL expression.   E.g.,
+{{{
+\*@ executes_when \true; */
+void f() {...}
+}}}
 
 Note: if the actual arguments have side-effects, the code is automatically refactored so that the side-effects occur once, before the call.