file_itr = FileUtils.iterateFiles(destDir, new String[] { "java" }, true);
- file_itr.forEachRemaining(file -> {
- boolean success = compile(file);
- if (!success) {
- unsuccessfulCompiles.add(file);
- } else {
- successfulCompiles.add(file);
- }
- });
- // TODO: Temporary added some extra Print statements
+ if (transformAll) {
+ file_itr.forEachRemaining(file -> unsuccessfulCompiles.add(file));
+ } else {
+ file_itr.forEachRemaining(file -> {
+ boolean success = compile(file);
+ if (!success) {
+ unsuccessfulCompiles.add(file);
+ } else {
+ successfulCompiles.add(file);
+ }
+ });
+ }
+
System.out.println("================================================\t");
System.out.println("Before Transformation:\t");
System.out.println("Number of unsuccessful intial compilation " + unsuccessfulCompiles.size() + "\t");
System.out.println("Number of successful intial compilation " + successfulCompiles.size());
System.out.println("================================================");
- // System.out.println(unsuccessfulCompiles + " ------- " + successfulCompiles);
+
+// System.out.println(unsuccessfulCompiles + " ------- " + successfulCompiles);
+
+
+
+ System.out.println(unsuccessfulCompiles + " ------- " + successfulCompiles);
Transformer transformer = new Transformer(unsuccessfulCompiles, target);
transformer.transformFiles(minTypeExpr, minTypeCond, minTypeParams, type);
@@ -153,10 +166,12 @@ public static void main(String[] args) throws IOException {
file_itr = FileUtils.iterateFiles(destDir, new String[] { "java" }, true);
+
// also delete those files where all methods after transformations
// were not be able to meet the selection criteria.
// do not remove uncompiled files if target is SVCOMP as for SVCOMP one
// dependency will not be compileable
+
file_itr.forEachRemaining(file -> {
boolean success = compile(file);
if (!success && !target.equals("SVCOMP")) {
@@ -174,8 +189,12 @@ public static void main(String[] args) throws IOException {
if (target.equals("SVCOMP")) {
prepareForSvcompBenchmark(file);
}
+
+ if(target.equals("SVCOMP")) {
+ prepareForSvcompBenchmark(file);
+ }
});
- // TODO: Temporary added some extra Print statements
+
System.out.println("================================================\t");
System.out.println("After Transformation:\t");
System.out.println("Number of unsuccessful intial compilation " + unsuccessfulCompiles.size() + "\t");
@@ -184,7 +203,7 @@ public static void main(String[] args) throws IOException {
// System.out.println(unsuccessfulCompiles.size() + " +++++ " +
// successfulCompiles.size());
-
+
try {
FileUtils.forceDelete(tmpDir);
} catch (IOException e) {
@@ -202,6 +221,7 @@ private static boolean compile(File file) {
if (compiler == null)
throw new RuntimeException("Could not get javac - are you running with a JDK or a JRE?");
+
ByteArrayOutputStream outputStream = new ByteArrayOutputStream();
ByteArrayOutputStream errorStream = new ByteArrayOutputStream();
int runErrors = compiler.run(null, outputStream, errorStream, "-g", "-d", buildDir.getAbsolutePath(), "-cp",
@@ -229,6 +249,7 @@ private static void removeEmptyDirs(File file) {
}
}
+
private static void prepareForSvcompBenchmark(File file) {
// Path to Save YML file
File parentDirectory = new File(file.getParent());
diff --git a/src/java/transform/Transformer.java b/src/java/transform/Transformer.java
index f33d2f4f..b56b4259 100644
--- a/src/java/transform/Transformer.java
+++ b/src/java/transform/Transformer.java
@@ -7,16 +7,9 @@
import java.nio.file.Files;
import java.nio.file.Paths;
import java.util.ArrayList;
-import java.util.Hashtable;
import java.util.Iterator;
import java.util.Map;
-import java.util.Map.Entry;
-
import org.apache.commons.io.FileUtils;
-import org.eclipse.core.resources.IProject;
-import org.eclipse.core.resources.ResourcesPlugin;
-import org.eclipse.core.runtime.CoreException;
-import org.eclipse.jdt.core.IJavaProject;
import org.eclipse.jdt.core.JavaCore;
import org.eclipse.jdt.core.dom.AST;
import org.eclipse.jdt.core.dom.ASTNode;
@@ -24,9 +17,7 @@
import org.eclipse.jdt.core.dom.CompilationUnit;
import org.eclipse.jdt.core.dom.MethodDeclaration;
import org.eclipse.jdt.core.dom.PackageDeclaration;
-import org.eclipse.jdt.core.dom.SimpleName;
import org.eclipse.jdt.core.dom.Statement;
-import org.eclipse.jdt.core.dom.Type;
import org.eclipse.jdt.core.dom.TypeDeclaration;
import org.eclipse.jdt.core.dom.rewrite.ASTRewrite;
import org.eclipse.jdt.core.dom.rewrite.ListRewrite;
@@ -149,7 +140,7 @@ public void transformFiles(int minTypeExpr, int minTypeCond, int minTypeParams,
parser.setUnitName(file.getPath());
String[] classPath = {Paths.get("build", "classes").toString()};
- String[] sourcePath = { Paths.get("suitablePrgms").toString() , Paths.get("src").toString()};
+ String[] sourcePath = { Paths.get(Main.source).toString() , Paths.get("src").toString()};
parser.setEnvironment(classPath, sourcePath, new String[] { "UTF-8", "UTF-8" }, true);
CompilationUnit cu = (CompilationUnit) parser.createAST(null);
diff --git a/src/java/transform/visitors/TransformVisitor.java b/src/java/transform/visitors/TransformVisitor.java
index c3ad90ea..5cbd8138 100644
--- a/src/java/transform/visitors/TransformVisitor.java
+++ b/src/java/transform/visitors/TransformVisitor.java
@@ -1,5 +1,6 @@
package transform.visitors;
+
import java.io.BufferedWriter;
import java.io.File;
import java.io.FileWriter;
@@ -114,6 +115,8 @@ public TransformVisitor(SymbolTable root, ASTRewrite rewriter, TypeTable typeTab
hasRandom = false;
}
+
+
// expr
@Override
public void endVisit(ArrayAccess node) {
@@ -235,7 +238,7 @@ public boolean visit(CompilationUnit node) {
//String[] importSplit = importName.split("\\.");
//String className = importSplit[importSplit.length - 1];
// if (!importName.startsWith("java.") && !importName.startsWith("javax.")) {
- if (!importName.startsWith("java.")){
+ if (!importName.startsWith("java.") || !importName.startsWith("org.sosy_lab.sv_benchmarks")){
//System.out.println("Removing import " + importName);
rewriter.remove(importDec, null);
}
@@ -252,10 +255,22 @@ public void endVisit(CompilationUnit node) {
ImportDeclaration id = ast.newImportDeclaration();
String importName = "";
switch(target){
- case "SPF" : importName = "gov.nasa.jpf.symbc.Debug";
- break;
- default: importName = hasRandom?"":"java.util.Random";
- }
+ case "SPF":
+ importName = "gov.nasa.jpf.symbc.Debug";
+ break;
+ case "SVCOMP":
+ importName = "org.sosy_lab.sv_benchmarks.Verifier";
+ break;
+ default:
+ importName = hasRandom?"":"java.util.Random";
+ break;
+ }
+// if (target.equals("SPF"))
+// importName = "gov.nasa.jpf.symbc.Debug";
+// else if (target.equals("SVCOMP"))
+// importName = "org.sosy_lab.sv_benchmarks.Verifier";
+// else
+// importName = hasRandom?"":"java.util.Random";
if(!importName.isEmpty()) {
id.setName(ast.newName(importName.split("\\.")));
ListRewrite listRewrite = rewriter.getListRewrite(node, CompilationUnit.IMPORTS_PROPERTY);
@@ -559,15 +574,14 @@ public void endVisit(MethodDeclaration node) {
}
}
- // stmt rule
- @Override
+// //stmt rule
+// @Override
public boolean visit(MethodInvocation node) {
// TODO: Check that the method contains unresolvable types before we remove it.
if (node.getLocationInParent() == ExpressionStatement.EXPRESSION_PROPERTY) {
ASTNode parent = node.getParent(); // ExpressionStatement
if (parent.getParent() instanceof Block) {
rewriter.remove(parent, null);
- //System.out.println("Removing " + node + " from " + parent);
} else {
rewriter.replace(parent, ast.newBlock(), null);
}
@@ -786,6 +800,8 @@ public boolean visit(SimpleName node) {
switch(target) {
case "SPF": randMethodInvocation = replaceWithSymbolicInteger();
break;
+ case "SVCOMP" : randMethodInvocation = replaceWithNodeInteger();
+ break;
default : randMethodInvocation = replaceWithRandomInteger();
}
@@ -816,6 +832,8 @@ public boolean visit(SimpleName node) {
switch(target) {
case "SPF": expression = replaceWithSymbolicFloat();
break;
+ case "SVCOMP" : expression = replaceWithNodeFloat();
+ break;
default : expression = replaceWithRandomFloat();
}
@@ -848,6 +866,9 @@ public boolean visit(SimpleName node) {
switch(target) {
case "SPF": randMethodInvocation = replaceWithSymbolicDouble();
break;
+ case "SVCOMP": randMethodInvocation = replaceWithNodeDouble();
+ break;
+
default : randMethodInvocation = replaceWithRandomDouble();
}
@@ -878,6 +899,8 @@ public boolean visit(SimpleName node) {
switch(target) {
case "SPF": randMethodInvocation = replaceWithSymbolicBoolean();
break;
+ case "SVCOMP" : randMethodInvocation = replaceWithNodeBoolean();
+ break;
default : randMethodInvocation = replaceWithRandomBoolean();
}
@@ -1134,11 +1157,17 @@ public boolean visit(VariableDeclarationStatement node) {
}
+/**================================================BOOLEAN==========================================================================*/
+
+/**================================================BOOLEAN==========================================================================*/
+
private void replaceBoolean(Expression exp) {
MethodInvocation randMethodInvocation = null;
switch(target) {
case "SPF" : randMethodInvocation = replaceWithSymbolicBoolean();
break;
+ case "SVCOMP" : randMethodInvocation = replaceWithNodeBoolean();
+ break;
default: randMethodInvocation = replaceWithRandomBoolean();
}
rewriter.replace(exp, randMethodInvocation, null);
@@ -1152,9 +1181,23 @@ private MethodInvocation replaceWithRandomBoolean() {
randMethodInvocation.setName(ast.newSimpleName("nextBoolean"));
randUsedInMethod = true;
-// randUsedInProgram = true;
+ //randUsedInProgram = true;
+ return randMethodInvocation;
+
+ }
+
+ private MethodInvocation replaceWithNodeBoolean() {
+ MethodInvocation randMethodInvocation = ast.newMethodInvocation();
+ randMethodInvocation.setExpression(ast.newSimpleName("Verifier"));
+ randMethodInvocation.setName(ast.newSimpleName("nondetBoolean"));
+
+ randUsedInMethod = false;
return randMethodInvocation;
+
}
+
+
+
private MethodInvocation replaceWithSymbolicBoolean() {
MethodInvocation randMethodInvocation = ast.newMethodInvocation();
@@ -1166,7 +1209,8 @@ private MethodInvocation replaceWithSymbolicBoolean() {
varNum++;
return randMethodInvocation;
}
-
+/**==============================================INTEGER==========================================================================*/
+
private MethodInvocation replaceWithSymbolicInteger() {
MethodInvocation randMethodInvocation = ast.newMethodInvocation();
randMethodInvocation.setExpression(ast.newSimpleName("Debug"));
@@ -1191,17 +1235,29 @@ private MethodInvocation replaceWithRandomInteger() {
}
+ private MethodInvocation replaceWithNodeInteger() {
+ MethodInvocation randMethodInvocation = ast.newMethodInvocation();
+ randMethodInvocation.setExpression(ast.newSimpleName("Verifier"));
+ randMethodInvocation.setName(ast.newSimpleName("nondetInt"));
+
+ randUsedInMethod = false;
+ return randMethodInvocation;
+
+ }
+
private void replaceInteger(Expression exp) {
MethodInvocation randMethodInvocation = null;
switch(target) {
case "SPF" : randMethodInvocation = replaceWithSymbolicInteger();
break;
+ case "SVCOMP" : randMethodInvocation = replaceWithNodeInteger();
+ break;
default: randMethodInvocation = replaceWithRandomInteger();
}
rewriter.replace(exp, randMethodInvocation, null);
}
-
+/**==============================================DOUBLE==========================================================================*/
/* Actually it is Double */
private void replaceDouble(Expression exp) {
@@ -1209,6 +1265,8 @@ private void replaceDouble(Expression exp) {
switch(target){
case "SPF" : randMethodInvocation = replaceWithSymbolicDouble();
break;
+ case "SVCOMP" : randMethodInvocation = replaceWithNodeDouble();
+ break;
default: randMethodInvocation = replaceWithRandomDouble();
}
@@ -1234,16 +1292,40 @@ private MethodInvocation replaceWithSymbolicDouble() {
return randMethodInvocation;
}
+
+ private MethodInvocation replaceWithNodeDouble() {
+ MethodInvocation randMethodInvocation = ast.newMethodInvocation();
+ randMethodInvocation.setExpression(ast.newSimpleName("Verifier"));
+ randMethodInvocation.setName(ast.newSimpleName("nondetDouble"));
+
+ randUsedInMethod = false;
+ return randMethodInvocation;
+
+ }
+
+/**==============================================FLOAT==========================================================================*/
+
private void replaceFloat(Expression exp) {
ASTNode expression = null;
switch(target) {
case "SPF": expression = replaceWithSymbolicFloat();
break;
+ case "SVCOMP" : expression = replaceWithNodeFloat();
+ break;
default: expression = replaceWithRandomFloat();
}
rewriter.replace(exp, expression , null);
}
+ private MethodInvocation replaceWithNodeFloat() {
+ MethodInvocation randMethodInvocation = ast.newMethodInvocation();
+ randMethodInvocation.setExpression(ast.newSimpleName("Verifier"));
+ randMethodInvocation.setName(ast.newSimpleName("nondetFloat"));
+
+ randUsedInMethod = false;
+ return randMethodInvocation;
+
+ }
private MethodInvocation replaceWithRandomFloat() {
MethodInvocation randMethodInvocation = ast.newMethodInvocation();
diff --git a/svcomp-benchmarks/ActiveCheck/Main.java b/svcomp-benchmarks/ActiveCheck/Main.java
new file mode 100644
index 00000000..c0e76233
--- /dev/null
+++ b/svcomp-benchmarks/ActiveCheck/Main.java
@@ -0,0 +1,64 @@
+/** filtered and transformed by PAClab */
+
+
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+/**
+ * Activecheck is used to submit passive checks to NSCA services. While it is
+ * intended to run as a daemon it can be used command line program as well.
+ *
+ * @author Frederik Happel mail@frederikhappel.de
+ */
+public class Main {
+ /** PACLab: suitable */
+ public static void start() {
+ int checkDumpInterval = Verifier.nondetInt();
+ int hostCheckInterval = Verifier.nondetInt();
+ int reloadInterval = Verifier.nondetInt();
+ if (Verifier.nondetBoolean()) {
+ final int bindPort = Verifier.nondetInt();
+ }
+ // main loop
+ long lastReloadMillis = Verifier.nondetInt();
+ long prevLastReloadMillis = lastReloadMillis;
+ long lastHostCheckMillis = 0;
+ long lastCheckDumpMillis = 0;
+ final long time = Verifier.nondetInt();
+ do {
+
+ if (time > 0) {
+ // reload configuration?
+ long diffMillis = time - lastReloadMillis;
+ if (reloadInterval * 1000 - diffMillis <= 1000) {
+ lastReloadMillis = time;
+ }
+
+ // submit a host check result?
+ diffMillis = time - lastHostCheckMillis;
+ if (hostCheckInterval * 1000 - diffMillis <= 1000) {
+ lastHostCheckMillis = time;
+ final long currentTime = Verifier.nondetInt();
+ final long uptime = Verifier.nondetInt() / 1000;
+ }
+
+ // output failed checks to file
+ diffMillis = time - lastCheckDumpMillis;
+ if (checkDumpInterval * 1000 - diffMillis <= 1000) {
+ lastCheckDumpMillis = time;
+ }
+
+
+ }
+ }
+ while (Verifier.nondetBoolean());
+ assert (lastCheckDumpMillis == 0 || lastCheckDumpMillis == time );
+ assert (lastHostCheckMillis == 0 || lastHostCheckMillis == time);
+ assert (lastReloadMillis == prevLastReloadMillis || lastReloadMillis == time);
+
+
+ }
+
+ public static void main(String[] args){
+ start();
+ }
+}
diff --git a/svcomp-benchmarks/Activecheck.yml b/svcomp-benchmarks/Activecheck.yml
new file mode 100644
index 00000000..5f220ff6
--- /dev/null
+++ b/svcomp-benchmarks/Activecheck.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- ActiveCheck/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/ArrayBasedCollectionTimer.yml b/svcomp-benchmarks/ArrayBasedCollectionTimer.yml
new file mode 100755
index 00000000..b791bba3
--- /dev/null
+++ b/svcomp-benchmarks/ArrayBasedCollectionTimer.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- assignment3/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/ArrayBasedCollectionTimer/Main.java b/svcomp-benchmarks/ArrayBasedCollectionTimer/Main.java
new file mode 100644
index 00000000..a25ca854
--- /dev/null
+++ b/svcomp-benchmarks/ArrayBasedCollectionTimer/Main.java
@@ -0,0 +1,60 @@
+/** filtered and transformed by PAClab */
+
+import org.sosy_lab.sv_benchmarks.Verifier;
+/**
+ * @author Paymon Saebi
+ * @author Cody Cortello
+ * @author Casey Nordgran
+ *
+ * ArrayBasedCollection timing experiments.
+ */
+public class Main {
+ /**
+ * This code is refactored from Paymon's SortDemo.java code provided on the class website
+ */
+ /** PACLab: suitable */
+ public static void timer() {
+ long startTime, midpointTime, stopTime;
+ // Setup for the timing experiment.
+ int timesToLoop = 150;
+ // First, spin computing stuff until one second has gone by.
+ // This allows this thread to stabilize.
+ // (As seen in lab1 experiment 8)
+ startTime = Verifier.nondetInt();
+ // Run complete timing for different values of N
+ for (int N = 1000; N <= 20000; N += 1000) {
+
+ int[] testArray = new int[N];
+ int index = 0;
+ while (Verifier.nondetInt() < N) {
+ int intToAdd = Verifier.nondetInt();
+ // fill the testArray with the ints then add to it at random indices
+ if (index < N)
+ testArray[index++] = intToAdd;
+ else
+ testArray[((int) (Verifier.nondetInt() * N))] = intToAdd;
+ }
+ assert(testArray != null);
+
+ // start timing analysis, only uncomment the current needed test below
+ startTime = Verifier.nondetInt();
+ // end time for the for loop above, and begin time of for loop below.
+ midpointTime = Verifier.nondetInt();
+ stopTime = Verifier.nondetInt();
+
+ // Compute the time, subtract the cost of running the loop
+ // from the cost of running the loop and computing the called methods
+ // Average it over the number of runs.
+ double averageTime = ((midpointTime - startTime) - (stopTime - midpointTime)) / timesToLoop;
+ if((midpointTime - startTime) == (stopTime - midpointTime)) {
+ assert (averageTime == 0);
+ }
+ }
+ }
+
+ public static void main(String[] args) {
+ timer();
+ }
+
+
+}
diff --git a/svcomp-benchmarks/Base.yml b/svcomp-benchmarks/Base.yml
new file mode 100644
index 00000000..d5313f27
--- /dev/null
+++ b/svcomp-benchmarks/Base.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- Base/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/Base/Main.java b/svcomp-benchmarks/Base/Main.java
new file mode 100644
index 00000000..484a4986
--- /dev/null
+++ b/svcomp-benchmarks/Base/Main.java
@@ -0,0 +1,71 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+
+public class Main{
+ public static byte[] encode(byte[] source, int off, int len, byte[] alphabet, int maxLineLength) {
+
+ assert alphabet.length <= 64;
+ assert source.length >= off + len;
+
+ assert (len > 0);
+ byte newLine = '\n';
+ int lenDiv3 = (len + 2) ; // ceil(len / 3)
+ assert (lenDiv3 == (len +2));
+ int len43 = lenDiv3 * 4;
+ byte[] outBuff = new byte[len43 + (len43 / maxLineLength)];// Main 4:3 // New lines
+ // this is getting success but it should fail?
+ assert (outBuff.length == len43 + (len43 / maxLineLength));
+
+ int d = 0;
+ int e = 0;
+ int len2 = len - 2;
+ int lineLength = 0;
+
+ for (; d < len2; d += 3, e += 4) {
+
+ // The following block of code is the same as
+ // encode3to4( source, d + off, 3, outBuff, e, alphabet );
+ // but inlined for faster encoding (~20% improvement)
+ int inBuff = Verifier.nondetInt();
+ outBuff[e] = alphabet[(inBuff >>> 18)];
+ outBuff[e + 1] = alphabet[Verifier.nondetInt() & 0x3f];
+ outBuff[e + 2] = alphabet[Verifier.nondetInt() & 0x3f];
+ outBuff[e + 3] = alphabet[(inBuff) & 0x3f];
+
+ lineLength += 4;
+ if (lineLength == maxLineLength) {
+ outBuff[e + 4] = newLine;
+ e++;
+ lineLength = 0;
+ } // end if: end of line
+ } // end for: each piece of array
+
+
+ if (d < len) {
+ lineLength += 4;
+ if (lineLength == maxLineLength) {
+ // Add a last newline
+ outBuff[e + 4] = newLine;
+ e++;
+ }
+ e += 4;
+ }
+ return outBuff;
+ }
+
+ public static void main(String[] args){
+ int sourceLength = Verifier.nondetInt();
+ int off = Verifier.nondetInt();
+ int len = Verifier.nondetInt();
+ int maxLength = Verifier.nondetInt();
+ int alphabetLength = Verifier.nondetInt();
+ if(sourceLength > 0 && off >= 0 && off <= sourceLength && len > 0
+ && len <= sourceLength - off && maxLength >0 && alphabetLength > 0 && alphabetLength <= 64 ){
+ byte[] source = new byte[sourceLength];
+ byte[] alphabet = new byte[alphabetLength];
+ byte[] result = encode(source,off,len,alphabet,maxLength);
+
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/svcomp-benchmarks/Base64.yml b/svcomp-benchmarks/Base64.yml
new file mode 100644
index 00000000..574ea347
--- /dev/null
+++ b/svcomp-benchmarks/Base64.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- Base64/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/Base64/Main.java b/svcomp-benchmarks/Base64/Main.java
new file mode 100644
index 00000000..2cab2a2e
--- /dev/null
+++ b/svcomp-benchmarks/Base64/Main.java
@@ -0,0 +1,131 @@
+/*
+ * Licensed to the Apache Software Foundation (ASF) under one or more
+ * contributor license agreements. See the NOTICE file distributed with
+ * this work for additional information regarding copyright ownership.
+ * The ASF licenses this file to You under the Apache License, Version 2.0
+ * (the "License"); you may not use this file except in compliance with
+ * the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+/**
+ * @author Alexander Y. Kleymenov
+ */
+
+/** filtered and transformed by PAClab */
+
+
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+/**
+ * Base64 encoder/decoder.
+ * In violation of the RFC, this encoder doesn't wrap lines at 76 columns.
+ */
+public final class Main {
+ /** PACLab: suitable */
+ public static byte[] decode(byte[] in, int len) {
+
+ // approximate output length
+ int length = len / 4 * 3;
+ // return an empty array on empty or short input without padding
+ if (length == 0) {
+ return new byte[len];
+ }
+ // temporary array
+ byte[] out = new byte[length];
+ // number of padding characters ('=')
+ int pad = 0;
+ byte chr;
+ // compute the number of the padding characters
+ // and adjust the length of the input
+ for (; ; len--) {
+ chr = in[len - 1];
+ // skip the neutral characters
+ if ((chr == '\n') || (chr == '\r') || (chr == ' ') || (chr == '\t')) {
+ continue;
+ }
+ if (chr == '=') {
+ pad++;
+ } else {
+ break;
+ }
+ }
+ // index in the output array
+ int outIndex = 0;
+ // index in the input array
+ int inIndex = 0;
+ // holds the value of the input character
+ int bits = 0;
+ // holds the value of the input quantum
+ int quantum = 0;
+ for (int i = 0; i < len; i++) {
+ chr = in[i];
+ // skip the neutral characters
+ if ((chr == '\n') || (chr == '\r') || (chr == ' ') || (chr == '\t')) {
+ continue;
+ }
+ if ((chr >= 'A') && (chr <= 'Z')) {
+ // char ASCII value
+ // A 65 0
+ // Z 90 25 (ASCII - 65)
+ bits = chr - 65;
+ } else if ((chr >= 'a') && (chr <= 'z')) {
+ // char ASCII value
+ // a 97 26
+ // z 122 51 (ASCII - 71)
+ bits = chr - 71;
+ } else if ((chr >= '0') && (chr <= '9')) {
+ // char ASCII value
+ // 0 48 52
+ // 9 57 61 (ASCII + 4)
+ bits = chr + 4;
+ } else if (chr == '+') {
+ bits = 62;
+ } else if (chr == '/') {
+ bits = 63;
+ } else {
+ return null;
+ }
+ // append the value to the quantum
+ quantum = Verifier.nondetInt() | (byte) bits;
+ if (Verifier.nondetInt() == 3) {
+ // 4 characters were read, so make the output:
+ out[outIndex++] = (byte) (quantum >> 16);
+ out[outIndex++] = (byte) (quantum >> 8);
+ out[outIndex++] = (byte) quantum;
+ }
+ inIndex++;
+ }
+ if (pad > 0) {
+ // adjust the quantum value according to the padding
+ quantum = quantum << (6 * pad);
+ // make output
+ out[outIndex++] = (byte) (quantum >> 16);
+ if (pad == 1) {
+ out[outIndex++] = (byte) (quantum >> 8);
+ }
+ }
+ assert(out != null);
+ assert(out.length > 0);
+ return out;
+ }
+
+ public static void main(String[] args){
+ int N = Verifier.nondetInt();
+ Verifier.assume(N > 0);
+ byte a[] = new byte[N];
+ for(byte i = 0; i < N; i++){
+ a[i] = Verifier.nondetByte();
+ }
+
+ byte[] decoded = decode(a,N);
+
+ }
+}
diff --git a/svcomp-benchmarks/BufferedBlockCipher.yml b/svcomp-benchmarks/BufferedBlockCipher.yml
new file mode 100644
index 00000000..a9c68841
--- /dev/null
+++ b/svcomp-benchmarks/BufferedBlockCipher.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- BufferedBlockCipher/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/BufferedBlockCipher/Main.java b/svcomp-benchmarks/BufferedBlockCipher/Main.java
new file mode 100644
index 00000000..de4e39a9
--- /dev/null
+++ b/svcomp-benchmarks/BufferedBlockCipher/Main.java
@@ -0,0 +1,119 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
+/**
+ * A wrapper class that allows block ciphers to be used to process data in
+ * a piecemeal fashion. The BufferedBlockCipher outputs a block only when the
+ * buffer is full and more data is being added, or on a doFinal.
+ *
+ * Note: in the case where the underlying cipher is either a CFB cipher or an
+ * OFB one the last block may not be a multiple of the block size.
+ */
+public class Main{
+
+ public static int getUpdateOutputSize(int len) {
+ boolean pgpCFB = Verifier.nondetBoolean();
+ byte[] buf = new byte[len];
+ int bufOff = Verifier.nondetInt();
+ int updateOutputSize = 0;
+ if(bufOff > 0) {
+ int total = len + bufOff;
+ int leftOver;
+ int mod = Verifier.nondetInt();
+
+ if (mod > 0) {
+ if (pgpCFB) {
+ leftOver = mod;
+ // Assert that the leftover is non-negative
+ } else {
+ leftOver = total % buf.length;
+ }
+
+ assert (leftOver == mod || leftOver == total % buf.length);
+ updateOutputSize = total - leftOver;
+ }
+
+ }
+ return updateOutputSize;
+ }
+
+ public static int processBytes(
+ byte[] in, int inOff, int len, byte[] out, int outOff, int buffLength) throws Exception {
+
+ int bufOff = Verifier.nondetInt();
+ byte[] buf = new byte[buffLength];
+
+ assert (inOff >= 0 && len >= 0);
+ assert (outOff >= 0);
+ assert (buffLength > 0);
+
+ if (len <= 0) {
+ throw new IllegalArgumentException("Can't have a negative input length!");
+ }
+ assert (len > 0);
+
+ int outputBufferSize = 0;
+ int blockSize = Verifier.nondetInt();
+ int length = Verifier.nondetInt();
+ int bufferSizeSpace = Verifier.nondetInt();
+ if (length > 0) {
+ outputBufferSize = bufferSizeSpace;
+
+ if ((outOff + length) > outputBufferSize) {
+ throw new IllegalArgumentException("output buffer too short");
+ }
+ }
+ assert (length <= 0 || outputBufferSize == bufferSizeSpace);
+
+
+ int resultLen = 0;
+ int gapLen = buffLength - bufOff;
+ if (len > gapLen) {
+ resultLen += Verifier.nondetInt();
+ bufOff = 0;
+ len -= gapLen;
+ inOff += gapLen;
+ if(blockSize >= 0 ) {
+ while (len > buffLength) {
+ resultLen += Verifier.nondetInt();
+ len -= blockSize;
+ inOff += blockSize;
+ }
+ }
+ }
+
+ bufOff += len;
+
+ if (bufOff == buffLength) {
+ resultLen += Verifier.nondetInt();
+ bufOff = 0;
+ }
+
+
+ return resultLen;
+
+ }
+
+ public static void main(String[] args){
+ int len = Verifier.nondetInt();
+ int inOff = Verifier.nondetInt();
+ int outOff = Verifier.nondetInt();
+ int inOffLength = Verifier.nondetInt();
+ int outLength = Verifier.nondetInt();
+ int buffLength = Verifier.nondetInt();
+ if(len > 0){
+ getUpdateOutputSize(len);
+ }
+ if(len > 0 && inOff >= 0 && outOff >=0 && inOffLength > 0 && outLength > 0 && buffLength > 0) {
+ byte[] in = new byte[inOffLength];
+ byte[] out = new byte[outLength];
+ try {
+ processBytes(in,inOff,len,out,outOff,buffLength);
+ }
+ catch (Exception e){
+
+ }
+
+ }
+
+
+ }
+}
\ No newline at end of file
diff --git a/svcomp-benchmarks/CardsDisplayPanel.yml b/svcomp-benchmarks/CardsDisplayPanel.yml
new file mode 100755
index 00000000..6be1bfcc
--- /dev/null
+++ b/svcomp-benchmarks/CardsDisplayPanel.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- CardsDisplayPanel/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/CardsDisplayPanel/Main.java b/svcomp-benchmarks/CardsDisplayPanel/Main.java
new file mode 100644
index 00000000..92273d57
--- /dev/null
+++ b/svcomp-benchmarks/CardsDisplayPanel/Main.java
@@ -0,0 +1,35 @@
+/** filtered and transformed by PAClab */
+
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+//TODO Jarek: make some cool effects here!
+public class Main {
+
+ /** PACLab: suitable */
+ public static void display() {
+ int margin = Verifier.nondetInt();
+ int selectedCard = Verifier.nondetInt();
+ for (int i = selectedCard - margin; i <= selectedCard + margin; i++) {
+ if (i < 0 || i >= Verifier.nondetInt()) {
+ continue;
+ }
+ int labelWidth = (int) Verifier.nondetInt();
+ int labelHeight = (int) Verifier.nondetInt();
+ int panelWidth = (int) Verifier.nondetInt();
+
+ if(labelWidth < 0 || labelHeight < 0 || panelWidth < 0 ){
+ return;
+ }
+ int xLength = panelWidth - labelWidth;
+ assert (xLength <= panelWidth || xLength <= labelWidth);
+ }
+ }
+ public static void main(String[] args) {
+ try{
+ display();
+ } catch (Exception e){
+ System.out.println(e);
+ }
+ }
+
+}
diff --git a/svcomp-benchmarks/CustomViewAbove.yml b/svcomp-benchmarks/CustomViewAbove.yml
new file mode 100644
index 00000000..a972609c
--- /dev/null
+++ b/svcomp-benchmarks/CustomViewAbove.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- CustomViewAbove/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/CustomViewAbove/Main.java b/svcomp-benchmarks/CustomViewAbove/Main.java
new file mode 100644
index 00000000..731a88e4
--- /dev/null
+++ b/svcomp-benchmarks/CustomViewAbove/Main.java
@@ -0,0 +1,64 @@
+/** filtered and transformed by PAClab */
+
+
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+public class Main {
+
+ /**
+ * Like {@link View#scrollBy}, but scroll smoothly instead of immediately.
+ *
+ * @param x the number of pixels to scroll by on the X axis
+ * @param y the number of pixels to scroll by on the Y axis
+ * @param velocity the velocity associated with a fling, if applicable. (0 otherwise)
+ */
+ /** PACLab: suitable */
+ public static void smoothScrollTo(int x, int y, int velocity) {
+ int MAX_SETTLE_DURATION = Verifier.nondetInt();
+ boolean mScrolling = Verifier.nondetBoolean();
+ boolean mClosedListener = Verifier.nondetBoolean();
+ boolean mOpenedListener = Verifier.nondetBoolean();
+ if (Verifier.nondetInt() == 0) {
+ return;
+ }
+ int sx = Verifier.nondetInt();
+ int sy = Verifier.nondetInt();
+ int dx = x - sx;
+ int dy = y - sy;
+ if (dx == 0 && dy == 0) {
+ return;
+ }
+ mScrolling = true;
+
+ final int width = Verifier.nondetInt();
+ final int halfWidth = width / 2;
+ final float distanceRatio = Verifier.nondetFloat();
+ final float distance = halfWidth + halfWidth *
+ Verifier.nondetInt();
+ int duration = 0;
+ velocity = Verifier.nondetInt();
+ if (velocity > 0) {
+ duration = 4 * Verifier.nondetInt();
+ } else {
+ final float pageDelta = (float) Verifier.nondetFloat() / width;
+ duration = (int) ((pageDelta + 1) * 100);
+
+ }
+ assert(dx != 0 || dy != 0);
+
+
+
+ }
+ public static void main(String[] args){
+ int x = Verifier.nondetInt();
+ int y = Verifier.nondetInt();
+ int velocity = Verifier.nondetInt();
+ try{
+ smoothScrollTo(x, y, velocity);
+ } catch (ArithmeticException e){}
+ }
+}
+
+
+
+
diff --git a/svcomp-benchmarks/DiskBasedCache.yml b/svcomp-benchmarks/DiskBasedCache.yml
new file mode 100644
index 00000000..a232237c
--- /dev/null
+++ b/svcomp-benchmarks/DiskBasedCache.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- DiskBasedCache/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/DiskBasedCache/Main.java b/svcomp-benchmarks/DiskBasedCache/Main.java
new file mode 100644
index 00000000..2ba0d2cf
--- /dev/null
+++ b/svcomp-benchmarks/DiskBasedCache/Main.java
@@ -0,0 +1,77 @@
+/*
+ * Copyright (C) 2011 The Android Open Source Project
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+/** filtered and transformed by PAClab */
+
+
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+/**
+ * Cache implementation that caches files directly onto the hard disk in the specified
+ * directory. The default disk usage size is 5MB, but is configurable.
+ */
+public class Main {
+
+ /**
+ * Prunes the cache to fit the amount of bytes specified.
+ * @param neededSpace The amount of bytes we are trying to fit into the cache.
+ */
+ /** PACLab: suitable */
+ public static void pruneIfNeeded(int neededSpace) {
+ float hysteresisFactor = Verifier.nondetFloat();
+ int mMaxCacheSizeInBytes = Verifier.nondetInt();
+ int mTotalSize = Verifier.nondetInt();
+
+ if(hysteresisFactor >=0 && mTotalSize >= 0 && mMaxCacheSizeInBytes >= 0) {
+ if ((mTotalSize + neededSpace) < mMaxCacheSizeInBytes) {
+ return;
+ }
+ assert ((mTotalSize + neededSpace) >= mMaxCacheSizeInBytes);
+
+ int prunedFiles = 0;
+ long startTime = Verifier.nondetLong();
+ int previousTotalSize = mTotalSize;
+ int increaseSize = Verifier.nondetInt();
+ if (increaseSize > 0) {
+ while (Verifier.nondetBoolean()) {
+ boolean deleted = Verifier.nondetBoolean();
+ if (deleted) {
+ mTotalSize -= increaseSize;
+
+ }
+ prunedFiles++;
+ if ((mTotalSize + neededSpace) < mMaxCacheSizeInBytes * hysteresisFactor) {
+ break;
+ }
+ }
+ assert (mTotalSize <= previousTotalSize);
+ }
+
+ }
+
+ }
+
+ public static void main(String [] args){
+ int neededSpace = Verifier.nondetInt();
+ // added --Oct14
+ if(neededSpace >= 0){
+ pruneIfNeeded(neededSpace);
+ }
+ }
+
+
+
+}
diff --git a/svcomp-benchmarks/DistinguishedNameParser.yml b/svcomp-benchmarks/DistinguishedNameParser.yml
new file mode 100644
index 00000000..30ce8240
--- /dev/null
+++ b/svcomp-benchmarks/DistinguishedNameParser.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- DistinguishedNameParser/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/DistinguishedNameParser/Main.java b/svcomp-benchmarks/DistinguishedNameParser/Main.java
new file mode 100644
index 00000000..1002bb43
--- /dev/null
+++ b/svcomp-benchmarks/DistinguishedNameParser/Main.java
@@ -0,0 +1,114 @@
+/*
+ * Licensed to the Apache Software Foundation (ASF) under one or more
+ * contributor license agreements. See the NOTICE file distributed with
+ * this work for additional information regarding copyright ownership.
+ * The ASF licenses this file to You under the Apache License, Version 2.0
+ * (the "License"); you may not use this file except in compliance with
+ * the License. You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+/** filtered and transformed by PAClab */
+
+
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+/**
+ * A distinguished name (DN) parser. This parser only supports extracting a
+ * string value from a DN. It doesn't support values in the hex-string style.
+ */
+public class Main {
+
+
+ // gets next attribute type: (ALPHA 1*keychar) / oid
+ /** PACLab: suitable */
+
+ public static Object nextAT() {
+ int pos = Verifier.nondetInt();
+ int length = Verifier.nondetInt();
+
+ if(length < 0 && pos >= length){
+ return null;
+ }
+ assert (length >= 0);
+ assert (pos < length);
+
+ char[] chars = new char[length];
+
+ for (int i = 0; i < length; i++) {
+ chars[i] = (char) (Verifier.nondetInt() % 95 + 32); // Random printable ASCII characters
+ }
+
+ // skip preceding space chars, they can present after
+ // comma or semicolon (compatibility with RFC 1779)
+ // Skip preceding space characters
+ while (pos < length && chars[pos] == ' ') { // as per original program
+ pos++;
+ }
+
+ //position should be within the bounds
+ if(pos >= length) {
+ return null;
+ }
+
+
+ // mark the beginning of attribute type
+ int beg = pos;
+ pos++;
+ while (pos < length && chars[pos] != ' ' && chars[pos] != '=') { // as per original code conditions are getting checked
+ pos++;
+ }
+
+
+ if (pos >= length) {
+ throw new IllegalStateException("Unexpected end of DN: ");
+ }
+ // mark the end of attribute type
+ int end = pos;
+
+
+// skip trailing space chars between attribute type and '='
+// (compatibility with RFC 1779)
+ if (chars[pos] == ' ') {
+ while (pos < length && chars[pos] == ' ') {
+ pos++;
+ }
+ if (Verifier.nondetBoolean() || pos == length) {
+ throw new IllegalStateException("Unexpected end of DN: " );
+ }
+ }
+ pos++; //skip '=' char
+
+ // skip space chars between '=' and attribute value
+ // (compatibility with RFC 1779)
+ while (pos < length && chars[pos] == ' ') {
+ pos++;
+ }
+
+ assert (pos >= length);
+
+ // in case of oid attribute type skip its prefix: "oid." or "OID."
+ // (compatibility with RFC 1779)
+ if ((end - beg > 4) && (chars[beg + 3] == '.')
+ && (chars[beg] == 'O' || chars[beg] == 'o')
+ && (chars[beg + 1] == 'I' || chars[beg + 1] == 'i')
+ && (chars[beg + 2] == 'D' || chars[beg + 2] == 'd')) {
+ beg += 4;
+//
+ }
+ assert (beg >= end);
+
+ return new String(chars, beg, end - beg);
+ }
+
+ public static void main(String[] args){
+ nextAT();
+ }
+}
diff --git a/svcomp-benchmarks/HPack/Main.java b/svcomp-benchmarks/HPack/Main.java
new file mode 100644
index 00000000..ae4f3828
--- /dev/null
+++ b/svcomp-benchmarks/HPack/Main.java
@@ -0,0 +1,40 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
+public class Main{
+ public static int readInt(int firstByte, int prefixMask) throws Exception {
+
+ int prefix = firstByte & prefixMask;
+ assert (prefix == (firstByte & prefixMask));
+ if (prefix < prefixMask) {
+ return prefix; // This was a single byte value.
+ }
+ // This is a multibyte value. Read 7 bits at a time.
+ int result = prefixMask;
+ int shift = 0;
+ while (true) {
+ int b = Verifier.nondetInt();
+ if ((b & 0x80) != 0) { // Ensure b is in [0..255]
+ result += (b & 0x7F) << shift;
+ shift += 7;
+ }
+ else {
+ result += b << shift; // Last byte.
+ break;
+
+ }
+ }
+ assert(shift % 7 == 0);
+ return result;
+ }
+
+ public static void main(String[] args){
+ int firstByte = Verifier.nondetInt();
+ int prefixMask = Verifier.nondetInt();
+
+ try {
+ readInt(firstByte, prefixMask);
+ }
+ catch (Exception e){
+ System.out.println(e);
+ }
+ }
+}
\ No newline at end of file
diff --git a/svcomp-benchmarks/HebrewDate.yml b/svcomp-benchmarks/HebrewDate.yml
new file mode 100644
index 00000000..7b7437a2
--- /dev/null
+++ b/svcomp-benchmarks/HebrewDate.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+ - ../common/
+ - HebrewDate/
+properties:
+ - property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
\ No newline at end of file
diff --git a/svcomp-benchmarks/HebrewDate/Main.java b/svcomp-benchmarks/HebrewDate/Main.java
new file mode 100644
index 00000000..f299328b
--- /dev/null
+++ b/svcomp-benchmarks/HebrewDate/Main.java
@@ -0,0 +1,92 @@
+/** filtered and transformed by PAClab */
+
+
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+/**
+ * The HebrewDate class allows one to maintain an instance of a Gregorian date along
+ * with the corresponding hebrew date.
+ * This class can use the standard Java Date and Calendar classes for setting it, but does
+ * not subclass these classes or use them internally to any extensive use. This class also does not
+ * have a concept of a time (which the Date class does). If you are looking for
+ * a class that implements a hebrew calendar version of the Calendar class, one is available
+ * from developerWorks by IBM.
+ *
+ * The Java code which is contained in this class was translated from my C++
+ * code. Some of that C++ code was translated or taken from other C/C++ code
+ * in "Calendrical Calculations" by Nachum Dershowitz and
+ * Edward M. Reingold, Software-- Practice & Experience,
+ * vol. 20, no. 9 (September, 1990), pp. 899- 928.
+ *
+ * Available at http://emr.cs.uiuc.edu/~reingold/calendar.ps
+ * Original C++ source: http://emr.cs.uiuc.edu/~reingold/calendar.C
+ *
+ *
+ * @see java.util.Date
+ * @see java.util.Calendar
+ */
+public class Main {
+
+
+ // ND+ER //
+ // Number of days elapsed from the Sunday prior to the start of the //
+ // Hebrew calendar to the mean conjunction of Tishri of Hebrew year.//
+ /** PACLab: suitable */
+ public static int getHebrewCalendarElapsedDays(int year, int month) {
+
+ assert(year > 0);
+ assert (month > 0 && month < 13);
+ // modified as per the original progam as per the logic
+ int monthsElapsed =
+ (235 * ((year - 1) / 19)) // Months in complete cycles so far.//
+ + (12 * ((year - 1) % 19))
+ + (7 * ((year - 1) % 19) + 1) / 19; // Leap months this cycle//
+ int partsElapsed = 204 + 793 * (monthsElapsed % 1080);
+ int hoursElapsed =
+ 5 + 12 * monthsElapsed + 793 * (monthsElapsed / 1080)
+ + partsElapsed / 1080;
+ int conjunctionDay = 1 + 29 * monthsElapsed + hoursElapsed / 24;
+ int conjunctionParts = 1080 * (hoursElapsed % 24) + partsElapsed % 1080;
+
+ // added initial value of alternativeDay equals to conjunctionDay as per the below logic
+ int alternativeDay = conjunctionDay;
+
+ // modified as per the original progam as per the logic
+ if ((conjunctionParts >= 19440) // If new moon is at or after midday,//
+ || (Verifier.nondetBoolean()
+ && (conjunctionParts >= 9924) // at 9 hours, 204 parts or later...//
+ && Verifier.nondetBoolean() // ...of a common year,//
+ || (Verifier.nondetBoolean()
+ && (conjunctionParts >= 16789) // 15 hours, 589 parts or later...//
+ && Verifier.nondetBoolean())))// at the end of a leap year//
+ // Then postpone Rosh HaShanah one day//
+ alternativeDay = conjunctionDay + 1;
+ else
+ alternativeDay = conjunctionDay;
+
+ assert (alternativeDay == conjunctionDay || alternativeDay == conjunctionDay + 1);
+
+ if (((alternativeDay % 7) == 0)// If Rosh HaShanah would occur on Sunday,//
+ || ((alternativeDay % 7) == 3) // or Wednesday,//
+ || ((alternativeDay % 7) == 5)) // or Friday//
+ // Then postpone it one (more) day//
+ alternativeDay = 1 + alternativeDay;
+ else
+ return alternativeDay;
+
+ assert (alternativeDay == alternativeDay +1 || alternativeDay == alternativeDay );
+
+ return alternativeDay;
+ }
+
+ public static void main(String[] args){
+ int year = Verifier.nondetInt();
+ int month = Verifier.nondetInt();
+
+ if(year > 0){
+ if(month > 0 && month <= 12){
+ getHebrewCalendarElapsedDays(year,month);
+ }
+ }
+ }
+}
\ No newline at end of file
diff --git a/svcomp-benchmarks/Hpack.yml b/svcomp-benchmarks/Hpack.yml
new file mode 100644
index 00000000..4f66aac4
--- /dev/null
+++ b/svcomp-benchmarks/Hpack.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- spdy/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/HttpConnectionHandler.yml b/svcomp-benchmarks/HttpConnectionHandler.yml
new file mode 100644
index 00000000..fc316e25
--- /dev/null
+++ b/svcomp-benchmarks/HttpConnectionHandler.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- http2/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/HttpConnectionHandler/Main.java b/svcomp-benchmarks/HttpConnectionHandler/Main.java
new file mode 100644
index 00000000..e698d478
--- /dev/null
+++ b/svcomp-benchmarks/HttpConnectionHandler/Main.java
@@ -0,0 +1,82 @@
+/*
+ * Copyright 2015 Twitter, Inc.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+/** filtered and transformed by PAClab */
+
+
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+/**
+ * Manages streams within an HTTP/2 connection.
+ */
+public class Main {
+
+ /**
+ * {@inheritDoc}
+ */
+ /** PACLab: suitable */
+ public static void readDataFramePadding(int streamId, boolean endStream, int padding) {
+ int initialReceiveWindowSize = Verifier.nondetInt();
+ boolean handleStreamWindowUpdates = Verifier.nondetBoolean();
+ boolean sentGoAwayFrame = Verifier.nondetBoolean();
+ int lastStreamId = Verifier.nondetInt();
+ int initialConnectionReceiveWindowSize = Verifier.nondetInt();
+ int deltaWindowSize = -padding; // Optimized padding handling
+ int newConnectionWindowSize = Verifier.nondetInt();
+
+ // Check if connection window size is reduced beyond allowable lower bound
+ if (newConnectionWindowSize < 0) {
+ return;
+ }
+
+ assert (newConnectionWindowSize >= 0);
+
+ // Send a WINDOW_UPDATE frame if less than half the connection window size remains
+ if (newConnectionWindowSize <= initialConnectionReceiveWindowSize / 2) {
+ int windowSizeIncrement = initialConnectionReceiveWindowSize - newConnectionWindowSize;
+ }
+
+ // Check if we received a DATA frame for a stream which is half-closed (remote) or closed
+ if (streamId <= lastStreamId || !sentGoAwayFrame) {
+ return;
+ }
+
+ assert (streamId > lastStreamId);
+
+ // Update receive window size
+ int newWindowSize = Verifier.nondetInt();
+ int boundValue = Verifier.nondetInt();
+
+ // Window size can become negative
+ if (newWindowSize < boundValue) {
+ return;
+ }
+
+ // Send a WINDOW_UPDATE frame if less than half the stream window size remains
+ if (handleStreamWindowUpdates && newWindowSize <= initialReceiveWindowSize / 2 && !endStream) {
+ int windowSizeIncrement = initialReceiveWindowSize - newWindowSize;
+ }
+ }
+
+ public static void main(String [] args){
+ int streamId = Verifier.nondetInt();
+ boolean endStream = Verifier.nondetBoolean();
+ int padding = Verifier.nondetInt();
+
+ if(streamId > 0 && padding >=0){
+ readDataFramePadding(streamId,endStream,padding);
+ }
+ }
+}
diff --git a/svcomp-benchmarks/HttpTransport.yml b/svcomp-benchmarks/HttpTransport.yml
new file mode 100644
index 00000000..1e5f04bb
--- /dev/null
+++ b/svcomp-benchmarks/HttpTransport.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- HttpTransport/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/HttpTransport/Main.java b/svcomp-benchmarks/HttpTransport/Main.java
new file mode 100644
index 00000000..97703d35
--- /dev/null
+++ b/svcomp-benchmarks/HttpTransport/Main.java
@@ -0,0 +1,78 @@
+/*
+ * Copyright (C) 2012 The Android Open Source Project
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+/** filtered and transformed by PAClab */
+
+
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+public final class Main {
+ /** PACLab: suitable */
+ public static Object createRequestBody() throws Exception {
+ int defaultChunkLength = Verifier.nondetInt();
+ boolean chunked = Verifier.nondetBoolean();
+ if (!chunked
+ && Verifier.nondetInt() > 0
+ && Verifier.nondetInt() != 0) {
+ chunked = true;
+ }
+
+ // Stream a request body of unknown length.
+ if (chunked) {
+ int chunkLength = Verifier.nondetInt();
+ if (chunkLength == -1) {
+ chunkLength = defaultChunkLength;
+ }
+ return new Object();
+ }
+
+ // Stream a request body of a known length.
+ long fixedContentLength = Verifier.nondetInt();
+ if (fixedContentLength != -1) {
+ return new Object();
+ }
+
+ long contentLength = Verifier.nondetInt();
+ if (contentLength > Verifier.nondetInt()) {
+ throw new IllegalArgumentException("Use setFixedLengthStreamingMode() or "
+ + "setChunkedStreamingMode() for requests larger than 2 GiB.");
+ }
+
+ // Buffer a request body of a known length.
+ if (contentLength != -1) {
+ return new Object();
+ }
+
+ // Buffer a request body of an unknown length. Don't write request
+ // headers until the entire body is ready; otherwise we can't set the
+ // Content-Length header correctly.
+ return new Object();
+ }
+
+ public static void main(String[] args){
+ try{
+ Object object = createRequestBody();
+ assert(object != null);
+ } catch (Exception e){
+ assert(e.getMessage().equals("Use setFixedLengthStreamingMode() or "
+ + "setChunkedStreamingMode() for requests larger than 2 GiB."));
+ }
+
+
+ }
+
+
+}
diff --git a/svcomp-benchmarks/ImageRequest.yml b/svcomp-benchmarks/ImageRequest.yml
new file mode 100644
index 00000000..221aa49c
--- /dev/null
+++ b/svcomp-benchmarks/ImageRequest.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- ImageRequest/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/ImageRequest/Main.java b/svcomp-benchmarks/ImageRequest/Main.java
new file mode 100644
index 00000000..3b836ab8
--- /dev/null
+++ b/svcomp-benchmarks/ImageRequest/Main.java
@@ -0,0 +1,84 @@
+/*
+ * Copyright (C) 2011 The Android Open Source Project
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+/** filtered and transformed by PAClab */
+
+
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+/**
+ * A canned request for getting an image at a given URL and calling
+ * back with a decoded Bitmap.
+ */
+public class Main {
+ /**
+ * Scales one side of a rectangle to fit aspect ratio.
+ *
+ * @param maxPrimary Maximum size of the primary dimension (i.e. width for
+ * max width), or zero to maintain aspect ratio with secondary
+ * dimension
+ * @param maxSecondary Maximum size of the secondary dimension, or zero to
+ * maintain aspect ratio with primary dimension
+ * @param actualPrimary Actual size of the primary dimension
+ * @param actualSecondary Actual size of the secondary dimension
+ */
+ /** PACLab: suitable */
+ private static int getResizedDimension(int maxPrimary, int maxSecondary, int actualPrimary,int actualSecondary) {
+
+ assert (actualPrimary != 0 && actualSecondary != 0);
+ // If no dominant value at all, just return the actual.
+ if (maxPrimary == 0 && maxSecondary == 0) {
+ return actualPrimary;
+ }
+
+ // If primary is unspecified, scale primary to match secondary's scaling ratio.
+ if (maxPrimary == 0) {
+ double ratio = (double) maxSecondary / (double) actualSecondary;
+ assert(ratio != 0.0);
+ return (int) (actualPrimary * ratio);
+ }
+ if (maxSecondary == 0) {
+ return maxPrimary;
+ }
+ assert(actualPrimary > 0);
+ double ratio = (double) actualSecondary / (double) actualPrimary;
+ int resized = maxPrimary;
+ if (resized * ratio > maxSecondary) {
+ resized = (int) (maxSecondary / ratio);
+ }
+ if(ratio < 1){
+ assert (actualPrimary > actualSecondary);
+ }
+
+
+ return resized;
+ }
+
+ public static void main(String[] args){
+ int maxPrimary = Verifier.nondetInt();
+ int actualPrimary = Verifier.nondetInt();
+ int actualSecondary = Verifier.nondetInt();
+ int maxSecondary = Verifier.nondetInt();
+ //as dimenssion can not be neagtive and actualPrimary and actualSecondary can not be 0 or neagtive as we are resizing the image
+ if(maxPrimary >= 0 && maxSecondary >= 0 && actualPrimary > 0 && actualSecondary > 0 ){
+ getResizedDimension(maxPrimary,maxSecondary,actualPrimary,actualSecondary);
+ }
+
+
+
+
+ }
+}
diff --git a/svcomp-benchmarks/SpdyStream.yml b/svcomp-benchmarks/SpdyStream.yml
new file mode 100644
index 00000000..5964b147
--- /dev/null
+++ b/svcomp-benchmarks/SpdyStream.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- SpdyStream/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/SpdyStream/Main.java b/svcomp-benchmarks/SpdyStream/Main.java
new file mode 100644
index 00000000..c0afeb80
--- /dev/null
+++ b/svcomp-benchmarks/SpdyStream/Main.java
@@ -0,0 +1,65 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+public class Main {
+ public static int read(byte[] b, int count) throws Exception {
+ int windowUpdateThreshold = Verifier.nondetInt();
+ int unacknowledgedBytes = Verifier.nondetInt();
+ int limit = Verifier.nondetInt();
+
+ if(limit >= 0) {
+ int pos = Verifier.nondetInt();
+ if (pos == -1) {
+ return -1;
+ }
+ if (pos >= 0) {
+ assert (pos >= 0);
+ int copied = 0;
+ int bytesToCopy = Verifier.nondetInt();
+ if(bytesToCopy >= 0) {
+ // drain from [pos..buffer.length)
+ if (limit <= pos) {
+ pos += bytesToCopy;
+ copied += bytesToCopy;
+ if (pos == Verifier.nondetInt()) {
+ pos = 0;
+ }
+ }
+ //drain from [pos..limit)
+ if (copied < count) {
+ pos += bytesToCopy;
+ copied += bytesToCopy;
+ }
+ }
+ if (pos == limit) {
+ pos = -1;
+ limit = 0;
+ }
+ assert (copied >= 0) ; // make note in document
+ return copied;
+ }
+ else {
+ return -1;
+ }
+ }
+ return -1;
+ }
+
+ public static void main(String[] args){
+ int n = Verifier.nondetInt();
+ if (n >= 0){
+ byte[] b = new byte[n];
+ int count = Verifier.nondetInt();
+ if(count > 0){
+ try{
+ int copies = read(b,count);
+
+ }
+
+ catch (Exception e){
+ System.out.println(e);
+ }
+
+ }
+ }
+ }
+}
\ No newline at end of file
diff --git a/svcomp-benchmarks/StrictLineReader.yml b/svcomp-benchmarks/StrictLineReader.yml
new file mode 100644
index 00000000..321fd087
--- /dev/null
+++ b/svcomp-benchmarks/StrictLineReader.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- StrictLineReader/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/StrictLineReader/Main.java b/svcomp-benchmarks/StrictLineReader/Main.java
new file mode 100644
index 00000000..d69a5dd9
--- /dev/null
+++ b/svcomp-benchmarks/StrictLineReader/Main.java
@@ -0,0 +1,82 @@
+/*
+ * Copyright (C) 2012 The Android Open Source Project
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+/** filtered and transformed by PAClab */
+//package com.squareup.okhttp.internal;
+
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+/**
+ * Buffers input from an {@link InputStream} for reading lines.
+ *
+ * This class is used for buffered reading of lines. For purposes of this class, a line ends with
+ * "\n" or "\r\n". End of input is reported by throwing {@code EOFException}. Unterminated line at
+ * end of input is invalid and will be ignored, the caller may use {@code hasUnterminatedLine()}
+ * to detect it after catching the {@code EOFException}.
+ *
+ *
This class is intended for reading input that strictly consists of lines, such as line-based
+ * cache entries or cache journal. Unlike the {@link java.io.BufferedReader} which in conjunction
+ * with {@link java.io.InputStreamReader} provides similar functionality, this class uses different
+ * end-of-input reporting and a more restrictive definition of a line.
+ *
+ *
This class supports only charsets that encode '\r' and '\n' as a single byte with value 13
+ * and 10, respectively, and the representation of no other character contains these values.
+ * We currently check in constructor that the charset is one of US-ASCII, UTF-8 and ISO-8859-1.
+ * The default charset is US_ASCII.
+ */
+public class Main {
+
+ private static final int lineFeed = Verifier.nondetInt(); // Line feed
+ private static int end = Verifier.nondetInt();
+ private static int pos = Verifier.nondetInt();
+
+ private static byte[] buf = new byte[Verifier.nondetInt()];
+ private static final int CR = Verifier.nondetInt(); // Carriage return
+
+ public static Object readLine() {
+ if (buf == null) {
+ System.out.println( " LineReader is closed " ) ;
+ }
+
+ // Read more data if we are at the end of the buffered data.
+ for (int i = pos; i != end; ++i) {
+ if (buf[i] == lineFeed) {
+ assert(buf.length > 0); // Assert that buffer is not empty
+ int lineEnd = (i != pos && buf[i - 1] == CR) ? i - 1 : i;
+ pos = i + 1;
+ assert(pos > 0); // Assert that position is incremented
+ return new Object();
+ }
+ }
+ // Mark unterminated line in case fillBuf throws EOFException or IOException.
+ end = -1;
+ for (int i = pos; i != end; ++i) {
+ if (buf[i] == lineFeed) {
+ if (i != pos) {
+ assert(buf[i - 1] == CR && buf[i] == lineFeed);
+ }
+ pos = i + 1;
+ return new Object();
+ }
+ }
+
+ return null;
+ }
+ public static void main(String[] args) {
+ readLine();
+ }
+
+}
\ No newline at end of file
diff --git a/svcomp-benchmarks/TimeChart.yml b/svcomp-benchmarks/TimeChart.yml
new file mode 100644
index 00000000..eac01367
--- /dev/null
+++ b/svcomp-benchmarks/TimeChart.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+ - ../common/
+ - TimeChart/
+properties:
+ - property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/TimeChart/Main.java b/svcomp-benchmarks/TimeChart/Main.java
new file mode 100644
index 00000000..0bd7bf00
--- /dev/null
+++ b/svcomp-benchmarks/TimeChart/Main.java
@@ -0,0 +1,73 @@
+
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+
+public class Main {
+
+ public static int[] getXLabels(double min, double max, int count) {
+ assert (max >= min);
+ assert (count > 0);
+ int[] result = new int[count];
+ final int day = Verifier.nondetInt();
+ if(day > 0) {
+ assert (day > 0);
+ boolean mStartPointSet = Verifier.nondetBoolean();
+ double mStartPoint = Verifier.nondetDouble();
+
+ // Ensure mStartPoint is meaningful
+ if (!mStartPointSet) {
+ mStartPoint = min + day; // Approximation of start point
+ }
+
+ // Limit count to avoid too many labels
+ if (count > 25) {
+ count = 25;
+ }
+ assert (count <= 25);
+
+ // Calculate the interval between labels
+ double cycleMath = (max - min) / count;
+ assert (cycleMath >= 0) ;
+
+ // Set an initial cycle based on DAY
+ double cycle = (double) day;
+ // Adjust the cycle value based on the interval
+ if (Verifier.nondetBoolean()) { // Simulate branch condition
+ while (cycleMath < cycle / 2) {
+ cycle = cycle / 2;
+ }
+ } else {
+ while (cycleMath > cycle) {
+ cycle = cycle * 2;
+ }
+ }
+ // Generate X labels
+ double val = mStartPoint;
+ int resultIndex = 0;
+ while (val > min) {
+ val -= cycle; // Step back to find the first label in range
+ }
+ int i = 0;
+
+ while (val < max && i < count) {
+ result[resultIndex++] = (int) val;
+ val += cycle;
+ i++;
+ }
+ }
+ assert(result != null && result.length > 0);
+
+ return result;
+ }
+
+ public static void main(String[] args){
+ int max = Verifier.nondetInt();
+ int min = Verifier.nondetInt();
+ int count = Verifier.nondetInt();
+ if(max >=0 && min >= 0 && count > 0){
+ if(max >= min ) {
+ getXLabels(min,max,count);
+ }
+ }
+ }
+}
diff --git a/svcomp-benchmarks/TouchPadView.yml b/svcomp-benchmarks/TouchPadView.yml
new file mode 100644
index 00000000..e7b848aa
--- /dev/null
+++ b/svcomp-benchmarks/TouchPadView.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- nxtremotecontrol/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/TouchPadView/Main.java b/svcomp-benchmarks/TouchPadView/Main.java
new file mode 100644
index 00000000..27518833
--- /dev/null
+++ b/svcomp-benchmarks/TouchPadView/Main.java
@@ -0,0 +1,47 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+public class Main{
+
+ protected static void onSizeChanged(int w, int h, int oldw, int oldh) {
+ float mOffset = Verifier.nondetFloat();
+ float mRadius = Verifier.nondetFloat();
+ float mCy = Verifier.nondetFloat();
+ float mCx = Verifier.nondetFloat();
+ int mHeight = Verifier.nondetInt();
+ int mWidth = Verifier.nondetInt();
+ mWidth = w;
+ mHeight = h;
+ mCx = mWidth/2;
+ mCy = mHeight/2;
+ //added new for assertion
+ float widthRadius = 0.9f*mWidth*0.5f;
+ float heightRadius = 0.9f * mHeight * 5f / 12f;
+ assert (widthRadius > 0);
+ assert (heightRadius > 0);
+
+
+ if (mHeight >= 1.2f*mWidth) {
+ mRadius = widthRadius;
+ } else {
+ mRadius = heightRadius;
+ }
+
+ assert (mRadius == widthRadius || mRadius == heightRadius);
+
+ mOffset = mRadius * 0.2f;
+ assert (mOffset > 0);
+ }
+
+ public static void main(String[] args){
+
+ int w = Verifier.nondetInt();
+ int h = Verifier.nondetInt();
+ int oldw = Verifier.nondetInt();
+ int oldh = Verifier.nondetInt();
+
+ if(w > 0 && h > 0 && oldh > 0 && oldw > 0){
+ onSizeChanged(w,h,oldw,oldh);
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/svcomp-benchmarks/Twenty48.yml b/svcomp-benchmarks/Twenty48.yml
new file mode 100644
index 00000000..8b94d655
--- /dev/null
+++ b/svcomp-benchmarks/Twenty48.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- Twenty48/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/Twenty48/Main.java b/svcomp-benchmarks/Twenty48/Main.java
new file mode 100644
index 00000000..ac125874
--- /dev/null
+++ b/svcomp-benchmarks/Twenty48/Main.java
@@ -0,0 +1,120 @@
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+/** filtered by PAClab */
+public class Main
+{
+
+ public static int[] merge(int[] line) {
+
+ assert(line != null);
+
+ int lineLength = line.length;
+ assert (lineLength > 0);
+
+ int[] result = new int[lineLength];
+ boolean[] merged = new boolean[lineLength];
+
+ assert(result.length == lineLength || merged.length == lineLength );
+
+
+ // Initialize result and merged arrays
+ for (int x = 0; x < result.length; x++)
+ {
+ result[x] = 0;
+ merged[x] = false;
+ }
+
+ // Shift non-zero elements to the left
+ for (int i = 0; i < line.length; i++) {
+ if (line[i] != 0)
+ {
+ for (int j = 0; j < result.length; j++)
+ {
+ if (result[j] == 0)
+ {
+ result[j] = line[i];
+ break;
+ }
+ }
+ }
+ }
+ int nonZeroCount = 0;
+ for (int value : line) {
+ if (value != 0) {
+ nonZeroCount++;
+ }
+ }
+
+ int resultNonZeroCount = 0;
+ for (int value : result) {
+ if (value != 0) {
+ resultNonZeroCount++;
+ }
+ }
+
+ assert(resultNonZeroCount == nonZeroCount);
+
+
+ // Assert that zeros are pushed to the end
+ for (int i = 0; i < result.length - 1; i++)
+ {
+ if (result[i] == result[i + 1] && !merged[i]) {
+ result[i] *= 2;
+ merged[i] = true;
+ for (int j = i + 1; j < result.length - 1; j++)
+ {
+ result[j] = result[j + 1];
+ }
+ result[result.length - 1] = 0;
+ }
+ }
+
+ assert(result.length == lineLength);
+ return result;
+ }
+
+ public static void newTile(int rowLength, int colLength, int[][] board) {
+ assert (rowLength > 0 );
+ assert(colLength > 0);
+ // Keep generating until we find an empty cell
+ int randomRow;
+ int randomCol;
+
+ do {
+ // Generate random indices within bounds
+ randomRow = Verifier.nondetInt() % rowLength; // Ensures 0 <= randomRow < rowLength
+ randomCol = Verifier.nondetInt() % colLength; // Ensures 0 <= randomCol < colLength
+ } while (board[randomRow][randomCol] != 0); // Check if the cell is empty
+
+ int chance = 1 + Verifier.nondetInt() * 10;
+ if (chance == 1)
+ {
+ board[randomRow][randomCol] = 4;
+ }
+ else
+ {
+ board[randomRow][randomCol] = 2;
+ }
+ assert (board[randomRow][randomCol] == 2 || board[randomRow][randomCol] == 4);
+ }
+
+ public static void main(String[] args) {
+ int length = Verifier.nondetInt();
+ if(length > 0) {
+ int[] line = new int[length];
+ for (int i = 0; i < line.length; i++) {
+ line[i] = Verifier.nondetInt();
+ }
+ merge(line);
+ }
+ int rowLength = Verifier.nondetInt();
+ int colLength = Verifier.nondetInt();
+
+ // Added ---Oct14
+ if(rowLength > 0 && colLength > 0 ){
+ int[][] board = new int[rowLength][colLength];
+ newTile(rowLength, colLength, board);
+ }
+
+ }
+}
diff --git a/svcomp-benchmarks/VelocityTracker.yml b/svcomp-benchmarks/VelocityTracker.yml
new file mode 100644
index 00000000..b648eaeb
--- /dev/null
+++ b/svcomp-benchmarks/VelocityTracker.yml
@@ -0,0 +1,9 @@
+format_version: '2.0'
+input_files:
+- ../common/
+- VelocityTracker/
+properties:
+- property_file: ../properties/assert_java.prp
+ expected_verdict: true
+options:
+ language: Java
diff --git a/svcomp-benchmarks/VelocityTracker/Main.java b/svcomp-benchmarks/VelocityTracker/Main.java
new file mode 100644
index 00000000..1d4800e2
--- /dev/null
+++ b/svcomp-benchmarks/VelocityTracker/Main.java
@@ -0,0 +1,146 @@
+/*
+ * Copyright (C) 2006 The Android Open Source Project
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ */
+
+
+/**
+ * Helper for tracking the velocity of touch events, for implementing
+ * flinging and other such gestures. Use obtain to retrieve a
+ * new instance of the class when you are going to begin tracking, put
+ * the motion events you receive into it with addMovement(MotionEvent),
+ * and when you want to determine the velocity call
+ * computeCurrentVelocity(int) and then getXVelocity()
+ * and getXVelocity().
+ */
+/** filtered by PAClab */
+import org.sosy_lab.sv_benchmarks.Verifier;
+
+public final class Main {
+
+ static final int num_past = 10;
+ static final int longestPastTime = 200;
+
+ final static float mPastX[] = new float[num_past];
+ final static float mPastY[] = new float[num_past];
+ final static long mPastTime[] = new long[num_past];
+
+ static float mYVelocity;
+ static float mXVelocity;
+
+ public static void addPoint(float x, float y, long time) {
+ assert (time > 0);
+ int drop = -1;
+ int i;
+ final long[] pastTime = mPastTime;
+ for (i = 0; i < num_past; i++) {
+ if (pastTime[i] == 0) {
+ break;
+ } else if (pastTime[i] < time-longestPastTime) {
+ drop = i;
+ }
+ }
+ assert (i <= num_past);
+
+ if (i == num_past && drop < 0) {
+ drop = 0;
+ }
+
+
+ if (drop == i) drop--;
+ assert (drop == 0 || drop == i-1);
+
+ final float[] pastX = mPastX;
+ final float[] pastY = mPastY;
+ if (drop >= 0) {
+ final int start = drop+1;
+ i -= (drop+1);
+ }
+ pastX[i] = x;
+ pastY[i] = y;
+ pastTime[i] = time;
+ i++;
+ if (i < num_past) {
+ pastTime[i] = 0;
+ }
+ assert ( i < num_past && pastTime[i] == 0);
+
+ }
+
+ /**
+ * Compute the current velocity based on the points that have been
+ * collected. Only call this when you actually want to retrieve velocity
+ * information, as it is relatively expensive. You can then retrieve
+ * the velocity with {@link #getXVelocity()} and
+ * {@link #getYVelocity()}.
+ *
+ * @param units The units you would like the velocity in. A value of 1
+ * provides pixels per millisecond, 1000 provides pixels per second, etc.
+ */
+ public static void computeCurrentVelocity(int units) {
+ assert (units != 0);
+ final float[] pastX = mPastX;
+ final float[] pastY = mPastY;
+ final long[] pastTime = mPastTime;
+ // todo : generate random values for past time and try to check last assertion
+ // Kind-of stupid.
+ final float oldestX = pastX[0];
+ final float oldestY = pastY[0];
+ final long oldestTime = pastTime[0];
+ float accumX = 0;
+ float accumY = 0;
+ int n = 0;
+ while (n < num_past) {
+ if (pastTime[n] == 0) {
+ break;
+ }
+ n++;
+ }
+ assert(n < num_past);
+
+ // Skip the last received event, since it is probably pretty noisy.
+ if (n > 3) n--;
+ assert(n <= 3);
+ for (int i = 1; i < n; i++) {
+ final int dur = (int)(pastTime[i] - oldestTime);
+ if (dur == 0) {continue;}
+ float dist = pastX[i] - oldestX;
+ float vel = (float)(dist/dur) * units; // pixels/frame.
+ if (accumX == 0) accumX = vel;
+ else accumX = (accumX + vel) * .5f;
+
+ dist = pastY[i] - oldestY;
+ vel = (dist/dur) * units; // pixels/frame.
+ if (accumY == 0) accumY = vel;
+ else accumY = (accumY + vel) * .5f;
+ }
+ mXVelocity = accumX;
+ mYVelocity = accumY;
+ assert(accumX != 0 || accumY != 0);
+ }
+
+ public static void main(String[] args) {
+ float x = Verifier.nondetFloat();
+ float y = Verifier.nondetFloat();
+ long time = Verifier.nondetLong();
+ int units = Verifier.nondetInt();
+
+ //updated
+
+ if(time > 0 && units > 0){
+ addPoint(x,y,time);
+ computeCurrentVelocity(units);
+ }
+ }
+}
diff --git a/svcomp-benchmarks/paclab-benchmarks.iml b/svcomp-benchmarks/paclab-benchmarks.iml
new file mode 100644
index 00000000..40ce4f76
--- /dev/null
+++ b/svcomp-benchmarks/paclab-benchmarks.iml
@@ -0,0 +1,13 @@
+
+
+
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file