KeY: ci-tool 1.1.0

ci-tool is a utility for supporting Java and JML contracts in Continuous Integration pipelines by providing support for checking the proofability of JML with KeY.

ci-tool is licensed under GPLv2+.

If you any suggestion feel to contact: Alexander Weigl.

Usage:

To use the ci-tool add the following lines to the ci config.

1. Get the latest version from the server:

$ wget -O ci-tool.jar  https://key-project.org/ci-tool/latest.php

1. Call ci-tool with your key-files or java file (or folder). ci-tool tries to verify all proofs automatically and uses found proofs or script files.

$ java -jar <jarfile> [files]

1. Find more parameters with -h

$ java -jar <jarfile> -h 

Examples

For travis-ci:

jdk:
  - openjdk11

language: java
install:
  - wget -O ci-tool.jar  https://key-project.org/ci-tool
script:
  - javac simplified/Keyserver.java
  - java -jar ci-tool.jar simplified/Keyserver.java

Changelog

• 1.3.0-alpha: Adding junit xml output

  • A new option --xml-output [FILE] was added. If specified, an XML file is written in the JUnit format.

• 1.2.0: Hot-fix for KeY

  • repairing model fields in set statements

• 1.1.0: bug fixes and support for proofs in key-files

  • Change of console output
  • Fix loading of proof files
  • Add download URL and a website
  • Known Bug: Something with the proof (search) path is wrong.

• 1.0.0 initial working version (24.01.2020)

  • first release of this project after positive of the a small jshell utility.
  • deploy on VerifyThis LTC 2020 repository

Future features

• Accumulate statistics
• If proof remains open,
• Calculate a coverage based on statements in the