Join GitHub today
Fetching latest commit…
Cannot retrieve the latest commit at this time.
|Failed to load latest commit information.|
Shellac is an Eclipse Plugin that can be added to Java projects in order to add protective dynamic checks, as well as static analysis, to ensure the project meets its safety requirements. Shellac allows for a hybrid approach of the dynamic checks and static analysis so that they may be interchanged. [TODO: add a link to the paper] SETUP ===== In order to install this plugin, it must be exported as a jar (plugin with fragments and aspectJ support), then this jar must be added as to the build path of the project you wish to protect. The jar must also be added to the AspectJ aspect path, but this can easily be done by right clicking on the jar in the Project References and selecting to add it to the aspect path. Once installed, be sure to bring up the Tasks view to see the proof obligations. TODO ==== This plugin should provide a single menu item to convert it to a Shellac project, which should bring in AspectJ support, the necessary project references, and setup the apsectj path. We should add static checks that assignments to output ReqVars can only be made through calls to annotated methods, and that either instance variables must not be set inside @Satisfies methods, or add annotations to the instance vars themselves. We should also add checks that the instance variables have getters if they are used as a requirements variable, and that the getters are simple (just return the value). Known Issues ============ 1. there are issues with the KnowledgeBase updating properly (you have to open all the files in a project to get all the annotations) 2. the task markers are getting deleted when marked complete. they should only be deleted if the proof obligations change. 3. requirement variable names must be unique, even across different theorems 4. a check in a class other than the class that has the Satisfies annotation will not be found / executed 5. some basic types are still not supported as output variables (or history variables)