cerc-io/solidity
11
0 Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity
19,958 Commits 348 Branches 121 Tags
6ae82fcec2cbae20f2f8481ce5f2c2dd28df972e
Commit Graph
100 Commits
This Branch
This Branch
All Branches
Author SHA1 Message Date
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
Leonardo Alt e3abde43f5 Change settings.modelChecker.targets to take an array instead of string 2021-04-19 17:53:03 +02:00
Leonardo 124db22f04 Merge pull request #11202 from ethereum/smt_remove_pragma 
[SMTChecker] Deprecate pragma SMTChecker
 2021-04-08 21:43:31 +02:00
Leonardo Alt 8a7e94c06f Keep pragma in smoke test for bytecode compare script 2021-04-08 21:03:39 +02:00
Leonardo Alt ad10bee8f0 update command line tests 2021-04-08 21:03:39 +02:00
Leonardo Alt d89be74e4a Update docs 2021-04-08 21:03:39 +02:00
Leonardo Alt c43ae60938 Changelog 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
Leonardo Alt b753cb6120 Deprecate pragma experimental SMTChecker 2021-04-08 21:03:38 +02:00
Leonardo cbccb53ee2 Merge pull request #11178 from blishko/smt-assign-refactor 
[SMTChecker] Small refactoring of assignment
 2021-03-31 16:31:29 +02:00
Leonardo 78d94737a4 Merge pull request #11188 from blishko/issue-11181 
[SMTChecker] Fix crash when analysing try-catch clauses with function call.
 2021-03-31 11:24:36 +02:00
Leonardo 510bbaf672 Merge pull request #11122 from ethereum/smt_cex_local_vars 
[SMTChecker] Show local variables in cex
 2021-03-30 19:14:35 +02:00
Leonardo Alt ba97d6ac4e Add local vars to cex 2021-03-30 17:55:21 +02:00
Leonardo a7e2a8acb2 Merge pull request #11145 from ethereum/smt_out_of_bounds 
[SMTChecker] Add `out of bounds` verification target
 2021-03-30 14:24:50 +02:00
Leonardo Alt dbd067d6db Report out of bounds index access 2021-03-30 10:28:48 +02:00
Leonardo dcc0267cf4 Merge pull request #11179 from ethereum/smt_fix_bfs_order 
[SMTChecker] Fix target warning order nondeterminism
 2021-03-26 14:00:47 +01:00
Leonardo Alt d1db41a5c8 Fix target warning order nondeterminism 2021-03-26 12:13:52 +01:00
Leonardo b3bbdacd48 Merge pull request #11126 from blishko/smt-no-targets-for-abstract 
[SMTChecker] Do not create verification targets for contracts that cannot be deployed.
 2021-03-25 18:04:02 +01:00
Leonardo 7e1be52281 Merge pull request #11165 from blishko/smt-abi-no-args 
[SMTChecker] Fix ICE on ABI functions with no arguments
 2021-03-25 15:21:57 +01:00
Leonardo 2f36e15009 Merge pull request #11146 from blishko/smt-fix-compound-assignment-to-push 
[SMTChecker] Fix compound assignment to push
 2021-03-24 16:12:48 +01:00
Leonardo 13d3b35141 Merge pull request #11116 from blishko/issue-10985 
[SMTChecker] Handle InaccessibleDynamicType
 2021-03-24 14:39:24 +01:00
Leonardo 70c1720903 Merge pull request #11129 from blishko/smt-ci-tests 
Run SMTChecker tests for all EVM versions
 2021-03-24 10:31:44 +01:00
Leonardo 66729a4ffe Merge pull request #11075 from ethereum/smt_tutorial 
[SMTChecker] Tutorial and docs cleanup
 2021-03-22 11:46:36 +01:00
Leonardo Alt 569afe711a SMTChecker tutorial and docs cleanup 2021-03-18 11:09:26 +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
Leonardo 6d8366967b Merge pull request #11112 from blishko/smt-small-refactor 
[SMTChecker] Small refactoring of defining SMT expressions for structs/tuples
 2021-03-16 19:02:16 +01:00
