 chriseth
|
4cbf9ff74c
|
Merge pull request #10143 from ethereum/issue-10084
ControlFlowAnalyser: Also consider called functions in a flow
|
2021-06-01 19:34:56 +02:00 |
|
 Leo Alt
|
bf21cd400c
|
Fix conversion from bytes to fixed bytes
|
2021-06-01 17:55:18 +02:00 |
|
 Mathias Baumann
|
56ebea8b2f
|
ControlFlowAnalyser: Also consider called functions in a flow
|
2021-06-01 15:54:37 +02:00 |
|
|
Leo Alt
|
547a6915ad
|
Fix ICE on external calls from constructor
|
2021-06-01 14:21:48 +02:00 |
|
|
Leo Alt
|
97a7c5429b
|
Add SMTChecker tests with modules
|
2021-06-01 13:35:44 +02:00 |
|
|
Leo Alt
|
8eb28b10cb
|
Add SMTChecker tests with modules
|
2021-06-01 13:35:10 +02:00 |
|
|
Leo Alt
|
d828aeee23
|
Update test nondet
|
2021-05-26 22:12:49 +02:00 |
|
 Martin Blicha
|
9c98ab59f0
|
SMTChecker: fixed struct constructor where FixedBytes member is initialized with a string literal
|
2021-05-17 13:52:37 +02:00 |
|
|
Leo Alt
|
880a2fffb6
|
tests
|
2021-05-11 21:20:42 +02:00 |
|
|
Leo Alt
|
1642c10f6e
|
Fix ICE in free functions
|
2021-05-03 10:57:11 +02:00 |
|
 Alex Beregszaszi
|
1be07c2b36
|
Trivial isoltest updates: missing // ---- at the end
|
2021-04-20 17:38:29 +02:00 |
|
|
Alex Beregszaszi
|
84c05d35f3
|
Trivial isoltest updates: normalized whitespace
|
2021-04-20 17:38:29 +02:00 |
|
|
Alex Beregszaszi
|
45c6bbe02b
|
Trivial isoltest updates: directives sorted alphabetically
|
2021-04-20 17:21:56 +02:00 |
|
|
Leonardo Alt
|
a39a6e26da
|
update tests
|
2021-04-19 19:23:18 +02:00 |
|
|
Leonardo Alt
|
80892c8a21
|
Fix nondeterminism
|
2021-04-19 19:23:18 +02:00 |
|
|
Leonardo Alt
|
36def3ef6e
|
tests for free constants
|
2021-04-19 19:23:18 +02:00 |
|
|
Leonardo Alt
|
fd8b4afb76
|
new free function tests
|
2021-04-19 19:23:18 +02:00 |
|
|
Leonardo Alt
|
095d337140
|
Basic support to free constants
|
2021-04-19 19:23:18 +02:00 |
|
|
Leonardo Alt
|
6ae82fcec2
|
Add tests for the library bug
|
2021-04-19 19:23:18 +02:00 |
|
|
Leonardo Alt
|
4e34359063
|
Basic support to free functions
|
2021-04-19 19:23:18 +02:00 |
|
 Kamil Śliwak
