cprover
|
During the analysis of a program CBMC transforms the input program in an intermediate language called extended goto. Then the tool performs a series of simplifications on the obtained goto program until the program is given to the solver.
We say that a program is in the symex ready goto form when all the extended goto features have been simplified.
More specifically, a program that is in symex ready goto form is one that can be passed to symex by using any solver deriving from goto_verifiert without requiring any lowering step.
At the time of writing, verifiers extending goto_verifiert are: