org.jmlspecs.jml4.lookup
Class JmlBinaryLookup

java.lang.Object
  org.jmlspecs.jml4.lookup.JmlBinaryLookup

public class JmlBinaryLookup
extends java.lang.Object

Constructor Summary

JmlBinaryLookup(JmlSourceLookup jmlSourceLookup)

Method Summary

void	decorateBindingWithJml_new(IBinaryType binaryType, BinaryTypeBinding binding)
void	decorateBindingWithJml(IBinaryType binaryType, BinaryTypeBinding binding) 1.
static FieldDeclaration	getDeclaration(FieldBinding binding, BinaryTypeBinding binaryTypeBinding)
static AbstractMethodDeclaration	getDeclaration(MethodBinding binding, BinaryTypeBinding binaryTypeBinding)
static void	mergeFields(FieldBinding[] sourceFields, FieldDeclaration[] specFields)
static void	mergeMethods(ProblemReporter problemReporter, MethodBinding[] sourceMethods, AbstractMethodDeclaration[] specMethods)
void	mergeWithSourceAndSpec(ProblemReporter problemReporter, ReferenceBinding referenceBinding)

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

JmlBinaryLookup

public JmlBinaryLookup(JmlSourceLookup jmlSourceLookup)

Method Detail

decorateBindingWithJml

public void decorateBindingWithJml(IBinaryType binaryType,
                                   BinaryTypeBinding binding)

1. find source/spec file {.java, .jml, .refines-spec, etc.} for a given .class file. 2. perform a diet parse on the file(s) found to get signature. 3. store the source/spec type declaration(s) in the binding.

Parameters:

binaryType - the class to modify

binding -

decorateBindingWithJml_new

public void decorateBindingWithJml_new(IBinaryType binaryType,
                                       BinaryTypeBinding binding)

mergeMethods

public static void mergeMethods(ProblemReporter problemReporter,
                                MethodBinding[] sourceMethods,
                                AbstractMethodDeclaration[] specMethods)

mergeFields

public static void mergeFields(FieldBinding[] sourceFields,
                               FieldDeclaration[] specFields)

mergeWithSourceAndSpec

public void mergeWithSourceAndSpec(ProblemReporter problemReporter,
                                   ReferenceBinding referenceBinding)

getDeclaration

public static AbstractMethodDeclaration getDeclaration(MethodBinding binding,
                                                       BinaryTypeBinding binaryTypeBinding)

getDeclaration

public static FieldDeclaration getDeclaration(FieldBinding binding,
                                              BinaryTypeBinding binaryTypeBinding)