Commit 57c787e
committed
Remove general contracts flags
Removes --enforce-all-contracts and --replace-all-calls-with-contracts flags.
The user must specify which functions to enforce or replace using contracts.
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>1 parent 923c623 commit 57c787e
File tree
132 files changed
+231
-301
lines changed- regression/contracts
- assigns_enforce_01
- assigns_enforce_02
- assigns_enforce_03
- assigns_enforce_04
- assigns_enforce_05
- assigns_enforce_06
- assigns_enforce_07
- assigns_enforce_08
- assigns_enforce_09
- assigns_enforce_10
- assigns_enforce_11
- assigns_enforce_12
- assigns_enforce_13
- assigns_enforce_14
- assigns_enforce_15
- assigns_enforce_16
- assigns_enforce_17
- assigns_enforce_18
- assigns_enforce_19
- assigns_enforce_20
- assigns_enforce_arrays_01
- assigns_enforce_arrays_02
- assigns_enforce_arrays_03
- assigns_enforce_arrays_04
- assigns_enforce_arrays_05
- assigns_enforce_arrays_10
- assigns_enforce_functions_in_contracts
- assigns_enforce_malloc_01
- assigns_enforce_malloc_02
- assigns_enforce_multi_file_01
- assigns_enforce_multi_file_02
- assigns_enforce_scoping_01
- assigns_enforce_scoping_02
- assigns_enforce_structs_01
- assigns_enforce_structs_02
- assigns_enforce_structs_03
- assigns_enforce_structs_04
- assigns_enforce_structs_05
- assigns_enforce_structs_06
- assigns_enforce_structs_07
- assigns_function_pointer
- assigns_repeated_ignored
- assigns_replace_01
- assigns_replace_02
- assigns_replace_03
- assigns_replace_04
- assigns_replace_05
- assigns_replace_06
- assigns_replace_07
- assigns_replace_08
- assigns_replace_09
- assigns_type_checking_invalid_case_01
- assigns_type_checking_invalid_case_02
- assigns_type_checking_valid_cases
- assigns_validity_pointer_04
- function-calls-01
- function-calls-02-1
- function-calls-02
- function-calls-03-1
- function-calls-03
- function-calls-04-1
- function-calls-04
- function-calls-05
- function_apply_01
- function_check_01
- function_check_02
- function_loop_history_ensures_fail
- function_loop_history_requires_fail
- history-pointer-both-01
- history-pointer-enforce-01
- history-pointer-enforce-02
- history-pointer-enforce-03
- history-pointer-enforce-04
- history-pointer-enforce-05
- history-pointer-enforce-06
- history-pointer-enforce-07
- history-pointer-enforce-08
- history-pointer-enforce-09
- history-pointer-enforce-10
- history-pointer-enforce-11
- history-pointer-replace-01
- history-pointer-replace-02
- history-pointer-replace-03
- history-pointer-replace-04
- ignored_return_value
- is_unique_01_replace
- quantifiers-exists-both-enforce
- quantifiers-exists-both-replace
- quantifiers-exists-ensures-enforce
- quantifiers-exists-ensures-replace
- quantifiers-exists-requires-enforce
- quantifiers-exists-requires-replace
- quantifiers-forall-both-enforce
- quantifiers-forall-both-replace
- quantifiers-forall-ensures-enforce
- quantifiers-forall-ensures-replace
- quantifiers-forall-requires-enforce
- quantifiers-forall-requires-replace
- quantifiers-nested-01
- quantifiers-nested-02
- quantifiers-nested-03
- quantifiers-nested-04
- quantifiers-nested-05
- quantifiers-nested-06
- quicksort_contracts_01
- test_aliasing_enforce
- test_aliasing_ensure_indirect
- test_aliasing_ensure
- test_aliasing_replace
- test_array_memory_enforce
- test_array_memory_replace
- test_array_memory_too_small_replace
- test_possibly_aliased_arguments
- test_scalar_memory_enforce
- test_scalar_memory_replace
- test_struct_enforce
- test_struct_member_enforce
- test_struct_replace
- trivial_contract_enforce
- trivial_contract_replace
- used_return_value
- variant_multidimensional_ackermann
- src/goto-instrument
- contracts
Some content is hidden
Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.
132 files changed
+231
-301
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
2 | 2 | | |
3 | | - | |
| 3 | + | |
4 | 4 | | |
5 | 5 | | |
6 | 6 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
2 | 2 | | |
3 | | - | |
| 3 | + | |
4 | 4 | | |
5 | 5 | | |
6 | 6 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
2 | 2 | | |
3 | | - | |
| 3 | + | |
4 | 4 | | |
5 | 5 | | |
6 | 6 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
2 | 2 | | |
3 | | - | |
| 3 | + | |
4 | 4 | | |
5 | 5 | | |
6 | 6 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
2 | 2 | | |
3 | | - | |
| 3 | + | |
4 | 4 | | |
5 | 5 | | |
6 | 6 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
2 | 2 | | |
3 | | - | |
| 3 | + | |
4 | 4 | | |
5 | 5 | | |
6 | 6 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
2 | 2 | | |
3 | | - | |
| 3 | + | |
4 | 4 | | |
5 | 5 | | |
6 | 6 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
2 | 2 | | |
3 | | - | |
| 3 | + | |
4 | 4 | | |
5 | 5 | | |
6 | 6 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
2 | 2 | | |
3 | | - | |
| 3 | + | |
4 | 4 | | |
5 | 5 | | |
6 | 6 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
1 | 1 | | |
2 | 2 | | |
3 | | - | |
| 3 | + | |
4 | 4 | | |
5 | 5 | | |
6 | 6 | | |
| |||
0 commit comments