Strongarm

[jsinglet]

Integration of Specification Inference. Includes changes to the Eclipse plugin that adds menu options (but not toolbar buttons) and preference panes for specification inference. Screenshots of the UI changes are included in this PR.

A new test suite is in the usual place at: /src/org/jmlspecs/openjmltest/testcases/strongarm.java

Summary of New Options:

    // Options Related to Specification Inference
    INFER("-infer",true,"POSTCONDITIONS","STRONGARM: Infer missing contracts (postconditions (default), preconditions)","-command=infer"),
    INFER_DEBUG("-infer-debug", false, null, "STRONGARM: Enable debugging of contract inference.", null),    
    INFER_DEFAULT_PRECONDITIONS("-infer-default-preconditions", false, null, "STRONGARM: If not specified, the precondition of methods lacking preconditions will be set to true (otherwise inference is skipped).", null),
    INFER_NO_EXIT("-noexit",true,null,"STRONGARM: Infer contracts (suppress exiting)","-command=infer-no-exit"),
    INFER_MINIMIZE_EXPRS("-infer-minimize-expressions", false, null, "STRONGARM: Minimize expressions where possible.", null),
    
    //
    // Inference decides to write specs based on the following conditions
    // 1) If -infer-persist-path is specified, specs are written to that directory (base)
    // 2) Else, if -specspath is specified, specs are written to that directory (base)
    // 3) Otherwise, we write the specs to the same directory were the java class source exists
    //
    INFER_WEAVE("-infer-weave", false, null, "STRONGARM: After inference, weave the inferred specs into the source code", null),    
    INFER_PERSIST("-infer-persist", false, null, "STRONGARM: Persist inferred specs (defaults to location of class source and can be overridden with -infer-persist-path and -specspath)", null),
    INFER_PERSIST_PATH("-infer-persist-path", true, null, "STRONGARM: Specify output directory of specifications (overrides -specspath)", null),
    INFER_MAX_DEPTH("-infer-max-depth", true, null, "STRONGARM: The largest CFG we will agree to process", null),
    INFER_TIMEOUT("-infer-timeout", true, null, "STRONGARM: Give up inference after this many seconds.", null),
    INFER_DEV_MODE("-infer-dev-mode", false, null, "STRONGARM: Special features for developers.", null),    
    DISABLE_VISIBILITY_CHECKING("-all-public", false, null, "Do not check visibility of fields used in specifications.", null),