Commit Graph

  • b63a94031f Generate expectations for moved Natspec syntax tests Kamil Śliwak 2023-08-21 11:29:36 +0200
  • dc68480f72 Move Natspec syntax tests to natspecJSON Kamil Śliwak 2023-08-21 11:28:03 +0200
  • d083925bed natspecJSON: Generate missing expectations (including errors) Kamil Śliwak 2023-08-21 12:32:33 +0200
  • 481c7256cb natspecJSON: Include version and kind fields in expectations where missing Kamil Śliwak 2023-08-09 19:33:35 +0200
  • 99bfdf930a SolidityNatspecJSON: Convert Boost-based test cases into natspectJSON/*.sol tests Kamil Śliwak 2023-08-09 18:16:14 +0200
  • ba019e5a01 SolidityNatspecJSON: Manual conversion of two test cases that would not be handled correctly by the script Kamil Śliwak 2023-08-10 16:43:18 +0200
  • 1041f071f0 SolidityNatspecJSON: A few tweaks and small fixes before automatic conversion Kamil Śliwak 2023-08-09 17:42:41 +0200
  • 91cc72bcd4 NatspecJSONTest based on SyntaxTest Kamil Śliwak 2023-07-31 19:52:27 +0200
  • 14aed39261 Introduce experimental analysis basic infrastructure Matheus Aguiar 2023-09-05 21:29:11 -0300
  • 2e22ddebeb no --opcodes Paul 2023-09-11 12:23:53 +0000
  • bbe1af4c28
    Merge branch 'ethereum:develop' into drop-opcodes-s Paul 2023-09-11 05:56:13 -0600
  • 8e3e63d35a Dropping --opcodes support Paul 2023-09-11 11:55:30 +0000
  • 34c86d90be
    Merge pull request #14556 from ethereum/homebrew-update r0qs 2023-09-11 13:34:56 +0200
  • 1cb04e84d9
    Upgrade homebrew packages r0qs 2023-09-11 12:31:42 +0200
  • f8261c6072
    Merge 8047171a13 into 16ae76cad7 Reuben Rodrigues 2023-09-08 07:08:07 +0800
  • 131018a432
    Merge 2a5f046e87 into 16ae76cad7 Emilio Almansi 2023-09-08 06:50:30 +0800
  • 17678d9eb4
    Nachtrag SECURE PAPER Isabel Schöps (Vitalik Buterin) 2023-09-07 00:18:46 +0200
  • 4e9f14fbce
    SECURITY.si Isabel Schöps (Vitalik Buterin) 2023-09-07 00:10:40 +0200
  • 05c95c16c8
    README.si Isabel Schöps (Vitalik Buterin) 2023-09-06 23:33:19 +0200
  • 1a94247851 fixup! Bytecode compare fix type-inference-bytecodecompare-fix Nikola Matic 2023-09-06 13:24:40 +0200
  • 31618b542e
    Update control-structures.rst William Entriken 2023-09-05 21:46:44 -0400
  • a8090baec0
    Merge 8996ae23d2 into 16ae76cad7 r0qs 2023-09-05 13:41:35 +0000
  • 8996ae23d2
    Restore osx cache osx-cache r0qs 2023-08-11 14:40:07 +0200
  • a44fbcf111 Bytecode compare fix Nikola Matic 2023-09-05 15:28:54 +0200
  • 2fb668fa47 Disable shellcheck SC2086 Nikola Matic 2023-09-05 15:14:40 +0200
  • 9b9ac7f607
    Merge pull request #14536 from ethereum/fix-type-inference-shellcheck Daniel 2023-09-05 15:05:34 +0200
  • fe8128fa9b Fix type inference shellcheck failure Nikola Matic 2023-09-05 15:02:38 +0200
  • 475cfe2532 Ignore standard error output from solvers smtlib-interface-for-everything Martin Blicha 2023-08-17 12:54:44 +0200
  • a4b4e70b67 Get invariants from eldarica Martin Blicha 2023-08-17 09:30:52 +0200
  • d8c1a124e7 Bring back solving with temporary file for Eldarica Martin Blicha 2023-08-17 09:13:46 +0200
  • 497ca183b4 Small cleanup Martin Blicha 2023-08-17 00:26:13 +0200
  • 1b68b5764d SMTChecker: Ignore model checking without callback Martin Blicha 2023-08-14 22:06:52 +0200
  • b6326f4d4d Do not stop reading solver's output after it terminated Martin Blicha 2023-08-12 20:53:00 +0200
  • 8e0e2cb1ae Throw when trying to read past the end of SMTLib stream Martin Blicha 2023-08-12 19:12:33 +0200
  • d3bbc51ee9 Update test after change in variable names Martin Blicha 2023-08-12 16:00:55 +0200
  • 4101c67cba Update to let inlining Martin Blicha 2023-08-11 21:39:51 +0200
  • bbd7ef447f Updates to command-line tests Martin Blicha 2023-08-11 17:53:18 +0200
  • ec10f46acb Parse BMC counterexample properly Martin Blicha 2023-08-11 18:00:22 +0200
  • af1acaba64 Refactor SMTLib parser to separate file Martin Blicha 2023-08-11 17:59:52 +0200
  • 3a01b432c4 Hack to get around problem in Z3 Martin Blicha 2023-08-11 12:44:34 +0200
  • 8c99c125c4 Add support for parsing invariants Martin Blicha 2023-08-10 20:14:42 +0200
  • b8f89fa45d SMTSolverCommand: Use pipe instead of temporary file for the query Martin Blicha 2023-08-09 12:08:29 +0200
  • 3f22118bbe More checks Martin Blicha 2023-08-07 15:34:09 +0200
  • 01ed412714 Stronger checks Martin Blicha 2023-08-03 11:35:01 +0200
  • 0c13b7ee8f Turn asserts into solAsserts Martin Blicha 2023-08-03 10:47:33 +0200
  • 83b60754a9 Update to the tests to combat nondeterminism Martin Blicha 2023-08-01 20:25:04 +0200
  • 342df8a515 Ensure SMT-LIB file is complete Martin Blicha 2023-07-28 14:55:09 +0200
  • 5569aaee78 Fix coding style Martin Blicha 2023-07-27 17:25:41 +0200
  • ecded11833 Tests: Disable checking CEX Martin Blicha 2023-07-27 17:21:20 +0200
  • 799f418bef Make counterexample deterministic Martin Blicha 2023-07-27 16:22:55 +0200
  • 4ecaa476fd Handle custom tuple sorts in a general way Martin Blicha 2023-07-27 16:19:53 +0200
  • 742642ebae Use answer from second Z3 call only when solved Martin Blicha 2023-07-27 15:16:17 +0200
  • 0fbeb3a69d Throw exception on unhandled cases in SMT-LIB Expression conversion Martin Blicha 2023-07-27 14:45:15 +0200
  • 4b50f26834 Negative numbers do not have to be atoms Martin Blicha 2023-07-27 14:40:05 +0200
  • 779db2d84f Use shared pointers, not raw pointers, for caching sorts Martin Blicha 2023-07-27 12:05:43 +0200
  • b65c37029d Fix parsing array expressions from SMT-LIB proof Martin Blicha 2023-07-27 10:26:02 +0200
  • d773e76704 Remove outdated FIXME Martin Blicha 2023-07-27 09:54:53 +0200
  • 451b6f8ced Fix handling of structs in SMT-LIB CEX Martin Blicha 2023-07-26 18:28:04 +0200
  • 9339b7074a Fix parsing of let expression to allow shadowing values Martin Blicha 2023-07-26 17:40:02 +0200
  • 92689e4256 Fix code style problems Martin Blicha 2023-07-21 17:14:29 +0200
  • 8ea8a1eb99 Cache sorts already in SMTLib2Interface Martin Blicha 2023-07-21 15:40:00 +0200
  • 6acbe2ec35 Towards translating proof from SMT-LIB response Martin Blicha 2023-07-16 12:56:40 +0200
  • 479bb9c3de Fix missing std Martin Blicha 2023-07-15 14:56:18 +0200
  • 2195b5e57a Solve UNSAT queries again with proof production enabled Martin Blicha 2023-07-03 16:47:59 +0200
  • c90b48af02 Update to the tests Martin Blicha 2023-06-27 11:50:24 +0200
  • 58d0579ba6 SMTCheckerTests: Use SMT callback Martin Blicha 2023-08-09 11:08:30 +0200
  • 1d60559551 Use same spacer parameters as before Martin Blicha 2023-07-03 16:09:25 +0200
  • d9dc8f475e Enable resource limit for Z3 Martin Blicha 2023-06-27 11:49:20 +0200
  • c6f274892e Fix SMTLib2Interface Martin Blicha 2023-06-26 16:38:59 +0200
  • f4b849972c Remove smtlib2 solver option Martin Blicha 2023-06-26 13:41:17 +0200
  • 72974adb92 Fix check for SMT query in UniversalCallback Martin Blicha 2023-06-26 13:24:52 +0200
  • e7fe310bc2 Remove unnecessary header Martin Blicha 2023-06-26 13:24:22 +0200
  • da2f4cb100 Try to parse values only for satisfiable answer Martin Blicha 2023-06-26 13:23:57 +0200
  • efb0d4253c Use callback properly in SMTLib2 interface Martin Blicha 2023-06-26 11:55:31 +0200
  • cabec89872 Removing SMT portfolio Martin Blicha 2023-06-26 10:31:02 +0200
  • 1e190abf6e Initial work on unified way to interact with solvers Martin Blicha 2023-06-20 16:10:45 +0200
  • c4af926a5d
    Merge pull request #14524 from ethereum/move-around-tests Daniel 2023-09-05 11:56:02 +0200
  • 42cfbdcd14 Exclude list for AST JSON tests Nikola Matic 2023-09-05 09:06:01 +0200
  • f30c0ed1d3 Move around experimental tests Nikola Matic 2023-08-29 14:35:58 +0200
  • b2bafc563e Remove bogus unused IRVariable implementation (to be redone). Daniel Kirchner 2023-08-22 21:05:36 +0200
  • 6fbf85e5c4 Platform fixes. Daniel Kirchner 2023-08-22 18:33:34 +0200
  • 13f34354d1 Add comment. Daniel Kirchner 2023-08-22 18:23:16 +0200
  • 7420a4fe19 error ids Daniel Kirchner 2023-08-22 18:17:14 +0200
  • 2bc62b0271 Fix compiler warning. Daniel Kirchner 2023-08-22 18:11:11 +0200
  • f7cbddb7d5 style fixes Daniel Kirchner 2023-08-22 17:56:26 +0200
  • 43ca0f0947 Eliminate using namespace std. Daniel Kirchner 2023-08-22 15:05:39 +0200
  • 45f00dda3b Type inference draft. Daniel Kirchner 2023-06-14 12:48:38 +0200
  • 6ec4d3dd98 Scanner hack. Daniel Kirchner 2023-06-13 20:42:59 +0200
  • 6347faa86f Basic infrastructure. Daniel Kirchner 2023-06-06 11:18:46 +0200
  • 16ae76cad7
    Merge pull request #14533 from ethereum/fix-std-namespace-asan Daniel 2023-09-05 11:04:13 +0200
  • ae36323edb Fix missing std qualifier for ASAN Nikola Matic 2023-09-05 08:49:23 +0200
  • e43968599e
    Merge pull request #14468 from ethereum/push0-rematerializer-default-sequence Daniel 2023-09-04 19:27:33 +0200
  • fdc6699159 Rematerialize zero literals with default cleanup sequence Nikola Matic 2023-08-04 17:31:39 +0200
  • 1b8e792eb6
    Merge pull request #14530 from ethereum/fix-oz-failing-test Daniel 2023-09-04 13:08:47 +0200
  • 76e0d81354 Fix failing OZ test Nikola Matic 2023-09-04 12:22:18 +0200
  • 737c1abbdf
    Merge pull request #14525 from molecula451/purge-std Nikola Matić 2023-09-04 11:02:15 +0200
  • b3230b0bdc deprecate using namespace std Paul 2023-08-30 00:08:06 +0000
  • 69d6812d4b
    Merge 0831f1bff2 into df03f1412d Alex Beregszaszi 2023-09-01 19:52:16 -0700
  • f41c2c9330
    Update abi-spec.rst devlynnx 2023-08-31 03:21:38 -0700
  • 4aca2abcb3 code-style fixes ssi91 2023-08-26 19:30:58 -0400