|
7b467a49d7
|
Disable assertion that gives non-deterministic results in in slice tests for SMTChecker
|
2021-04-15 17:14:21 +02:00 |
|
|
Leonardo Alt
|
8a7e94c06f
|
Keep pragma in smoke test for bytecode compare script
|
2021-04-08 21:03:39 +02:00 |
|
|
Leonardo Alt
|
0a4afa71bd
|
Update old tests
|
2021-04-08 21:03:39 +02:00 |
|
|
Leonardo Alt
|
d617ef461e
|
Add new tests
|
2021-04-08 21:03:38 +02:00 |
|
|
Martin Blicha
|
330fb8f4d0
|
[SMTChecker] Assignment refactoring
|
2021-03-31 13:36:50 +02:00 |
|
|
Martin Blicha
|
2d231f1859
|
[SMTChecker] Changed SMTEncoder::mergeVariables to work regardless which branch has been visited first
|
2021-03-30 20:35:44 +02:00 |
|
|
Leonardo Alt
|
ba97d6ac4e
|
Add local vars to cex
|
2021-03-30 17:55:21 +02:00 |
|
|
Leonardo Alt
|
dbd067d6db
|
Report out of bounds index access
|
2021-03-30 10:28:48 +02:00 |
|
|
Martin Blicha
|
85358dfe30
|
[SMTChecker] Do not create targets for contracts that cannot be deployed
|
2021-03-25 15:38:37 +01:00 |
|
|
Martin Blicha
|
5293f05ee3
|
[SMTChecker] Fix ICE on ABI functions with no arguments
|
2021-03-25 13:28:29 +01:00 |
|
|
Martin Blicha
|
98446782e2
|
[SMTChecker] Fix compound assignment to push
|
2021-03-24 14:54:13 +01:00 |
|
|
Martin Blicha
|
852e877ae7
|
[SMTChecker] Handle InaccessibleDynamicType
|
2021-03-24 11:53:06 +01:00 |
|
|
Leonardo
|
25b31111df
|
Merge pull request #11040 from ethereum/smt_fix_virtual_one_more_time
[SMTChecker] Fix bug in virtual functions called by constructor
|
2021-03-17 16:54:36 +01:00 |
|
|
Martin Blicha
|
432944d0b4
|
[SMTChecker] Small refactoring of defining SMT expressions for structs/tuples
|
2021-03-16 15:34:43 +01:00 |
|
|
Martin Blicha
|
2f52affcc2
|
[SMTChecker] Correctly resolve current scope contract in VariableUsage.
|
2021-03-15 13:55:14 +01:00 |
|
|
Martin Blicha
|
6aa6c5f5f9
|
[SMTChecker] Reset reference variables on assignment to a variable of reference type
|
2021-03-12 19:51:31 +01:00 |
|
|
Leonardo Alt
|
998346e599
|
Fix bug in virtual functions called by constructor.
|
2021-03-12 16:42:28 +01:00 |
|
|
Martin Blicha
|
0cb75293f9
|
[SMTChecker] fix handling of assignments of array/mapping state variable accessed using contract name
|
2021-03-12 14:01:07 +01:00 |
|
|
Leonardo Alt
|
6fd76e830d
|
Fix CHC cex order
|
2021-03-11 10:36:40 +01:00 |
|
|
Martin Blicha
|
4285c2803b
|
[SMTChecker] Fix ICE on array.pop nested inside 1-tuple
|
2021-03-09 20:00:51 +01:00 |
|
|
Martin Blicha
|
5af01f6896
|
[SMTChecker] Use same sort name for array slice as for the underlying array.
|
2021-03-09 11:06:22 +01:00 |
|
|
Martin Blicha
|
385a664f3c
|
[SMTChecker] Fix public getter for array of structs.
|
2021-03-08 17:34:20 +01:00 |
|
|
Martin Blicha
|
0340510c53
|
[SMTChecker] correct handling of FixedBytes constants initialized with string literal
|
2021-03-04 15:14:47 +01:00 |
|
|
Martin Blicha
|
9e81c81560
|
[SMTChecker] updated tests
|
2021-03-03 17:11:42 +01:00 |
|
|
Leonardo
|
7405dc5b7f
|
Merge pull request #10836 from ethereum/smt_fix_cex_inheritance
Fix inheritance bug in CHC cex
|
2021-02-03 18:49:25 +01:00 |
|
|
Martin Blicha
|
4bcdac71df
|
[SMTChecker] updates to the tests
|
2021-02-03 15:53:58 +01:00 |
|
|
Leonardo Alt
|
665ce27c18
|
Fix inheritance bug in CHC cex
|
2021-02-02 18:06:32 +01:00 |
|
 Martin Blicha
|
a49950cdf3
|
[SMTChecker] Added transaction constraints also for contract deployment
|
2021-02-01 16:46:34 +01:00 |
|
|
Leonardo Alt
|
545305a31f
|
[SMTChecker] Fix super and virtual
|
2021-01-28 18:51:29 +01:00 |
|
|
Martin Blicha
|
deb90d84a6
|
[SMTChecker] added missing type constraints for Address
|
2021-01-27 20:39:24 +01:00 |
|