Skip to content

Latest commit

 

History

History
150 lines (104 loc) · 5.89 KB

Developing.md

File metadata and controls

150 lines (104 loc) · 5.89 KB
Raw

CPAchecker Developing Instructions

More details can be found in the other files in this directory.

Please read and follow at least StyleGuide.md, Logging.md, Test.md, and VersionControl.md.

Getting the code

There are four possibilities to retrieve the source code:

Only our SVN repository allows committing, all mirrors are read-only. We recommend to use our own repository hosting, because it avoids the risk that the synchronization to a third party fails or causes problems.

For browsing through the code online, there are these possibilities:

For bug tracking, we use GitLab. The issue tracker is only accessible for CPAchecker developers, please click on Request Access after signing in to GitLab or contact us.

For building the code on the command line, c.f. ../INSTALL.md.

If you like to use Git, use the following commands to create a working copy that allows you to transparently commit to the SVN repository (with git svn dcommit) while still using Git to fetch the commits:

git clone -o mirror https://svn.sosy-lab.org/software/cpachecker.git/
cd cpachecker
git svn init --prefix=mirror/ -s https://svn.sosy-lab.org/software/cpachecker

This also works with GitHub.

Develop CPAchecker from within Eclipse

  1. Install a Java 8 compatible JDK (c.f. ../INSTALL.md).

  2. Install Eclipse with at least version 4.6, with JDT.

  3. IMPORTANT: Install the Eclipse plugin for [google-java-format]: Download the google-java-format-eclipse-plugin-*.jar from the most recent google-java-format release and put it into the dropins folder of your Eclipse installation (where you extracted the Eclipse archive, not the workspace).

  4. Install an SVN plugin for Eclipse, e.g. SubClipse. Create new project from SVN repository (or use GIT as described above).

  5. Copy the file .factorypath.template to .factorypath, and (if necessary) adjust the path to the CPAchecker directory within it.

  6. If Eclipse complains about a missing JDK (Unbound classpath container: 'JRE System Library [JavaSE-1.8]'), go to Window -> Preferences -> Java -> Installed JREs, click the "Search" button and select the path where your Java 8 installation can be found (on Ubuntu /usr/lib/jvm will do).

  7. In order to run CPAchecker, use one of the supplied launch configurations or create your own. To select the configuration, specification, and program files use the text box "program arguments" in the launch configuration editor. The text box "VM arguments" should contain "-ea" to enable assertion checking.

  8. Recommended: If you want the sources of the libraries (like Guava or CDT), run ant install-contrib once in the CPAchecker directory.

Code-Quality Checks and Continuous Integration

We use javac, Google Error-Prone, the Eclipse Java Compiler, and SpotBugs for findings bugs in the source, and we keep CPAchecker free of warnings from all these tools. You can run them all at once (plus the unit tests) with ant all-checks.

Our BuildBot will also execute these checks and send mails to the developer list (cf. Mailing.md, please apply for membership if you commit to CPAchecker).

If any of these tools or the unit tests find a problem, please fix them as soon as possible (ideally before committing).

The BuildBot also executes integration tests with thousands of CPAchecker runs in various configurations on every commit and checks for regression. All major projects and configurations within CPAchecker should be part of this test suite. Please refer to Test.md for more information.

Debugging

For attaching a debugger to a CPAchecker process started on the command line (even remotely), just run scripts/cpa.sh -debug ... and point your debugger to TCP port 5005 of the respective machine.

Releasing a new Version

  1. Preparations: Update NEWS.txt with notes for all important changes since the last CPAchecker release (i.e., new analyses and features, important changes to configuration etc.), and ensure that Copyright.txt and Authors.txt are up-to-date.

  2. Define a new version by setting version.base in build.xml to the new value.

  3. Build binary versions with ant clean dist and test them to ensure that all necessary files are contained in them.

  4. Update homepage:

    • Add release archives to /html in the repository.
    • Put changelog of newest into /html/NEWS-<version>.txt.
    • Add links to /html/download.php.
    • Move the old download links to /html/download-oldversions.php.
    • Update section News on /html/index.php.

  5. Add a tag in the repository with name cpachecker-<version>.

  6. Send a mail with the release announcement to cpachecker-announce and cpachecker-users mailing lists.

  7. Prepare for next development cycle by setting version.base in build.xml to a new development version (ending with -svn).