Skip to content

Commit 9d8abbf

Browse files
Merge pull request #2846 from peterschrammel/jbmc-no-cover-tests
JBMC tests should not use --cover
2 parents d33bd22 + e152c92 commit 9d8abbf

File tree

129 files changed

+345
-318
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

129 files changed

+345
-318
lines changed
Binary file not shown.

jbmc/regression/jbmc-cover/generics/test.desc

Lines changed: 0 additions & 9 deletions
This file was deleted.
Binary file not shown.

jbmc/regression/jbmc-strings/StringBuilderSetCharAt/Test.java

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,9 @@ public String det()
1818
builder.setCharAt(11, ':');
1919
builder.setCharAt(16, ':');
2020
builder.setCharAt(18, ':');
21-
return builder.toString();
21+
String result = builder.toString();
22+
assert result.length() < 5;
23+
return result;
2224
}
2325

2426
public String nonDet(String s, char c, int i)
@@ -42,7 +44,9 @@ public String nonDet(String s, char c, int i)
4244
builder.setCharAt(11, ':');
4345
builder.setCharAt(16, ':');
4446
builder.setCharAt(18, ':');
45-
return builder.toString();
47+
String result = builder.toString();
48+
assert result.length() < 5;
49+
return result;
4650
}
4751

4852
public String withDependency(boolean b)

0 commit comments

Comments
 (0)