package info (click to toggle)
cbmc 6.6.0-4
  • links: PTS
  • area: main
  • in suites: forky, sid, trixie
  • size: 153,852 kB
  • sloc: cpp: 386,459; ansic: 114,466; java: 28,405; python: 6,003; yacc: 4,552; makefile: 4,041; lex: 2,487; xml: 2,388; sh: 2,050; perl: 557; pascal: 184; javascript: 163; ada: 36

Folder: contracts

d .. (parent)
d d rwxr-xr-x 47 assigns-enforce-malloc-zero
d d rwxr-xr-x 47 assigns-replace-ignored-return-value
d d rwxr-xr-x 47 assigns-replace-malloc-zero
d d rwxr-xr-x 47 assigns_enforce_02
d d rwxr-xr-x 47 assigns_enforce_03
d d rwxr-xr-x 47 assigns_enforce_04
d d rwxr-xr-x 47 assigns_enforce_05
d d rwxr-xr-x 47 assigns_enforce_06
d d rwxr-xr-x 47 assigns_enforce_07
d d rwxr-xr-x 47 assigns_enforce_08
d d rwxr-xr-x 47 assigns_enforce_09
d d rwxr-xr-x 47 assigns_enforce_10
d d rwxr-xr-x 47 assigns_enforce_11
d d rwxr-xr-x 47 assigns_enforce_15
d d rwxr-xr-x 47 assigns_enforce_18
d d rwxr-xr-x 47 assigns_enforce_19
d d rwxr-xr-x 47 assigns_enforce_20
d d rwxr-xr-x 47 assigns_enforce_21
d d rwxr-xr-x 47 assigns_enforce_arrays_02
d d rwxr-xr-x 47 assigns_enforce_arrays_05
d d rwxr-xr-x 47 assigns_enforce_arrays_10
d d rwxr-xr-x 47 assigns_enforce_conditional_function_call_condition
d d rwxr-xr-x 47 assigns_enforce_conditional_lvalue
d d rwxr-xr-x 47 assigns_enforce_conditional_lvalue_list
d d rwxr-xr-x 47 assigns_enforce_conditional_pointer_object
d d rwxr-xr-x 47 assigns_enforce_conditional_pointer_object_list
d d rwxr-xr-x 75 assigns_enforce_conditional_unions
d d rwxr-xr-x 47 assigns_enforce_detect_local_statics
d d rwxr-xr-x 47 assigns_enforce_detect_replaced_local_statics
d d rwxr-xr-x 47 assigns_enforce_free_dead
d d rwxr-xr-x 47 assigns_enforce_havoc_object
d d rwxr-xr-x 47 assigns_enforce_malloc_02
d d rwxr-xr-x 66 assigns_enforce_multi_file_02
d d rwxr-xr-x 47 assigns_enforce_offsets_2
d d rwxr-xr-x 47 assigns_enforce_offsets_4
d d rwxr-xr-x 47 assigns_enforce_scoping_01
d d rwxr-xr-x 47 assigns_enforce_scoping_02
d d rwxr-xr-x 47 assigns_enforce_statics
d d rwxr-xr-x 47 assigns_enforce_structs_04
d d rwxr-xr-x 47 assigns_enforce_structs_06
d d rwxr-xr-x 47 assigns_enforce_structs_07
d d rwxr-xr-x 47 assigns_enforce_structs_08
d d rwxr-xr-x 47 assigns_enforce_subfunction_calls
d d rwxr-xr-x 47 assigns_repeated_ignored
d d rwxr-xr-x 47 assigns_replace_02
d d rwxr-xr-x 47 assigns_replace_08
d d rwxr-xr-x 47 assigns_replace_09
d d rwxr-xr-x 100 assigns_replace_havoc_dependent_targets_fail
d d rwxr-xr-x 123 assigns_replace_havoc_dependent_targets_pass
d d rwxr-xr-x 47 assigns_type_checking_valid_cases
d d rwxr-xr-x 47 contracts_with_function_pointers
d d rwxr-xr-x 47 cprover-assignable-fail
d d rwxr-xr-x 47 cprover-assignable-pass
d d rwxr-xr-x 47 detect_loop_locals
d d rwxr-xr-x 47 detect_loop_locals2
d d rwxr-xr-x 47 do_while_syntax_fail
d d rwxr-xr-x 47 do_while_syntax_pass
d d rwxr-xr-x 73 enforce-replace-unknown-function
d d rwxr-xr-x 47 frees-clause-and-predicates
d d rwxr-xr-x 75 function-calls-01
d d rwxr-xr-x 99 function-calls-02
d d rwxr-xr-x 99 function-calls-02-1
d d rwxr-xr-x 75 function-calls-03
d d rwxr-xr-x 81 function-calls-03-1
d d rwxr-xr-x 103 function-calls-04
d d rwxr-xr-x 115 function-calls-04-1
d d rwxr-xr-x 47 function-calls-05
d d rwxr-xr-x 47 function-calls-recursive-01
d d rwxr-xr-x 47 function-pointer-contracts-enforce
d d rwxr-xr-x 47 function-pointer-contracts-replace
d d rwxr-xr-x 47 github_6168_infinite_unwinding_bug
d d rwxr-xr-x 47 history-index
d d rwxr-xr-x 47 history-invalid
d d rwxr-xr-x 47 history-pointer-enforce-10
d d rwxr-xr-x 47 history-pointer-replace-01
d d rwxr-xr-x 47 history-pointer-replace-02
d d rwxr-xr-x 47 history-pointer-replace-03
d d rwxr-xr-x 47 history-pointer-replace-04
d d rwxr-xr-x 47 invar_assigns_empty
d d rwxr-xr-x 47 invar_assigns_opt
d d rwxr-xr-x 47 invar_check_break_fail
d d rwxr-xr-x 47 invar_check_break_pass
d d rwxr-xr-x 47 invar_check_continue
d d rwxr-xr-x 47 invar_check_large
d d rwxr-xr-x 47 invar_check_multiple_loops
d d rwxr-xr-x 47 invar_check_nested_loops
d d rwxr-xr-x 47 invar_check_pointer_modifies-01
d d rwxr-xr-x 47 invar_check_pointer_modifies-02
d d rwxr-xr-x 47 invar_check_sufficiency
d d rwxr-xr-x 47 invar_dynamic_struct_member
d d rwxr-xr-x 47 invar_havoc_dynamic_array
d d rwxr-xr-x 47 invar_havoc_dynamic_array_const_idx
d d rwxr-xr-x 47 invar_havoc_dynamic_multi-dim_array
d d rwxr-xr-x 47 invar_havoc_dynamic_multi-dim_array_all_const_idx
d d rwxr-xr-x 47 invar_havoc_dynamic_multi-dim_array_partial_const_idx
d d rwxr-xr-x 47 invar_havoc_static_array
d d rwxr-xr-x 47 invar_havoc_static_array_const_idx
d d rwxr-xr-x 47 invar_havoc_static_multi-dim_array
d d rwxr-xr-x 47 invar_havoc_static_multi-dim_array_all_const_idx
d d rwxr-xr-x 47 invar_havoc_static_multi-dim_array_partial_const_idx
d d rwxr-xr-x 47 invar_loop-entry_check
d d rwxr-xr-x 47 invar_loop-entry_fail
d d rwxr-xr-x 47 invar_loop_constant_fail
d d rwxr-xr-x 47 invar_loop_constant_no_modify
d d rwxr-xr-x 74 invar_loop_constant_pass
d d rwxr-xr-x 47 invar_loop_with_goto
d d rwxr-xr-x 47 invar_struct_member
d d rwxr-xr-x 47 invariant_side_effects
d d rwxr-xr-x 47 is_unique_01_replace
d d rwxr-xr-x 47 labled_loop_head
d d rwxr-xr-x 47 loop-freeness-check
d d rwxr-xr-x 47 loop_assigns-01
d d rwxr-xr-x 47 loop_assigns-02
d d rwxr-xr-x 47 loop_assigns-03
d d rwxr-xr-x 47 loop_assigns-04
d d rwxr-xr-x 47 loop_assigns-05
d d rwxr-xr-x 47 loop_assigns-fail
d d rwxr-xr-x 47 loop_assigns-slice-assignable-ptr
d d rwxr-xr-x 47 loop_assigns-slice-assignable-scalar
d d rwxr-xr-x 47 loop_assigns-slice-from
d d rwxr-xr-x 47 loop_assigns-slice-upto-fail
d d rwxr-xr-x 47 loop_assigns-slice-upto-pass
d d rwxr-xr-x 47 loop_assigns_inference-01
d d rwxr-xr-x 47 loop_assigns_inference-02
d d rwxr-xr-x 47 loop_assigns_inference-03
d d rwxr-xr-x 47 loop_assigns_inference-04
d d rwxr-xr-x 47 loop_assigns_scoped_local_statics
d d rwxr-xr-x 47 loop_assigns_scoped_local_statics_propagate
d d rwxr-xr-x 47 loop_body_with_hole
d d rwxr-xr-x 47 loop_contracts_binary_search
d d rwxr-xr-x 47 loop_contracts_do_while
d d rwxr-xr-x 47 loop_contracts_no_unwind
d d rwxr-xr-x 47 loop_contracts_reject_overlapping_loops
d d rwxr-xr-x 47 loop_contracts_statement_expression
d d rwxr-xr-x 47 loop_guard_with_side_effects
d d rwxr-xr-x 47 loop_guard_with_side_effects_fail
d d rwxr-xr-x 47 no_redudant_checks
d d rwxr-xr-x 47 nonvacuous_loop_contracts
d d rwxr-xr-x 47 quantifiers-exists-ensures-enforce
d d rwxr-xr-x 47 quantifiers-forall-ensures-enforce
d d rwxr-xr-x 47 quantifiers-loop-01
d d rwxr-xr-x 47 quantifiers-loop-02
d d rwxr-xr-x 47 quantifiers-loop-03
d d rwxr-xr-x 47 quantifiers-nested-03
d d rwxr-xr-x 47 quicksort_contracts_01
d d rwxr-xr-x 47 test_aliasing_enforce
d d rwxr-xr-x 47 test_aliasing_ensure
d d rwxr-xr-x 47 test_aliasing_ensure_indirect
d d rwxr-xr-x 47 test_array_memory_replace
d d rwxr-xr-x 47 test_array_memory_too_small_replace
d d rwxr-xr-x 47 test_scalar_memory_replace
d d rwxr-xr-x 47 variant_init_inside_loop
d d rwxr-xr-x 47 variant_missing_invariant_warning
d d rwxr-xr-x 47 variant_multi_instruction_loop_head
d d rwxr-xr-x 67 variant_multidimensional_ackermann
d d rwxr-xr-x 47 variant_multidimensional_not_decreasing_fail1
d d rwxr-xr-x 47 variant_multidimensional_not_decreasing_fail2
d d rwxr-xr-x 47 variant_multidimensional_two_index_variables
d d rwxr-xr-x 47 variant_not_decreasing_fail
d d rwxr-xr-x 47 variant_weak_invariant_fail
d d rwxr-xr-x 47 variant_while_true_pass
- - rw-r--r-- 1,425 CMakeLists.txt
- - rw-r--r-- 1,190 Makefile
- - rwxr-xr-x 1,040 chain.sh