Is there way to verify my program has no memory leaks?
You can use valgrind. It's a memory debugging tool for Linux and other UNIX-like systems that finds memory leaks as well as invalid memory accesses.
When I run this code through valgrind, it outputs the following:
[dbush@db-centos7 ~]$ valgrind ./x1
==3406== Memcheck, a memory error detector
==3406== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==3406== Using Valgrind-3.14.0 and LibVEX; rerun with -h for copyright info
==3406== Command: ./x1
==3406==
left: 4, right: 12, sum: 69
==3406==
==3406== HEAP SUMMARY:
==3406== in use at exit: 300 bytes in 25 blocks
==3406== total heap usage: 49 allocs, 24 frees, 588 bytes allocated
==3406==
==3406== LEAK SUMMARY:
==3406== definitely lost: 300 bytes in 25 blocks
==3406== indirectly lost: 0 bytes in 0 blocks
==3406== possibly lost: 0 bytes in 0 blocks
==3406== still reachable: 0 bytes in 0 blocks
==3406== suppressed: 0 bytes in 0 blocks
==3406== Rerun with --leak-check=full to see details of leaked memory
==3406==
==3406== For counts of detected and suppressed errors, rerun with: -v
==3406== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)
So you have some leaks. Now let's pass the --leak-check=full option to see where exactly those leaks are:
==11531== Memcheck, a memory error detector
==11531== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==11531== Using Valgrind-3.14.0 and LibVEX; rerun with -h for copyright info
==11531== Command: ./x1
==11531==
left: 4, right: 12, sum: 69
==11531==
==11531== HEAP SUMMARY:
==11531== in use at exit: 300 bytes in 25 blocks
==11531== total heap usage: 49 allocs, 24 frees, 588 bytes allocated
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 1 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007A8: max_subarray (x1.c:49)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 2 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007B6: max_subarray (x1.c:50)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 3 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007A8: max_subarray (x1.c:49)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 4 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007B6: max_subarray (x1.c:50)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 5 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007A8: max_subarray (x1.c:49)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 6 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007B6: max_subarray (x1.c:50)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 7 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007A8: max_subarray (x1.c:49)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 8 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007B6: max_subarray (x1.c:50)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 9 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007A8: max_subarray (x1.c:49)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 10 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007B6: max_subarray (x1.c:50)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 11 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007A8: max_subarray (x1.c:49)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 12 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007B6: max_subarray (x1.c:50)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 13 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007A8: max_subarray (x1.c:49)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 14 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007B6: max_subarray (x1.c:50)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 15 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007A8: max_subarray (x1.c:49)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 16 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007B6: max_subarray (x1.c:50)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 17 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007A8: max_subarray (x1.c:49)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 18 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007B6: max_subarray (x1.c:50)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 19 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007A8: max_subarray (x1.c:49)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 20 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007B6: max_subarray (x1.c:50)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 21 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007A8: max_subarray (x1.c:49)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 22 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007B6: max_subarray (x1.c:50)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 23 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007A8: max_subarray (x1.c:49)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 24 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x4007B6: max_subarray (x1.c:50)
==11531== by 0x4007CE: max_subarray (x1.c:51)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x4007E9: max_subarray (x1.c:52)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== 12 bytes in 1 blocks are definitely lost in loss record 25 of 25
==11531== at 0x4C29EA3: malloc (vg_replace_malloc.c:309)
==11531== by 0x40065B: max_crossing_subarray (x1.c:13)
==11531== by 0x400802: max_subarray (x1.c:53)
==11531== by 0x400931: main (x1.c:73)
==11531==
==11531== LEAK SUMMARY:
==11531== definitely lost: 300 bytes in 25 blocks
==11531== indirectly lost: 0 bytes in 0 blocks
==11531== possibly lost: 0 bytes in 0 blocks
==11531== still reachable: 0 bytes in 0 blocks
==11531== suppressed: 0 bytes in 0 blocks
==11531==
==11531== For counts of detected and suppressed errors, rerun with: -v
==11531== ERROR SUMMARY: 25 errors from 25 contexts (suppressed: 0 from 0)
Most of these leaks are coming from these two lines:
struct Interval * left = malloc(sizeof(struct Interval));
struct Interval * right = malloc(sizeof(struct Interval));
And if we look at the next two lines it's apparent why:
left = max_subarray(A, low, mid);
right = max_subarray(A, mid+1, high);
So right after you assign the address of allocated memory to these pointers you overwrite those addresses with other values, causing a leak. This can be fixed by getting rid of the malloc calls and initializing with the result of the function calls:
struct Interval * left = max_subarray(A, low, mid);
struct Interval * right = max_subarray(A, mid+1, high);
The last one is in max_crossing_subarray
struct Interval * crossing = malloc(sizeof(struct Interval));
This pointer is returned from the function, so we need to see where the missing free is. After some looking around, we see that it is called from max_subarray, which eventually returns it to main as result:
struct Interval * result = max_subarray(A, 0, 13-1);
printf("left: %i, right: %i, sum: %i\n", result->max_left, result->max_right, result->sum);
return 0;
But as you can see, there's no call to free here, so let's add it:
struct Interval * result = max_subarray(A, 0, 13-1);
printf("left: %i, right: %i, sum: %i\n", result->max_left, result->max_right, result->sum);
free(result);
return 0;
Now after making those fixes we'll run through valgrind again:
==11736== Memcheck, a memory error detector
==11736== Copyright (C) 2002-2017, and GNU GPL'd, by Julian Seward et al.
==11736== Using Valgrind-3.14.0 and LibVEX; rerun with -h for copyright info
==11736== Command: ./x1
==11736==
left: 4, right: 12, sum: 69
==11736==
==11736== HEAP SUMMARY:
==11736== in use at exit: 0 bytes in 0 blocks
==11736== total heap usage: 25 allocs, 25 frees, 300 bytes allocated
==11736==
==11736== All heap blocks were freed -- no leaks are possible
==11736==
==11736== For counts of detected and suppressed errors, rerun with: -v
==11736== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0)
And the leaks are gone.
In general you cannot prove your program correctness unless you restrict the language to a sublanguage (like misra) with less features. In general the problem is undecidable.
But you can use software like lint for static check of math patterns, or valgrind for dynamic check, or languages like Coq in which the programs are proofs and they use the Hoare logic to make statements about your code. For example, using Hoare logic, it is proved that the kernel of Windows never segment faults.