HTTPS SSH

Program Analysis for Missile Firing

Information

This is an implementation of the following project: Program Analysis. All code except template is written by Robin Vaaler, Till Haug and Marcel Mohler.

The program uses the Soot Framework (transformers of the APRON polyhedra domain (Polka)) to do a program analysis of a missile firing code fragment. It prints out weather it is SAFE or UNSAFE.

Example

Input:

public class MyTest {
  public static void l() {
    MissileBattery r = new MissileBattery(6);
    int i = 20;
    r.fire(i);
  }
}

Output:

Program is UNSAFE