-
Notifications
You must be signed in to change notification settings - Fork 0
Examples
NOTE: This information is outdated. For a list of examples, see the examples folder.
| Example | Verification status |
|---|---|
| arrays | fail |
| arrays_simple | fail |
| basic_arrays_read | fail |
| basic_arrays_write | fail |
| basic_assign_assign | success |
| basic_assign_increment | success |
| basic_function_call_caller | fail |
| basic_function_call_reader | success |
| basic_lock_read | success |
| basic_lock_unlock | success |
| basic_lock_security_read | success |
| basic_lock_security_write | success |
| basic_loop_assign | success |
| basic_loop_loop | fail |
| basic_sec_policy_read | success |
| basic_sec_policy_write | success |
| basicassign | fail |
| basicassign_gamma0 | success |
| basicassign1 | fail |
| basicassign2 | fail |
| basicassign3 | fail |
| basicfree | success |
| basicpointer | fail |
| cjump | success |
| cntlm | fail |
| cntlm2 | fail |
| function | success |
| function1 | success |
| functions_with_params | success |
| ifbranches | success |
| ifglobal | success |
| iflocal | fail |
| loops | fail |
| nestedif | success |
| nestedifglobal | fail |
| no_interference_update_x | success |
| no_interference_update_y | success |
| secret_write | success |
| simple_jump | success |
| switch | success |
| switch2 | fail |
| using_gamma_conditional | success |
| using_gamma_write_z | success |
| Example | Intentionally fails | Loops | Stack detection | Specifying arrays | Indirect calls | Irreducible control flow | Non-32-bit global variables | Other |
|---|---|---|---|---|---|---|---|---|
| arrays | x | x | ||||||
| arrays_simple | x | |||||||
| basic_arrays_read | x | |||||||
| basic_arrays_write | x | |||||||
| basic_function_call_caller | x | |||||||
| basic_loop_loop | x | |||||||
| basicassign | x | |||||||
| basicassign1 | x | |||||||
| basicassign2 | x | x | ||||||
| basicassign3 | x | |||||||
| basicpointer | x | x | ||||||
| cntlm | x | x | x | x | x | |||
| cntlm2 | x | x | x | x | x | |||
| iflocal | x | |||||||
| loops | x | |||||||
| nestedifglobal | x | |||||||
| switch2 | x |
The example is designed not to verify, so failure to verify is a positive outcome.
Loops are not currently supported due to the need for loop invariants.
There are currently some issues with detecting the stack as a distinct region of memory, which causes some examples not to verify.
Some examples require specifications relating to array properties, which are not yet supported by the specification system.
Some examples have indirect calls, which are not currently supported, as analysis to resolve their possible destinations is currently incomplete.
Irreducible control flow is not supported by Boogie, so implementing a method of transforming programs with irreducible control flow into programs with reducible control flow is needed to support these examples.
Some examples have global variables that are not 32-bit, which are not fully supported by the specifications at present.