Code Prover Assumptions About main Function

A C/C++ program that compiles into a complete executable contains a main function. A Code Prover analysis treats the main function differently from other functions.

main Function as Top of Call Hierarchy

Code Prover considers the main function as the starting point of verification. If you do not provide a main function, for instance, when verifying a library, the verification generates one. By default, the generated main calls functions that are not called anywhere else.

The verification then proceeds from the main function onwards into the functions called from main and so on down the call hierarchy.

To adjust the verification time or precision:

  • You can change the content of the generated main using analysis options.

    See Configure Library Verification.

  • You can write your own main function that calls only the functions that you want to verify.

main Function Arguments

The main function can have one of three forms:

  • The no-argument form:

    int main() {}

  • The two-argument form:

    int main(int argc, char* argv[]) {}

  • Any other implementation-defined form.

In keeping with the C/C++ Standard specifications, the verification makes certain assumptions on the main function arguments. If the main function has arguments with data types that match the second form, Code Prover assumes this form and imposes corresponding restrictions on the arguments. In particular:

  • If the first argument of the main function is an integer (or a typdef to integer), the verification assumes that the argument is nonnegative. This argument denotes the number of additional arguments to the program from its external environment.

    The assumption holds true even when the main function has only that one argument.

  • If the first argument is an integer and the second argument is a pointer to a pointer (or a typedef to one), the verification assumes that the second argument is allocated a buffer of size equal to the first argument, argc. Each element of the buffer, argv[0], argv[1],…,argv[argc-1] is also assumed to be an initialized pointer. This argument stores the additional arguments to the program from its external environment.

See Also

Topics