Skip to content

Commit 20c87ee

Browse files
author
davidcok
committed
Touch up test output
1 parent 5b2dd72 commit 20c87ee

File tree

2 files changed

+16
-3
lines changed

2 files changed

+16
-3
lines changed

tutorial/T_Feasibility1.out

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
T_Feasibility1.java:6: verify: There is no feasible path to program point at program exit in method T_Feasibility1.m(int)
2-
public int m(int i) {
3-
^
1+
T_Feasibility1.java:9: verify: There is no feasible path to program point at program exit in method T_Feasibility1.m(int)
2+
}
3+
^
44
1 verification failure

tutorial/T_Nullness1.out1

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
T_Nullness1.java:15: verify: The prover cannot establish an assertion (NullFormal: T_Nullness1.java:4:) in method test: s in has(String,char)
2+
b = has(make(2), 'a');
3+
^
4+
T_Nullness1.java:4: verify: Associated declaration: T_Nullness1.java:15:
5+
public static boolean has(String s, char c) {
6+
^
7+
T_Nullness1.java:14: verify: The prover cannot establish an assertion (NullFormal: T_Nullness1.java:4:) in method test: s in has(String,char)
8+
boolean b = has(ss,'a');
9+
^
10+
T_Nullness1.java:4: verify: Associated declaration: T_Nullness1.java:14:
11+
public static boolean has(String s, char c) {
12+
^
13+
4 verification failures

0 commit comments

Comments
 (0)