72 Commits

Author	SHA1	Message	Date
Daniel Kirchner	3c9f18b749	Use IRVariable's in IR code generation and implement tuples.	2020-02-12 12:36:14 +01:00
chriseth	b3fe84a6ea	Merge pull request #7153 from djudjuu/newImportAST ... import ast from JSON	2020-01-14 17:56:53 +01:00
djudjuu	e8556fa1b2	Ast-Import from standard-json	2020-01-14 17:15:53 +01:00
Christian Parpart	abb9f1eed7	CMake: Renaming devcore static library to solutil (to match source code paths)	2020-01-13 15:52:46 +01:00
chriseth	93d84f3554	Split out override checker into its own file.	2019-12-10 16:00:05 +01:00
chriseth	e061f1e743	Merge remote-tracking branch 'origin/develop' into HEAD	2019-12-05 16:44:26 +01:00
Gaith Hallak	4d90180e24	Support referencing other constants in inline assembly	2019-12-05 13:27:17 +03:00
chriseth	216e1749f4	Merge remote-tracking branch 'origin/develop' into develop_060	2019-11-14 13:42:46 +01:00
Leonardo Alt	5f43b8dbeb	Output the storage layout of a contract via storageLayout artifact	2019-11-14 10:19:17 +01:00
chriseth	2e5a42836c	Merge pull request #7681 from ethereum/develop ... Merge develop into develop_060	2019-11-11 16:42:03 +01:00
chriseth	138ee647f1	Provide different options for reason strings.	2019-11-07 14:13:53 +01:00
Leonardo Alt	6b10efff8c	Add CHCSmtLib2Interface	2019-11-07 11:12:11 +01:00
Daniel Kirchner	5d69bdf81e	Remove ASTPrinter.	2019-09-06 12:38:55 +02:00
Leonardo Alt	03cc124f32	Add CHC skeleton	2019-07-19 11:52:05 +02:00
Leonardo Alt	71144d0d39	[CHCChecker] Add CHCSolverInterface and Z3CHCSolverInterface	2019-07-15 17:31:39 +02:00
Leonardo Alt	3cb4ed83c1	[SMTChecker] Split SMTChecker into SMTEncoder and BMC	2019-07-01 15:05:03 +02:00
Daniel Kirchner	226f8bb64d	Use imported cmake targets for boost.	2019-06-06 18:49:34 +02:00
Daniel Kirchner	9f5340fa53	Try to find Z3 using CONFIG_MODE before manual search.	2019-06-04 15:58:03 +02:00
chriseth	aa4d4afcdc	LValues and state variables of value type.	2019-05-02 17:03:22 +02:00
Leonardo Alt	dd1afeba52	[SMTChecker] Support this as address	2019-04-18 17:56:52 +02:00
chriseth	0bfd587363	Merge pull request #6527 from rocky/move-SemVerHandler ... Move SemVerHandler to analysis to parsing to increase modularity...	2019-04-18 13:00:45 +02:00
rocky	b424446c5f	Move SemVerHandler to analysis to parsing to increase modularity... ... If ever you want to separate building analysis from scanning/parsing/ast, this will help.	2019-04-17 10:13:42 -04:00
Christian Parpart	bf43eebea9	libsolidity: Introducing TypeProvider API, for clear type system ownership.	2019-04-16 18:26:45 +02:00
chriseth	18ab8aeb85	Overflow-checked addition.	2019-04-11 15:45:14 +02:00
chriseth	420a7dc3d6	Initial IR generator.	2019-04-04 15:02:42 +02:00
chriseth	d515d77bfe	Extract utility functions from ABI encoder.	2019-03-05 22:13:55 +01:00
Alex Beregszaszi	cf5c13f9c7	Introduce global optimiser settings.	2019-03-04 11:40:28 +01:00
chriseth	d073eb1544	Move AssemblyStack to libyul.	2019-02-13 12:23:07 +01:00
chriseth	1ff6f2c71c	Move AsmCodeGen.	2019-02-13 11:20:15 +01:00
Leonardo Alt	4058978b3b	Require Z3 >= 4.6.0	2019-02-07 14:24:40 +01:00
chriseth	e970590675	Merge pull request #5664 from ethereum/cmakeUpdates ... Use imported CMake targets.	2018-12-18 17:45:23 +01:00
Daniel Kirchner	2f698b6efe	Use imported CMake targets.	2018-12-17 15:15:11 +01:00
Daniel Kirchner	2353f73c39	Add headers to targets in CMakeLists.txt.	2018-12-17 15:01:02 +01:00
chriseth	0ec7a0e72c	Move AsmCodeGen.	2018-12-04 15:20:23 +01:00
chriseth	0bd9db480f	Add skeleton for contract level checker.	2018-11-30 16:30:19 +01:00
chriseth	a46d5c6580	Fix merge problem in CMake files.	2018-11-26 14:50:04 +01:00
Christian Parpart	cdd8c72c9d	CMake: Explicitly state which files to compile instead of relying on globbing. ... Also remove header file lists, as there is no need to add them to add_library() or add_executable(), which should lower maintenance of the cmake files.	2018-11-26 14:39:24 +01:00
Christian Parpart	3734f40d31	CMake: Isolate libyul into its own static library	2018-11-23 12:37:37 +01:00
Christian Parpart	80371e2d25	Ensure liblangutil is compiled and linked as its own static library.	2018-11-21 18:58:36 +00:00
Christian Parpart	87821c53c3	Isolating files shared between Yul- and Solidity language frontend.	2018-11-21 18:58:12 +00:00
Christian Parpart	9a4bec7e47	Renaming libjulia to libyul	2018-10-15 11:52:35 +02:00
Daniel Kirchner	c7a0f44159	Do not force GMP to be present as dependency of CVC4, but also allow CLN instead.	2018-08-08 19:02:59 +02:00
Daniel Kirchner	9b4546c487	Add workarounds for building against CVC4 on ArchLinux.	2018-08-08 19:02:59 +02:00
Matías Aereal Aeón	4b20708c49	cmake flags to make solvers optional. Implementation of #4651	2018-08-08 12:43:57 -03:00
Leonardo Alt	87a38e1abe	[SMTChecker] SMTPortfolio: use all SMT solvers available	2018-07-27 16:15:34 +01:00
mingchuan	dbd0a7ed60	Fix link error when using boost shared library	2018-05-11 11:20:19 +08:00
Leonardo Alt	ae3350ae03	[SMTChecker] Integration with CVC4	2018-04-17 12:26:58 +01:00
Alex Beregszaszi	372c6693ea	Improve Z3 message in cmake	2017-10-13 13:33:18 +01:00
chriseth	c9cf24458b	Prepare build system for Z3.	2017-08-23 17:37:35 +02:00
chriseth	1ece7bf443	z3 conditions	2017-08-23 14:24:04 +02:00