Nathan Chong nchong
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| CBMC version 5.4 64-bit x86_64 macos | |
| Parsing jmptest.c | |
| Converting | |
| Type-checking jmptest | |
| Generating GOTO Program | |
| Adding CPROVER library (x86_64) | |
| Function Pointer Removal | |
| Partial Inlining | |
| Generic Property Instrumentation | |
| Starting Bounded Model Checking |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| CBMC version 5.4 64-bit x86_64 macos | |
| Parsing simple.c | |
| Converting | |
| Type-checking simple | |
| Generating GOTO Program | |
| Adding CPROVER library (x86_64) | |
| Function Pointer Removal | |
| Partial Inlining | |
| Generic Property Instrumentation | |
| Starting Bounded Model Checking |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* Recursive coordinate bisection is a technique for partitioning a list of coordinates | |
| * into roughly equal sized partitions of spatially close elements. The general principle | |
| * is find the dimension that spans the greatest distance and find a pivot that will | |
| * split the list into two roughly equal halves. Then recurse down. | |
| *) | |
| (* Sort a list of floating point values *) | |
| let sort_float_list l = | |
| List.sort (fun x y -> int_of_float (x -. y)) l |