Request for advice about how to verify a function like `int main(int argc, char *argv[])`

[eleehiga]

Currently I am trying to verify this function:

#include <errno.h>
#include <limits.h>
#include <stdarg.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <time.h>

int main(int argc, char* argv[])
{       
        int i = 0;
        if(argc == 1)
                i = argv[1];
        assert(i == 1);
}  

However, I am unsure how to test this with inputting parameters for main. Therefore was wondering how I can verify this function with inputting the parameters for main?

[tautschnig]

Would goto-instrument's --model-argc-argv perhaps do the trick for you?

[eleehiga]

@tautschnig I think so but I was wondering where can I find more information about how to use this?

[tautschnig]

There's just goto-instrument --help at present, which says that you need to give the maximum number of arguments you'd like to model. Apologies that we don't have more than that little piece of documentation at the moment. So it would be:

goto-cc foo.c
goto-instrument --model-argc-argv 3 a.out a.out
cbmc a.out

to emulate 0, 1, 2, 3 arguments.

[eleehiga]

@tautschnig No problem but for the main function I first posted, when using the command goto-instrument --model-argc-argv 2 a.out (before this command I did run goto-c test.c) there is the output:

Reading GOTO program from 'a.out'
Adding up to 2 command line arguments
Linking not done, missing __CPROVER__start
Numeric exception : 0

Where would I put __CPROVER__start?

[tautschnig]

Unless there is a bug (which I wasn't able to reproduce) this very much looks like you've done goto-cc -c test.c (note the -c option) instead of goto-cc test.c.

[eleehiga]

@tautschnig Thank you turns out I was verifying the wrong code and now I am able to verify the right code and it works out how you said it would. However, I was wondering, is there a way to specify what inputs to go into the main function's arguments like trying to input 1 for the code in my first post?

[tautschnig]

See #5965 for a discussion on how to implement/accomplish this (there's also a PR linked that sought to provide this feature). In absence of a working implementation, and depending on your precise verification workflow, you might either create a separate harness that sets up argc and argv appropriately, or use --model-argc-argv and then add assumptions in your main function.

[eleehiga]

@tautschnig I understand, probably will do the harness method, thank you.