OpenMP: Loop fusion
This verification example demonstrates how two loops that must be fused to be race free can be specified and verified.
|Language||OpenMP for C|
|Features||Arrays, Iteration contracts, Pragmas, Quantified permissions|
|Path to example file||openmp/add-spec.c|
|Lines of code||62 lines (comments not included)|
|Lines of specification||15 lines (24.19% of the total)|
|Computation time||27785 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.