Leonardo 86e1e4a2dd Merge pull request #11092 from blishko/issue-10957 
[SMTChecker] Resolve current contract context correctly in VariableUsage
 2021-03-15 15:01:51 +01:00
Leonardo 2c00939ad8 Merge pull request #11097 from blishko/smt-reset-reference-variables 
[SMTChecker] Reset reference variables on assignment to a variable of reference type
 2021-03-15 12:06:37 +01:00
Leonardo Alt 998346e599 Fix bug in virtual functions called by constructor. 2021-03-12 16:42:28 +01:00
Leonardo ccd9de137a Merge pull request #11088 from blishko/smt-assignment-cleanup 
[SMTChecker] Fix handling of assignments of array/mapping state variable accessed using contract name.
 2021-03-12 15:44:27 +01:00
Leonardo dd0f5be0c3 Merge pull request #11058 from ethereum/smt_fix_cex_order 
[SMTChecker] Fix CHC cex order
 2021-03-11 12:17:55 +01:00
Leonardo Alt 6fd76e830d Fix CHC cex order 2021-03-11 10:36:40 +01:00
Leonardo b4c08b9bfe Merge pull request #11076 from blishko/issue-11005 
[SMTChecker] Fix ICE on array.pop nested inside 1-tuple
 2021-03-10 10:36:42 +01:00
Leonardo 5677df86af Merge pull request #11069 from blishko/smt-array-slice-fix 
[SMTChecker] Use same sort name for array slice as for the underlying array
 2021-03-09 16:39:12 +01:00
Leonardo 1d95f95635 Merge pull request #11059 from blishko/smt-array_of_structs-getter 
[SMTChecker] Fix public getter for array of structs.
 2021-03-09 10:39:34 +01:00
Leonardo d42d0faf41 Merge pull request #11052 from blishko/issue-10986 
[SMTChecker] Correct handling of FixedBytes constants initialized with string literal
 2021-03-04 16:51:22 +01:00
Leonardo be5647735e Merge pull request #11032 from blishko/smt_string_to_bytes 
[SMTChecker] Fix analysis of push to a string casted to bytes
 2021-03-03 20:29:51 +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
Leonardo 43ce5d3f79 Merge pull request #10884 from blishko/smt-refactor 
[SMTChecker] Small refactoring
 2021-02-03 17:26:53 +01:00
Leonardo d393624384 Merge pull request #10585 from ethereum/fix-quoting-and-whitespace-in-shell-scripts 
Fix quoting in shell scripts
 2021-02-03 11:27:40 +01:00
Leonardo Alt 665ce27c18 Fix inheritance bug in CHC cex 2021-02-02 18:06:32 +01:00
Leonardo dde6353c5d Merge pull request #10704 from blishko/smt-tx-constraints-constructor 
[SMTChecker] Added type constraints on transaction variables also for the contract deployment phase.
 2021-02-01 18:22:19 +01:00
Leonardo 70882cc494 Merge pull request #10850 from ethereum/smt_fix_super 
[SMTChecker] Fix buggy virtual and super
 2021-01-28 19:54:30 +01:00
Leonardo Alt 545305a31f [SMTChecker] Fix super and virtual 2021-01-28 18:51:29 +01:00
Leonardo 73b9a03f21 Merge pull request #10851 from blishko/smt-address-constraints 
[SMTChecker] Add missing type constraints for Address
 2021-01-28 10:06:32 +01:00
Leonardo 38d1ec3efe Merge pull request #10835 from blishko/smt-assembly 
[SMTChecker] Basic support for inline assembly that over-approximates its effects.
 2021-01-26 22:35:25 +01:00
Leonardo c35fdda2ec Merge pull request #10844 from ethereum/smt_z3_docker_4_18_10 
Bump docker images for z3 4.8.10
 2021-01-26 13:05:50 +01:00
Leonardo 6488dd5b96 Merge pull request #10843 from ethereum/updatez3ppa 
Update z3 to 4.8.10.
 2021-01-26 11:40:30 +01:00
