Custom relation-based contracts; hardcoded contracts for string methods (charAt, substring)

This commit is contained in:
Tagir Valeev
2017-04-11 10:46:44 +07:00
parent 3457fe2b55
commit 761a376ad2
34 changed files with 1033 additions and 656 deletions
@@ -7,8 +7,8 @@ class CandidateInfo<T> {
}
static void test() {
new <warning descr="The call to CandidateInfo always fails, according to its method contracts">CandidateInfo</warning>(null, true, false);
new <warning descr="The call to CandidateInfo always fails, according to its method contracts">CandidateInfo</warning>(null, true, true);
new <warning descr="The call to 'CandidateInfo' always fails, according to its method contracts">CandidateInfo</warning>(null, true, false);
new <warning descr="The call to 'CandidateInfo' always fails, according to its method contracts">CandidateInfo</warning>(null, true, true);
new CandidateInfo(null, false, true);
new CandidateInfo(new Object(), true, true);
@@ -0,0 +1,30 @@
public class CustomContracts {
public void testSubstring(String s) {
if (s.<warning descr="The call to 'substring' always fails, according to its method contracts">substring</warning>(-1).length() == 0) {
System.out.println("Oops");
}
}
public void testSubstring2(String s, int index) {
if (s.substring(0, index).length() == 0 || <warning descr="Condition 'index < 0' is always 'false' when reached">index < 0</warning>) {
System.out.println("Oops");
}
}
public void testSubstring3(String s, int index) {
if (s.substring(3, index).equals("foo") || <warning descr="Condition 'index == 1' is always 'false' when reached">index == 1</warning>) {
System.out.println("Oops");
}
}
public void testCharAt(String s) {
int index = 0;
while (Character.isDigit(s.charAt(index))) {
index++;
}
if (index == 0 || <warning descr="Condition 'index == s.length()' is always 'false' when reached">index == s.length()</warning>) {
System.out.println("Wrong");
}
}
}
@@ -0,0 +1,9 @@
public class DoubleNaN {
void test() {
double x = Double.NaN;
double y = Double.NaN;
if(<warning descr="Condition 'x >= y' is always 'false'">x >= y</warning>) {
System.out.println("oops");
}
}
}
@@ -0,0 +1,45 @@
import org.jetbrains.annotations.Contract;
import org.jetbrains.annotations.NotNull;
import org.jetbrains.annotations.Nullable;
import java.io.IOException;
public class FlushVariableOnStackToNotNullType {
private String str;
@Contract(value = "null -> true", pure = true)
public static boolean isEmpty(@Nullable String s) {
return s == null || s.equals("");
}
interface State {
@Nullable
String get() throws IOException;
}
@Nullable
public String getMessage(State currentState, boolean x, @NotNull String message) {
String errorMessage = null;
if (x) {
errorMessage = message;
}
try {
errorMessage = currentState.get();
} catch (IOException ignored) {
}
if (isEmpty(errorMessage) && !isEmpty(str)) {
errorMessage = "foo";
}
if (isEmpty(errorMessage)) {
try {
errorMessage = currentState.get();
} catch (IOException ignored) {
}
}
return errorMessage;
}
}
@@ -8,7 +8,7 @@ class Test {
String a = notNull(getNullable());
@NotNull
String b = <warning descr="The call to notNull always fails, according to its method contracts">notNull</warning>(null);
String b = <warning descr="The call to 'notNull' always fails, according to its method contracts">notNull</warning>(null);
}
@Nullable
@@ -1,5 +1,6 @@
import java.time.LocalDateTime;
import java.util.List;
import java.util.Scanner;
public class LongRangeKnownMethods {
void testIndexOf(String s) {
@@ -81,7 +82,7 @@ public class LongRangeKnownMethods {
}
void testEqualsIgnoreCase(String s) {
if(s.equalsIgnoreCase("xyz") && s.isEmpty()) {
if(<warning descr="Condition 's.equalsIgnoreCase(\"xyz\") && s.isEmpty()' is always 'false'">s.equalsIgnoreCase("xyz") && <warning descr="Condition 's.isEmpty()' is always 'false' when reached">s.isEmpty()</warning></warning>) {
System.out.println("Never");
}
}
@@ -150,4 +151,41 @@ public class LongRangeKnownMethods {
System.out.println("impossible");
}
}
void testStringComparison(String name) {
// Parentheses misplaced -- found in AndroidStudio
if (!(name.equals("layout_width") && <warning descr="Condition '!(name.equals(\"layout_height\"))' is always 'true'">!(name.equals("layout_height"))</warning> &&
<warning descr="Condition '!(name.equals(\"id\"))' is always 'true'">!(name.equals("id"))</warning>)) {
System.out.println("ok");
}
}
void testFlush(MyReader r) {
if(r.getValue().equals("abc")) {
r.readNext();
if(r.getValue().equals("abcd")) {
System.out.println("ok");
}
}
}
void testNoFlush(MyReader r) {
if(r.getValue().equals("abc")) {
if(<warning descr="Condition 'r.getValue().equals(\"abcd\")' is always 'false'">r.getValue().equals("abcd")</warning>) {
System.out.println("ok");
}
}
}
static class MyReader {
private String value = "";
final String getValue() {
return value;
}
void readNext() {
value = new Scanner(System.in).next();
}
}
}
@@ -82,7 +82,7 @@ class OptionalWithoutIsPresent {
}
if (maybe.isPresent()) {
maybe = Optional.empty();
System.out.println(maybe.<warning descr="The call to get always fails, according to its method contracts">get</warning>());
System.out.println(maybe.<warning descr="The call to 'get' always fails, according to its method contracts">get</warning>());
}
boolean b = <warning descr="Condition '((maybe.isPresent()))' is always 'false'">((maybe.isPresent()))</warning> && maybe.get() == 1;
boolean c = <warning descr="Condition '(!maybe.isPresent())' is always 'true'">(!maybe.isPresent())</warning> || maybe.get() == 1;
@@ -118,7 +118,7 @@ class OptionalWithoutIsPresent {
boolean absent = !present;
boolean otherAbsent = !!absent;
if(otherAbsent) {
System.out.println(opt.<warning descr="The call to get always fails, according to its method contracts">get</warning>());
System.out.println(opt.<warning descr="The call to 'get' always fails, according to its method contracts">get</warning>());
} else {
System.out.println(opt.get());
}
@@ -151,12 +151,12 @@ class OptionalWithoutIsPresent {
o2 = getOptional();
org.junit.Assert.assertTrue(!o2.isPresent());
System.out.println(o2.<warning descr="The call to get always fails, according to its method contracts">get</warning>());
System.out.println(o2.<warning descr="The call to 'get' always fails, according to its method contracts">get</warning>());
}
private void checkAsserts2() {
Optional<String> o3 = Optional.empty();
org.testng.Assert.<warning descr="The call to assertTrue always fails, according to its method contracts">assertTrue</warning>(o3.isPresent());
org.testng.Assert.<warning descr="The call to 'assertTrue' always fails, according to its method contracts">assertTrue</warning>(o3.isPresent());
System.out.println(o3.get());
}
@@ -180,7 +180,7 @@ class OptionalWithoutIsPresent {
} else {
test = Optional.empty();
}
System.out.println(test.<warning descr="The call to get always fails, according to its method contracts">get</warning>());
System.out.println(test.<warning descr="The call to 'get' always fails, according to its method contracts">get</warning>());
}
@@ -228,7 +228,7 @@ class OptionalWithoutIsPresent {
void order(Optional<String> order, boolean b) {
order.ifPresent(o -> System.out.println(order.get()));
System.out.println(order.orElseGet(() -> order.<warning descr="The call to get always fails, according to its method contracts">get</warning>().trim()));
System.out.println(order.orElseGet(() -> order.<warning descr="The call to 'get' always fails, according to its method contracts">get</warning>().trim()));
}
public static void two(Optional<Object> o1,Optional<Object> o2) {
@@ -359,8 +359,8 @@ class OptionalWithoutIsPresent {
public void testThrowFail(Optional<String> arg) {
if(!arg.isPresent()) {
System.out.println(arg.<warning descr="The call to orElseThrow always fails, according to its method contracts">orElseThrow</warning>(IllegalAccessError::new));
System.out.println(arg.<warning descr="The call to 'orElseThrow' always fails, according to its method contracts">orElseThrow</warning>(IllegalAccessError::new));
}
String res = Optional.<String>empty().<warning descr="The call to orElseThrow always fails, according to its method contracts">orElseThrow</warning>(RuntimeException::new);
String res = Optional.<String>empty().<warning descr="The call to 'orElseThrow' always fails, according to its method contracts">orElseThrow</warning>(RuntimeException::new);
}
}