But wait ... wasn't it explicitly stated in GuardedCondition that it doesn't take switch case statement into account ? So what's the point of valueControls?

It looks like the QLDoc for hasn't been updated since we added support for switch statements (for what it's worth, this was done in #15941). I've opened a PR to fix the documentation here.

That should hopefully take care of the first part of your question :)

Now let's take the next part:

Nor do I understand what does "dertermined by this guard" means in the documentation despite reading this I supposed it means "in the direct basic block after evaluation" [...]

"determined by this guard" means "implied by this guard". That is, if you have a guard such as:

if(a == b + 42 && c > 0) { ... }

then both a == b + 42 and c > 0 are GuardConditions. So there can be multiple GuardConditions from a given guard in the source code, and we "determine those GuardConditions from the guard". I hope that clears up some confusion.

Finally:

but I also don't understand the point of k in left == right+k (why do we need 3 variable for a comparison ?), so I'm probably mistaken elsewhere

You don't need three variables for the comparison, but you can use it if it's useful to you. The point is that, there are many ways of writing a comparison such as a == b + 42 (for example, maybe someone wrote a - 2 == b + 40 or a - b - 42 == 0), and the GuardCondition library "normalizes" such comparisons for you so that you can reason about them as if they were all of the form a == b + k.

If you don't care about k you can simply put 0 there and you're left with equalities of the form a == b. For example:

from GuardCondition gc, Expr left, Expr right, boolean b
where gc.comparesEq(left, right, 0, true, b)
select gc, left, right, b

finds values gc, left, right, b such that left == right is true when gc evaluates to b.