Skip to content

Latest commit

 

History

History
220 lines (159 loc) · 9 KB

Developing.md

File metadata and controls

220 lines (159 loc) · 9 KB

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.

For JavaScript code read ReportTemplateStyleGuide.md, and for Python code read PythonStyleGuide.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.

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 11 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. Create a copy of the file .factorypath.template and name it .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-11]'), go to Window -> Preferences -> Java -> Installed JREs, click the "Search" button and select the path where your Java 11 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.

License and Copyright

All files in the CPAchecker repository need to have a header with a declaration of copyright and license in the REUSE format.

After installing the reuse tool, use the following command to add our standard header:

reuse addheader --template=header.jinja2 --license Apache-2.0 --copyright 'Dirk Beyer <https://www.sosy-lab.org>' <FILES>

Of course, you can adjust license and copyright if necessary (e.g., when integrating third-party code). However, for all original contributions please consider transferring the copyright to us and use our standard license in order to make license handling easier for us and all users of CPAchecker. In accordance with the Apache license, all contributions to CPAchecker are by default under the Apache license as well unless explicitly marked otherwise.

Code-Quality Checks and Continuous Integration

We use javac, the Eclipse Java Compiler, Google Error Prone, SpotBugs, Checkstyle, and Policeman's Forbidden API Checker 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.md 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 Authors.md are up-to-date.

  2. Define a new version by setting version.base in build.xml to the new value. The version tag is constructed as outlined below in Sect. "Release Tagging".

  3. Build binary versions with ant clean dist and test them to ensure that all necessary files are contained in them. Make sure that you do not have any local changes or unversioned files in your checkout.

  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>, where <version> is constructed as outlined below in Sect. "Release Tagging".

  6. Update version number in build/Dockerfile.release and .gitlab-ci.yml and either build and push the Docker image manually or trigger the scheduled GitLab CI job after pushing (https://gitlab.com/sosy-lab/software/cpachecker/pipeline_schedules).

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

  8. Prepare for next development cycle by setting version.base in build.xml to a new development version, which is the next possible version number with the suffix -svn. For example, if 1.9 was just released, the next possible feature release is 1.9.1 and the new development version should be 1.9.1-svn.

Version Numbering and Release Tagging

We use the following schema to construct version numbers for CPAchecker releases (from version 1.8 onwards):

  • X.Y is the yearly release in year 20XY. There is exactly one such CPAchecker release every year.
  • X.Y.Z is a feature release, where
    • X.Y is the last yearly release that already exists and that the new release builds on, and
    • Z is n+1 if a release X.Y.n already exists, and 1 otherwise.
  • X.Y[.z]-<component-version> is a component release, where X.Y[.z] is defined as above and <component-version> is a label that should give a hint on a special purpose for the release. Ideally, the component version ends with a date stamp.
  • Examples:
    • 1.9 is the yearly release for 2019.
    • 1.8-coveritest-sttt-20190729 is a component release after yearly release 1.8, which points to a commit that was made on 2019-07-29 for the purpose of tagging the component version used for the STTT paper on CoVeriTest.

The tags in our repository are named cpachecker-VERSION, e.g. cpachecker-1.9 and cpachecker-1.8-coveritest-sttt-20190729.