[tanvir-ux]

ServerSocket.accept was modeled as Basic.skip, so Pulse never tracked the Socket it returns. Closing the listener while leaving the accepted socket open was not reported.

This models accept with Resource.allocate_returned (java.net.Socket, throws java.io.IOException), the same pattern as the other factories that return a fresh resource. getInputStream and getOutputStream are unchanged.

Notes:

• Because accept can now throw, serverSocketNotClosedAfterAcceptBad and FN_serverSocketNotClosedBad report the listener on the exceptional path.
• In serverSocketWithSocketClosedOk, a throwing PrintWriter.close() skipped socket.close() in the same finally; the socket close is now in a nested finally, and the test stays clean.
• The leak message says allocated by constructor java.net.Socket(), which is how allocate_returned records the resource class.

Test plan:

• Before: serverSocketAcceptNotClosedBad was not reported.
• After: it reports PULSE_RESOURCE_LEAK for java.net.Socket; serverSocketAcceptClosedOk, serverSocketAcceptTryWithResourcesOk, serverSocketClosedOk, serverSocketClosedAfterAcceptOk and serverSocketWithSocketClosedOk are clean.
• make -C infer/tests/codetoanalyze/java/pulse test passes; ocamlformat 0.29.0 clean.

[dulmarod]

there is a conflict now

[tanvir-ux]

Thanks, Dulma. I merged main and resolved the conflict with #2302 in PulseModelsJava.ml; the test expectations now include both. Should be good to import.

[dulmarod]

Sorry it says there are still conflicts

[tanvir-ux]

Sorry about that, Dulma. I've rebased the branch onto the latest main as a single commit with no merge commit, so it should import cleanly now.