Skip to content

Commit 1861bb5

Browse files
Write the returned-value note as Origin: <File>:<line>, <call> guarantees ...
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 parent c3fd4a7 commit 1861bb5

2 files changed

Lines changed: 2 additions & 2 deletions

File tree

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/OriginNotes.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,7 @@ static List<String> returnedValues(RefinementError error, Context context) {
9090
String says = isTrue(guaranteed) ? "guarantees nothing about " + value
9191
: "guarantees only " + ExpressionFormatter.format(
9292
guaranteed.substitute(new Var(Keys.WILDCARD), new Var(variable)), error.getDisplayNames());
93-
notes.add(String.format("From: %s (%s:%d) %s", value, declared.getFile().getName(), declared.getLine(),
93+
notes.add(String.format("Origin: %s:%d, %s %s", declared.getFile().getName(), declared.getLine(), value,
9494
says));
9595
}
9696
return notes;

‎liquidjava-verifier/src/test/java/liquidjava/api/tests/TestOriginNotes.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ void callArgumentIsTracedToWhatItsReturnRefinementGuaranteesAboutIt() {
4747
CommandLineLauncher.launch(TEST_SUITE + "classes/found_binders_error");
4848
LJError pick = Diagnostics.getInstance().getErrors().stream().filter(e -> e.getPosition().getLine() == 25)
4949
.findFirst().orElseThrow();
50-
assertEquals(List.of("From: items.size() (ArrayListRefinements.java:13) guarantees only items.size() >= 0"),
50+
assertEquals(List.of("Origin: ArrayListRefinements.java:13, items.size() guarantees only items.size() >= 0"),
5151
pick.getMessageNotes());
5252
}
5353

0 commit comments

Comments
 (0)