Join GitHub today
GitHub is home to over 50 million developers working together to host and review code, manage projects, and build software together.
Sign upChecker-Annotation #1260
Checker-Annotation #1260
Conversation
@@ -123,7 +125,7 @@ public Graph(Edge[] edges) { | |||
/** | |||
* Runs dijkstra using a specified source vertex | |||
*/ | |||
public void dijkstra(String startName) { | |||
public void dijkstra(@NonNull String startName) { |
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
@@ -104,7 +106,7 @@ public String toString() { | |||
/** | |||
* Builds a graph from a set of edges | |||
*/ | |||
public Graph(Edge[] edges) { | |||
public Graph(@Positive Edge[] edges) { |
This comment has been minimized.
This comment has been minimized.
Maxi17
Mar 26, 2020
The @Positive
annotation is not in the NullnessChecker hierarchy. You mixed the NullnessChecker and IndexChecker qualifiers in this case study. It is not wrong to annotate a file using 2 type systems, but it is not the usual way a case study is done.
Also, the annotation is incorrect. What you meant is that the array edges
contains objects of type Edge
, which can't be @Positive
, because it is meaningless. Only types like int
, which represent a number can be @Positive
, @NonNegative
and some other IndexChecker qualifiers.
This comment has been minimized.
This comment has been minimized.
@@ -95,7 +97,7 @@ public int compareTo(Vertex other) { | |||
return Integer.compare(dist, other.dist); | |||
} | |||
|
|||
@Override | |||
@Override |
This comment has been minimized.
This comment has been minimized.
@@ -56,7 +58,7 @@ public static void main(String[] args) { | |||
public final String v1, v2; | |||
public final int dist; | |||
|
|||
public Edge(String v1, String v2, int dist) { | |||
public Edge(@NonNull String v1, @NonNull String v2, @NonNegative int dist) { |
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
@@ -56,7 +58,7 @@ public static void main(String[] args) { | |||
public final String v1, v2; | |||
public final int dist; |
This comment has been minimized.
This comment has been minimized.
Maxi17
Mar 26, 2020
I expected a @NonNegative
annotation here, too. This field is initialized in the constructor with a non-negative value.
guy34code commentedMar 25, 2020
No description provided.