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
Files
8bb371ffa9bd3c9ebe2e81308bf68b00a608ba74
solidity/test/libsolidity/smtCheckerTests/operators
T
History
Leonardo Alt ba97d6ac4e Add local vars to cex
2021-03-30 17:55:21 +02:00
..
shifts
Add local vars to cex
2021-03-30 17:55:21 +02:00
assignment_contract_member_variable_array_2.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
assignment_contract_member_variable_array_3.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
assignment_contract_member_variable_array.sol
Remove extra line breaks
2021-01-12 14:00:07 +01:00
assignment_contract_member_variable.sol
[SMTChecker] Adding unary increment and decrement as under/overflow verification targets for the CHC engine
2020-12-11 17:41:50 +01:00
assignment_module_contract_member_variable.sol
Remove extra line breaks
2021-01-12 14:00:07 +01:00
bitwise_and_fixed_bytes.sol
Remove extra line breaks
2021-01-12 14:00:07 +01:00
bitwise_and_int.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
bitwise_and_rational.sol
Remove extra line breaks
2021-01-12 14:00:07 +01:00
bitwise_and_uint.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
bitwise_combo.sol
[SMTChecker] Support bitwise or, xor and not.
2020-08-26 11:06:56 +02:00
bitwise_not_fixed_bytes.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
bitwise_not_int.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
bitwise_not_uint.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
bitwise_or_fixed_bytes.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
bitwise_or_int.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
bitwise_or_uint.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
bitwise_rational_1.sol
Tests/Docs after "stricter explicit conversion from Literals to Integers"
2020-11-03 14:31:44 +01:00
bitwise_rational_2.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
bitwise_xor_fixed_bytes.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
bitwise_xor_int.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
bitwise_xor_uint.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
bytes_new.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_add_array_index.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
compound_add_chain.sol
Arithmetic compound assignment operators tests
2019-03-28 15:27:52 +01:00
compound_add_mapping.sol
Remove extra line breaks
2021-01-12 14:00:07 +01:00
compound_add.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_assignment_division_1.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_assignment_division_2.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
compound_assignment_division_3.sol
Remove extra line breaks
2021-01-12 14:00:07 +01:00
compound_assignment_right_shift.sol
added test
2020-12-08 13:05:16 +01:00
compound_bitwise_and_fixed_bytes.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_bitwise_and_int.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_bitwise_and_uint.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_bitwise_or_fixed_bytes.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_bitwise_or_int_1.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
compound_bitwise_or_int.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_bitwise_or_uint_1.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
compound_bitwise_or_uint_2.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
compound_bitwise_or_uint_3.sol
Add unknown message to all verification targets
2020-10-19 20:54:13 +01:00
compound_bitwise_or_uint.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_bitwise_string_literal_2.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_bitwise_string_literal_3.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_bitwise_string_literal.sol
[SMTChecker] Added constraints for block properties
2020-12-29 22:17:44 +01:00
compound_bitwise_xor_fixed_bytes.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_bitwise_xor_int.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_bitwise_xor_uint.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_mul_array_index.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
compound_mul_mapping.sol
Remove extra line breaks
2021-01-12 14:00:07 +01:00
compound_mul.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
compound_shl_1.sol
[SMTChecker] Updating old and adding new tests for compound shift operators.
2020-09-23 11:31:37 +02:00
compound_shr_1.sol
[SMTChecker] Add engine prefix to verification target error messages
2020-09-25 19:09:06 +02:00
compound_sub_array_index.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
compound_sub_mapping.sol
Add and update tests
2020-12-17 14:42:49 +01:00
compound_sub.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
conditional_assignment_1.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
conditional_assignment_2.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
conditional_assignment_3.sol
[SMTChecker] Added transaction constraints also for contract deployment
2021-02-01 16:46:34 +01:00
conditional_assignment_4.sol
[SMTChecker] Supporting conditional operator
2020-08-20 21:39:35 +02:00
conditional_assignment_5.sol
Add msgvalue to cex
2021-01-21 19:05:44 +01:00
conditional_assignment_6.sol
[SMTChecker] Supporting conditional operator
2020-08-20 21:39:35 +02:00
conditional_assignment_always_false.sol
[SMTChecker] Add engine prefix to verification target error messages
2020-09-25 19:09:06 +02:00
conditional_assignment_always_true.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
conditional_assignment_function_1.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
conditional_assignment_function_2.sol
Move CHC counterexamples to primary location
2020-12-09 19:55:18 +01:00
conditional_assignment_nested_always_true.sol
[SMTChecker] Add engine prefix to verification target error messages
2020-09-25 19:09:06 +02:00
conditional_assignment_nested_unsafe.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
conditional_assignment_statevar_1.sol
[SMTChecker] Support check/unchecked
2020-12-30 12:14:30 +01:00
const_exp_1.sol
Remove extra line breaks
2021-01-12 14:00:07 +01:00
constant_propagation_1.sol
Remove extra line breaks
2021-01-12 14:00:07 +01:00
constant_propagation_2.sol
Fix constant evaluation build
2020-12-16 17:59:00 +01:00
delete_array_2d.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
delete_array_index_2d.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
delete_array_index.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
delete_array_push.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
delete_array.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
delete_function.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
delete_multid_array.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
delete_struct.sol
Update current tests
2020-09-03 15:19:03 +02:00
delete_tuple.sol
[SMTChecker] Fix internal error when array.push() is used as LHS of assignment
2020-11-02 13:32:53 +00:00
div_zero.sol
Add contract name to called function in cex
2021-01-04 10:03:16 +01:00
division_1.sol
Add contract name to called function in cex
2021-01-04 10:03:16 +01:00
division_2.sol
Extract SMTChecker division tests
2019-12-09 15:32:08 +01:00
division_3.sol
Add contract name to called function in cex
2021-01-04 10:03:16 +01:00
division_4.sol
[SMTChecker] encoding division and modulo operations using slack variables
2020-10-16 16:06:31 +02:00
division_5.sol
[SMTChecker] Support check/unchecked
2020-12-30 12:14:30 +01:00
division_6.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
division_7.sol
Extract SMTChecker division tests
2019-12-09 15:32:08 +01:00
division_truncates_correctly_1.sol
[SMTChecker] encoding division and modulo operations using slack variables
2020-10-16 16:06:31 +02:00
division_truncates_correctly_2.sol
[SMTChecker] encoding division and modulo operations using slack variables
2020-10-16 16:06:31 +02:00
division_truncates_correctly_3.sol
[SMTChecker] encoding division and modulo operations using slack variables
2020-10-16 16:06:31 +02:00
division_truncates_correctly_4.sol
[SMTChecker] encoding division and modulo operations using slack variables
2020-10-16 16:06:31 +02:00
division_truncates_correctly_5.sol
[SMTChecker] encoding division and modulo operations using slack variables
2020-10-16 16:06:31 +02:00
exp.sol
Remove extra line breaks
2021-01-12 14:00:07 +01:00
fixed_point_add.sol
[SMTChecker] Support type conversions
2020-10-02 10:26:02 +02:00
fixed_point_compound_add.sol
Update remaining tests
2020-08-14 12:58:27 +02:00
function_call_named_arguments.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
index_access_for_bytes.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
index_access_for_bytesNN.sol
[SMTChecker] Keep knowledge about string literals
2020-09-25 11:32:23 +01:00
index_access_for_string.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
index_access_side_effect.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
integer_new.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
mod_even.sol
[SMTChecker] encoding division and modulo operations using slack variables
2020-10-16 16:06:31 +02:00
mod_n_uint16.sol
[SMTChecker] encoding division and modulo operations using slack variables
2020-10-16 16:06:31 +02:00
mod_n.sol
[SMTChecker] encoding division and modulo operations using slack variables
2020-10-16 16:06:31 +02:00
mod_signed.sol
Add unknown message to all verification targets
2020-10-19 20:54:13 +01:00
mod.sol
[SMTChecker] encoding division and modulo operations using slack variables
2020-10-16 16:06:31 +02:00
named_arguments_in_any_order.sol
[SMTChecker] Support named arguments in function calls
2020-11-20 11:52:26 -01:00
named_arguments_overload_in_any_order.sol
[SMTChecker] Support named arguments in function calls
2020-11-20 11:52:26 -01:00
slice_bytes.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
slice_default_end.sol
Natspec: Fix internal error when different return name was inherited
2020-11-17 11:56:32 +01:00
slice_default_start.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
slice.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
slices_1.sol
Support array slices
2020-10-01 11:52:02 +02:00
slices_2.sol
[SMTChecker] Use same sort name for array slice as for the underlying array.
2021-03-09 11:06:22 +01:00
slices_3.sol
[SMTChecker] Use same sort name for array slice as for the underlying array.
2021-03-09 11:06:22 +01:00
tuple_rationals_conditional.sol
Fix ICE on conditions with tuples of rationals
2020-10-23 14:47:53 +01:00
unary_add_array_push_1.sol
Remove extra line breaks
2021-01-12 14:00:07 +01:00
unary_add_array_push_2.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
unary_add_array.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
unary_add_mapping.sol
[SMTChecker] Adding unary increment and decrement as under/overflow verification targets for the CHC engine
2020-12-11 17:41:50 +01:00
unary_add_minus_overflow_detected.sol
Remove extra line breaks
2021-01-12 14:00:07 +01:00
unary_add_overflows_correctly_struct.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
unary_add_overflows_correctly.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
unary_add.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
unary_operators_tuple_1.sol
[SMTChecker] Fix unary operator on lvalue tuple
2020-09-01 08:25:06 +02:00
unary_operators_tuple_2.sol
[SMTChecker] Fix unary operator on lvalue tuple
2020-09-01 08:25:06 +02:00
unary_operators_tuple_3.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00
unary_sub_array.sol
Report out of bounds index access
2021-03-30 10:28:48 +02:00
unary_sub_mapping.sol
Add and update tests
2020-12-17 14:42:49 +01:00
unary_sub.sol
Add local vars to cex
2021-03-30 17:55:21 +02:00