Leonardo Alt
cff0836c03
Fix PR comments
2018-02-28 18:05:20 +01:00
Leonardo Alt
21c6b80fc9
Supported types listed in SSAVariable
2018-02-28 18:05:20 +01:00
Leonardo Alt
3b2851ee41
Integer min and max values placed under SymbolicIntVar instead of SMTChecker
2018-02-28 18:05:20 +01:00
Leonardo Alt
f41591b3dd
[SMTChecker] A little refactoring on SSA vars
2018-02-28 18:05:20 +01:00
Leonardo Alt
d0abc5359b
[SMTChecker] Variables are merged after branches (ite variables)
2018-01-04 18:20:12 +01:00
Leonardo Alt
b588134840
[SMTChecker] Fix typo in the code (satisifable->satisfiable)
2017-12-18 17:31:27 +01:00
Leonardo Alt
a1e296e392
[SMTChecker] Helper functions to add an expression to the solver conjoined with or implied by the current path conditions
2017-12-13 17:59:36 +01:00
Leonardo Alt
2af4d7c7dd
[SMTChecker] Keep track of current path conditions
2017-12-13 17:39:10 +01:00
chriseth
a256983320
Fix expression creation problems.
2017-11-30 01:20:21 +01:00
chriseth
d160ec8595
Fix signed division.
2017-11-30 01:20:21 +01:00
chriseth
19e067465a
Unary operators and division.
2017-11-30 01:20:21 +01:00
chriseth
0e2a9658d2
Explain IntIntFun and merge assertion.
2017-11-23 19:02:47 +01:00
chriseth
762d591a47
Introduce sorts for smt expressions.
2017-11-22 15:20:26 +01:00
chriseth
8538a25f8d
Fix problem with non-value-typed variables.
2017-11-22 02:35:34 +00:00
chriseth
19d5c42429
For loop.
2017-11-22 02:35:34 +00:00
chriseth
95a65dc04c
Fix boolean constants.
2017-11-22 02:35:34 +00:00
chriseth
22c689d516
Check for conditions being constant.
2017-11-22 02:35:34 +00:00
chriseth
e5de4a66ed
Tests.
2017-11-22 02:35:34 +00:00
chriseth
b37377641d
Track usage of variables.
2017-11-22 02:35:34 +00:00
chriseth
f62caf587e
Handle branches.
2017-11-22 02:35:34 +00:00
chriseth
7d0e46bf59
Merge pull request #3030 from ethereum/smt-variable-types
...
SMT enforce variable types
2017-10-20 16:55:09 +02:00
Alex Beregszaszi
7a4c165518
Remove unused variable in Z3
2017-10-18 23:18:11 +01:00
chriseth
153ae98878
Catch exception in Z3.
...
Note: This exception might not be the result of resource limitation,
it might also hint towards usage error.
2017-10-17 18:30:10 +01:00
Alex Beregszaszi
a71c6faf0f
Remove duplicate >= in Z3
2017-10-17 18:30:07 +01:00
chriseth
1f97c1ea8f
Rename variables in SMT checker.
2017-10-17 18:29:53 +01:00
Alex Beregszaszi
18ae0c3d78
SMT enforce variable types
2017-10-05 12:29:20 +01:00
Alex Beregszaszi
10529e994f
SMT should not crash on typecast/structs
2017-10-05 11:41:11 +01:00
Alex Beregszaszi
66b188cce9
Merge pull request #3022 from ethereum/assert
...
Use solAssert and not assert
2017-10-04 14:11:43 +01:00
Alex Beregszaszi
a9847c9551
Use solAssert and not assert
2017-10-04 13:05:55 +01:00
chriseth
5ee3ceaef7
Remove leftover couts.
2017-09-29 12:44:39 +02:00
Alex Beregszaszi
1c0c5d923a
Mark constructors explicit
2017-09-20 01:23:21 +01:00
chriseth
9e63710b8e
Remove parameter names for defaulted functions.
2017-08-31 12:16:41 +02:00
chriseth
cf5e1d6120
Review changes.
2017-08-23 17:37:35 +02:00
chriseth
c93f0434cd
Use experimental feature pragma for SMT checker.
2017-08-23 17:37:35 +02:00
chriseth
75f09f2a84
Partial support for if statements.
2017-08-23 17:37:35 +02:00
chriseth
5bfd5d98c1
Format numbers more nicely.
2017-08-23 17:37:35 +02:00
chriseth
1e05ebe50e
Refactor Z3 read callback.
2017-08-23 17:37:35 +02:00
chriseth
9ac2ac14c1
Rename read file callback.
2017-08-23 17:37:35 +02:00
chriseth
ab5e3a8f6d
Introduce native Z3 support.
2017-08-23 17:37:35 +02:00
chriseth
4cea3d4aa4
Insert abstraction layer.
2017-08-23 17:37:35 +02:00
chriseth
c9cf24458b
Prepare build system for Z3.
2017-08-23 17:37:35 +02:00
chriseth
b3f8ed457a
Cleanup.
2017-08-23 14:24:30 +02:00
chriseth
39fc798999
Use file to communicate with z3.
2017-08-23 14:24:05 +02:00
chriseth
df848859da
Rewrite using SMTLIB2 interface.
2017-08-23 14:24:05 +02:00
chriseth
1ece7bf443
z3 conditions
2017-08-23 14:24:04 +02:00
Alex Beregszaszi
555dc4f46f
Remove Why3 generator
2017-06-25 12:26:16 +01:00
Rhett Aultman
89b60ffbd4
Refactor error reporting
...
This commit introduces ErrorReporter, a utility class which consolidates
all of the error logging functionality into a common set of functions.
It also replaces all direct interactions with an ErrorList with calls to
an ErrorReporter.
This commit resolves issue #2209
2017-05-30 07:28:31 -07:00
djudjuu
1d22233a43
refactoring functionCallAnnotation
2017-05-19 15:48:07 +02:00
Alex Beregszaszi
3ae88377d6
Change references to FunctionType::Location
2017-03-16 12:49:52 +00:00
VoR0220
3f9f725737
Fix licensing headers
...
Signed-off-by: VoR0220 <rj@erisindustries.com >
2016-11-23 12:22:33 +01:00
Leonardo Alt
chriseth
Alex Beregszaszi
Rhett Aultman
djudjuu
VoR0220