Leonardo Alt
77b9416d3e
Extract SMTChecker mod test
2019-12-09 15:32:08 +01:00
Leonardo Alt
02343208ad
Extract SMTChecker compound assignment division tests
2019-12-09 15:32:08 +01:00
Leonardo Alt
ae6cdc3442
Extract more SMTChecker division tests
2019-12-09 15:32:08 +01:00
Leonardo Alt
b870e4ea31
Extract SMTChecker division tests
2019-12-09 15:32:08 +01:00
Leonardo Alt
a774b2d905
[SMTChecker] Zero-initialize arrays
2019-09-02 22:37:30 +02:00
Leonardo Alt
c27235b2f5
[SMTChecker] Adapt division test for Z3 only
2019-08-23 17:33:29 +02:00
Leonardo Alt
955b97097c
[SMTChecker] Relax expectations for complex nonlinear tests
2019-08-11 22:20:31 +02:00
Leonardo Alt
4214cd1354
[SMTChecker] Fix ICE when reporting cex concerning state vars from different source files
2019-08-10 20:56:52 +02:00
Leonardo Alt
7b22496b1f
[SMTChecker] Fix ICE when inlining functions that use state vars and are in a different source
2019-08-09 17:50:52 +02:00
rocky
ca3afea1d7
Add Steve Johnson-style parser recovery rules:
...
SourceUnit = Error $
Block = '{' Error '}'
ContractDefinition = '{' Error '}'
Statement = Error ';'
Co-Authored-By: chriseth <chris@ethereum.org>
2019-06-17 14:47:07 +02:00
chriseth
4ee703e6e5
Revert "Add Steve Johnson-style parser recovery rules:"
...
This reverts commit 97f8ee0d1b
.
2019-05-28 18:09:24 +02:00
rocky
97f8ee0d1b
Add Steve Johnson-style parser recovery rules:
...
SourceUnit = Error $
Block = '{' Error '}'
ContractDefinition = '{' Error '}'
Statement = Error ';'
Co-Authored-By: chriseth <chris@ethereum.org>
2019-05-28 15:06:34 +02:00
Leonardo Alt
af9f16e014
[SMTChecker] Support mod
2019-04-12 12:39:25 +02:00
Leonardo Alt
c7e5468505
Arithmetic compound assignment operators tests
2019-03-28 15:27:52 +01:00
Leonardo Alt
123d0857c5
[SMTChecker] Move tests that contain division to boost tests
2019-02-20 12:17:03 +01:00
Alex Beregszaszi
636da48e82
Move most of SMTChecker tests from C++ to isoltest
...
But keep divison in C++ because results differ between different solvers
2018-11-22 13:33:24 +00:00
Christian Parpart
d67322a186
Introduce namespace langutil
in liblangutil directory.
...
Also:
- Use {}-style list initialisation for SourceLocation construction
- Introduce new system includes
- Changes the API of the Scanner to take source as value (with move) as opposed to as a reference
2018-11-21 19:13:44 +00:00
Leonardo Alt
b46b827c30
[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash
2018-10-19 15:52:16 +02:00
Leonardo Alt
e4851cf59e
[SMTChecker] Inline calls to internal functions
2018-10-15 15:11:21 +02:00
liangdzou
808c3f3df5
fix some format typos
2018-09-17 22:13:21 +08:00
Leonardo Alt
90f319615f
SMT model variables are sorted and printed as secondary source location
2018-08-01 23:27:46 +02:00
Chase McDermott
f48d01d066
Added default data locations to parameters for end to end tests.
2018-07-16 14:18:16 +02:00
Alex Beregszaszi
c7f842d4cc
Do not change SMT tests
2018-06-25 16:17:50 +02:00
Jason Cobb
98c9ca2575
Update tests for strict address literals
2018-06-25 16:17:50 +02:00
Leonardo Alt
8862b3092b
C99 scoping rules by default
2018-06-20 12:53:38 +02:00
Leonardo Alt
0b6eea0c55
Bool variables should not allow arithmetic comparison
2018-05-16 18:32:47 +02:00
Leonardo Alt
a0b42105e4
Testing state vars that are declared after functions that use them
2018-05-15 14:28:08 +02:00
Leonardo Alt
4117e859eb
[SMTChecker] Declaring all state vars before any function is visited
2018-05-15 14:28:08 +02:00
Leonardo Alt
2dbb35d4a8
[SMTChecker] Support to integer and Bool storage vars
2018-05-15 14:22:50 +02:00
chriseth
8debded743
Revert "BREAKING: Bool variables should not allow arithmetic comparison"
2018-05-02 15:56:59 +02:00
Leonardo Alt
ab251c7e7d
Bool variables should not allow arithmetic comparison
2018-04-27 11:35:58 +02:00
Leonardo Alt
c2d26eb6a2
[SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests.
2018-03-12 20:16:47 +01:00
Leonardo Alt
6a940f0a99
[SMTChecker] Support to Bool variables
2018-03-12 20:16:47 +01:00
chriseth
69f5f2eb65
Adjust tests.
2018-02-27 12:17:25 +01:00
chriseth
c182284d28
Do not warn about analysis-only experimental features.
2018-02-22 14:50:20 +01:00
chriseth
676cf52264
Support searching inside multiple errors.
2018-02-12 16:41:31 +01:00
Leonardo Alt
d0abc5359b
[SMTChecker] Variables are merged after branches (ite variables)
2018-01-04 18:20:12 +01:00
Alex Beregszaszi
b32d7a84fc
Move some struct tests to require ABIEncoderV2
2017-12-11 02:42:09 +00:00
chriseth
6d609557b6
Fix test.
2017-12-04 12:57:36 +01:00
chriseth
00e252a39f
Another test for division.
2017-11-30 01:20:21 +01:00
chriseth
19e067465a
Unary operators and division.
2017-11-30 01:20:21 +01:00
chriseth
19d5c42429
For loop.
2017-11-22 02:35:34 +00:00
chriseth
5e2c066778
Test for multi-branches.
2017-11-22 02:35:34 +00:00
chriseth
95a65dc04c
Fix boolean constants.
2017-11-22 02:35:34 +00:00
chriseth
90fb14f525
Tests.
2017-11-22 02:35:34 +00:00
chriseth
e5de4a66ed
Tests.
2017-11-22 02:35:34 +00:00
Alex Beregszaszi
10529e994f
SMT should not crash on typecast/structs
2017-10-05 11:41:11 +01:00
chriseth
5028ccbe84
Tests for SMT checker.
2017-09-29 15:31:00 +02:00