com.surelogic
Annotation Type RegionEffects

@Documented
@Target(value={METHOD,CONSTRUCTOR})
public @interface RegionEffects

Declares the regions that may be read or written during execution of the method or constructor to which this annotation is applied. In general the annotation syntax is

@RegionEffects("reads readTarget, ... ; writes writeTarget, ... ")

The annotation contains reads and writes clauses that each have a list of one or more targets. The reads clause describes the data that may be read by the method/constructor; the writes clause describes the state that may be read or written by the method/constructor. Because writing includes reading, there is no need to list a target in the reads clause if its state is already described in the writes clause.

Both the reads and writes clauses are optional: to indicate that there are no effects use @RegionEffects("none"). An unannotated method is assumed to have the annotation @RegionEffects("writes All") which declares that the method could read from or write to any state in the program.

A target is an extrinsic syntactic mechanism to name references to regions, and can be one of

Region

If region is an instance region, then it is the same as this:region (see below). If region is a static region, it must be a region declared in the annotated class or one of its ancestors, and the method affects the given region.

this:Region

Region is an instance region of the class containing the method. The method affects the named region of the receiver object.

param:Region

param is a parameter of the method that references an object. Region is a region of the class of param's type. The method affects the named region of the object referenced by param at the start of the method's execution.

pkg.C.this:Region

pkg.C is an "outer class" of the class that contains the annotated method. That is, the method being annotated is in class D, and D is an inner class of C. Region is a region of pkg.C. The method affects the named region of the given outer class receiver.

any(pkg.C):Region

pkg.C is a class name and Region is a region of pkg.C. This target indicates that the method affects the given region of any object of class pkg.C.

pkg.C:Region

Region is a static region of class pkg.C . The method affects the given static region.

The analysis checks that the actual effects of the method implementation are no greater than its declared effects. There are several fine points to this:

• Uses of final fields produce no effects and do not need to be declared.
• Effects on local variables are not visible outside of a method/constructor and do not need to be declared.
• Effects on objects created within a method are not visible outside of a method and do not need to be declared.
• Constructors do not have to declare the effects on the Instance region of the object under construction.
• Region aggregation (see Aggregate and AggregateInRegion) is taken into account.

Examples:

Here is a simple "variable" class with effects annotations.

 @Region("public ValueRegion")
 public class Var {
 
   @InRegion("ValueRegion")
   private int value;
 
   @RegionEffects("none")
   public Var(int v) {
     value = v;
   }
 
   @RegionEffects("reads ValueRegion")
   public int getValue() {
     return value;
   }
 
   @RegionEffects("writes ValueRegion")
   public void setValue(int v) {
     value = v;
   }
 }
 

Javadoc usage notes:

This annotation may placed in Javadoc, which can be useful for Java 1.4 code which does not include language support for annotations, via the @annotate tag.

 /**
  * @annotate Region("public ValueRegion")
  */
 public class Var {
 
   /**
    * @annotate InRegion("ValueRegion")
    */
   private int value;
 
   /**
    * @annotate RegionEffects("none")
    */
   public Var(int v) {
     value = v;
   }
 
   /**
    * @annotate RegionEffects("reads ValueRegion")
    */
   public int getValue() {
     return value;
   }
 
   /**
    * @annotate RegionEffects("writes ValueRegion")
    */
   public void setValue(int v) {
     value = v;
   }
 }
 

Required Element Summary

String

value This attribute is either "none" to indicate that the method/constructor has no visible effects or divided into separate (and optional) reads and writes clauses.

Element Detail

value

public abstract String value

This attribute is either "none" to indicate that the method/constructor has no visible effects or divided into separate (and optional) reads and writes clauses. Each clause is a list of comma-separated targets describing the regions that may be read/written. The clauses are separated by a semicolon.

Examples:

 @RegionEffects("reads this:Instance; writes other:Instance")
 @RegionEffects("writes C:StaticRegion, any(D):Instance; reads this:Instance")
 @RegionEffects("reads this:Instance")
 @RegionEffects("writes this:Instance")
 @RegionEffects("none")
 

The value of this attribute must conform to the following grammar (in Augmented Backus–Naur Form):

 value =
   none /  ; No effects
   readsEffect [";" writesEffect] /
   writesEffect [";" readsEffect]
 
 readsEffect = "reads" effectsSpecification
 
 writesEffect = "writes" effectsSpecification
 
 effectsSpecification = "nothing" / effectSpecification *("," effectSpecification)
   
 effectSpecification =
   simpleEffectExpression ":" simpleRegionSpecification /
   IDENTIFIER   ; instance region of "this" or a static region declared in the current class or one of its ancestors 
 
 simpleEffectExpression =
   "any" "(" namedType ")" /    ; any instance
   namedType "." "this" /       ; qualified this expression
   namedType /                  ; class name 
   simpleExpression             ; parameter name
 
 namedType = IDENTIFIER *("." IDENTIFIER)
 
 simpleExpression = "this" / IDENTIFIER
 
 simpleRegionSpecification = IDENTIFIER / "[" "]"  ; Region of the class being annotated
 
 IDENTIFIER = Legal Java Identifier