Improve False Positives

[gidonkatten]

In the limitted analysis that I have done it seems like the tool does not recognise the following rekey check, leading to false positives:

txn GroupIndex
int 3
==
assert
gtxn 3 RekeyTo
global ZeroAddress
==
assert

which is the equivalent of

txn RekeyTo
global ZeroAddress
==
assert

This may also extend to other checks.

[GuidoDipietro]

I have also stumbled upon "Lack of OnCompletion check allows to update/delete the app" despite explicit OnCompletion checks existing:

File test.teal:

// Dummy sample TEAL code
#pragma version 5

// No Rekeying or CloseTo
txn RekeyTo
global ZeroAddress
==
txn CloseRemainderTo
global ZeroAddress
==
&&
txn AssetCloseTo
global ZeroAddress
==
&&
assert

// No high fees
txn Fee
int 10000
<=
assert

// Just 1 tx
global GroupSize
int 1
==
assert

// Only app calls
txn TypeEnum
int appl
==
assert

// Only accept NOOPs
txn OnCompletion
int NoOp
==
assert

// Also added these extra unnecessary checks to make sure Delete and Update are REJECTED
txn OnCompletion
int DeleteApplication
!=
assert
txn OnCompletion
int UpdateApplication
!=
assert

// End

int 1
return

Command ran:

tealer test.teal

Output:

Graphs (both identical):