The goal of the user is to prove some properties over an input program. Usual properties are: all array accesses are within boundaries, no division by zero, all used values are initialized, all de-referenced pointers are non-null, etc... The kind of properties that makes a program safe to run and crash-free.
The tool will either prove that all the properties hold (user is happy), or prove that some property does not hold at some point in the program (user knows what to fix usually), or bail-out with no proof at all for a property at some point (user has to modify the program to make it more understandable by the tool).
The accepted language is still Turing-complete (C or C++) and the tool is not solving the halting problem in the general case since it can bail-out with no proof.
The tool will either prove that all the properties hold (user is happy), or prove that some property does not hold at some point in the program (user knows what to fix usually), or bail-out with no proof at all for a property at some point (user has to modify the program to make it more understandable by the tool).
The accepted language is still Turing-complete (C or C++) and the tool is not solving the halting problem in the general case since it can bail-out with no proof.