 |
|
|
|
.. (parent) |
|
d |
rwxr-xr-x |
47 |
assigns-enforce-malloc-zero
|
|
d |
rwxr-xr-x |
47 |
assigns-frees-clauses-check-side-effects
|
|
d |
rwxr-xr-x |
47 |
assigns-local-composite
|
|
d |
rwxr-xr-x |
47 |
assigns-replace-ignored-return-value
|
|
d |
rwxr-xr-x |
47 |
assigns-replace-malloc-zero
|
|
d |
rwxr-xr-x |
116 |
assigns-slice-targets
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_01
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_02
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_03
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_04
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_05
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_06
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_07
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_08
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_09
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_10
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_11
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_12
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_13
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_14
|
|
d |
rwxr-xr-x |
99 |
assigns_enforce_15
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_16
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_17
|
|
d |
rwxr-xr-x |
99 |
assigns_enforce_18
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_19_a
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_19_b
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_20
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_21
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_23
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_address_of
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_arrays_01
|
|
d |
rwxr-xr-x |
73 |
assigns_enforce_arrays_02
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_arrays_03
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_arrays_04
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_arrays_05
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_arrays_10
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_function_call_condition
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_lvalue
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_lvalue_list
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_non_lvalue_target
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_non_lvalue_target_list
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_pointer_object
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_pointer_object_list
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_side_effect_condition
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_side_effect_target
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_side_effect_target_list
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_ternary_target
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_ternary_target_list
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_unions
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_void_target
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_conditional_void_target_list
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_detect_local_statics
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_detect_replaced_local_statics
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_free_dead
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_function_calls
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_function_calls_ignored
|
|
d |
rwxr-xr-x |
86 |
assigns_enforce_functions_in_contracts
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_havoc_object
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_literal
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_malloc_01
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_malloc_02
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_malloc_03
|
|
d |
rwxr-xr-x |
66 |
assigns_enforce_multi_file_01
|
|
d |
rwxr-xr-x |
66 |
assigns_enforce_multi_file_02
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_object_wrong_args
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_offsets_1
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_offsets_2
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_offsets_3
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_offsets_4
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_scoping_01
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_scoping_02
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_side_effects_1
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_side_effects_2
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_side_effects_3
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_statics
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_structs_01
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_structs_02
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_structs_03
|
|
d |
rwxr-xr-x |
119 |
assigns_enforce_structs_04
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_structs_05
|
|
d |
rwxr-xr-x |
96 |
assigns_enforce_structs_06
|
|
d |
rwxr-xr-x |
73 |
assigns_enforce_structs_07
|
|
d |
rwxr-xr-x |
73 |
assigns_enforce_structs_08
|
|
d |
rwxr-xr-x |
47 |
assigns_enforce_subfunction_calls
|
|
d |
rwxr-xr-x |
47 |
assigns_function_pointer
|
|
d |
rwxr-xr-x |
47 |
assigns_repeated_ignored
|
|
d |
rwxr-xr-x |
47 |
assigns_replace_01
|
|
d |
rwxr-xr-x |
47 |
assigns_replace_02
|
|
d |
rwxr-xr-x |
47 |
assigns_replace_03
|
|
d |
rwxr-xr-x |
47 |
assigns_replace_04
|
|
d |
rwxr-xr-x |
47 |
assigns_replace_05
|
|
d |
rwxr-xr-x |
47 |
assigns_replace_06
|
|
d |
rwxr-xr-x |
47 |
assigns_replace_07
|
|
d |
rwxr-xr-x |
47 |
assigns_replace_08
|
|
d |
rwxr-xr-x |
47 |
assigns_replace_09
|
|
d |
rwxr-xr-x |
47 |
assigns_replace_conditional_targets
|
|
d |
rwxr-xr-x |
123 |
assigns_replace_havoc_dependent_targets_fail
|
|
d |
rwxr-xr-x |
123 |
assigns_replace_havoc_dependent_targets_pass
|
|
d |
rwxr-xr-x |
47 |
assigns_type_checking_invalid_case_01
|
|
d |
rwxr-xr-x |
47 |
assigns_type_checking_invalid_case_02
|
|
d |
rwxr-xr-x |
4,096 |
assigns_type_checking_valid_cases
|
|
d |
rwxr-xr-x |
47 |
assigns_validity_pointer_01
|
|
d |
rwxr-xr-x |
47 |
assigns_validity_pointer_02
|
|
d |
rwxr-xr-x |
47 |
assigns_validity_pointer_03
|
|
d |
rwxr-xr-x |
47 |
assigns_validity_pointer_04
|
|
d |
rwxr-xr-x |
47 |
contracts_with_function_pointers
|
|
d |
rwxr-xr-x |
47 |
cprover-assignable-fail
|
|
d |
rwxr-xr-x |
47 |
cprover-assignable-pass
|
|
d |
rwxr-xr-x |
47 |
detect_loop_locals
|
|
d |
rwxr-xr-x |
47 |
detect_loop_locals2
|
|
d |
rwxr-xr-x |
102 |
dont_skip_cprover_prefixed_vars_fail
|
|
d |
rwxr-xr-x |
102 |
dont_skip_cprover_prefixed_vars_pass
|
|
d |
rwxr-xr-x |
47 |
embedded_contract_fail_01
|
|
d |
rwxr-xr-x |
47 |
embedded_contract_fail_02
|
|
d |
rwxr-xr-x |
73 |
enforce-replace-unknown-function
|
|
d |
rwxr-xr-x |
47 |
entry_point
|
|
d |
rwxr-xr-x |
47 |
frees-clause-and-predicates
|
|
d |
rwxr-xr-x |
47 |
frees-clause-and-predicates-fail
|
|
d |
rwxr-xr-x |
47 |
frees-clause-and-predicates-fail2
|
|
d |
rwxr-xr-x |
47 |
frees-clause-and-predicates-is_freeable-bad-arity
|
|
d |
rwxr-xr-x |
47 |
frees-clause-and-predicates-is_freed-bad-arity
|
|
d |
rwxr-xr-x |
47 |
function-calls-01-enforce-failure
|
|
d |
rwxr-xr-x |
47 |
function-calls-01-enforce-success
|
|
d |
rwxr-xr-x |
47 |
function-calls-01-replace-failure
|
|
d |
rwxr-xr-x |
47 |
function-calls-01-replace-success
|
|
d |
rwxr-xr-x |
112 |
function-calls-02-failure
|
|
d |
rwxr-xr-x |
112 |
function-calls-02-success
|
|
d |
rwxr-xr-x |
77 |
function-calls-03-direct-recursion
|
|
d |
rwxr-xr-x |
4,096 |
function-calls-04-mutual-recursion-failure
|
|
d |
rwxr-xr-x |
4,096 |
function-calls-04-mutual-recursion-success
|
|
d |
rwxr-xr-x |
47 |
function-calls-05-function-pointer-call-fail
|
|
d |
rwxr-xr-x |
47 |
function-calls-05-function-pointer-call-pass
|
|
d |
rwxr-xr-x |
82 |
function-calls-recursive-function-1
|
|
d |
rwxr-xr-x |
47 |
function-calls-recursive-function-2
|
|
d |
rwxr-xr-x |
4,096 |
function-contract-mapping
|
|
d |
rwxr-xr-x |
47 |
function-pointer-contracts-enforce
|
|
d |
rwxr-xr-x |
47 |
function-pointer-contracts-replace-1
|
|
d |
rwxr-xr-x |
47 |
function-pointer-contracts-replace-2
|
|
d |
rwxr-xr-x |
47 |
function-pointer-contracts-typecheck-error-1
|
|
d |
rwxr-xr-x |
47 |
function-pointer-contracts-typecheck-error-2
|
|
d |
rwxr-xr-x |
47 |
function-pointer-contracts-typecheck-error-3
|
|
d |
rwxr-xr-x |
47 |
function-pointer-contracts-typecheck-error-4
|
|
d |
rwxr-xr-x |
47 |
function_apply_01
|
|
d |
rwxr-xr-x |
47 |
function_check_01
|
|
d |
rwxr-xr-x |
47 |
function_check_02
|
|
d |
rwxr-xr-x |
47 |
function_check_03
|
|
d |
rwxr-xr-x |
47 |
function_check_04
|
|
d |
rwxr-xr-x |
47 |
function_check_05
|
|
d |
rwxr-xr-x |
47 |
function_check_mem_01
|
|
d |
rwxr-xr-x |
47 |
function_loop_history_ensures_fail
|
|
d |
rwxr-xr-x |
47 |
function_loop_history_requires_fail
|
|
d |
rwxr-xr-x |
47 |
function_no_apply_01
|
|
d |
rwxr-xr-x |
47 |
github_6168_infinite_unwinding_bug
|
|
d |
rwxr-xr-x |
108 |
havoc-conditional-target
|
|
d |
rwxr-xr-x |
75 |
havoc-static
|
|
d |
rwxr-xr-x |
47 |
history-constant
|
|
d |
rwxr-xr-x |
102 |
history-index
|
|
d |
rwxr-xr-x |
47 |
history-invalid
|
|
d |
rwxr-xr-x |
47 |
history-pointer-both-01
|
|
d |
rwxr-xr-x |
47 |
history-pointer-enforce-01
|
|
d |
rwxr-xr-x |
47 |
history-pointer-enforce-02
|
|
d |
rwxr-xr-x |
47 |
history-pointer-enforce-03
|
|
d |
rwxr-xr-x |
47 |
history-pointer-enforce-04
|
|
d |
rwxr-xr-x |
47 |
history-pointer-enforce-05
|
|
d |
rwxr-xr-x |
47 |
history-pointer-enforce-06
|
|
d |
rwxr-xr-x |
47 |
history-pointer-enforce-07
|
|
d |
rwxr-xr-x |
47 |
history-pointer-enforce-08
|
|
d |
rwxr-xr-x |
47 |
history-pointer-enforce-09
|
|
d |
rwxr-xr-x |
99 |
history-pointer-enforce-10
|
|
d |
rwxr-xr-x |
47 |
history-pointer-enforce-11
|
|
d |
rwxr-xr-x |
47 |
history-pointer-replace-01
|
|
d |
rwxr-xr-x |
47 |
history-pointer-replace-02
|
|
d |
rwxr-xr-x |
47 |
history-pointer-replace-03
|
|
d |
rwxr-xr-x |
47 |
history-pointer-replace-04
|
|
d |
rwxr-xr-x |
47 |
history-typecast
|
|
d |
rwxr-xr-x |
47 |
ignored_return_value
|
|
d |
rwxr-xr-x |
47 |
invar_assigns_empty
|
|
d |
rwxr-xr-x |
47 |
invar_assigns_opt
|
|
d |
rwxr-xr-x |
47 |
invar_check_break_fail
|
|
d |
rwxr-xr-x |
47 |
invar_check_break_pass
|
|
d |
rwxr-xr-x |
47 |
invar_check_continue
|
|
d |
rwxr-xr-x |
47 |
invar_check_large
|
|
d |
rwxr-xr-x |
47 |
invar_check_multiple_loops
|
|
d |
rwxr-xr-x |
47 |
invar_check_nested_loops
|
|
d |
rwxr-xr-x |
47 |
invar_check_pointer_modifies-01
|
|
d |
rwxr-xr-x |
47 |
invar_check_pointer_modifies-02
|
|
d |
rwxr-xr-x |
47 |
invar_check_sufficiency
|
|
d |
rwxr-xr-x |
47 |
invar_dynamic_struct_member
|
|
d |
rwxr-xr-x |
47 |
invar_function-old_fail
|
|
d |
rwxr-xr-x |
47 |
invar_havoc_dynamic_array
|
|
d |
rwxr-xr-x |
47 |
invar_havoc_dynamic_array_const_idx
|
|
d |
rwxr-xr-x |
47 |
invar_havoc_dynamic_multi-dim_array
|
|
d |
rwxr-xr-x |
47 |
invar_havoc_dynamic_multi-dim_array_all_const_idx
|
|
d |
rwxr-xr-x |
47 |
invar_havoc_dynamic_multi-dim_array_partial_const_idx
|
|
d |
rwxr-xr-x |
47 |
invar_havoc_static_array
|
|
d |
rwxr-xr-x |
47 |
invar_havoc_static_array_const_idx
|
|
d |
rwxr-xr-x |
47 |
invar_havoc_static_multi-dim_array
|
|
d |
rwxr-xr-x |
47 |
invar_havoc_static_multi-dim_array_all_const_idx
|
|
d |
rwxr-xr-x |
47 |
invar_havoc_static_multi-dim_array_partial_const_idx
|
|
d |
rwxr-xr-x |
47 |
invar_loop-entry_check
|
|
d |
rwxr-xr-x |
47 |
invar_loop-entry_fail
|
|
d |
rwxr-xr-x |
47 |
invar_loop_constant_fail
|
|
d |
rwxr-xr-x |
47 |
invar_loop_constant_no_modify
|
|
d |
rwxr-xr-x |
74 |
invar_loop_constant_pass
|
|
d |
rwxr-xr-x |
47 |
invar_loop_with_goto
|
|
d |
rwxr-xr-x |
47 |
invar_struct_member
|
|
d |
rwxr-xr-x |
47 |
invariant_side_effects
|
|
d |
rwxr-xr-x |
47 |
is_fresh_indirect_calls
|
|
d |
rwxr-xr-x |
47 |
is_unique_01_replace
|
|
d |
rwxr-xr-x |
47 |
labeled_loop_head
|
|
d |
rwxr-xr-x |
47 |
loop-freeness-check
|
|
d |
rwxr-xr-x |
47 |
loop_assigns-01
|
|
d |
rwxr-xr-x |
47 |
loop_assigns-02
|
|
d |
rwxr-xr-x |
47 |
loop_assigns-03
|
|
d |
rwxr-xr-x |
47 |
loop_assigns-04
|
|
d |
rwxr-xr-x |
47 |
loop_assigns-05
|
|
d |
rwxr-xr-x |
47 |
loop_assigns-fail
|
|
d |
rwxr-xr-x |
47 |
loop_assigns-slice-assignable-ptr
|
|
d |
rwxr-xr-x |
47 |
loop_assigns-slice-assignable-scalar
|
|
d |
rwxr-xr-x |
47 |
loop_assigns-slice-from
|
|
d |
rwxr-xr-x |
47 |
loop_assigns-slice-upto-fail
|
|
d |
rwxr-xr-x |
47 |
loop_assigns-slice-upto-pass
|
|
d |
rwxr-xr-x |
47 |
loop_assigns_function_paramters
|
|
d |
rwxr-xr-x |
47 |
loop_assigns_inference-01
|
|
d |
rwxr-xr-x |
47 |
loop_assigns_inference-02
|
|
d |
rwxr-xr-x |
47 |
loop_assigns_inference-03
|
|
d |
rwxr-xr-x |
47 |
loop_assigns_inference-04
|
|
d |
rwxr-xr-x |
47 |
loop_assigns_inference-05
|
|
d |
rwxr-xr-x |
47 |
loop_assigns_scoped_local_statics
|
|
d |
rwxr-xr-x |
47 |
loop_assigns_scoped_local_statics_propagate
|
|
d |
rwxr-xr-x |
47 |
loop_assigns_target_base_idents
|
|
d |
rwxr-xr-x |
47 |
loop_body_with_hole
|
|
d |
rwxr-xr-x |
47 |
loop_contracts_binary_search
|
|
d |
rwxr-xr-x |
4,096 |
loop_contracts_do_while
|
|
d |
rwxr-xr-x |
4,096 |
loop_contracts_file_fail
|
|
d |
rwxr-xr-x |
102 |
loop_contracts_memcmp
|
|
d |
rwxr-xr-x |
47 |
loop_contracts_no_unwind
|
|
d |
rwxr-xr-x |
47 |
loop_contracts_reject_inner_loops_without_contracts
|
|
d |
rwxr-xr-x |
47 |
loop_contracts_reject_loops_instruction_not_in_head_latch
|
|
d |
rwxr-xr-x |
47 |
loop_contracts_reject_loops_overlapping_spans
|
|
d |
rwxr-xr-x |
47 |
loop_contracts_reject_loops_two_latches
|
|
d |
rwxr-xr-x |
47 |
loop_contracts_statement_expression
|
|
d |
rwxr-xr-x |
47 |
loop_guard_with_side_effects
|
|
d |
rwxr-xr-x |
47 |
loop_guard_with_side_effects_fail
|
|
d |
rwxr-xr-x |
4,096 |
memory-predicates-is-fresh-failure-modes
|
|
d |
rwxr-xr-x |
47 |
memory-predicates-pointer-in-range-nondet
|
|
d |
rwxr-xr-x |
47 |
memory-predicates-pointer-in-range-requires
|
|
d |
rwxr-xr-x |
47 |
memory-predicates-pointer-in-range-typecheck-failure-01
|
|
d |
rwxr-xr-x |
47 |
memory-predicates-pointer-in-range-typecheck-failure-02
|
|
d |
rwxr-xr-x |
47 |
memory-predicates-user-defined-ensures-enforce
|
|
d |
rwxr-xr-x |
47 |
memory-predicates-user-defined-ensures-replace
|
|
d |
rwxr-xr-x |
47 |
memory-predicates-user-defined-mutually-recursive-fail
|
|
d |
rwxr-xr-x |
47 |
memory-predicates-user-defined-recursive-alternation
|
|
d |
rwxr-xr-x |
47 |
memory-predicates-user-defined-requires-enforce
|
|
d |
rwxr-xr-x |
47 |
memory-predicates-user-defined-requires-replace
|
|
d |
rwxr-xr-x |
47 |
missing-function-body
|
|
d |
rwxr-xr-x |
4,096 |
named-contracts
|
|
d |
rwxr-xr-x |
47 |
no_redudant_checks
|
|
d |
rwxr-xr-x |
47 |
nonvacuous_loop_contracts
|
|
d |
rwxr-xr-x |
126 |
quantifiers-exists-both-enforce
|
|
d |
rwxr-xr-x |
126 |
quantifiers-exists-both-replace
|
|
d |
rwxr-xr-x |
73 |
quantifiers-exists-ensures-enforce
|
|
d |
rwxr-xr-x |
47 |
quantifiers-exists-ensures-replace
|
|
d |
rwxr-xr-x |
47 |
quantifiers-exists-requires-enforce
|
|
d |
rwxr-xr-x |
47 |
quantifiers-exists-requires-replace
|
|
d |
rwxr-xr-x |
47 |
quantifiers-forall-both-enforce
|
|
d |
rwxr-xr-x |
47 |
quantifiers-forall-both-replace
|
|
d |
rwxr-xr-x |
47 |
quantifiers-forall-ensures-enforce
|
|
d |
rwxr-xr-x |
47 |
quantifiers-forall-ensures-replace
|
|
d |
rwxr-xr-x |
47 |
quantifiers-forall-requires-enforce
|
|
d |
rwxr-xr-x |
47 |
quantifiers-forall-requires-replace
|
|
d |
rwxr-xr-x |
47 |
quantifiers-loop-01
|
|
d |
rwxr-xr-x |
47 |
quantifiers-loop-02
|
|
d |
rwxr-xr-x |
47 |
quantifiers-loop-03
|
|
d |
rwxr-xr-x |
47 |
quantifiers-loop-05
|
|
d |
rwxr-xr-x |
47 |
quantifiers-loops-fresh-bound-vars-smt
|
|
d |
rwxr-xr-x |
47 |
quantifiers-nested-01
|
|
d |
rwxr-xr-x |
47 |
quantifiers-nested-02
|
|
d |
rwxr-xr-x |
47 |
quantifiers-nested-03
|
|
d |
rwxr-xr-x |
47 |
quantifiers-nested-04
|
|
d |
rwxr-xr-x |
47 |
quantifiers-nested-05
|
|
d |
rwxr-xr-x |
47 |
quantifiers-nested-06
|
|
d |
rwxr-xr-x |
47 |
quicksort_contracts_01
|
|
d |
rwxr-xr-x |
47 |
recursive-function-and-loop-contracts
|
|
d |
rwxr-xr-x |
47 |
reject_history_expr_in_assigns_clause
|
|
d |
rwxr-xr-x |
47 |
reject_history_expr_in_preconditions
|
|
d |
rwxr-xr-x |
47 |
reject_return_value_in_assigns_clause
|
|
d |
rwxr-xr-x |
47 |
reject_return_value_in_preconditions
|
|
d |
rwxr-xr-x |
47 |
replace-nondet-return-value
|
|
d |
rwxr-xr-x |
108 |
skip_loop_instrumentation
|
|
d |
rwxr-xr-x |
47 |
skip_unused_instrumentation
|
|
d |
rwxr-xr-x |
47 |
ternary-lhs-loop-contract
|
|
d |
rwxr-xr-x |
47 |
test_aliasing_enforce
|
|
d |
rwxr-xr-x |
47 |
test_aliasing_ensure
|
|
d |
rwxr-xr-x |
120 |
test_aliasing_ensure_indirect
|
|
d |
rwxr-xr-x |
47 |
test_aliasing_replace
|
|
d |
rwxr-xr-x |
47 |
test_array_memory_enforce
|
|
d |
rwxr-xr-x |
47 |
test_array_memory_replace
|
|
d |
rwxr-xr-x |
47 |
test_array_memory_too_small_replace
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_enforce_ensures_fail_separation_against_ensures
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_enforce_ensures_fail_separation_against_requires
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_enforce_ensures_fail_size
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_enforce_ensures_pass
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_enforce_requires_disjunction_fail
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_enforce_requires_disjunction_pass
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_enforce_requires_pass
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_replace_ensures_disjunction_fail
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_replace_ensures_disjunction_pass
|
|
d |
rwxr-xr-x |
83 |
test_is_fresh_replace_ensures_pass
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_replace_requires_fail_separation
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_replace_requires_fail_size
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_replace_requires_pass
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_weak_assert_ensures_fail
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_weak_assert_ensures_pass
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_weak_assert_requires_fail
|
|
d |
rwxr-xr-x |
47 |
test_is_fresh_weak_assert_requires_pass
|
|
d |
rwxr-xr-x |
47 |
test_pointer_equals_enforce_requires_disjunction_fail
|
|
d |
rwxr-xr-x |
47 |
test_pointer_equals_enforce_requires_disjunction_pass
|
|
d |
rwxr-xr-x |
47 |
test_pointer_equals_replace_ensures_disjunction_fail
|
|
d |
rwxr-xr-x |
47 |
test_pointer_equals_replace_ensures_disjunction_pass
|
|
d |
rwxr-xr-x |
47 |
test_pointer_in_range_enforce_requires_disjunction_fail
|
|
d |
rwxr-xr-x |
47 |
test_pointer_in_range_enforce_requires_disjunction_pass
|
|
d |
rwxr-xr-x |
47 |
test_pointer_in_range_replace_ensures_disjunction_fail
|
|
d |
rwxr-xr-x |
47 |
test_pointer_in_range_replace_ensures_disjunction_pass
|
|
d |
rwxr-xr-x |
47 |
test_pointer_pred_unique_enforce_fail
|
|
d |
rwxr-xr-x |
47 |
test_pointer_pred_unique_enforce_pass
|
|
d |
rwxr-xr-x |
47 |
test_pointer_pred_unique_replace_fail
|
|
d |
rwxr-xr-x |
47 |
test_pointer_pred_unique_replace_pass
|
|
d |
rwxr-xr-x |
47 |
test_possibly_aliased_arguments
|
|
d |
rwxr-xr-x |
47 |
test_scalar_memory_enforce
|
|
d |
rwxr-xr-x |
47 |
test_scalar_memory_replace
|
|
d |
rwxr-xr-x |
47 |
test_struct_enforce
|
|
d |
rwxr-xr-x |
47 |
test_struct_member_enforce
|
|
d |
rwxr-xr-x |
47 |
test_struct_replace
|
|
d |
rwxr-xr-x |
47 |
trivial_contract_enforce
|
|
d |
rwxr-xr-x |
47 |
trivial_contract_replace
|
|
d |
rwxr-xr-x |
47 |
typed_target_fail_wrong_nof_operand
|
|
d |
rwxr-xr-x |
47 |
typed_target_pointer
|
|
d |
rwxr-xr-x |
47 |
used_return_value
|
|
d |
rwxr-xr-x |
47 |
variant_function_call_fail
|
|
d |
rwxr-xr-x |
47 |
variant_init_inside_loop
|
|
d |
rwxr-xr-x |
47 |
variant_missing_invariant_warning
|
|
d |
rwxr-xr-x |
102 |
variant_multi_instruction_loop_head
|
|
d |
rwxr-xr-x |
47 |
variant_multidimensional_ackermann
|
|
d |
rwxr-xr-x |
47 |
variant_multidimensional_not_decreasing_fail1
|
|
d |
rwxr-xr-x |
47 |
variant_multidimensional_not_decreasing_fail2
|
|
d |
rwxr-xr-x |
47 |
variant_multidimensional_two_index_variables
|
|
d |
rwxr-xr-x |
47 |
variant_not_decreasing_fail
|
|
d |
rwxr-xr-x |
47 |
variant_parsing_multiple_clauses_fail
|
|
d |
rwxr-xr-x |
47 |
variant_parsing_statement_fail
|
|
d |
rwxr-xr-x |
47 |
variant_side_effects_fail
|
|
d |
rwxr-xr-x |
47 |
variant_weak_invariant_fail
|
|
d |
rwxr-xr-x |
47 |
variant_while_true_pass
|
 |
- |
rw-r--r-- |
1,695 |
CMakeLists.txt
|
|
- |
rw-r--r-- |
1,389 |
Makefile
|
|
- |
rwxr-xr-x |
1,598 |
chain.sh
|
