If you are working on the virtual machine in the lab, all tools are prepared in the /home/cloud/tools directory and you can skip this preparation step. Otherwise, if you are working on your own computer, you have to download and install Infer and CPAchecker. Note, that Infer has binaries for OS X and Linux, whereas CPAchecker has binares for Linux and Windows.

Infer can be run in different ways depending on the build system of your project. For more information, take a quick look at the workflow section of the documentation.

If you are only analyzing a few files (without a project) Infer can be executed based on the javac command.

• Try Infer on the simple example files located in the Java examples folder of the Infer repository!
  infer run -- javac Hello.java Pointers.java Resources.java
  Remark: by default, you have to type the full path to the infer binary (~/tools/<infer_directory>/bin/infer on the VM). Alternatively you can add the bin folder to the PATH or create an alias.
• The results of the analysis are displayed in the console and also in the file infer-out/bugs.txt. Examine the results!

Infer supports various build systems, including Maven (see full list).

• Clone the Algorithms project located on GitHub!
• The configuration of the project is a bit outdated, add the following to the pom.xml:

<properties>
    <maven.compiler.target>1.8</maven.compiler.target>
    <maven.compiler.source>1.8</maven.compiler.source>
</properties>

• Check if the project can be compiled with mvn compile!
• Make sure that the project is clean (mvn clean) before running Infer!
• Run Infer by infer run -- mvn compile! Note, that for the first run, it might take some minutes.
• Examine the results!
  • Classify the bugs found! Are there any false alarms? If yes, was it trivial to detect that it is a false alarm?
  • Are there any potential bugs?
  • CHECK: Create a screenshot of the list of bugs. Write next to each bug whether it is a false alarm or a pontential bug. Hint: you can open the infer-out/bugs.txt file and write below/above each bug.
  • If there are potential bugs, fix one of them! Run Infer again and examine the results!

• Clone the JodaTime project located on GitHub! This project also uses the maven build system.
• This project is also a bit outdated now -- you will have to open the pom.xml file at the root of the project and find the lines

<maven.compiler.source>1.5</maven.compiler.source>
<maven.compiler.target>1.5</maven.compiler.target>

around the end of it. Change 1.5 to 1.8 in both lines.

• Check if the project can be compiled with mvn compile!
• Make sure that the project is clean (mvn clean) before running Infer!
• Run Infer by infer run -- mvn compile!
• Note, that this will take quite a few minutes (~10-15 minutes), as this project is larger than the last one.
  • If you don't have anything else to do while waiting for Infer and want to have a good laugh, you can check out this article about why time/date libraries (such as this project) are important and not worth to reinvent.
  • You can also start the next (CPAChecker) exercise while waiting for Infer.
• Examine the results!
  • In this case Infer finds a lot more issues, but truncates the output in the terminal. Check out infer-out/report.txt!
  • What is the type of issue Infer reported the highest number of? Is it easy to detect if the issue is a false alarm or not in these cases? Is it easy to find these type of issues without a static analyzer?
  • Find this type of issue on this page of the Infer documentation to understand it better.
  • CHECK: Create a screenshot of showing this type of issue in the Infer output. Based on what conditions these types of issues were checked and reported in this case and not in the Algorithms project? Write down into the text file on the screenshot in a short answer. (Hint: the answer is in the Infer documentation you just checked out above.)

• The commands for CPAchecker should be executed from its own directory (/home/cloud/tools/<cpachecker_directory>/ on the VM).

• Run CPAchecker on the example program (this will run CPAchecker in the default configuration):

  ./scripts/cpa.sh -default doc/examples/example.c

• The result of verification appears on the console and additional files are generated in the ./output folder. Examine the results, starting with the html file (Report.html or Counterexample.html depending on the result)!

  • The CFA (Control Flow Automata) tab contains the graphical representation of the program.
  • The ARG tab contains the abstract reachability graph, which represents the possible states of the program.
  • The Source tab shows the original code.

• Introduce an error in the program, e.g., by replacing a = 0 with a = 5 in the initialization!

• Run CPAchecker again! Make sure to remove the ./output folder first.

• Examine the result again! CPAchecker should highlight the counterexample in the Control Flow Automata.

• CHECK: Create a screenshot of the modified program and the counterexample on the CFA tab.