Skip to content
Snippets Groups Projects
Commit 7d96519c authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Fix mainargs test

The `argv` pointer si valid from 0 to `argc` included.
parent 265fec74
No related branches found
No related tags found
No related merge requests found
......@@ -9,7 +9,7 @@
int main(int argc, char **argv) {
int i;
/*@ assert \forall int k; 0 <= k && k < argc ==> \valid(argv + k) ; */
/*@ assert \forall int k; 0 <= k && k <= argc ==> \valid(argv + k) ; */
/*@ assert \block_length(argv) == (argc+1)*sizeof(char*) ; */
/*@ assert argv[argc] == \null ; */
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment