I'm trying to compute weakest preconditions working backwards from the postcondition c > 10. Specifically, I want to determine what conditions func_1() should satisfy (i.e., what value of b it should return) to ensure certain properties of c hold after func_2. The challenge I'm facing is that whether c depends on b at all is determined by alpha inside func_2. When alpha is False, c is just set to a and b has no effect. Is it possible to compute meaningful preconditions in such a case? If so, how should I approach it? If not, why is it impossible? I suspect this might be a fundamental limitation, but I'd appreciate insights from those more experienced with program analysis.

b = func_1()
c = func_2(b)

def func_2(b):
    a = d.val()  # gets some value from object d
    if alpha:
        c = a + b
    else:
        c = a
    return c