For an evaluation I need to check the correctness of "dataflow constraints" which describe the relationships between the parameters and return values passed to api function calls. I have the corresponding source files in C / C++.
For example, a code snippet like this:
x0 = NtOpenFile(_, 3222274176, _, _, _, 42); RtlNtStatusToDosError(x0);
Would generate the following constraint:
Are there any static code analyzers suitable for this task?