From my testing, f32::atan2(y, x).is_sign_positive() == y.is_sign_positive(). I was even able to make kani prove that for the libm implementation.

use kani::*;

#[kani::proof]
fn nan() {
    let x: f32 = any();
    let y: f32 = any();
    assume(x.is_nan() || y.is_nan());
    let res = libm::atan2f(y, x);
    assert!(res.is_nan());
}

#[kani::proof]
fn atan2() {
    let x: f32 = any();
    assume(!x.is_nan());
    let y: f32 = any();
    assume(!y.is_nan());
    let res = libm::atan2f(y, x);
    assert!(res.is_finite());
    assert_eq!(res.is_sign_positive(), y.is_sign_positive());
    assert!(res <= core::f32::consts::PI);
    assert!(res >= -core::f32::consts::PI);
}

@rustbot claim

I think I'll put up a PR adjusting documentation.

triage: @GrigorenkoPV still planning on working on this?

also note that this should be updated for other float types too (f16, f32, and f128)

triage: @GrigorenkoPV still planning on working on this?

I do, but not sure when I will have time, so I should probably unclaim this for now.

@rustbot release-assignment

Also, I think the fix here is pretty easy: as I see it, one just needs to mention that the sign of the result is the same as the sign of the first argument, and that -0 & +0 both exist with floats and are two slightly different things.

So probably just specify the output ranges for four of the cases:
x >= +0, y >= +0
x <= -0, y >= +0
x >= +0, y <= -0
x <= -0, y <= -0

@rustbot label +E-easy

@rustbot claim