SRI-CSL solidity issues

SRI-CSL / solidity

This is solc-verify, a modular verifier for Solidity.

https://github.com/SRI-CSL/solidity/blob/boogie/SOLC-VERIFY-README.md

GNU General Public License v3.0

51 stars 14 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Foundings of solc-verify

#175 vincenth1 opened 1 year ago
0
Error when trying to verify a contract that uses tx.origin state variable

#174 jcrreis opened 2 years ago
4
solc-verify: UNKNOWN_PROCESS_ERROR when running examples

#173 thanhtoantnt closed 2 years ago
2
For solc-verify, Docker file needs an update?

#172 thomas-genet closed 2 years ago
13
Support for encode function

#171 dongyu123 opened 2 years ago
0
Verification of existentially quantified postcondition fails

#170 zhao-nan closed 3 years ago
5
Parser error: quantifiers after other expressions or in parentheses

#169 zhao-nan closed 3 years ago
1
undeclared identifier: __verifier_idx_uint error with --arithmetic mod option

#168 nelaturuk closed 3 years ago
2
Enum definition not found internal exception

#166 nelaturuk closed 3 years ago
2
Postcondition of function with function call not verifiable

#165 zhao-nan closed 3 years ago
3
[0.7] Add more informative error messages for unsupported new features

#164 hajduakos closed 3 years ago
1
[0.7] Support for function options (gas, value, salt, ...) is broken (FunctionCallOptions)

#163 dddejan closed 3 years ago
1
[0.7] Unsupported special member: timestamp

#162 hajduakos closed 3 years ago
1
[0.7] Wrong result with repacking

#161 hajduakos closed 3 years ago
2
[0.7] Only allowed integer magic identifier is 'now'

#160 hajduakos closed 3 years ago
3
[0.7] Base contract member not visible in function annotation

#159 hajduakos closed 3 years ago
0
[0.7] Identifier this not available for contract annotations

#158 hajduakos closed 3 years ago
1
[0.7] Segmentation faults

#157 hajduakos closed 3 years ago
1
[0.7] Loop annotations are missing

#156 hajduakos closed 3 years ago
1
Inheritance of specs in overloaded functions

#155 hajduakos opened 3 years ago
3
[0.7] Identifier this not visible for function annotations

#154 hajduakos closed 3 years ago
0
[0.7] Error in solidity::frontend::Visibility

#153 hajduakos closed 3 years ago
2
internal exception: Expected tuple as RHS

#152 dddejan opened 4 years ago
0
Unsupported identifier as base of local storage pointer

#151 dddejan closed 3 years ago
1
Error: Unsupported emit statement, could not determine event

#150 dddejan closed 3 years ago
1
Merge

#149 dddejan closed 4 years ago
1
Event tracking doesn't handle references

#148 dddejan opened 4 years ago
0
solc-verify reports mismatched types

#147 zhao-nan closed 3 years ago
7
Issue with casting and verifier functions

#146 dddejan opened 4 years ago
5
Run boogie in parallel with different solvers

#145 dddejan closed 4 years ago
2
Work on case analysis (with extra stuff)

#144 dddejan closed 4 years ago
1
Quantifiers and TCCs

#143 dddejan closed 4 years ago
2
Implicit constructor for libraries

#142 hajduakos closed 4 years ago
3
Event neither specified, nor emitted

#141 hajduakos closed 4 years ago
1
TCCs for array return values

#140 dddejan closed 4 years ago
2
Introduce separate flag to control solvers for solc-verify

#139 hajduakos closed 4 years ago
0
Use .NET Core Boogie

#138 hajduakos closed 4 years ago
0
Friendlier messages when implicit constructor cannot be created

#137 hajduakos opened 4 years ago
2
Further referencing storage pointers

#136 hajduakos closed 4 years ago
0
support for addmod

#135 dddejan opened 4 years ago
0
Constants should not be indexed in packing/unpacking

#134 dddejan closed 4 years ago
1
Further dereferencing local storage pointer

#133 hajduakos closed 4 years ago
3
constructor calls with additional msg parameters

#132 dddejan opened 4 years ago
0
complex modifiers and variable redeclarations

#131 dddejan closed 4 years ago
1
call to undeclared procedure: address_0x...

#130 dddejan opened 4 years ago
0
Struct and constructors from other contracts

#129 dddejan closed 4 years ago
1
don't havoc constants

#128 dddejan closed 4 years ago
1
Error: undeclared identifier: msg

#127 dddejan closed 4 years ago
1
call to undeclared procedure: gasleft

#126 dddejan opened 4 years ago
0
call to undeclared procedure: blockhash

#125 dddejan opened 4 years ago
0