Changes between Version 37 and Version 38 of ContractReduction


Ignore:
Timestamp:
12/11/15 13:28:57 (10 years ago)
Author:
zmanchun
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • ContractReduction

    v37 v38  
    55* `guards` clause: specify the guard of a function, i.e., the specified predicate should hold in order to enable the execution of the function body
    66* `depends` clause: specify the dependency relation of the function, usually used for partial order reduction (POR) or other analysis
     7 * `\calls(fun, arg0, arg1, ...)`: an action of invoking a function with certain arguments
     8 * `\noact`: empty set of actions
     9 * `\anyact`: any actions
    710* `reads` clause: specify memory locations read by the function, the syntax of which is similar to `assigns` clause
    811* additional parameter for `allocates` clause: specify the scope of the heap for allocation; if absent then the root scope `$root` is used