Skip to content

Examples

Thomas-Malcolm edited this page Jun 30, 2023 · 2 revisions

NOTE

This information is possibly outdated. For a list of examples to check for yourself, see the examples folder.

Verification Status

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

Reasons for failure

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

Intentionally fails

The example is designed not to verify, so failure to verify is a positive outcome.

Loops

Loops are not currently supported due to the need for loop invariants.

Stack detection

There are currently some issues with detecting the stack as a distinct region of memory, which causes some examples not to verify.

Specifying arrays

Some examples require specifications relating to array properties, which are not yet supported by the specification system.

Indirect calls

Some examples have indirect calls, which are not currently supported, as analysis to resolve their possible destinations is currently incomplete.

Irreducible control flow

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.

Non-32-bit global variables

Some examples have global variables that are not 32-bit, which are not fully supported by the specifications at present.

Clone this wiki locally