Sources/SolToBoogie/ProcedureTranslator.cs (21 lines):
	- line 349: // TODO: move to earlier
	- line 352: // TODO: each local array variable should be distinct and 0 initialized
	- line 617: // TODO: add the initializations outside of constructors
	- line 701: // TODO: add the initialization of m[i][j]
	- line 760: // TODO: Cleanup, StartsWith("uint") can include uint[12] as well.
	- line 857: bigInt = TranslateExpr(varDecl.Value); //TODO: any complex expression will crash
	- line 867: // Issue with inferring Array[] expressions in GetBoogieTypesFromMapping (TODO: use GetBoogieTypesFromMapping after fix)
	- line 977: // TODO: refactor this code with the code to generate constructor code when definition is present
	- line 1480: // TODO: this part should go into Translate a function call expression
	- line 1667: BoogieExpr retExpr = TranslateExpr(node.Expression); //TODO: handle tuples here?
	- line 1678: //turn the tuple assignment into a serial assignment [TODO: understand the evaluation semantics]
	- line 1686: currentStmtList.AppendStmtList(BoogieStmtList.MakeSingletonStmtList(assignCmd)); //TODO: simultaneous updates
	- line 1698: currentStmtList.AppendStmtList(BoogieStmtList.MakeSingletonStmtList(assignCmd)); //TODO: simultaneous updates
	- line 2030: // TODO: Handle static arrauy
	- line 2100: // TODO: Many times the type is unknown...
	- line 2348: // TODO:
	- line 2357: // TODO:
	- line 3002: //TODO: do we want to check that the contract the struct variable is declared
	- line 3013: // TODO: example?
	- line 3096: // TODO: we need a way to determine type of receiver from "x.Foo()"
	- line 3558: // TODO: Need to introduce opcode for power operation


Sources/SolToBoogie/TransUtils.cs (4 lines):
	- line 180: // TODO: The warning below could probably be suppressed:
	- line 191: // TODO: constant is TupleExpression:
	- line 260: // TODO: Provide a better way to check for dynamic array type
	- line 267: // TODO: Provide a better way to check for array type


Sources/SolidityAST/SolidityAST.cs (4 lines):
	- line 834: // TODO: type
	- line 1394: // TODO: switch to enum type
	- line 1475: // TODO: switch to enum type
	- line 1512: // TODO: switch to enum type


Sources/VeriSol/VeriSolExecuter.cs (2 lines):
	- line 226: // This should never happen; TODO: Debug.Assert(false)?
	- line 428: // TODO: should set up a timeout here


Sources/SolToBoogie/FunctionEventResolver.cs (2 lines):
	- line 25: // TODO: resolve events
	- line 68: // TODO: Do we need to lookup by signature?


Sources/SolToBoogie/TranslatorContext.cs (2 lines):
	- line 14: // TODO: Make these configurable.
	- line 65: // FIXME: getters for public state variables


Sources/SolToBoogie/ParseUtils.cs (1 line):
	- line 15: // TODO: extract into a VerificationFlags structure


Sources/SolToBoogie/RevertLogicGenerator.cs (1 line):
	- line 114: // TODO: handle this properly.


Sources/SolToBoogie/MapArrayHelper.cs (1 line):
	- line 33: //TODO: use TypeDescriptions::IsInt/IsStruct etc., but need typeDescription instead of typeString


Sources/SolToBoogieTest/RegressionExecutor.cs (1 line):
	- line 239: // TODO: should set up a timeout here