SE547: CBMC: CBMC Algorithm [14/19]

The tricky part is:

5) Calculate the constraints of the program C, and the properties we're checking of the program P.

For a program I, the constraints are C(I,true) where C(I,g) is defined:

C(I;J, g) = C(I, g) C(I, g)
C(if (c) { I } else { J }, g) = C(I, g c) C(J, g c)
C(assume(c), g) = g c
C(x=e, g) = g x=e
C(anything else, g) = true

For a program I, the properties are P(I,true) where P(I,g) is defined:

P(I;J, g) = P(I, g) P(I, g)
P(if (c) { I } else { J }, g) = P(I, g c) P(J, g c)
P(assert(c), g) = g c
P(anything else, g) = true