class APPLICATION create make feature make do -- create tc1 -- tc1.generated_test_1 -- create tc2 -- tc2.generated_test_1 -- create tc3 -- tc3.generated_test_1 -- create tc4 -- tc4.generated_test_1 -- create tc5 -- tc5.generated_test_1 -- create tc6 -- tc6.generated_test_1 -- create tc7 -- tc7.generated_test_1 -- create tc8 -- tc8.generated_test_1 -- create tc9 -- tc9.generated_test_1 -- create tc10 -- tc10.generated_test_1 -- create tc11 -- tc11.generated_test_1 -- create tc12 -- tc12.generated_test_1 create tc13 tc13.generated_test_1 end tc1: TC__ACTIVE_LIST__update_for_added__F__c3__b1__REC_INTERACTIVE_LIST__update_for_added__TAG_valid_cursor_index__1256473039143958 -- Can fix tc2: TC__TWO_WAY_SORTED_SET__duplicate__F__c3__b2__REC_TWO_WAY_SORTED_SET__duplicate__TAG_readable__1256547952341725 -- Can fix, wrong postconditions. tc3: TC__ARRAYED_CIRCULAR__duplicate__F__c3__b1__REC_ARRAYED_CIRCULAR__new_chain__TAG_at_least_one__1256547823247256 -- Can fix tc4: TC__ARRAYED_CIRCULAR__go_i_th__F__c6__b6__REC_CIRCULAR__go_i_th__TAG_off_definition__1256547825248697 -- Wrong definition of contracts tc5: TC__ARRAYED_CIRCULAR__make__F__c6__b2__REC_ARRAYED_CIRCULAR__make__TAG_valid_starter__1256547826249823 -- Can fix tc6: TC__ARRAYED_CIRCULAR__prune_all__F__c6__b8__REC_DYNAMIC_CHAIN__prune_all__TAG_isfirst_definition__1256547830252892 -- Can fix tc7: TC__ARRAYED_CIRCULAR__put_front__F__c4__b3__REC_ARRAYED_CIRCULAR__put_front__TAG_item_inserted__1256547826249123 -- Don't understand the fault. tc8: TC__ARRAYED_CIRCULAR__remove_left__F__c4__b8__REC_ARRAYED_CIRCULAR__remove_left__TAG_new_index__1256547829252140 -- Wrong postconditions tc9: TC__ARRAYED_CIRCULAR__remove_right__F__c4__b8__REC_ARRAYED_CIRCULAR__start__TAG_at_first__1256547822246107 -- Check later tc10: TC__ARRAYED_CIRCULAR__sequential_occurrences__F__c6__b3__REC_LINEAR__occurrences__TAG_valid_starter__1256547822246067 -- Check later tc11: TC__ARRAYED_LIST__is_inserted__F__c7__b1__REC_ARRAYED_LIST__is_inserted__TAG_put_constraint__1256473025137721 -- Wrong usage of API tc12: TC__ARRAYED_LIST__resize__F__c6__b3__REC_ARRAYED_LIST__resize__TAG_empty_means_storage_empty__125654759198069 -- Can fix tc13: TC__ARRAYED_LIST__there_exists__F__c3__b1__REC_ARRAY__there_exists__TAG_valid_operands__125647279924165 tc14: TC__ARRAYED_LIST__for_all__F__c3__b1__REC_ARRAY__for_all__TAG_valid_operands__1256500504156803 -- Check, should be able to fix. -- lll: ITP_INTERPRETER_ROOT attr0: DATE_VALIDITY_CHECKER attr1: DATE_TIME_SET attr2: DATE_TIME_VALUE attr3: DATE_TIME_CODE_STRING attr4: DATE_DURATION attr5: TIME_VALIDITY_CHECKER attr6: DATE_TIME attr7: DATE_TIME_VALIDITY_CHECKER attr8: TIME_UTILITY attr9: DATE_VALUE attr10: DATE_TIME_PARSER attr11: TIME attr12: FIND_SEPARATOR_FACILITY attr13: TIME_VALUE attr14: INTERVAL [ABSOLUTE] attr15: TIME_DURATION attr16: DATE_TIME_TOOLS attr17: CODE_VALIDITY_CHECKER attr18: TIME_SET attr19: DATE_TIME_DURATION attr20: DATE_TIME_CODE attr21: DATE_SET attr22: DATE attr23: LEXICAL attr24: SCANNING attr25: LEX_ARRAY [ ANY] attr26: STATE_OF_DFA attr27: TOKEN attr28: PDFA attr29: METALEX attr30: FIXED_AUTOMATON [STATE] attr31: LINKED_AUTOMATON [STATE] attr32: LEX_BUILDER attr33: LINKED_DFA attr34: ERROR_LIST attr35: FIXED_INTEGER_SET attr36: FIXED_DFA attr37: STATE attr38: HIGH_BUILDER attr39: DS_ARRAYED_LIST [ ANY] attr40: DS_ARRAY_BUBBLE_SORTER [ ANY] attr41: DS_BINARY_SEARCH_TREE_SET_NODE [ ANY] attr42: DS_HASH_SET [HASHABLE] attr43: DS_LEFT_LEANING_RED_BLACK_TREE_SET [ ANY] attr44: DS_ARRAY_SHELL_SORTER [ ANY] attr45: DS_QUICK_SORTER [ ANY] attr46: DS_LINKED_STACK [ ANY] attr47: DS_SHELL_SORTER [ ANY] attr48: DS_ARRAYED_STACK [ ANY] attr49: DS_AVL_TREE_NODE [ ANY, ANY] attr50: DS_LEFT_LEANING_RED_BLACK_TREE [ ANY, ANY] attr51: DS_LINKED_LIST [ ANY] attr52: DS_MULTIARRAYED_HASH_SET [HASHABLE] attr53: DS_NESTED_LIST_FLATTENER [ ANY] attr54: DS_BINARY_SEARCH_TREE_NODE [ ANY, ANY] attr55: DS_BINARY_SEARCH_TREE [ ANY, ANY] attr56: DS_RED_BLACK_TREE_NODE [ ANY, ANY] attr57: DS_LINKED_QUEUE [ ANY] attr58: DS_SPARSE_TABLE_KEYS [ ANY, ANY] attr59: DS_BILINKED_LIST [ ANY] attr60: DS_BINARY_SEARCH_TREE_SET [ ANY] attr61: DS_RED_BLACK_TREE_SET_NODE [ ANY] attr62: DS_BUBBLE_SORTER [ ANY] attr63: DS_AVL_TREE_SET [ ANY] attr64: DS_RED_BLACK_TREE [ ANY, ANY] attr65: DS_AVL_TREE [ ANY, ANY] attr66: DS_RED_BLACK_TREE_SET [ ANY] attr67: DS_AVL_TREE_SET_NODE [ ANY] attr68: DS_HEAP_SORTER [ ANY] attr69: DS_ARRAY_QUICK_SORTER [ ANY] attr70: DS_MULTIARRAYED_HASH_TABLE [ ANY, HASHABLE] attr71: LX_START_CONDITION_SPECIFIED_TWICE_ERROR attr72: LX_WILDCARD_PARSER attr73: LX_FULL_AND_META_ERROR attr74: LX_INCOMPLETE_NAME_DEFINITION_ERROR attr75: LX_MULTIPLE_EOF_RULES_ERROR attr76: LX_REGEXP_SCANNER attr77: LX_TRANSITION_TABLE [LX_STATE] attr78: LX_ITERATION_NOT_POSITIVE_ERROR attr79: LX_START_CONDITION_DECLARED_TWICE_ERROR attr80: LX_BAD_ITERATION_VALUES_ERROR attr81: LX_BAD_CHARACTER_ERROR attr82: LX_PROTO_QUEUE attr83: LX_BUFFER attr84: LX_START_CONDITIONS attr85: LX_UNDEFINED_DEFINITION_ERROR attr86: LX_LEX_PARSER attr87: LX_FULL_AND_VARIABLE_TRAILING_CONTEXT_ERROR attr88: LX_BAD_START_CONDITION_ERROR attr89: LX_RULE attr90: LX_MISSING_QUOTE_ERROR attr91: LX_WILDCARD_SCANNER attr92: LX_ALL_START_CONDITIONS_EOF_ERROR attr93: LX_DEFAULT_RULE_CAN_BE_MATCHED_ERROR attr94: LX_REGEXP_TOKENS attr95: LX_UNDECLARED_START_CONDITION_ERROR attr96: LX_LEX_TOKENS attr97: LX_NFA attr98: LX_DANGEROUS_TRAILING_CONTEXT_ERROR attr99: LX_EPSILON_TRANSITION [LX_STATE] attr100: LX_FULL_DFA attr101: LX_DFA_WILDCARD attr102: LX_WILDCARD_TOKENS attr103: LX_NFA_STATE attr104: LX_SYMBOL_CLASS attr105: LX_ACTION_FACTORY attr106: LX_TEMPLATE_LIST attr107: YY_BUFFER attr108: LX_SYMBOL_TRANSITION [LX_STATE] attr109: LX_CHARACTER_OUT_OF_RANGE_ERROR attr110: LX_UNRECOGNIZED_DIRECTIVE_ERROR attr111: LX_UNRECOGNIZED_OPTION_ERROR attr112: LX_BAD_CHARACTER_CLASS_ERROR attr113: LX_TRANSITION [LX_STATE] attr114: LX_BAD_START_CONDITION_LIST_ERROR attr115: LX_RULE_CANNOT_BE_MATCHED_ERROR attr116: LX_FULL_SCANNER attr117: LX_SYMBOL_CLASS_TRANSITION [LX_STATE] attr118: LX_NAME_DEFINED_TWICE_ERROR attr119: LX_FULL_TABLES attr120: LX_LEX_SCANNER attr121: LX_UNRECOGNIZED_RULE_ERROR attr122: LX_SYMBOL_PARTITIONS attr123: LX_START_CONDITION attr124: LX_MISSING_BRACKET_ERROR attr125: LX_SINGLETON attr126: LX_PROTO attr127: LX_NEGATIVE_RANGE_IN_CHARACTER_CLASS_ERROR attr128: LX_DFA_STATE attr129: LX_DFA attr130: LX_FULL_AND_REJECT_ERROR attr131: LX_REGEXP_PARSER attr132: LX_BAD_CHARACTER_IN_BRACKETS_ERROR attr133: LX_EQUIVALENCE_CLASSES attr134: LX_DFA_REGULAR_EXPRESSION attr135: LX_DIRECTIVE_EXPECTED_ERROR attr136: LX_START_CONDITION_EXPECTED_ERROR attr137: LX_DESCRIPTION attr138: LX_INTEGER_TOO_LARGE_ERROR attr139: LX_ACTION attr140: KL_COMPARABLE_COMPARATOR [COMPARABLE] attr141: KL_ARRAY_ROUTINES [ ANY] attr142: KL_INTEGER_ROUTINES attr143: KL_IMPORTED_ANY_ROUTINES attr144: UC_STRING_COMPARATOR attr145: UC_STRING attr146: KL_CHARACTER_ROUTINES attr147: KL_GREGORIAN_CALENDAR attr148: KL_IMPORTED_BOOLEAN_ROUTINES attr149: KL_STRING attr150: KL_REVERSE_COMPARATOR [ ANY] attr151: KL_EQUALITY_TESTER [ ANY] attr152: KL_IMPORTED_CHARACTER_ROUTINES attr153: KL_ANY_ROUTINES attr154: KL_CHARACTER_BUFFER attr155: KL_AGENT_HASH_FUNCTION [ ANY] attr156: UC_CHARACTER attr157: KL_HASHABLE_ROUTINES attr158: KL_CASE_INSENSITIVE_STRING_EQUALITY_TESTER attr159: KL_IMPORTED_STRING_ROUTINES attr160: KL_REVERSE_PART_COMPARATOR [ ANY] attr161: KL_HASHABLE_HASH_FUNCTION [HASHABLE] attr162: KL_STRING_ROUTINES attr163: DIFF_LINE_ADD attr164: DIFF [HASHABLE] attr165: DIFF_LINE_DEL attr166: DIFF_TEXT attr167: DIFF_LINE_MATCH attr168: DIFF_INDEX_LINK attr169: PART_SORTED_TWO_WAY_LIST [PART_COMPARABLE] attr170: BINARY_TREE [ ANY] attr171: BASIC_ROUTINES attr172: ARRAYED_CIRCULAR [ ANY] attr173: TWO_WAY_LIST [ ANY] attr174: HEAP_PRIORITY_QUEUE [COMPARABLE] attr175: SUBSET_STRATEGY_TREE [COMPARABLE] attr176: LINKED_CURSOR_TREE [ ANY] attr177: SINGLE_MATH attr178: FIXED_LIST [ ANY] attr179: ARRAYED_SET [ ANY] attr180: STRING_SEARCHER attr181: TWO_WAY_SORTED_SET [COMPARABLE] attr182: STRING_HANDLER attr183: NUMERIC_INFORMATION attr184: ACTIVE_INTEGER_INTERVAL attr185: PRIMES attr186: ARRAYED_QUEUE [ ANY] attr187: TWO_WAY_CIRCULAR [ ANY] attr188: DOUBLE_MATH attr189: LINKED_CIRCULAR [ ANY] attr190: LINKED_LIST [ ANY] attr191: CREATE_ON_DEFERRED attr192: SORTED_TWO_WAY_LIST [COMPARABLE] attr193: INTEGER_OVERFLOW_CHECKER attr194: ACTIVE_LIST [ ANY] attr195: INTEGER_INTERVAL attr196: LINEAR_ITERATOR [ ANY] attr197: SUBSET_STRATEGY_GENERIC [ ANY] attr198: LINKED_QUEUE [ ANY] attr199: TRACING_SETTING attr200: LINKED_TREE [ ANY] attr201: BOUNDED_STACK [ ANY] attr202: RANDOM attr203: COMPACT_CURSOR_TREE [ ANY] attr204: MULTI_ARRAY_LIST [ ANY] attr205: DECLARATOR attr206: PART_SORTED_SET [PART_COMPARABLE] attr207: LINKED_STACK [ ANY] attr208: TUPLE attr209: TWO_WAY_CHAIN_ITERATOR [ ANY] attr210: ARRAYED_TREE [ ANY] attr211: LINKED_PRIORITY_QUEUE [COMPARABLE] attr212: LINKED_SET [ ANY] attr213: FORMAT_DOUBLE attr214: ARRAYED_STACK [ ANY] attr215: HASH_TABLE [ ANY, HASHABLE] attr216: TWO_WAY_TREE [ ANY] attr217: ARRAY [ ANY] attr218: ARRAYED_LIST [ ANY] attr219: FIBONACCI attr220: FIXED_TREE [ ANY] attr221: NATIVE_ARRAY [ ANY] attr222: BOUNDED_QUEUE [ ANY] attr223: FORMAT_INTEGER attr224: BINARY_SEARCH_TREE [COMPARABLE] attr225: ARRAY2 [ ANY] attr226: BINARY_SEARCH_TREE_SET [COMPARABLE] attr227: TWO_WAY_CURSOR_TREE [ ANY] attr228: DS_HASH_TABLE [ANY, HASHABLE] end