solidity/test/libsolidity/smtCheckerTests/functions
Martin Blicha cdfc19b503 SMTChecker: Bring back counterexample checks in regression tests
Since the default is now to ignore the counterexamples when checking
test output, we bring back counterexample checks in tests where the
counterexample is (mostly) deterministic.
2023-07-25 12:26:21 +02:00
..
getters SMTChecker: Bring back counterexample checks in regression tests 2023-07-25 12:26:21 +02:00
abi_encode_functions.sol
constructor_base_basic.sol
constructor_hierarchy_2.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_3.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_4.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_diamond_2.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_diamond_3.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_diamond_empty_middle_empty_base.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_diamond_empty_middle.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_diamond.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_empty_chain.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_empty_middle_no_invocation.sol
constructor_hierarchy_empty_middle.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_mixed_chain_empty_base.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_mixed_chain_local_vars.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_mixed_chain_with_params_2.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_mixed_chain_with_params.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_mixed_chain.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_hierarchy_modifier.sol
constructor_hierarchy_same_var.sol
constructor_hierarchy.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_simple.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_state_value_inherited.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_state_value_parameter.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_state_value.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
constructor_this.sol
function_call_does_not_clear_local_vars.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
function_call_state_var_init.sol
function_external_call_should_not_inline_1.sol
function_external_call_should_not_inline_2.sol
function_inline_chain.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
function_inside_branch_modify_state_var_2.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
function_inside_branch_modify_state_var_3.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
function_inside_branch_modify_state_var.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
functions_attached_1_fail.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
functions_attached_1.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
functions_external_1.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
functions_external_2.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
functions_external_3.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
functions_external_4.sol
functions_identifier_nested_tuple_1.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
functions_identifier_nested_tuple_2.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
functions_identifier_nested_tuple_3.sol
functions_identity_1_fail.sol SMTChecker: Bring back counterexample checks in regression tests 2023-07-25 12:26:21 +02:00
functions_identity_1.sol Remove EWASM backend. 2023-05-11 10:56:55 -05:00
functions_identity_2_fail.sol SMTChecker: Bring back counterexample checks in regression tests 2023-07-25 12:26:21 +02:00
functions_identity_2.sol Remove EWASM backend. 2023-05-11 10:56:55 -05:00
functions_identity_as_tuple_fail.sol Remove EWASM backend. 2023-05-11 10:56:55 -05:00
functions_identity_as_tuple.sol Remove EWASM backend. 2023-05-11 10:56:55 -05:00
functions_library_1_fail.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
functions_library_1.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
functions_library_internal.sol Fix error in SMTChecker: Use rich indentifier instead of external identifier to ecnode member access to functions 2023-06-23 15:24:55 +02:00
functions_recursive_indirect.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
functions_recursive.sol Remove EWASM backend. 2023-05-11 10:56:55 -05:00
functions_storage_var_1_fail.sol Remove EWASM backend. 2023-05-11 10:56:55 -05:00
functions_storage_var_1.sol Remove EWASM backend. 2023-05-11 10:56:55 -05:00
functions_storage_var_2_fail.sol Remove EWASM backend. 2023-05-11 10:56:55 -05:00
functions_storage_var_2.sol Remove EWASM backend. 2023-05-11 10:56:55 -05:00
functions_trivial_condition_for_only_call.sol
functions_trivial_condition_if.sol
functions_trivial_condition_require_only_call.sol
functions_trivial_condition_require.sol
functions_trivial_condition_while_only_call.sol
internal_call_inheritance.sol
internal_call_state_var_init_2.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
internal_call_state_var_init.sol
internal_call_with_assertion_1_fail.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
internal_call_with_assertion_1.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
internal_call_with_assertion_inheritance_1_fail.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
internal_call_with_assertion_inheritance_1.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
internal_multiple_calls_with_assertion_1_fail.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
internal_multiple_calls_with_assertion_1.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
library_after_contract.sol Remove EWASM backend. 2023-05-11 10:56:55 -05:00
library_constant_2.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
library_constant.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
library_public_called_as_internal_1.sol Fix SMTChecker bug when a public library function is called internally by an internal library function, which in turn is called internally by a contract. 2022-11-28 13:07:18 +01:00
library_public_called_as_internal_2.sol Fix SMTChecker bug when a public library function is called internally by an internal library function, which in turn is called internally by a contract. 2022-11-28 13:07:18 +01:00
payable_1.sol Fix BMCs constraints on internal functions 2021-09-15 14:42:39 +02:00
payable_2.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
recursive_multi_return_2.sol
recursive_multi_return.sol
super_function_assert.sol SMTChecker: Bring back counterexample checks in regression tests 2023-07-25 12:26:21 +02:00
this_external_call_2.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
this_external_call_return.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
this_external_call_sender.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
this_external_call_tx_origin.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
this_external_call.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
this_state.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
virtual_function_assert.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00
virtual_function_called_by_constructor.sol Report safe properties in BMC and CHC 2023-03-09 14:59:32 +01:00