Leonardo Alt fbfcb4e71d Bump docker for z3 4.8.10 2021-01-26 11:37:11 +01:00
Leonardo 22ad64a0fd Merge pull request #10845 from ethereum/smt_z3_4-8-10 
Update smtCheckerTests for z3 4.8.10
 2021-01-26 11:37:03 +01:00
Leonardo Alt 40221a90c4 Update smtCheckerTests for z3 4.8.10 2021-01-26 10:18:52 +01:00
Leonardo ead1a26f21 Merge pull request #10797 from ethereum/refactor-and-shellcheck-cleanup-in-report-errors-sh 
Refactor and shellcheck cleanup in report_errors.sh and check_style.sh
 2021-01-22 12:12:39 +01:00
Leonardo 3045770a6f Merge pull request #10828 from ethereum/smt_cex_value 
[SMTChecker] Add msgvalue to cex if > 0
 2021-01-21 21:34:38 +01:00
Leonardo Alt a612daa783 Add msgvalue to cex 2021-01-21 19:05:44 +01:00
Leonardo a75b87c80e Merge pull request #10813 from ethereum/smt_targets_option 
Add CLI and JSON option to select SMTChecker targets
 2021-01-20 18:37:08 +01:00
Leonardo Alt 3b23cadbdc Add CLI and JSON option to select SMTChecker targets 2021-01-20 17:35:37 +01:00
Leonardo 0b023b893e Merge pull request #10817 from ethereum/splitShiftBytesTest 
Split shift bytes test.
 2021-01-19 16:16:45 +01:00
Leonardo 9bde92ca20 Merge pull request #10807 from ethereum/fixIRReasonStrings 
Properly omit require revert strings in IR code generator if requested.
 2021-01-19 10:31:15 +01:00
Leonardo 957e9995a0 Merge pull request #10801 from blishko/issue-10793 
[SMTChecker] Gather local variables also from nested try/catch clauses
 2021-01-18 22:37:16 +01:00
Leonardo 51b7dc69b7 Merge pull request #10802 from ethereum/smt_fix_override 
[SMTChecker] Fix static virtual resolution
 2021-01-18 17:10:31 +01:00
Leonardo Alt c7ca87c012 Fix static virtual resolution 2021-01-18 16:23:38 +01:00
Leonardo 726c5ff68c Merge pull request #10777 from blishko/smt-fix-checked 
[SMTChecker] Fix BMC crash related to `unchecked` blocks
 2021-01-15 16:46:32 +01:00
Leonardo 93b25dc783 Merge pull request #10741 from ethereum/smt_cex_external_calls 
[SMTChecker] Synthesize untrusted functions called externally
 2021-01-15 15:31:56 +01:00
Leonardo Alt 007d39871b [SMTChecker] Synthesize untrusted functions called externally 2021-01-15 11:56:26 +01:00
Leonardo 110e0e1f25 Merge pull request #10763 from blishko/smt-abi-fixes 
[SMTChecker] Small fixes in handling ABI functions
 2021-01-14 16:00:49 +01:00
Leonardo 501461147e Merge pull request #10750 from blishko/issue-10657 
[SMTChecker] Fixed pushing string literal to bytes array
 2021-01-13 17:28:42 +01:00
Leonardo fe344ed6e5 Merge pull request #10748 from blishko/smt-refactoring 
[SMTChecker] Refactoring common functionality
 2021-01-13 14:23:19 +01:00
Leonardo fa28e48415 Merge pull request #10727 from ethereum/smt_cex_internal_calls 
[SMTChecker] Report internal calls in CHC transaction trace
 2021-01-12 15:44:12 +01:00
Leonardo Alt b3c3836388 Output internal calls 2021-01-12 14:57:04 +01:00
Leonardo Alt f1ae24abc7 Remove extra line breaks 2021-01-12 14:00:07 +01:00
Leonardo 66a773aef9 Merge pull request #10721 from blishko/smt-try-catch 
[SMTChecker] Support try-catch statements
 2021-01-12 12:04:38 +01:00
Leonardo 7824ccb56d Merge pull request #10663 from ethereum/check_style_exclude_list_support 
scripts/check_style.sh: add exclude list support.
 2021-01-12 11:28:26 +01:00
