package testclasses;

import de.unifreiburg.cs.proglang.jgs.support.Casts;
import de.unifreiburg.cs.proglang.jgs.support.Constraints;
import de.unifreiburg.cs.proglang.jgs.support.Effects;
import de.unifreiburg.cs.proglang.jgs.support.Sec;

/**
 * Created by Nicolas Müller on 14.03.17.
 */
public class SimpleFail {

    @Constraints({"LOW <= @0 "})
    public static void main(String[] args) {
        String hello1 = "Hello World";
        String hello = (aStaticMethodWithCasts(hello1)); // fails at run-time due to an bad cast in aStaticMethodWithCasts
    }

    int answer = 42;

    @Sec("HIGH")
    int high = 123;

    @Sec("HIGH")
    Object highObject = new Object();


    static int aStatic = 0;

    @Constraints({"LOW <= @0 ", "@0 <= @ret"})
    @Effects({})
    static int aStaticMethod(int i) {
        if (i == 0) {
            return 1;
        } else {
            return 0;
        }
    }

    @Constraints({"HIGH <= @0 ", "@0 <= @ret"})
    @Effects({})
    static String aStaticMethodWithCasts(String i) {
        String x = Casts.cast("HIGH ~> ?", i);
        if (i == null) {
            return Casts.cast("? ~> LOW", x);
        } else {
            return null;
        }
    }

    @Constraints({"pub <= @0", "? <= @1", "@0 <= @ret", "@1 <= @ret"})
    public int methodWithImplicitFlows(boolean i, boolean j) {
        int z = 0;
        if (i) {
            z += 10;
        }
        if (j) {
            z += 1;
        }
        return z;
    }
}

@@ -562,356 +562,8 @@
  %7D%0A%0A
-    int answer = 42;%0A%0A    @Sec(%22HIGH%22)%0A    int high = 123;%0A%0A    @Sec(%22HIGH%22)%0A    Object highObject = new Object();%0A%0A%0A    static int aStatic = 0;%0A%0A    @Constraints(%7B%22LOW %3C= @0 %22, %22@0 %3C= @ret%22%7D)%0A    @Effects(%7B%7D)%0A    static int aStaticMethod(int i) %7B%0A        if (i == 0) %7B%0A            return 1;%0A        %7D else %7B%0A            return 0;%0A        %7D%0A    %7D%0A%0A
     
@@ -857,278 +857,6 @@
  %7D%0A%0A
-    @Constraints(%7B%22pub %3C= @0%22, %22? %3C= @1%22, %22@0 %3C= @ret%22, %22@1 %3C= @ret%22%7D)%0A    public int methodWithImplicitFlows(boolean i, boolean j) %7B%0A        int z = 0;%0A        if (i) %7B%0A            z += 10;%0A        %7D%0A        if (j) %7B%0A            z += 1;%0A        %7D%0A        return z;%0A    %7D%0A
 %7D%0A

add SimpleFail