Constructor Detail

• public ProcessingContextInformation(ClassNode classNode, SourceUnit sourceUnit, ReaderSource source)

  Creates the processing context for one class and the contract model derived from it.

  Parameters:

  classNode - the class currently being transformed

  sourceUnit - the owning source unit

  source - the reader source backing the source unit

Method Detail

• public void addError(String msg, ASTNode expr)

  Adds a syntax error tied to the given AST node while allowing compilation to continue collecting errors.

  Parameters:

  msg - the error message

  expr - the AST node providing source coordinates

• public Contract contract()

  Returns the mutable contract domain model associated with the current class.

  Returns:

  the contract model

• public Object get(String key)

  Returns an auxiliary value previously stored in the per-class processing context.

  Parameters:

  key - the metadata key

  Returns:

  the associated value, or null if none has been stored

• public boolean isClassInvariantsEnabled()

  Indicates whether class invariant processing is currently enabled.

  Returns:

  true if class invariants should be generated

• public boolean isConstructorAssertionsEnabled()

  Indicates whether constructor assertions are currently enabled.

  Returns:

  true if constructor assertions should be generated

• public boolean isPostconditionsEnabled()

  Indicates whether postcondition processing is currently enabled.

  Returns:

  true if postconditions should be generated

• public boolean isPreconditionsEnabled()

  Indicates whether precondition processing is currently enabled.

  Returns:

  true if preconditions should be generated

• public void put(String key, Object value)

  Stores an auxiliary value in the per-class processing context.

  Parameters:

  key - the metadata key

  value - the value to store

• public ReaderSource readerSource()

  Returns the reader source used to look up source fragments during code generation.

  Returns:

  the reader source

• public void setConstructorAssertionsEnabled(boolean other)

  Enables or disables constructor assertion generation for the current class.

  Parameters:

  other - true to keep constructor assertions enabled

• public SourceUnit sourceUnit()

  Returns the source unit currently being transformed.

  Returns:

  the source unit