Leonardo Alt 5f39662235 Fix BFS visit 2021-01-11 13:18:59 +01:00
Leonardo d11cf15d37 Merge pull request #10722 from ethereum/smt_cex_calls 
[SMTChecker] Refactor cex loop
 2021-01-07 23:57:52 +01:00
Leonardo Alt 11f56861c3 Refactor cex loop 2021-01-07 23:13:02 +01:00
Leonardo 130fc0701b Merge pull request #10716 from ethereum/rename_bfs 
Make BFS correct again
 2021-01-06 11:55:34 +01:00
Leonardo Alt ced79497f5 Fix BFS 2021-01-06 10:17:17 +01:00
Leonardo fdbb4d9a8f Merge pull request #10705 from ethereum/smt_cex_contract 
[SMTChecker] Output contract's name in counterexample
 2021-01-04 12:57:06 +01:00
Leonardo Alt b02722ebda Add contract name to called function in cex 2021-01-04 10:03:16 +01:00
Leonardo Alt 78d55e6b4a [SMTChecker] Support check/unchecked 2020-12-30 12:14:30 +01:00
Leonardo eb05826857 Merge pull request #10702 from blishko/smt-block-constraints 
[SMTChecker] Add missing constraints for block properties
 2020-12-30 09:14:47 +01:00
Leonardo 86c30b4cf5 Merge pull request #10685 from ethereum/smt_virtual_functions 
[SMTChecker] Fix calls to virtual/overriden functions
 2020-12-29 15:05:29 +01:00
Leonardo Alt 9482e7de23 [SMTChecker] Fix calls to virtual/overriden functions 2020-12-29 11:25:20 +01:00
Leonardo 840b194bea Merge pull request #10662 from blishko/smt-external-error 
[SMTChecker] Carry error information across external calls
 2020-12-29 11:05:21 +01:00
Leonardo 03946bcd3c Merge pull request #10694 from suriyaa/patch-1 
Update Natspec documentation URL
 2020-12-28 11:08:02 +01:00
Leonardo 6bcae84610 Merge pull request #10678 from blishko/refactor 
[SMTChecker] Small refactoring to define a single way of gathering functions belonging to a given contract.
 2020-12-22 13:50:26 +01:00
Leonardo a48106ca1f Merge pull request #10670 from blishko/smt-virtual-modifiers-fix 
[SMTChecker] Fix virtual modifier called statically
 2020-12-21 18:05:02 +01:00
Leonardo 158154bac3 Merge pull request #10345 from ethereum/ir-runtime 
Output runtime object in IR
 2020-12-18 17:19:40 +01:00
Leonardo Alt 034d1ab90f [SMTChecker] Replace constants by their value in-place 2020-12-18 14:22:28 +01:00
Leonardo 6b482d4b41 Merge pull request #10647 from ethereum/ppaStaticRelease 
Build solidity-upgrade and yul-phaser statically on static PPA builds.
 2020-12-18 14:20:44 +01:00
Leonardo 16832985f5 Merge pull request #10614 from blishko/smt-overidden-modifiers 
[SMTChecker] Fix analysis of overriding modifiers
 2020-12-18 09:26:34 +01:00
Leonardo Alt 50be39fc21 Add and update tests 2020-12-17 14:42:49 +01:00
Leonardo Alt 7ba91cdc33 Changelog 2020-12-17 14:03:17 +01:00
Leonardo Alt 2cbf33ca1c SMTChecker support ABI functions as UFs 2020-12-17 14:03:17 +01:00
Leonardo Alt f5c96ea6da Fix constant evaluation build 2020-12-16 17:59:00 +01:00
Leonardo Alt 80e85b772b [SMTChecker] Apply const eval to arithmetic binary expressions 2020-12-16 14:58:00 +01:00
Leonardo Alt 59428b8f76 Fix SMTChecker tests on breaking 2020-12-15 19:49:57 +01:00
Leonardo 2552a9b7b0 Merge pull request #10601 from blishko/smt-fix-constructor-recursive-struct 
[SMTChecker] Fix internal error on constructor of a recursive struct
 2020-12-15 12:15:16 +01:00