From 45851a07d99726e3a85a3d91ec4876e5a7c32a94 Mon Sep 17 00:00:00 2001 From: trdthg Date: Mon, 5 Aug 2024 22:33:42 +0800 Subject: [PATCH] comment --- log.test.txt | 368 ++ test.log.txt | 4313 +++++++++++++++++ test/sailcov/Makefile | 13 +- test/sailcov/nested_mapping.expect | 33 + test/sailcov/nested_mapping1.expect | 32 + test/sailcov/nested_mapping1.sail | 28 + test/sailcov/nested_mapping2.expect | 33 + test/sailcov/nested_mapping2.sail | 22 + test/sailcov/nested_mapping3.expect | 33 + test/sailcov/nested_mapping3.sail | 22 + test/sailcov/nested_mapping4.sail | 22 + test/sailcov/nested_mapping5.sail | 29 + .../sailcov/nested_mapping_demo.full_branches | 27 + test/sailcov/nested_mapping_demo.sail | 22 + 14 files changed, 4992 insertions(+), 5 deletions(-) create mode 100644 log.test.txt create mode 100644 test.log.txt create mode 100644 test/sailcov/nested_mapping.expect create mode 100644 test/sailcov/nested_mapping1.expect create mode 100644 test/sailcov/nested_mapping1.sail create mode 100644 test/sailcov/nested_mapping2.expect create mode 100644 test/sailcov/nested_mapping2.sail create mode 100644 test/sailcov/nested_mapping3.expect create mode 100644 test/sailcov/nested_mapping3.sail create mode 100644 test/sailcov/nested_mapping4.sail create mode 100644 test/sailcov/nested_mapping5.sail create mode 100644 test/sailcov/nested_mapping_demo.full_branches create mode 100644 test/sailcov/nested_mapping_demo.sail diff --git a/log.test.txt b/log.test.txt new file mode 100644 index 000000000..750391988 --- /dev/null +++ b/log.test.txt @@ -0,0 +1,368 @@ +Sail is /home/trdthg/repo/sail/sail +Sail dir is /home/trdthg/repo/sail +------------------------ +Testing passing programs +------------------------ +Running 16 tests in parallel. Set TEST_PAR to configure +default_order.sail ..................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +deinfix_plus.sail ...................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +add_vec_exts_no_annot.sail ............. ok +Running 16 tests in parallel. Set TEST_PAR to configure +bitwise_not_gen.sail ................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +real.sail .............................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +function_namespace.sail ................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +vector_append.sail ..................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +overload_overload.sail ................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +floor_pow2.sail ........................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +funcl_guard.sail ....................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +vector_concat_assign.sail .............. ok +Running 16 tests in parallel. Set TEST_PAR to configure +exist_synonym.sail ..................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +exist2.sail ............................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +lexp_vec.sail .......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +implicits.sail ......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +vector_subrange_pattern.sail ........... ok +Running 16 tests in parallel. Set TEST_PAR to configure +while_PM.sail .......................... ok +varity.sail ............................ ok +as_pattern.sail ........................ ok +vec_pat1.sail .......................... ok +while_PP.sail .......................... ok +atomcase.sail .......................... ok +vector_subrange_gen.sail ............... ok +repeat_constraint.sail ................. ok +vec_length_inc.sail .................... ok +equation_return.sail ................... ok +true_false.sail ........................ ok +wildcard_mapping.sail .................. ok +nlflow.sail ............................ ok +tuple_bitvector_int_pat.sail ........... ok +existential_ast.sail ................... ok +existential_ast3.sail .................. ok +exit2.sail ............................. ok +add_real.sail .......................... ok +arm_FPEXC1.sail ........................ ok +commentfix.sail ........................ ok +extension_constructor.sail ............. ok +return_simple4.sail .................... ok +sizeof_fixed.sail ...................... ok +bool_mapping.sail ...................... ok +tautology.sail ......................... ok +multiple_unifiers.sail ................. ok +constraint_syn.sail .................... ok +constraint_ctor.sail ................... ok +flow_lteq1.sail ........................ ok +Replicate.sail ......................... ok +arm_types.sail ......................... ok +concurrency_interface_inc.sail ......... ok +nzcv.sail .............................. ok +exit3.sail ............................. ok +pat_completeness.sail .................. ok +patternrefinement.sail ................. ok +bind_typ_var.sail ...................... ok +custom_flow.sail ....................... ok +bool_bits_mapping.sail ................. ok +decode_patterns.sail ................... ok +struct_field_constraint.sail ........... ok +bool_mapping2.sail ..................... ok +execute_decode_hard.sail ............... ok +overload_int_nat.sail .................. ok +poly_list.sail ......................... ok +vector_pattern_split.sail .............. ok +string_append_non_exec.sail ............ ok +wf_specs.sail .......................... ok +cons_pattern.sail ...................... ok +list_cons2.sail ........................ ok +if_var_updates.sail .................... ok +return_simple1.sail .................... ok +option_tuple.sail ...................... ok +list_lit.sail .......................... ok +complex_exist_sat.sail ................. ok +vector_subrange_mapping.sail ........... ok +type_if_then_else.sail ................. ok +complete_pattern_let.sail .............. ok +exist1.sail ............................ ok +allpats.sail ........................... ok +fpthreesimp.sail ....................... ok +tuple_assign.sail ...................... ok +ex_vector_infer.sail ................... ok +short_circuit_bool_ex.sail ............. ok +bitwise_not.sail ....................... ok +union_infer.sail ....................... ok +procstate1.sail ........................ ok +anon_rec.sail .......................... ok +mod_var.sail ........................... ok +option_either.sail ..................... ok +reg_mod.sail ........................... ok +simple_record_access.sail .............. ok +nonexistent_pragma.sail ................ ok +add_vec_lit.sail ....................... ok +abstract_bool2.sail .................... ok +set_constraint.sail .................... ok +type_div.sail .......................... ok +bitfield_updates0.sail ................. ok +global_type_var.sail ................... ok +pow_32_64.sail ......................... ok +assignment_simple.sail ................. ok +reg_list.sail .......................... ok +while_MP.sail .......................... ok +case_simple2.sail ...................... ok +exist_true.sail ........................ ok +equation_arguments.sail ................ ok +pow_unify.sail ......................... ok +abstract_bool.sail ..................... ok +pure_let_var2.sail ..................... ok +tuple_fun.sail ......................... ok +pure_let_var.sail ...................... ok +flow_gteq1.sail ........................ ok +mutrec.sail ............................ ok +poly_vector.sail ....................... ok +if_infer.sail .......................... ok +exist_tlb.sail ......................... ok +cons_pattern_synonym.sail .............. ok +overlap_field.sail ..................... ok +reg_ref.sail ........................... ok +let_subtyp_bug.sail .................... ok +reg_option.sail ........................ ok +pure_record2.sail ...................... ok +phantom_bitlist_struct.sail ............ ok +type_pow_zero.sail ..................... skip +inc_prelude.sail ....................... ok +bitfield_mod.sail ...................... ok +type_pow_zero.sail ..................... skip +bitfield_abs.sail ...................... ok +tuple_bitvector_int_pat3.sail .......... ok +tuple_bitvector_int_pat2.sail .......... ok +type_pow_zero.sail ..................... skip +mapping_clause.sail .................... ok +bool_typ_pat.sail ...................... ok +enum_map.sail .......................... ok +type_pow_zero.sail ..................... skip +pure_record.sail ....................... ok +issue250.sail .......................... ok +simple_scattered.sail .................. ok +exit1.sail ............................. ok +existential_constraint_synonym.sail .... ok +plus_one_unify.sail .................... ok +int_synonym.sail ....................... ok +modify_type_chain.sail ................. ok +rmem_rmemt_same.sail ................... ok +no_val_recur.sail ...................... ok +dec_prelude.sail ....................... ok +if_return.sail ......................... ok +recursion.sail ......................... ok +unsigned_index.sail .................... ok +flow_gt1.sail .......................... ok +string_literal_type.sail ............... ok +scattered_union_doc.sail ............... ok +single_enum.sail ....................... ok +exist_subrange.sail .................... ok +vector_append_gen.sail ................. ok +cast_simple.sail ....................... ok +return_simple2.sail .................... ok +scattered_enum.sail .................... ok +eqn_inst.sail .......................... ok +ex_list_infer.sail ..................... ok +if_type_if.sail ........................ ok +shadow_let.sail ........................ ok +flow_lt1.sail .......................... ok +bits_concat_pattern.sail ............... ok +nexp_synonym.sail ...................... ok +vec_length.sail ........................ ok +reg_32_64.sail ......................... ok +ex_cast.sail ........................... ok +overload_plus.sail ..................... ok +lt_flow.sail ........................... ok +cast_lexp1.sail ........................ ok +exist_simple.sail ...................... ok +bitvector_param.sail ................... ok +crlf.sail .............................. ok +zero_length_bv.sail .................... ok +mapping_rreg.sail ...................... ok +if_infer2.sail ......................... ok +bitfield_exponential.sail .............. ok +struct_pattern.sail .................... ok +tyvar_shadow.sail ...................... ok +bitfield_updates.sail .................. ok +list_infer.sail ........................ ok +constrained_struct.sail ................ ok +bitwise_not_x3.sail .................... ok +nat_set.sail ........................... ok +single_union.sail ...................... ok +case_simple1.sail ...................... ok +return_simple3.sail .................... ok +foreach_var_updates.sail ............... ok +exint.sail ............................. ok +zeros_implicit.sail .................... ok +phantom_bitlist_union.sail ............. ok +union_ctor_constraint.sail ............. ok +guards.sail ............................ ok +new_bitfields.sail ..................... ok +scattered_mapping_doc.sail ............. ok +existential_ast2.sail .................. ok +bool_constraint.sail ................... ok +concurrency_interface_dec.sail ......... ok +add_vec_exts_no_annot_overload.sail .... ok +phantom_num.sail ....................... ok +bitfield_pc.sail ....................... ok +try_while_try.sail ..................... ok +nexp_synonym2.sail ..................... ok +single_assign_in_block.sail ............ ok +struct_pattern_partial.sail ............ ok +inline_typ.sail ........................ ok +synth_ex_vs.sail ....................... ok +type_if_then_else_alt.sail ............. ok +flow_lt2.sail .......................... ok +enum_cast.sail ......................... ok +tuple_type_cast.sail ................... ok +not_pattern.sail ....................... ok +negative_bits_list.sail ................ ok +outcome_impl.sail ...................... ok +vector_access_dec.sail ................. ok +bv_simple_index_bit.sail ............... ok +vector_access.sail ..................... ok +while_MM.sail .......................... ok +list_cons.sail ......................... ok +cast_lexp2.sail ........................ ok +modify_assignment1.sail ................ ok +priv_fn_no_val.sail .................... ok +pure_record3.sail ...................... ok +issue434.sail .......................... ok +phantom_option.sail .................... ok +bits_if.sail ........................... ok +foreach_e.sail ......................... ok +outcome_impl_quant.sail ................ ok +wf_register_type.sail .................. ok +222 passes and 0 failures +------------------------ +Testing failing programs +------------------------ +Running 16 tests in parallel. Set TEST_PAR to configure +strict_var.sail ........................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +scattered_map_mod.sail ................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +synonym_rec.sail ....................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +duplicate_type_id.sail ................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +duplicate_type_id4.sail ................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +add_vec_lit_old.sail ................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +prelude_no_order.sail .................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +scattered_enum_mod.sail ................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +undefined_infer.sail ................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +struct_pattern_duplicate_field.sail .... ok +Running 16 tests in parallel. Set TEST_PAR to configure +and_let_bool.sail ...................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +unbound_tyvar2.sail .................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +mapping_body_private.sail .............. ok +Running 16 tests in parallel. Set TEST_PAR to configure +negative_bits_existential.sail ......... ok +Running 16 tests in parallel. Set TEST_PAR to configure +issue277.sail .......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +modify_enum2.sail ...................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +union_rec.sail ......................... ok +scattered_union_mod.sail ............... ok +enum_functions_partial.sail ............ ok +enum_shadow_let.sail ................... ok +scattered_function_mod.sail ............ ok +unbound_tyvar.sail ..................... ok +missing_tick.sail ...................... ok +modify_immutable2.sail ................. ok +issue244_3.sail ........................ ok +mix_declaration_update.sail ............ ok +undeclared_field_assignment.sail ....... ok +pub_val_priv_fn.sail ................... ok +duplicate_toplevel_let.sail ............ ok +abstract_bool_inconsistent.sail ........ ok +vector_pattern_split.sail .............. ok +issue243.sail .......................... ok +duplicate_type_id6.sail ................ ok +overload_member_scope.sail ............. ok +assignment_simple.sail ................. ok +procstate1.sail ........................ ok +duplicate_type_id2.sail ................ ok +scattered_union_rec.sail ............... ok +private_extension.sail ................. ok +bv_update_error.sail ................... ok +mapping_two_type.sail .................. ok +non_synonym.sail ....................... ok +poly_ab_mapping.sail ................... ok +unscope_val.sail ....................... ok +negative_bits_struct2.sail ............. ok +negative_bits_struct.sail .............. ok +duplicate_quant.sail ................... ok +struct_incomplete_literal.sail ......... ok +private_scattered_enum.sail ............ ok +private_scattered_map.sail ............. ok +duplicate_ctor.sail .................... ok +struct_rec.sail ........................ ok +union_recf.sail ........................ ok +issue244_1.sail ........................ ok +private_union.sail ..................... ok +empty_su.sail .......................... ok +empty_vector_infer.sail ................ ok +bitfield_bits_field.sail ............... ok +private_ctor.sail ...................... ok +issue244_4.sail ........................ ok +mapping_length_mismatch.sail ........... ok +encdec_unknown_and_error.sail .......... ok +negative_bits_tuple.sail ............... ok +enum_function_override.sail ............ ok +duplicate_type_id3.sail ................ ok +private_scattered_union.sail ........... ok +duplicate_builtin.sail ................. ok +private_scattered_fn.sail .............. ok +global_false_constraint.sail ........... ok +shadow_leak_infer.sail ................. ok +shadow_leak_check.sail ................. ok +no_possible_overload.sail .............. ok +issue244_2.sail ........................ ok +no_function3.sail ...................... ok +invalid_function_val.sail .............. ok +private_function.sail .................. ok +negative_bits_union2.sail .............. ok +duplicate_binding.sail ................. ok +negative_bits_union.sail ............... ok +undeclared_vector_assignment.sail ...... ok +overload_bound.sail .................... ok +duplicate_type_id5.sail ................ ok +private_clause.sail .................... ok +enum_shadow_reg.sail ................... ok +cond_mod.sail .......................... ok +duplicate_toplevel_let_mod.sail ........ ok +enum_shadow.sail ....................... ok +no_function.sail ....................... ok +modify_immutable.sail .................. ok +unscope_let.sail ....................... ok +nonexistent_overload.sail .............. ok +unscope_type.sail ...................... ok +bitfield_error.sail .................... ok +no_function2.sail ...................... ok +unscope_enum.sail ...................... ok +modify_enum.sail ....................... ok +unscope_register.sail .................. ok +wf_assign_type.sail .................... ok +98 passes and 0 failures diff --git a/test.log.txt b/test.log.txt new file mode 100644 index 000000000..929c7cc0b --- /dev/null +++ b/test.log.txt @@ -0,0 +1,4313 @@ +SAIL_DIR=`pwd` SAIL=`pwd`/sail test/run_tests.sh + +========================================== +Lexing tests +========================================== +Sail is /home/trdthg/repo/sail/sail +Sail dir is /home/trdthg/repo/sail +------------- +Testing lexer +------------- +Running 16 tests in parallel. Set TEST_PAR to configure +help_option_pragma.sail ................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +cr_invisible.sail ...................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +illegal_escape.sail .................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +unknown_operator.sail .................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +bad_option_pragma.sail ................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +pragma_block.sail ...................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +doc_comment_eof.sail ................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +unbalanced_comment2.sail ............... ok +Running 16 tests in parallel. Set TEST_PAR to configure +unterminated_ifdef.sail ................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +line_comment_eof.sail .................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +import_reserved.sail ................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +module_reserved.sail ................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +unbalanced_comment.sail ................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +bad_option_pragma2.sail ................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +unterminated_string.sail ............... ok +Running 16 tests in parallel. Set TEST_PAR to configure +extended_ascii.sail .................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +16 passes and 0 failures + +========================================== +Pattern completeness tests +========================================== +Sail is /home/trdthg/repo/sail/sail +Sail dir is /home/trdthg/repo/sail +------------------------------------ +Testing pattern completeness checker +------------------------------------ +Running 16 tests in parallel. Set TEST_PAR to configure +mapping_let.sail ....................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +unbounded_int_annot.sail ............... ok +Running 16 tests in parallel. Set TEST_PAR to configure +warn_empty_list.sail ................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +warn_cons_incomplete.sail .............. ok +Running 16 tests in parallel. Set TEST_PAR to configure +int_pattern.sail ....................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +warn_double_cons_incomplete.sail ....... ok +Running 16 tests in parallel. Set TEST_PAR to configure +warn_int_pattern.sail .................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +some_none.sail ......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +two_argument.sail ...................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +warn_struct_pattern_incomplete.sail .... ok +Running 16 tests in parallel. Set TEST_PAR to configure +constrained_function.sail .............. ok +Running 16 tests in parallel. Set TEST_PAR to configure +set_match.sail ......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +cons_wildcard_insert.sail .............. ok +Running 16 tests in parallel. Set TEST_PAR to configure +warn_unbounded_nat.sail ................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +warn_cons_wildcard_insert2.sail ........ ok +Running 16 tests in parallel. Set TEST_PAR to configure +warn_cannot_wildcard.sail .............. ok +Running 16 tests in parallel. Set TEST_PAR to configure +warn_partial_lookup.sail ............... ok +warn_unbounded_int.sail ................ ok +some_none_int.sail ..................... ok +lookup.sail ............................ ok +warn_range_redundant.sail .............. ok +constrained_function_scattered.sail .... ok +warn_partial_scattered.sail ............ ok +range.sail ............................. ok +warn_tuple_bitvector_pat.sail .......... ok +struct_pattern.sail .................... ok +warn_cons_wildcard_insert1.sail ........ ok +warn_missing_enum.sail ................. ok +warn_mapping_imcomplete.sail ........... ok +29 passes and 0 failures + +========================================== +Typechecking tests +========================================== +Sail is /home/trdthg/repo/sail/sail +Sail dir is /home/trdthg/repo/sail +------------------------ +Testing passing programs +------------------------ +Running 16 tests in parallel. Set TEST_PAR to configure +default_order.sail ..................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +add_vec_exts_no_annot.sail ............. ok +Running 16 tests in parallel. Set TEST_PAR to configure +bitwise_not_gen.sail ................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +real.sail .............................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +deinfix_plus.sail ...................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +function_namespace.sail ................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +vector_append.sail ..................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +overload_overload.sail ................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +floor_pow2.sail ........................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +funcl_guard.sail ....................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +vector_concat_assign.sail .............. ok +Running 16 tests in parallel. Set TEST_PAR to configure +exist_synonym.sail ..................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +exist2.sail ............................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +lexp_vec.sail .......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +implicits.sail ......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +vector_subrange_pattern.sail ........... ok +Running 16 tests in parallel. Set TEST_PAR to configure +while_PM.sail .......................... ok +varity.sail ............................ ok +as_pattern.sail ........................ ok +vec_pat1.sail .......................... ok +while_PP.sail .......................... ok +atomcase.sail .......................... ok +repeat_constraint.sail ................. ok +vector_subrange_gen.sail ............... ok +vec_length_inc.sail .................... ok +equation_return.sail ................... ok +true_false.sail ........................ ok +wildcard_mapping.sail .................. ok +nlflow.sail ............................ ok +tuple_bitvector_int_pat.sail ........... ok +existential_ast.sail ................... ok +existential_ast3.sail .................. ok +exit2.sail ............................. ok +add_real.sail .......................... ok +arm_FPEXC1.sail ........................ ok +commentfix.sail ........................ ok +extension_constructor.sail ............. ok +return_simple4.sail .................... ok +sizeof_fixed.sail ...................... ok +bool_mapping.sail ...................... ok +multiple_unifiers.sail ................. ok +tautology.sail ......................... ok +constraint_syn.sail .................... ok +flow_lteq1.sail ........................ ok +constraint_ctor.sail ................... ok +Replicate.sail ......................... ok +arm_types.sail ......................... ok +concurrency_interface_inc.sail ......... ok +pat_completeness.sail .................. ok +nzcv.sail .............................. ok +exit3.sail ............................. ok +patternrefinement.sail ................. ok +bind_typ_var.sail ...................... ok +custom_flow.sail ....................... ok +struct_field_constraint.sail ........... ok +decode_patterns.sail ................... ok +bool_bits_mapping.sail ................. ok +bool_mapping2.sail ..................... ok +execute_decode_hard.sail ............... ok +overload_int_nat.sail .................. ok +poly_list.sail ......................... ok +string_append_non_exec.sail ............ ok +vector_pattern_split.sail .............. ok +wf_specs.sail .......................... ok +cons_pattern.sail ...................... ok +if_var_updates.sail .................... ok +list_cons2.sail ........................ ok +option_tuple.sail ...................... ok +return_simple1.sail .................... ok +list_lit.sail .......................... ok +complex_exist_sat.sail ................. ok +vector_subrange_mapping.sail ........... ok +type_if_then_else.sail ................. ok +complete_pattern_let.sail .............. ok +allpats.sail ........................... ok +exist1.sail ............................ ok +fpthreesimp.sail ....................... ok +tuple_assign.sail ...................... ok +short_circuit_bool_ex.sail ............. ok +ex_vector_infer.sail ................... ok +union_infer.sail ....................... ok +bitwise_not.sail ....................... ok +procstate1.sail ........................ ok +anon_rec.sail .......................... ok +mod_var.sail ........................... ok +option_either.sail ..................... ok +reg_mod.sail ........................... ok +simple_record_access.sail .............. ok +add_vec_lit.sail ....................... ok +nonexistent_pragma.sail ................ ok +abstract_bool2.sail .................... ok +set_constraint.sail .................... ok +type_div.sail .......................... ok +bitfield_updates0.sail ................. ok +global_type_var.sail ................... ok +pow_32_64.sail ......................... ok +reg_list.sail .......................... ok +assignment_simple.sail ................. ok +while_MP.sail .......................... ok +exist_true.sail ........................ ok +case_simple2.sail ...................... ok +equation_arguments.sail ................ ok +abstract_bool.sail ..................... ok +pow_unify.sail ......................... ok +pure_let_var2.sail ..................... ok +tuple_fun.sail ......................... ok +pure_let_var.sail ...................... ok +flow_gteq1.sail ........................ ok +mutrec.sail ............................ ok +poly_vector.sail ....................... ok +if_infer.sail .......................... ok +exist_tlb.sail ......................... ok +cons_pattern_synonym.sail .............. ok +overlap_field.sail ..................... ok +reg_ref.sail ........................... ok +let_subtyp_bug.sail .................... ok +reg_option.sail ........................ ok +pure_record2.sail ...................... ok +type_pow_zero.sail ..................... skip +inc_prelude.sail ....................... ok +phantom_bitlist_struct.sail ............ ok +type_pow_zero.sail ..................... skip +bitfield_abs.sail ...................... ok +bitfield_mod.sail ...................... ok +tuple_bitvector_int_pat3.sail .......... ok +tuple_bitvector_int_pat2.sail .......... ok +type_pow_zero.sail ..................... skip +mapping_clause.sail .................... ok +bool_typ_pat.sail ...................... ok +enum_map.sail .......................... ok +type_pow_zero.sail ..................... skip +exit1.sail ............................. ok +pure_record.sail ....................... ok +simple_scattered.sail .................. ok +issue250.sail .......................... ok +plus_one_unify.sail .................... ok +existential_constraint_synonym.sail .... ok +int_synonym.sail ....................... ok +modify_type_chain.sail ................. ok +dec_prelude.sail ....................... ok +rmem_rmemt_same.sail ................... ok +no_val_recur.sail ...................... ok +unsigned_index.sail .................... ok +if_return.sail ......................... ok +recursion.sail ......................... ok +flow_gt1.sail .......................... ok +string_literal_type.sail ............... ok +scattered_union_doc.sail ............... ok +single_enum.sail ....................... ok +vector_append_gen.sail ................. ok +exist_subrange.sail .................... ok +cast_simple.sail ....................... ok +return_simple2.sail .................... ok +scattered_enum.sail .................... ok +eqn_inst.sail .......................... ok +ex_list_infer.sail ..................... ok +if_type_if.sail ........................ ok +shadow_let.sail ........................ ok +bits_concat_pattern.sail ............... ok +flow_lt1.sail .......................... ok +nexp_synonym.sail ...................... ok +vec_length.sail ........................ ok +reg_32_64.sail ......................... ok +ex_cast.sail ........................... ok +lt_flow.sail ........................... ok +overload_plus.sail ..................... ok +cast_lexp1.sail ........................ ok +exist_simple.sail ...................... ok +bitvector_param.sail ................... ok +crlf.sail .............................. ok +zero_length_bv.sail .................... ok +mapping_rreg.sail ...................... ok +if_infer2.sail ......................... ok +bitfield_exponential.sail .............. ok +struct_pattern.sail .................... ok +tyvar_shadow.sail ...................... ok +bitfield_updates.sail .................. ok +list_infer.sail ........................ ok +constrained_struct.sail ................ ok +bitwise_not_x3.sail .................... ok +nat_set.sail ........................... ok +single_union.sail ...................... ok +case_simple1.sail ...................... ok +return_simple3.sail .................... ok +foreach_var_updates.sail ............... ok +exint.sail ............................. ok +zeros_implicit.sail .................... ok +phantom_bitlist_union.sail ............. ok +union_ctor_constraint.sail ............. ok +guards.sail ............................ ok +new_bitfields.sail ..................... ok +scattered_mapping_doc.sail ............. ok +existential_ast2.sail .................. ok +bool_constraint.sail ................... ok +concurrency_interface_dec.sail ......... ok +add_vec_exts_no_annot_overload.sail .... ok +phantom_num.sail ....................... ok +bitfield_pc.sail ....................... ok +nexp_synonym2.sail ..................... ok +single_assign_in_block.sail ............ ok +try_while_try.sail ..................... ok +struct_pattern_partial.sail ............ ok +inline_typ.sail ........................ ok +synth_ex_vs.sail ....................... ok +type_if_then_else_alt.sail ............. ok +flow_lt2.sail .......................... ok +not_pattern.sail ....................... ok +tuple_type_cast.sail ................... ok +enum_cast.sail ......................... ok +negative_bits_list.sail ................ ok +outcome_impl.sail ...................... ok +vector_access_dec.sail ................. ok +bv_simple_index_bit.sail ............... ok +while_MM.sail .......................... ok +vector_access.sail ..................... ok +list_cons.sail ......................... ok +cast_lexp2.sail ........................ ok +modify_assignment1.sail ................ ok +priv_fn_no_val.sail .................... ok +pure_record3.sail ...................... ok +bits_if.sail ........................... ok +issue434.sail .......................... ok +phantom_option.sail .................... ok +outcome_impl_quant.sail ................ ok +foreach_e.sail ......................... ok +wf_register_type.sail .................. ok +222 passes and 0 failures +------------------------ +Testing failing programs +------------------------ +Running 16 tests in parallel. Set TEST_PAR to configure +synonym_rec.sail ....................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +duplicate_type_id.sail ................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +undefined_infer.sail ................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +scattered_map_mod.sail ................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +duplicate_type_id4.sail ................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +strict_var.sail ........................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +prelude_no_order.sail .................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +scattered_enum_mod.sail ................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +add_vec_lit_old.sail ................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +struct_pattern_duplicate_field.sail .... ok +Running 16 tests in parallel. Set TEST_PAR to configure +and_let_bool.sail ...................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +unbound_tyvar2.sail .................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +mapping_body_private.sail .............. ok +Running 16 tests in parallel. Set TEST_PAR to configure +negative_bits_existential.sail ......... ok +Running 16 tests in parallel. Set TEST_PAR to configure +issue277.sail .......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +modify_enum2.sail ...................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +union_rec.sail ......................... ok +scattered_union_mod.sail ............... ok +enum_functions_partial.sail ............ ok +enum_shadow_let.sail ................... ok +scattered_function_mod.sail ............ ok +unbound_tyvar.sail ..................... ok +missing_tick.sail ...................... ok +modify_immutable2.sail ................. ok +issue244_3.sail ........................ ok +undeclared_field_assignment.sail ....... ok +mix_declaration_update.sail ............ ok +pub_val_priv_fn.sail ................... ok +abstract_bool_inconsistent.sail ........ ok +duplicate_toplevel_let.sail ............ ok +vector_pattern_split.sail .............. ok +issue243.sail .......................... ok +duplicate_type_id6.sail ................ ok +overload_member_scope.sail ............. ok +assignment_simple.sail ................. ok +procstate1.sail ........................ ok +duplicate_type_id2.sail ................ ok +scattered_union_rec.sail ............... ok +private_extension.sail ................. ok +bv_update_error.sail ................... ok +unscope_val.sail ....................... ok +poly_ab_mapping.sail ................... ok +duplicate_quant.sail ................... ok +negative_bits_struct.sail .............. ok +non_synonym.sail ....................... ok +struct_incomplete_literal.sail ......... ok +negative_bits_struct2.sail ............. ok +mapping_two_type.sail .................. ok +duplicate_ctor.sail .................... ok +union_recf.sail ........................ ok +private_scattered_map.sail ............. ok +private_scattered_enum.sail ............ ok +struct_rec.sail ........................ ok +bitfield_bits_field.sail ............... ok +issue244_4.sail ........................ ok +issue244_1.sail ........................ ok +private_union.sail ..................... ok +private_ctor.sail ...................... ok +empty_su.sail .......................... ok +empty_vector_infer.sail ................ ok +encdec_unknown_and_error.sail .......... ok +negative_bits_tuple.sail ............... ok +mapping_length_mismatch.sail ........... ok +enum_function_override.sail ............ ok +private_scattered_union.sail ........... ok +duplicate_type_id3.sail ................ ok +duplicate_builtin.sail ................. ok +global_false_constraint.sail ........... ok +private_scattered_fn.sail .............. ok +shadow_leak_infer.sail ................. ok +shadow_leak_check.sail ................. ok +negative_bits_union2.sail .............. ok +no_function3.sail ...................... ok +undeclared_vector_assignment.sail ...... ok +duplicate_binding.sail ................. ok +private_function.sail .................. ok +no_possible_overload.sail .............. ok +issue244_2.sail ........................ ok +negative_bits_union.sail ............... ok +invalid_function_val.sail .............. ok +duplicate_type_id5.sail ................ ok +overload_bound.sail .................... ok +private_clause.sail .................... ok +enum_shadow_reg.sail ................... ok +cond_mod.sail .......................... ok +duplicate_toplevel_let_mod.sail ........ ok +enum_shadow.sail ....................... ok +nonexistent_overload.sail .............. ok +no_function2.sail ...................... ok +no_function.sail ....................... ok +modify_immutable.sail .................. ok +unscope_let.sail ....................... ok +unscope_type.sail ...................... ok +bitfield_error.sail .................... ok +modify_enum.sail ....................... ok +unscope_enum.sail ...................... ok +unscope_register.sail .................. ok +wf_assign_type.sail .................... ok +98 passes and 0 failures + +========================================== +OCaml tests +========================================== +$SAIL is /home/trdthg/repo/sail/sail +built bitfield/: ok +built for_bounds/: ok +built hello_world/: ok +built is_x_subrange/: ok +built loop/: ok +built lsl/: ok +built new_bitfields/: ok +built pattern1/: ok +built pure_rebind/: ok +built reg_alias/: ok +built reg_passing/: ok +built reg_ref/: ok +built short_circuit/: ok +built string_equality/: ok +built string_of_struct/: ok +built trycatch/: ok +built types/: ok +built vec_32_64/: ok +built void/: ok +Ocaml testing: Passed 19 out of 19 + +built bitfield/: ok +built for_bounds/: ok +built hello_world/: ok +built is_x_subrange/: ok +built loop/: ok +built lsl/: ok +built new_bitfields/: ok +built pattern1/: ok +built pure_rebind/: ok +built reg_alias/: ok +built reg_passing/: ok +built reg_ref/: ok +built short_circuit/: ok +built string_equality/: ok +built string_of_struct/: ok +built trycatch/: ok +built types/: ok +built vec_32_64/: ok +built void/: ok +Ocaml trace testing: Passed 19 out of 19 + + +========================================== +Floating point tests +========================================== +Sail is /home/trdthg/repo/sail/sail +Sail dir is /home/trdthg/repo/sail +--------------------------------------------------------------------- +Testing floating point c optimized with C options: -O2 Sail options: +--------------------------------------------------------------------- +Running 16 tests in parallel. Set TEST_PAR to configure +zero_test.sail ......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +sign_test.sail ......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +normal_test.sail ....................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +nan_test.sail .......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +inf_test.sail .......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +ne_test.sail ........................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +eq_test.sail ........................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +lt_test.sail ........................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +8 passes and 0 failures + +========================================== +Lem tests +========================================== +Sail is /home/trdthg/repo/sail/sail +Sail dir is /home/trdthg/repo/sail +------------------------- +Testing Lem with bitlists +------------------------- +Running 16 tests in parallel. Set TEST_PAR to configure +deinfix_plus.sail ...................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +function_namespace.sail ................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +real.sail .............................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +add_vec_exts_no_annot.sail ............. ok +Running 16 tests in parallel. Set TEST_PAR to configure +default_order.sail ..................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +vector_append.sail ..................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +bitwise_not_gen.sail ................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +lexp_vec.sail .......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +funcl_guard.sail ....................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +exist_synonym.sail ..................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +vector_subrange_pattern.sail ........... ok +Running 16 tests in parallel. Set TEST_PAR to configure +implicits.sail ......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +floor_pow2.sail ........................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +overload_overload.sail ................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +vector_concat_assign.sail .............. ok +Running 16 tests in parallel. Set TEST_PAR to configure +exist2.sail ............................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +while_PP.sail .......................... ok +while_PM.sail .......................... ok +as_pattern.sail ........................ ok +vec_length_inc.sail .................... ok +varity.sail ............................ ok +repeat_constraint.sail ................. ok +wildcard_mapping.sail .................. ok +equation_return.sail ................... ok +atomcase.sail .......................... ok +vector_subrange_gen.sail ............... ok +true_false.sail ........................ ok +vec_pat1.sail .......................... ok +nlflow.sail ............................ ok +tuple_bitvector_int_pat.sail ........... ok +existential_ast3.sail .................. ok +existential_ast.sail ................... ok +concurrency_interface_inc.sail ......... skip +extension_constructor.sail ............. ok +concurrency_interface_inc.sail ......... skip +exit2.sail ............................. ok +concurrency_interface_inc.sail ......... skip +arm_FPEXC1.sail ........................ ok +concurrency_interface_inc.sail ......... skip +commentfix.sail ........................ ok +add_real.sail .......................... ok +concurrency_interface_inc.sail ......... skip +constraint_ctor.sail ................... ok +concurrency_interface_inc.sail ......... skip +constraint_syn.sail .................... skip +multiple_unifiers.sail ................. ok +return_simple4.sail .................... ok +sizeof_fixed.sail ...................... ok +bool_mapping.sail ...................... ok +concurrency_interface_inc.sail ......... skip +Replicate.sail ......................... ok +concurrency_interface_inc.sail ......... skip +flow_lteq1.sail ........................ ok +concurrency_interface_inc.sail ......... skip +tautology.sail ......................... ok +concurrency_interface_inc.sail ......... skip +arm_types.sail ......................... ok +concurrency_interface_inc.sail ......... skip +constraint_syn.sail .................... skip +pat_completeness.sail .................. ok +nzcv.sail .............................. ok +exit3.sail ............................. ok +patternrefinement.sail ................. ok +poly_list.sail ......................... ok +bind_typ_var.sail ...................... ok +overload_int_nat.sail .................. ok +wf_specs.sail .......................... ok +bool_bits_mapping.sail ................. ok +custom_flow.sail ....................... ok +vector_pattern_split.sail .............. ok +bool_mapping2.sail ..................... ok +decode_patterns.sail ................... ok +execute_decode_hard.sail ............... ok +struct_field_constraint.sail ........... ok +string_append_non_exec.sail ............ ok +cons_pattern.sail ...................... ok +list_lit.sail .......................... ok +return_simple1.sail .................... ok +list_cons2.sail ........................ ok +option_tuple.sail ...................... ok +if_var_updates.sail .................... ok +complex_exist_sat.sail ................. ok +tuple_assign.sail ...................... ok +type_if_then_else.sail ................. ok +ex_vector_infer.sail ................... ok +complete_pattern_let.sail .............. ok +vector_subrange_mapping.sail ........... ok +allpats.sail ........................... ok +short_circuit_bool_ex.sail ............. ok +fpthreesimp.sail ....................... ok +exist1.sail ............................ ok +simple_record_access.sail .............. ok +abstract_bool2.sail .................... skip +mod_var.sail ........................... ok +abstract_bool2.sail .................... skip +union_infer.sail ....................... ok +abstract_bool2.sail .................... skip +bitwise_not.sail ....................... ok +abstract_bool2.sail .................... skip +procstate1.sail ........................ ok +abstract_bool2.sail .................... skip +anon_rec.sail .......................... ok +option_either.sail ..................... ok +abstract_bool2.sail .................... skip +nonexistent_pragma.sail ................ ok +type_div.sail .......................... ok +abstract_bool2.sail .................... skip +add_vec_lit.sail ....................... ok +set_constraint.sail .................... ok +abstract_bool2.sail .................... skip +reg_mod.sail ........................... ok +abstract_bool2.sail .................... skip +global_type_var.sail ................... ok +bitfield_updates0.sail ................. ok +pow_32_64.sail ......................... ok +abstract_bool2.sail .................... skip +reg_list.sail .......................... ok +while_MP.sail .......................... ok +assignment_simple.sail ................. ok +case_simple2.sail ...................... ok +exist_true.sail ........................ ok +pure_let_var.sail ...................... ok +abstract_bool.sail ..................... skip +equation_arguments.sail ................ ok +pure_let_var2.sail ..................... ok +pow_unify.sail ......................... ok +mutrec.sail ............................ ok +abstract_bool.sail ..................... skip +flow_gteq1.sail ........................ ok +abstract_bool.sail ..................... skip +if_infer.sail .......................... ok +abstract_bool.sail ..................... skip +poly_vector.sail ....................... ok +abstract_bool.sail ..................... skip +tuple_fun.sail ......................... ok +exist_tlb.sail ......................... ok +abstract_bool.sail ..................... skip +cons_pattern_synonym.sail .............. ok +reg_option.sail ........................ ok +overlap_field.sail ..................... ok +pure_record2.sail ...................... ok +enum_map.sail .......................... ok +phantom_bitlist_struct.sail ............ ok +type_pow_zero.sail ..................... skip +inc_prelude.sail ....................... ok +type_pow_zero.sail ..................... skip +bitfield_abs.sail ...................... ok +bool_typ_pat.sail ...................... ok +let_subtyp_bug.sail .................... ok +reg_ref.sail ........................... ok +bitfield_mod.sail ...................... ok +tuple_bitvector_int_pat2.sail .......... ok +tuple_bitvector_int_pat3.sail .......... ok +type_pow_zero.sail ..................... skip +mapping_clause.sail .................... ok +type_pow_zero.sail ..................... skip +simple_scattered.sail .................. ok +pure_record.sail ....................... ok +exit1.sail ............................. ok +issue250.sail .......................... ok +existential_constraint_synonym.sail .... ok +plus_one_unify.sail .................... ok +string_literal_type.sail ............... ok +dec_prelude.sail ....................... ok +rmem_rmemt_same.sail ................... ok +no_val_recur.sail ...................... ok +int_synonym.sail ....................... ok +if_return.sail ......................... ok +unsigned_index.sail .................... ok +flow_gt1.sail .......................... ok +modify_type_chain.sail ................. ok +recursion.sail ......................... ok +scattered_enum.sail .................... ok +scattered_union_doc.sail ............... ok +vec_length.sail ........................ ok +return_simple2.sail .................... ok +single_enum.sail ....................... ok +nexp_synonym.sail ...................... ok +cast_simple.sail ....................... ok +exist_subrange.sail .................... ok +eqn_inst.sail .......................... ok +vector_append_gen.sail ................. ok +ex_list_infer.sail ..................... ok +if_type_if.sail ........................ ok +flow_lt1.sail .......................... ok +bits_concat_pattern.sail ............... ok +shadow_let.sail ........................ ok +reg_32_64.sail ......................... ok +overload_plus.sail ..................... ok +lt_flow.sail ........................... ok +ex_cast.sail ........................... ok +crlf.sail .............................. ok +cast_lexp1.sail ........................ ok +zero_length_bv.sail .................... ok +if_infer2.sail ......................... ok +bitvector_param.sail ................... ok +constrained_struct.sail ................ ok +struct_pattern.sail .................... ok +bitfield_updates.sail .................. ok +exist_simple.sail ...................... ok +tyvar_shadow.sail ...................... ok +list_infer.sail ........................ ok +bitfield_exponential.sail .............. ok +mapping_rreg.sail ...................... ok +bitwise_not_x3.sail .................... ok +single_union.sail ...................... ok +phantom_bitlist_union.sail ............. skip +nat_set.sail ........................... ok +case_simple1.sail ...................... ok +phantom_bitlist_union.sail ............. skip +return_simple3.sail .................... ok +union_ctor_constraint.sail ............. ok +foreach_var_updates.sail ............... ok +phantom_bitlist_union.sail ............. skip +guards.sail ............................ ok +exint.sail ............................. ok +scattered_mapping_doc.sail ............. ok +new_bitfields.sail ..................... ok +phantom_bitlist_union.sail ............. skip +bool_constraint.sail ................... ok +phantom_bitlist_union.sail ............. skip +zeros_implicit.sail .................... ok +existential_ast2.sail .................. ok +phantom_bitlist_union.sail ............. skip +concurrency_interface_dec.sail ......... skip +add_vec_exts_no_annot_overload.sail .... ok +phantom_num.sail ....................... ok +not_pattern.sail ....................... ok +struct_pattern_partial.sail ............ ok +negative_bits_list.sail ................ ok +synth_ex_vs.sail ....................... ok +inline_typ.sail ........................ ok +bitfield_pc.sail ....................... ok +nexp_synonym2.sail ..................... ok +outcome_impl.sail ...................... ok +type_if_then_else_alt.sail ............. ok +flow_lt2.sail .......................... ok +try_while_try.sail ..................... ok +single_assign_in_block.sail ............ ok +enum_cast.sail ......................... ok +tuple_type_cast.sail ................... ok +phantom_option.sail .................... skip +vector_access.sail ..................... ok +phantom_option.sail .................... skip +cast_lexp2.sail ........................ ok +phantom_option.sail .................... skip +while_MM.sail .......................... ok +phantom_option.sail .................... skip +list_cons.sail ......................... ok +vector_access_dec.sail ................. ok +phantom_option.sail .................... skip +priv_fn_no_val.sail .................... ok +phantom_option.sail .................... skip +bv_simple_index_bit.sail ............... ok +phantom_option.sail .................... skip +bits_if.sail ........................... ok +phantom_option.sail .................... skip +pure_record3.sail ...................... ok +wf_register_type.sail .................. ok +phantom_option.sail .................... skip +outcome_impl_quant.sail ................ ok +phantom_option.sail .................... skip +issue434.sail .......................... ok +modify_assignment1.sail ................ ok +phantom_option.sail .................... skip +foreach_e.sail ......................... ok +phantom_option.sail .................... skip +215 passes and 0 failures +------------------------------ +Testing Lem with machine words +------------------------------ +Running 16 tests in parallel. Set TEST_PAR to configure +vector_append.sail ..................... skip +real.sail .............................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +add_vec_exts_no_annot.sail ............. ok +Running 16 tests in parallel. Set TEST_PAR to configure +deinfix_plus.sail ...................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +vector_append.sail ..................... skip +function_namespace.sail ................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +vector_append.sail ..................... skip +bitwise_not_gen.sail ................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +default_order.sail ..................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +exist_synonym.sail ..................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +exist2.sail ............................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +overload_overload.sail ................. ok +Running 16 tests in parallel. Set TEST_PAR to configure +floor_pow2.sail ........................ ok +Running 16 tests in parallel. Set TEST_PAR to configure +funcl_guard.sail ....................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +vector_subrange_pattern.sail ........... ok +Running 16 tests in parallel. Set TEST_PAR to configure +lexp_vec.sail .......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +implicits.sail ......................... ok +Running 16 tests in parallel. Set TEST_PAR to configure +vector_concat_assign.sail .............. ok +Running 16 tests in parallel. Set TEST_PAR to configure +vector_append.sail ..................... skip +varity.sail ............................ ok +repeat_constraint.sail ................. ok +while_PM.sail .......................... skip +as_pattern.sail ........................ ok +while_PP.sail .......................... ok +while_PM.sail .......................... skip +atomcase.sail .......................... ok +while_PM.sail .......................... skip +true_false.sail ........................ ok +vec_pat1.sail .......................... ok +wildcard_mapping.sail .................. ok +equation_return.sail ................... ok +nlflow.sail ............................ ok +tuple_bitvector_int_pat.sail ........... ok +while_PM.sail .......................... skip +vector_subrange_gen.sail ............... ok +while_PM.sail .......................... skip +vec_length_inc.sail .................... ok +while_PM.sail .......................... skip +existential_ast3.sail .................. ok +while_PM.sail .......................... skip +existential_ast.sail ................... ok +while_PM.sail .......................... skip +concurrency_interface_inc.sail ......... skip +extension_constructor.sail ............. ok +concurrency_interface_inc.sail ......... skip +commentfix.sail ........................ ok +add_real.sail .......................... ok +concurrency_interface_inc.sail ......... skip +exit2.sail ............................. ok +concurrency_interface_inc.sail ......... skip +constraint_ctor.sail ................... ok +return_simple4.sail .................... ok +concurrency_interface_inc.sail ......... skip +constraint_syn.sail .................... skip +multiple_unifiers.sail ................. ok +concurrency_interface_inc.sail ......... skip +arm_FPEXC1.sail ........................ ok +sizeof_fixed.sail ...................... ok +bool_mapping.sail ...................... ok +concurrency_interface_inc.sail ......... skip +flow_lteq1.sail ........................ ok +concurrency_interface_inc.sail ......... skip +tautology.sail ......................... ok +concurrency_interface_inc.sail ......... skip +Replicate.sail ......................... ok +concurrency_interface_inc.sail ......... skip +arm_types.sail ......................... ok +concurrency_interface_inc.sail ......... skip +constraint_syn.sail .................... skip +execute_decode_hard.sail ............... skip +exit3.sail ............................. ok +execute_decode_hard.sail ............... skip +patternrefinement.sail ................. skip +nzcv.sail .............................. ok +execute_decode_hard.sail ............... skip +patternrefinement.sail ................. skip +pat_completeness.sail .................. ok +execute_decode_hard.sail ............... skip +patternrefinement.sail ................. skip +poly_list.sail ......................... ok +execute_decode_hard.sail ............... skip +bind_typ_var.sail ...................... ok +execute_decode_hard.sail ............... skip +patternrefinement.sail ................. skip +bool_bits_mapping.sail ................. ok +execute_decode_hard.sail ............... skip +patternrefinement.sail ................. skip +bool_mapping2.sail ..................... ok +execute_decode_hard.sail ............... skip +patternrefinement.sail ................. skip +wf_specs.sail .......................... ok +execute_decode_hard.sail ............... skip +patternrefinement.sail ................. skip +overload_int_nat.sail .................. ok +execute_decode_hard.sail ............... skip +patternrefinement.sail ................. skip +vector_pattern_split.sail .............. ok +execute_decode_hard.sail ............... skip +patternrefinement.sail ................. skip +custom_flow.sail ....................... ok +execute_decode_hard.sail ............... skip +patternrefinement.sail ................. skip +decode_patterns.sail ................... ok +execute_decode_hard.sail ............... skip +patternrefinement.sail ................. skip +string_append_non_exec.sail ............ ok +execute_decode_hard.sail ............... skip +patternrefinement.sail ................. skip +struct_field_constraint.sail ........... ok +execute_decode_hard.sail ............... skip +patternrefinement.sail ................. skip +ex_vector_infer.sail ................... skip +list_lit.sail .......................... ok +ex_vector_infer.sail ................... skip +cons_pattern.sail ...................... ok +list_cons2.sail ........................ ok +ex_vector_infer.sail ................... skip +option_tuple.sail ...................... ok +if_var_updates.sail .................... ok +ex_vector_infer.sail ................... skip +complete_pattern_let.sail .............. ok +ex_vector_infer.sail ................... skip +complex_exist_sat.sail ................. ok +ex_vector_infer.sail ................... skip +return_simple1.sail .................... ok +ex_vector_infer.sail ................... skip +tuple_assign.sail ...................... ok +ex_vector_infer.sail ................... skip +allpats.sail ........................... ok +short_circuit_bool_ex.sail ............. ok +exist1.sail ............................ ok +ex_vector_infer.sail ................... skip +vector_subrange_mapping.sail ........... ok +type_if_then_else.sail ................. ok +fpthreesimp.sail ....................... ok +ex_vector_infer.sail ................... skip +pow_32_64.sail ......................... skip +simple_record_access.sail .............. skip +abstract_bool2.sail .................... skip +union_infer.sail ....................... ok +pow_32_64.sail ......................... skip +simple_record_access.sail .............. skip +abstract_bool2.sail .................... skip +bitwise_not.sail ....................... ok +pow_32_64.sail ......................... skip +simple_record_access.sail .............. skip +abstract_bool2.sail .................... skip +anon_rec.sail .......................... ok +pow_32_64.sail ......................... skip +simple_record_access.sail .............. skip +abstract_bool2.sail .................... skip +mod_var.sail ........................... ok +option_either.sail ..................... ok +pow_32_64.sail ......................... skip +simple_record_access.sail .............. skip +abstract_bool2.sail .................... skip +procstate1.sail ........................ ok +pow_32_64.sail ......................... skip +simple_record_access.sail .............. skip +abstract_bool2.sail .................... skip +nonexistent_pragma.sail ................ ok +pow_32_64.sail ......................... skip +simple_record_access.sail .............. skip +abstract_bool2.sail .................... skip +reg_mod.sail ........................... ok +pow_32_64.sail ......................... skip +simple_record_access.sail .............. skip +abstract_bool2.sail .................... skip +add_vec_lit.sail ....................... ok +pow_32_64.sail ......................... skip +simple_record_access.sail .............. skip +abstract_bool2.sail .................... skip +global_type_var.sail ................... ok +pow_32_64.sail ......................... skip +simple_record_access.sail .............. skip +set_constraint.sail .................... ok +pow_32_64.sail ......................... skip +simple_record_access.sail .............. skip +type_div.sail .......................... ok +bitfield_updates0.sail ................. ok +pow_32_64.sail ......................... skip +simple_record_access.sail .............. skip +abstract_bool2.sail .................... skip +exist_true.sail ........................ ok +exist_tlb.sail ......................... skip +while_MP.sail .......................... ok +exist_tlb.sail ......................... skip +assignment_simple.sail ................. ok +exist_tlb.sail ......................... skip +case_simple2.sail ...................... ok +exist_tlb.sail ......................... skip +reg_list.sail .......................... ok +exist_tlb.sail ......................... skip +pure_let_var.sail ...................... ok +exist_tlb.sail ......................... skip +abstract_bool.sail ..................... skip +tuple_fun.sail ......................... ok +exist_tlb.sail ......................... skip +pure_let_var2.sail ..................... ok +exist_tlb.sail ......................... skip +abstract_bool.sail ..................... skip +poly_vector.sail ....................... ok +exist_tlb.sail ......................... skip +abstract_bool.sail ..................... skip +if_infer.sail .......................... ok +mutrec.sail ............................ ok +exist_tlb.sail ......................... skip +abstract_bool.sail ..................... skip +flow_gteq1.sail ........................ ok +exist_tlb.sail ......................... skip +pow_unify.sail ......................... ok +exist_tlb.sail ......................... skip +abstract_bool.sail ..................... skip +equation_arguments.sail ................ ok +exist_tlb.sail ......................... skip +abstract_bool.sail ..................... skip +bitfield_mod.sail ...................... skip +cons_pattern_synonym.sail .............. ok +bitfield_mod.sail ...................... skip +overlap_field.sail ..................... ok +bitfield_mod.sail ...................... skip +type_pow_zero.sail ..................... skip +inc_prelude.sail ....................... ok +bitfield_mod.sail ...................... skip +bool_typ_pat.sail ...................... ok +bitfield_mod.sail ...................... skip +phantom_bitlist_struct.sail ............ ok +bitfield_mod.sail ...................... skip +pure_record2.sail ...................... ok +bitfield_mod.sail ...................... skip +reg_option.sail ........................ ok +bitfield_mod.sail ...................... skip +enum_map.sail .......................... ok +bitfield_mod.sail ...................... skip +let_subtyp_bug.sail .................... ok +bitfield_mod.sail ...................... skip +reg_ref.sail ........................... ok +bitfield_mod.sail ...................... skip +tuple_bitvector_int_pat2.sail .......... ok +bitfield_mod.sail ...................... skip +type_pow_zero.sail ..................... skip +mapping_clause.sail .................... ok +tuple_bitvector_int_pat3.sail .......... ok +bitfield_mod.sail ...................... skip +type_pow_zero.sail ..................... skip +bitfield_abs.sail ...................... skip +existential_constraint_synonym.sail .... skip +exit1.sail ............................. ok +existential_constraint_synonym.sail .... skip +issue250.sail .......................... ok +existential_constraint_synonym.sail .... skip +pure_record.sail ....................... ok +existential_constraint_synonym.sail .... skip +plus_one_unify.sail .................... ok +existential_constraint_synonym.sail .... skip +simple_scattered.sail .................. ok +existential_constraint_synonym.sail .... skip +string_literal_type.sail ............... ok +existential_constraint_synonym.sail .... skip +dec_prelude.sail ....................... ok +existential_constraint_synonym.sail .... skip +rmem_rmemt_same.sail ................... ok +existential_constraint_synonym.sail .... skip +no_val_recur.sail ...................... ok +existential_constraint_synonym.sail .... skip +modify_type_chain.sail ................. ok +existential_constraint_synonym.sail .... skip +if_return.sail ......................... ok +existential_constraint_synonym.sail .... skip +int_synonym.sail ....................... ok +existential_constraint_synonym.sail .... skip +recursion.sail ......................... ok +existential_constraint_synonym.sail .... skip +unsigned_index.sail .................... ok +existential_constraint_synonym.sail .... skip +flow_gt1.sail .......................... ok +existential_constraint_synonym.sail .... skip +ex_list_infer.sail ..................... skip +scattered_enum.sail .................... ok +scattered_union_doc.sail ............... ok +ex_list_infer.sail ..................... skip +vector_append_gen.sail ................. skip +exist_subrange.sail .................... ok +ex_list_infer.sail ..................... skip +vec_length.sail ........................ ok +ex_list_infer.sail ..................... skip +single_enum.sail ....................... ok +ex_list_infer.sail ..................... skip +nexp_synonym.sail ...................... ok +ex_list_infer.sail ..................... skip +cast_simple.sail ....................... ok +ex_list_infer.sail ..................... skip +eqn_inst.sail .......................... ok +ex_list_infer.sail ..................... skip +return_simple2.sail .................... ok +ex_list_infer.sail ..................... skip +vector_append_gen.sail ................. skip +shadow_let.sail ........................ ok +bits_concat_pattern.sail ............... ok +ex_list_infer.sail ..................... skip +flow_lt1.sail .......................... ok +ex_list_infer.sail ..................... skip +reg_32_64.sail ......................... ok +if_type_if.sail ........................ ok +ex_list_infer.sail ..................... skip +vector_append_gen.sail ................. skip +bitfield_exponential.sail .............. skip +zero_length_bv.sail .................... skip +lt_flow.sail ........................... ok +ex_cast.sail ........................... ok +crlf.sail .............................. ok +bitfield_exponential.sail .............. skip +cast_lexp1.sail ........................ ok +struct_pattern.sail .................... ok +list_infer.sail ........................ ok +bitfield_exponential.sail .............. skip +if_infer2.sail ......................... ok +constrained_struct.sail ................ ok +bitfield_exponential.sail .............. skip +tyvar_shadow.sail ...................... ok +exist_simple.sail ...................... ok +bitfield_exponential.sail .............. skip +mapping_rreg.sail ...................... ok +bitvector_param.sail ................... ok +bitfield_exponential.sail .............. skip +bitfield_updates.sail .................. ok +bitfield_exponential.sail .............. skip +zero_length_bv.sail .................... skip +overload_plus.sail ..................... skip +single_union.sail ...................... ok +bitwise_not_x3.sail .................... ok +nat_set.sail ........................... ok +case_simple1.sail ...................... ok +return_simple3.sail .................... ok +phantom_bitlist_union.sail ............. ok +union_ctor_constraint.sail ............. ok +zeros_implicit.sail .................... ok +exint.sail ............................. ok +foreach_var_updates.sail ............... ok +guards.sail ............................ ok +bool_constraint.sail ................... ok +scattered_mapping_doc.sail ............. ok +new_bitfields.sail ..................... ok +existential_ast2.sail .................. ok +concurrency_interface_dec.sail ......... skip +negative_bits_list.sail ................ skip +add_vec_exts_no_annot_overload.sail .... ok +negative_bits_list.sail ................ skip +phantom_num.sail ....................... ok +negative_bits_list.sail ................ skip +struct_pattern_partial.sail ............ ok +negative_bits_list.sail ................ skip +bitfield_pc.sail ....................... ok +negative_bits_list.sail ................ skip +outcome_impl.sail ...................... ok +nexp_synonym2.sail ..................... ok +negative_bits_list.sail ................ skip +single_assign_in_block.sail ............ ok +negative_bits_list.sail ................ skip +try_while_try.sail ..................... ok +negative_bits_list.sail ................ skip +type_if_then_else_alt.sail ............. ok +not_pattern.sail ....................... ok +synth_ex_vs.sail ....................... ok +negative_bits_list.sail ................ skip +enum_cast.sail ......................... ok +negative_bits_list.sail ................ skip +inline_typ.sail ........................ ok +negative_bits_list.sail ................ skip +flow_lt2.sail .......................... ok +tuple_type_cast.sail ................... ok +negative_bits_list.sail ................ skip +wf_register_type.sail .................. skip +phantom_option.sail .................... skip +list_cons.sail ......................... ok +wf_register_type.sail .................. skip +phantom_option.sail .................... skip +cast_lexp2.sail ........................ ok +vector_access_dec.sail ................. ok +wf_register_type.sail .................. skip +phantom_option.sail .................... skip +while_MM.sail .......................... skip +vector_access.sail ..................... ok +wf_register_type.sail .................. skip +phantom_option.sail .................... skip +bv_simple_index_bit.sail ............... ok +wf_register_type.sail .................. skip +phantom_option.sail .................... skip +pure_record3.sail ...................... ok +wf_register_type.sail .................. skip +phantom_option.sail .................... skip +priv_fn_no_val.sail .................... ok +wf_register_type.sail .................. skip +phantom_option.sail .................... skip +outcome_impl_quant.sail ................ ok +wf_register_type.sail .................. skip +modify_assignment1.sail ................ ok +wf_register_type.sail .................. skip +phantom_option.sail .................... skip +issue434.sail .......................... ok +wf_register_type.sail .................. skip +phantom_option.sail .................... skip +while_MM.sail .......................... skip +foreach_e.sail ......................... ok +wf_register_type.sail .................. skip +phantom_option.sail .................... skip +bits_if.sail ........................... ok +wf_register_type.sail .................. skip +phantom_option.sail .................... skip +while_MM.sail .......................... skip +197 passes and 0 failures + +========================================== +Monomorphisation tests +========================================== +$SAIL is /home/trdthg/repo/sail/sail +tested assert expecting pass: pass +tested assert2 expecting pass: pass +tested assign_range expecting pass: pass +tested atomsplit expecting pass: pass +tested builtins expecting pass: pass +tested castreq expecting pass: pass +tested castrequnion expecting pass: pass +tested constprop expecting pass: pass +tested control_deps expecting pass: pass +tested exint expecting pass: pass +tested feature_no_effects expecting pass: pass +tested flow_extend expecting pass: pass +tested fsplitsign expecting pass: pass +tested itself_rewriting expecting pass: pass +tested letsplit expecting pass: pass +tested mapping expecting pass: pass +tested mutrecmono expecting pass: pass +tested nonlinearpat expecting pass: pass +tested parameterchoice expecting pass: pass +tested range expecting pass: pass +tested repeatedint expecting pass: pass +tested rewrites expecting pass: pass +tested set expecting pass: pass +tested set3 expecting pass: pass +tested splitreturn expecting pass: pass +tested structparam2 expecting pass: pass +tested time8_continue expecting pass: pass +tested times8 expecting pass: pass +tested times8div8 expecting pass: pass +tested tupledeps expecting pass: pass +tested tupledeps2 expecting pass: pass +tested union-exist expecting pass: pass +tested union-exist2 expecting pass: pass +tested union-exist_manual expecting pass: pass +tested union_split expecting pass: pass +tested varmatch expecting pass: pass +tested varmatch_manual expecting pass: pass +tested varpatterns expecting pass: pass +tested vector expecting pass: pass +tested vector_manual expecting pass: pass +tested vectorsize expecting pass: pass +monomorphisation tests: Passed 41 out of 41 + + +========================================== +LaTeX tests +========================================== +./let.sail +./reference-type.sail +./reg.sail +./candperm.sail +./bitfield.sail +Generating LaTeX for bitfield.sail: ok +Building LaTeX for bitfield.sail: latexmk not installed +Files /tmp/tmp.m8JU8I5Fxy/out/commands.tex and candperm.commands.tex.exp differ +--- /tmp/tmp.m8JU8I5Fxy/out/commands.tex 2024-07-29 15:49:32.277277982 +0800 ++++ candperm.commands.tex.exp 2024-07-26 09:11:18.863870876 +0800 +@@ -9,30 +9,6 @@ + \providecommand\saildoclet[2]{#1 #2} + \providecommand\saildocregister[2]{#1 #2} + +-\newcommand{\sailvalinternalPick}{\saildoclabelled{sailzinternalzypick}{\saildocval{}{\lstinputlisting[language=sail]{out/valzinternal_pick0eb5adfbcccbb1785fa494f00459100d.tex}}}} +- +-\newcommand{\sailvalundefinedBool}{\saildoclabelled{sailzundefinedzybool}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_bool243ac67bbc90a729a829b61aebdfb100.tex}}}} +- +-\newcommand{\sailvalundefinedBit}{\saildoclabelled{sailzundefinedzybit}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_bitda1641f2d65bcfe8a6543bdf76182545.tex}}}} +- +-\newcommand{\sailvalundefinedInt}{\saildoclabelled{sailzundefinedzyint}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_intd4ae6556082aadeaaedb4f74f01376ce.tex}}}} +- +-\newcommand{\sailvalundefinedNat}{\saildoclabelled{sailzundefinedzynat}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_natd1f1df7de8df3f2d01791e80cbd35531.tex}}}} +- +-\newcommand{\sailvalundefinedReal}{\saildoclabelled{sailzundefinedzyreal}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_realc5ec14397a5a0720672cdd9ba3506589.tex}}}} +- +-\newcommand{\sailvalundefinedString}{\saildoclabelled{sailzundefinedzystring}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_stringe5c8a6af28b8ac03b9fd048eaa331eb8.tex}}}} +- +-\newcommand{\sailvalundefinedList}{\saildoclabelled{sailzundefinedzylist}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_list642d622904a8c0888aa4e72a844c6812.tex}}}} +- +-\newcommand{\sailvalundefinedRange}{\saildoclabelled{sailzundefinedzyrange}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_range78fb4a60a699f8333068f57d526860fa.tex}}}} +- +-\newcommand{\sailvalundefinedVector}{\saildoclabelled{sailzundefinedzyvector}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_vector7dcc506a79e97a89a0d66bc54b515466.tex}}}} +- +-\newcommand{\sailvalundefinedBitvector}{\saildoclabelled{sailzundefinedzybitvector}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_bitvectorc0153f961b53b1b17bf36adcf5409590.tex}}}} +- +-\newcommand{\sailvalundefinedUnit}{\saildoclabelled{sailzundefinedzyunit}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_unitd751910db26c6cf7ec5d02a503ad4f9e.tex}}}} +- + \newcommand{\sailtypeast}{\saildoclabelled{sailtypezast}{\saildoctype{}{\lstinputlisting[language=sail]{out/typezast6bb070d12e82e4887160cdfd016230c8.tex}}}} + + \newcommand{\sailvalexecute}{\saildoclabelled{sailzexecute}{\saildocval{}{\lstinputlisting[language=sail]{out/valzexecute33a689e3a631b9b905b85461d3814943.tex}}}} +@@ -84,81 +60,22 @@ + \begin{itemize} + \item \emph{cs1.tag} is not set. + \item \emph{cs1} is sealed. +- + \end{itemize} + }{\lstinputlisting[language=sail]{out/fclCAndPermMarkdownWithExceptionszexecute33a689e3a631b9b905b85461d3814943.tex}}}} + + + +-\newcommand{\sailvalinitializzeRegisters}{\saildoclabelled{sailzinitializzezyregisters}{\saildocval{}{\lstinputlisting[language=sail]{out/valzinitializze_registerscd0d92787ce5f32f7391468692054f16.tex}}}} +- +-\newcommand{\sailfninitializzeRegisters}{\saildoclabelled{sailfnzinitializzezyregisters}{\saildocfn{}{\lstinputlisting[language=sail]{out/fnzinitializze_registerscd0d92787ce5f32f7391468692054f16.tex}}}} +- + \newcommand{\sailval}[1]{ +- \ifstrequal{#1}{execute}{\sailvalexecute}{}% +- \ifstrequal{#1}{initialize_registers}{\sailvalinitializzeRegisters}{}% +- \ifstrequal{#1}{initialize\_registers}{\sailvalinitializzeRegisters}{}% +- \ifstrequal{#1}{internal_pick}{\sailvalinternalPick}{}% +- \ifstrequal{#1}{internal\_pick}{\sailvalinternalPick}{}% +- \ifstrequal{#1}{undefined_bit}{\sailvalundefinedBit}{}% +- \ifstrequal{#1}{undefined\_bit}{\sailvalundefinedBit}{}% +- \ifstrequal{#1}{undefined_bitvector}{\sailvalundefinedBitvector}{}% +- \ifstrequal{#1}{undefined\_bitvector}{\sailvalundefinedBitvector}{}% +- \ifstrequal{#1}{undefined_bool}{\sailvalundefinedBool}{}% +- \ifstrequal{#1}{undefined\_bool}{\sailvalundefinedBool}{}% +- \ifstrequal{#1}{undefined_int}{\sailvalundefinedInt}{}% +- \ifstrequal{#1}{undefined\_int}{\sailvalundefinedInt}{}% +- \ifstrequal{#1}{undefined_list}{\sailvalundefinedList}{}% +- \ifstrequal{#1}{undefined\_list}{\sailvalundefinedList}{}% +- \ifstrequal{#1}{undefined_nat}{\sailvalundefinedNat}{}% +- \ifstrequal{#1}{undefined\_nat}{\sailvalundefinedNat}{}% +- \ifstrequal{#1}{undefined_range}{\sailvalundefinedRange}{}% +- \ifstrequal{#1}{undefined\_range}{\sailvalundefinedRange}{}% +- \ifstrequal{#1}{undefined_real}{\sailvalundefinedReal}{}% +- \ifstrequal{#1}{undefined\_real}{\sailvalundefinedReal}{}% +- \ifstrequal{#1}{undefined_string}{\sailvalundefinedString}{}% +- \ifstrequal{#1}{undefined\_string}{\sailvalundefinedString}{}% +- \ifstrequal{#1}{undefined_unit}{\sailvalundefinedUnit}{}% +- \ifstrequal{#1}{undefined\_unit}{\sailvalundefinedUnit}{}% +- \ifstrequal{#1}{undefined_vector}{\sailvalundefinedVector}{}% +- \ifstrequal{#1}{undefined\_vector}{\sailvalundefinedVector}{}} ++ \ifstrequal{#1}{execute}{\sailvalexecute}{}} + + \newcommand{\sailrefval}[2]{ +- \ifstrequal{#1}{execute}{\hyperref[sailzexecute]{#2}}{}% +- \ifstrequal{#1}{initialize_registers}{\hyperref[sailzinitializzezyregisters]{#2}}{}% +- \ifstrequal{#1}{initialize\_registers}{\hyperref[sailzinitializzezyregisters]{#2}}{}% +- \ifstrequal{#1}{internal_pick}{\hyperref[sailzinternalzypick]{#2}}{}% +- \ifstrequal{#1}{internal\_pick}{\hyperref[sailzinternalzypick]{#2}}{}% +- \ifstrequal{#1}{undefined_bit}{\hyperref[sailzundefinedzybit]{#2}}{}% +- \ifstrequal{#1}{undefined\_bit}{\hyperref[sailzundefinedzybit]{#2}}{}% +- \ifstrequal{#1}{undefined_bitvector}{\hyperref[sailzundefinedzybitvector]{#2}}{}% +- \ifstrequal{#1}{undefined\_bitvector}{\hyperref[sailzundefinedzybitvector]{#2}}{}% +- \ifstrequal{#1}{undefined_bool}{\hyperref[sailzundefinedzybool]{#2}}{}% +- \ifstrequal{#1}{undefined\_bool}{\hyperref[sailzundefinedzybool]{#2}}{}% +- \ifstrequal{#1}{undefined_int}{\hyperref[sailzundefinedzyint]{#2}}{}% +- \ifstrequal{#1}{undefined\_int}{\hyperref[sailzundefinedzyint]{#2}}{}% +- \ifstrequal{#1}{undefined_list}{\hyperref[sailzundefinedzylist]{#2}}{}% +- \ifstrequal{#1}{undefined\_list}{\hyperref[sailzundefinedzylist]{#2}}{}% +- \ifstrequal{#1}{undefined_nat}{\hyperref[sailzundefinedzynat]{#2}}{}% +- \ifstrequal{#1}{undefined\_nat}{\hyperref[sailzundefinedzynat]{#2}}{}% +- \ifstrequal{#1}{undefined_range}{\hyperref[sailzundefinedzyrange]{#2}}{}% +- \ifstrequal{#1}{undefined\_range}{\hyperref[sailzundefinedzyrange]{#2}}{}% +- \ifstrequal{#1}{undefined_real}{\hyperref[sailzundefinedzyreal]{#2}}{}% +- \ifstrequal{#1}{undefined\_real}{\hyperref[sailzundefinedzyreal]{#2}}{}% +- \ifstrequal{#1}{undefined_string}{\hyperref[sailzundefinedzystring]{#2}}{}% +- \ifstrequal{#1}{undefined\_string}{\hyperref[sailzundefinedzystring]{#2}}{}% +- \ifstrequal{#1}{undefined_unit}{\hyperref[sailzundefinedzyunit]{#2}}{}% +- \ifstrequal{#1}{undefined\_unit}{\hyperref[sailzundefinedzyunit]{#2}}{}% +- \ifstrequal{#1}{undefined_vector}{\hyperref[sailzundefinedzyvector]{#2}}{}% +- \ifstrequal{#1}{undefined\_vector}{\hyperref[sailzundefinedzyvector]{#2}}{}} ++ \ifstrequal{#1}{execute}{\hyperref[sailzexecute]{#2}}{}} + + \newcommand{\sailfn}[1]{ +- \ifstrequal{#1}{initialize_registers}{\sailfninitializzeRegisters}{}% +- \ifstrequal{#1}{initialize\_registers}{\sailfninitializzeRegisters}{}} ++ } + + \newcommand{\sailreffn}[2]{ +- \ifstrequal{#1}{initialize_registers}{\hyperref[sailfnzinitializzezyregisters]{#2}}{}% +- \ifstrequal{#1}{initialize\_registers}{\hyperref[sailfnzinitializzezyregisters]{#2}}{}} ++ } + + \newcommand{\sailtype}[1]{ + \ifstrequal{#1}{ast}{\sailtypeast}{}} +Generating LaTeX for candperm.sail: output is different +Building LaTeX for candperm.sail: latexmk not installed +Files /tmp/tmp.LGX6FgtpCd/out/commands.tex and let.commands.tex.exp differ +--- /tmp/tmp.LGX6FgtpCd/out/commands.tex 2024-07-29 15:49:32.307277980 +0800 ++++ let.commands.tex.exp 2024-07-26 09:11:18.863870876 +0800 +@@ -9,101 +9,21 @@ + \providecommand\saildoclet[2]{#1 #2} + \providecommand\saildocregister[2]{#1 #2} + +-\newcommand{\sailvalinternalPick}{\saildoclabelled{sailzinternalzypick}{\saildocval{}{\lstinputlisting[language=sail]{out/valzinternal_pick0eb5adfbcccbb1785fa494f00459100d.tex}}}} +- +-\newcommand{\sailvalundefinedBool}{\saildoclabelled{sailzundefinedzybool}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_bool243ac67bbc90a729a829b61aebdfb100.tex}}}} +- +-\newcommand{\sailvalundefinedBit}{\saildoclabelled{sailzundefinedzybit}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_bitda1641f2d65bcfe8a6543bdf76182545.tex}}}} +- +-\newcommand{\sailvalundefinedInt}{\saildoclabelled{sailzundefinedzyint}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_intd4ae6556082aadeaaedb4f74f01376ce.tex}}}} +- +-\newcommand{\sailvalundefinedNat}{\saildoclabelled{sailzundefinedzynat}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_natd1f1df7de8df3f2d01791e80cbd35531.tex}}}} +- +-\newcommand{\sailvalundefinedReal}{\saildoclabelled{sailzundefinedzyreal}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_realc5ec14397a5a0720672cdd9ba3506589.tex}}}} +- +-\newcommand{\sailvalundefinedString}{\saildoclabelled{sailzundefinedzystring}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_stringe5c8a6af28b8ac03b9fd048eaa331eb8.tex}}}} +- +-\newcommand{\sailvalundefinedList}{\saildoclabelled{sailzundefinedzylist}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_list642d622904a8c0888aa4e72a844c6812.tex}}}} +- +-\newcommand{\sailvalundefinedRange}{\saildoclabelled{sailzundefinedzyrange}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_range78fb4a60a699f8333068f57d526860fa.tex}}}} +- +-\newcommand{\sailvalundefinedVector}{\saildoclabelled{sailzundefinedzyvector}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_vector7dcc506a79e97a89a0d66bc54b515466.tex}}}} +- +-\newcommand{\sailvalundefinedBitvector}{\saildoclabelled{sailzundefinedzybitvector}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_bitvectorc0153f961b53b1b17bf36adcf5409590.tex}}}} +- +-\newcommand{\sailvalundefinedUnit}{\saildoclabelled{sailzundefinedzyunit}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_unitd751910db26c6cf7ec5d02a503ad4f9e.tex}}}} +- + \newcommand{\sailletfive}{\saildoclabelled{sailletzfive}{\saildoclet{}{\lstinputlisting[language=sail]{out/letzfivecd794ea050dab71d846e756689b83a36.tex}}}} + + \newcommand{\sailletseven}{\saildoclabelled{sailletzseven}{\saildoclet{}{\lstinputlisting[language=sail]{out/letzseven4931f12072db48c84b4f78b84a6a1b73.tex}}}} + +-\newcommand{\sailvalinitializzeRegisters}{\saildoclabelled{sailzinitializzezyregisters}{\saildocval{}{\lstinputlisting[language=sail]{out/valzinitializze_registerscd0d92787ce5f32f7391468692054f16.tex}}}} +- +-\newcommand{\sailfninitializzeRegisters}{\saildoclabelled{sailfnzinitializzezyregisters}{\saildocfn{}{\lstinputlisting[language=sail]{out/fnzinitializze_registerscd0d92787ce5f32f7391468692054f16.tex}}}} +- + \newcommand{\sailval}[1]{ +- \ifstrequal{#1}{initialize_registers}{\sailvalinitializzeRegisters}{}% +- \ifstrequal{#1}{initialize\_registers}{\sailvalinitializzeRegisters}{}% +- \ifstrequal{#1}{internal_pick}{\sailvalinternalPick}{}% +- \ifstrequal{#1}{internal\_pick}{\sailvalinternalPick}{}% +- \ifstrequal{#1}{undefined_bit}{\sailvalundefinedBit}{}% +- \ifstrequal{#1}{undefined\_bit}{\sailvalundefinedBit}{}% +- \ifstrequal{#1}{undefined_bitvector}{\sailvalundefinedBitvector}{}% +- \ifstrequal{#1}{undefined\_bitvector}{\sailvalundefinedBitvector}{}% +- \ifstrequal{#1}{undefined_bool}{\sailvalundefinedBool}{}% +- \ifstrequal{#1}{undefined\_bool}{\sailvalundefinedBool}{}% +- \ifstrequal{#1}{undefined_int}{\sailvalundefinedInt}{}% +- \ifstrequal{#1}{undefined\_int}{\sailvalundefinedInt}{}% +- \ifstrequal{#1}{undefined_list}{\sailvalundefinedList}{}% +- \ifstrequal{#1}{undefined\_list}{\sailvalundefinedList}{}% +- \ifstrequal{#1}{undefined_nat}{\sailvalundefinedNat}{}% +- \ifstrequal{#1}{undefined\_nat}{\sailvalundefinedNat}{}% +- \ifstrequal{#1}{undefined_range}{\sailvalundefinedRange}{}% +- \ifstrequal{#1}{undefined\_range}{\sailvalundefinedRange}{}% +- \ifstrequal{#1}{undefined_real}{\sailvalundefinedReal}{}% +- \ifstrequal{#1}{undefined\_real}{\sailvalundefinedReal}{}% +- \ifstrequal{#1}{undefined_string}{\sailvalundefinedString}{}% +- \ifstrequal{#1}{undefined\_string}{\sailvalundefinedString}{}% +- \ifstrequal{#1}{undefined_unit}{\sailvalundefinedUnit}{}% +- \ifstrequal{#1}{undefined\_unit}{\sailvalundefinedUnit}{}% +- \ifstrequal{#1}{undefined_vector}{\sailvalundefinedVector}{}% +- \ifstrequal{#1}{undefined\_vector}{\sailvalundefinedVector}{}} ++ } + + \newcommand{\sailrefval}[2]{ +- \ifstrequal{#1}{initialize_registers}{\hyperref[sailzinitializzezyregisters]{#2}}{}% +- \ifstrequal{#1}{initialize\_registers}{\hyperref[sailzinitializzezyregisters]{#2}}{}% +- \ifstrequal{#1}{internal_pick}{\hyperref[sailzinternalzypick]{#2}}{}% +- \ifstrequal{#1}{internal\_pick}{\hyperref[sailzinternalzypick]{#2}}{}% +- \ifstrequal{#1}{undefined_bit}{\hyperref[sailzundefinedzybit]{#2}}{}% +- \ifstrequal{#1}{undefined\_bit}{\hyperref[sailzundefinedzybit]{#2}}{}% +- \ifstrequal{#1}{undefined_bitvector}{\hyperref[sailzundefinedzybitvector]{#2}}{}% +- \ifstrequal{#1}{undefined\_bitvector}{\hyperref[sailzundefinedzybitvector]{#2}}{}% +- \ifstrequal{#1}{undefined_bool}{\hyperref[sailzundefinedzybool]{#2}}{}% +- \ifstrequal{#1}{undefined\_bool}{\hyperref[sailzundefinedzybool]{#2}}{}% +- \ifstrequal{#1}{undefined_int}{\hyperref[sailzundefinedzyint]{#2}}{}% +- \ifstrequal{#1}{undefined\_int}{\hyperref[sailzundefinedzyint]{#2}}{}% +- \ifstrequal{#1}{undefined_list}{\hyperref[sailzundefinedzylist]{#2}}{}% +- \ifstrequal{#1}{undefined\_list}{\hyperref[sailzundefinedzylist]{#2}}{}% +- \ifstrequal{#1}{undefined_nat}{\hyperref[sailzundefinedzynat]{#2}}{}% +- \ifstrequal{#1}{undefined\_nat}{\hyperref[sailzundefinedzynat]{#2}}{}% +- \ifstrequal{#1}{undefined_range}{\hyperref[sailzundefinedzyrange]{#2}}{}% +- \ifstrequal{#1}{undefined\_range}{\hyperref[sailzundefinedzyrange]{#2}}{}% +- \ifstrequal{#1}{undefined_real}{\hyperref[sailzundefinedzyreal]{#2}}{}% +- \ifstrequal{#1}{undefined\_real}{\hyperref[sailzundefinedzyreal]{#2}}{}% +- \ifstrequal{#1}{undefined_string}{\hyperref[sailzundefinedzystring]{#2}}{}% +- \ifstrequal{#1}{undefined\_string}{\hyperref[sailzundefinedzystring]{#2}}{}% +- \ifstrequal{#1}{undefined_unit}{\hyperref[sailzundefinedzyunit]{#2}}{}% +- \ifstrequal{#1}{undefined\_unit}{\hyperref[sailzundefinedzyunit]{#2}}{}% +- \ifstrequal{#1}{undefined_vector}{\hyperref[sailzundefinedzyvector]{#2}}{}% +- \ifstrequal{#1}{undefined\_vector}{\hyperref[sailzundefinedzyvector]{#2}}{}} ++ } + + \newcommand{\sailfn}[1]{ +- \ifstrequal{#1}{initialize_registers}{\sailfninitializzeRegisters}{}% +- \ifstrequal{#1}{initialize\_registers}{\sailfninitializzeRegisters}{}} ++ } + + \newcommand{\sailreffn}[2]{ +- \ifstrequal{#1}{initialize_registers}{\hyperref[sailfnzinitializzezyregisters]{#2}}{}% +- \ifstrequal{#1}{initialize\_registers}{\hyperref[sailfnzinitializzezyregisters]{#2}}{}} ++ } + + \newcommand{\sailtype}[1]{ + } +Generating LaTeX for let.sail: output is different +Building LaTeX for let.sail: latexmk not installed +Files /tmp/tmp.DbfiHehxjm/out/commands.tex and reference-type.commands.tex.exp differ +--- /tmp/tmp.DbfiHehxjm/out/commands.tex 2024-07-29 15:49:32.397277975 +0800 ++++ reference-type.commands.tex.exp 2024-07-26 09:11:18.863870876 +0800 +@@ -9,30 +9,6 @@ + \providecommand\saildoclet[2]{#1 #2} + \providecommand\saildocregister[2]{#1 #2} + +-\newcommand{\sailvalinternalPick}{\saildoclabelled{sailzinternalzypick}{\saildocval{}{\lstinputlisting[language=sail]{out/valzinternal_pick0eb5adfbcccbb1785fa494f00459100d.tex}}}} +- +-\newcommand{\sailvalundefinedBool}{\saildoclabelled{sailzundefinedzybool}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_bool243ac67bbc90a729a829b61aebdfb100.tex}}}} +- +-\newcommand{\sailvalundefinedBit}{\saildoclabelled{sailzundefinedzybit}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_bitda1641f2d65bcfe8a6543bdf76182545.tex}}}} +- +-\newcommand{\sailvalundefinedInt}{\saildoclabelled{sailzundefinedzyint}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_intd4ae6556082aadeaaedb4f74f01376ce.tex}}}} +- +-\newcommand{\sailvalundefinedNat}{\saildoclabelled{sailzundefinedzynat}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_natd1f1df7de8df3f2d01791e80cbd35531.tex}}}} +- +-\newcommand{\sailvalundefinedReal}{\saildoclabelled{sailzundefinedzyreal}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_realc5ec14397a5a0720672cdd9ba3506589.tex}}}} +- +-\newcommand{\sailvalundefinedString}{\saildoclabelled{sailzundefinedzystring}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_stringe5c8a6af28b8ac03b9fd048eaa331eb8.tex}}}} +- +-\newcommand{\sailvalundefinedList}{\saildoclabelled{sailzundefinedzylist}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_list642d622904a8c0888aa4e72a844c6812.tex}}}} +- +-\newcommand{\sailvalundefinedRange}{\saildoclabelled{sailzundefinedzyrange}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_range78fb4a60a699f8333068f57d526860fa.tex}}}} +- +-\newcommand{\sailvalundefinedVector}{\saildoclabelled{sailzundefinedzyvector}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_vector7dcc506a79e97a89a0d66bc54b515466.tex}}}} +- +-\newcommand{\sailvalundefinedBitvector}{\saildoclabelled{sailzundefinedzybitvector}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_bitvectorc0153f961b53b1b17bf36adcf5409590.tex}}}} +- +-\newcommand{\sailvalundefinedUnit}{\saildoclabelled{sailzundefinedzyunit}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_unitd751910db26c6cf7ec5d02a503ad4f9e.tex}}}} +- + \newcommand{\sailvaleqUnit}{\saildoclabelled{sailzeqzyunit}{\saildocval{}{\lstinputlisting[language=sail]{out/valzeq_unit996f84433ac0995f4aadfca5b68cd358.tex}}}} + + \newcommand{\sailvaleqBit}{\saildoclabelled{sailzeqzybit}{\saildocval{}{\lstinputlisting[language=sail]{out/valzeq_bit7182cc37406e2c0d4c1e739a98e248ea.tex}}}} +@@ -67,27 +43,27 @@ + + \newcommand{\sailvalgtInt}{\saildoclabelled{sailzgtzyint}{\saildocval{}{\lstinputlisting[language=sail]{out/valzgt_intef94a8c66f39b1f715cb72941ed95921.tex}}}} + +-\newcommand{\sailoverloadAzEightoperatorzZerozJzJzNine}{\saildoclabelled{sailoverloadAzz8operatorz0zJzJz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzz8operatorz0zjzjz9c650f45e06411dd4e97578ff2bad6338.tex}}}} ++\newcommand{\sailoverloadBzEightoperatorzZerozJzJzNine}{\saildoclabelled{sailoverloadBzz8operatorz0zJzJz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadBzz8operatorz0zjzjz9c650f45e06411dd4e97578ff2bad6338.tex}}}} + +-\newcommand{\sailoverloadAzEightoperatorzZerozOnezJzNine}{\saildoclabelled{sailoverloadAzz8operatorz0z1zJz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzz8operatorz0z1zjz981ebe433e26f9e2dfa2a9d2c7f4fe1f4.tex}}}} ++\newcommand{\sailoverloadCzEightoperatorzZerozOnezJzNine}{\saildoclabelled{sailoverloadCzz8operatorz0z1zJz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadCzz8operatorz0z1zjz981ebe433e26f9e2dfa2a9d2c7f4fe1f4.tex}}}} + +-\newcommand{\sailoverloadAzEightoperatorzZerozUzNine}{\saildoclabelled{sailoverloadAzz8operatorz0zUz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzz8operatorz0zuz99af95b281314726fa91893b57fc290dc.tex}}}} ++\newcommand{\sailoverloadDzEightoperatorzZerozUzNine}{\saildoclabelled{sailoverloadDzz8operatorz0zUz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadDzz8operatorz0zuz99af95b281314726fa91893b57fc290dc.tex}}}} + +-\newcommand{\sailoverloadAzEightoperatorzZerozSixzNine}{\saildoclabelled{sailoverloadAzz8operatorz0z6z9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzz8operatorz0z6z9d3731bb9b1c9d765858778ad48ba6b3a.tex}}}} ++\newcommand{\sailoverloadEzEightoperatorzZerozSixzNine}{\saildoclabelled{sailoverloadEzz8operatorz0z6z9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadEzz8operatorz0z6z9d3731bb9b1c9d765858778ad48ba6b3a.tex}}}} + +-\newcommand{\sailoverloadAzEightoperatorzZerozIzJzNine}{\saildoclabelled{sailoverloadAzz8operatorz0zIzJz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzz8operatorz0zizjz95c366628fed7d8b7c251f1acd527ee3b.tex}}}} ++\newcommand{\sailoverloadFzEightoperatorzZerozIzJzNine}{\saildoclabelled{sailoverloadFzz8operatorz0zIzJz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadFzz8operatorz0zizjz95c366628fed7d8b7c251f1acd527ee3b.tex}}}} + +-\newcommand{\sailoverloadAzEightoperatorzZerozIzNine}{\saildoclabelled{sailoverloadAzz8operatorz0zIz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzz8operatorz0ziz9714b8c400aed24ebd80eac39b4f9d751.tex}}}} ++\newcommand{\sailoverloadGzEightoperatorzZerozIzNine}{\saildoclabelled{sailoverloadGzz8operatorz0zIz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadGzz8operatorz0ziz9714b8c400aed24ebd80eac39b4f9d751.tex}}}} + +-\newcommand{\sailoverloadAzEightoperatorzZerozKzJzNine}{\saildoclabelled{sailoverloadAzz8operatorz0zKzJz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzz8operatorz0zkzjz94161e4bfad2d20e5d25bc774612b6588.tex}}}} ++\newcommand{\sailoverloadHzEightoperatorzZerozKzJzNine}{\saildoclabelled{sailoverloadHzz8operatorz0zKzJz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadHzz8operatorz0zkzjz94161e4bfad2d20e5d25bc774612b6588.tex}}}} + +-\newcommand{\sailoverloadAzEightoperatorzZerozKzNine}{\saildoclabelled{sailoverloadAzz8operatorz0zKz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzz8operatorz0zkz93747e4d4a6f99eb3fca0b477d2437ed5.tex}}}} ++\newcommand{\sailoverloadIzEightoperatorzZerozKzNine}{\saildoclabelled{sailoverloadIzz8operatorz0zKz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadIzz8operatorz0zkz93747e4d4a6f99eb3fca0b477d2437ed5.tex}}}} + + \newcommand{\sailvalId}{\saildoclabelled{sailzzyzyid}{\saildocval{}{\lstinputlisting[language=sail]{out/valz__ided888b8991a27578d5dd72f84db80bce.tex}}}} + + \newcommand{\sailfnId}{\saildoclabelled{sailfnzzyzyid}{\saildocfn{}{\lstinputlisting[language=sail]{out/fnz__ided888b8991a27578d5dd72f84db80bce.tex}}}} + +-\newcommand{\sailoverloadASizze}{\saildoclabelled{sailoverloadAzzyzysizze}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAz__sizze5b2e36a5dbb42eaba80b4d164e45d3ae.tex}}}} ++\newcommand{\sailoverloadJSizze}{\saildoclabelled{sailoverloadJzzyzysizze}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadJz__sizze5b2e36a5dbb42eaba80b4d164e45d3ae.tex}}}} + + \newcommand{\sailvalDeref}{\saildoclabelled{sailzzyzyderef}{\saildocval{}{\lstinputlisting[language=sail]{out/valz__deref1dbc379e24bd1b182e1db755dea8c453.tex}}}} + +@@ -95,21 +71,19 @@ + + \newcommand{\sailvaleqBits}{\saildoclabelled{sailzeqzybits}{\saildocval{}{\lstinputlisting[language=sail]{out/valzeq_bits886ce7cf3ec93a28308e8d4e9d63f4be.tex}}}} + +-\newcommand{\sailoverloadBzEightoperatorzZerozJzJzNine}{\saildoclabelled{sailoverloadBzz8operatorz0zJzJz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadBzz8operatorz0zjzjz9c650f45e06411dd4e97578ff2bad6338.tex}}}} ++\newcommand{\sailoverloadKzEightoperatorzZerozJzJzNine}{\saildoclabelled{sailoverloadKzz8operatorz0zJzJz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadKzz8operatorz0zjzjz9c650f45e06411dd4e97578ff2bad6338.tex}}}} + + \newcommand{\sailvalneqBits}{\saildoclabelled{sailzneqzybits}{\saildocval{}{\lstinputlisting[language=sail]{out/valzneq_bits167748c906c068e62596c88540a84f42.tex}}}} + + \newcommand{\sailfnneqBits}{\saildoclabelled{sailfnzneqzybits}{\saildocfn{}{\lstinputlisting[language=sail]{out/fnzneq_bits167748c906c068e62596c88540a84f42.tex}}}} + +-\newcommand{\sailoverloadBzEightoperatorzZerozOnezJzNine}{\saildoclabelled{sailoverloadBzz8operatorz0z1zJz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadBzz8operatorz0z1zjz981ebe433e26f9e2dfa2a9d2c7f4fe1f4.tex}}}} ++\newcommand{\sailoverloadLzEightoperatorzZerozOnezJzNine}{\saildoclabelled{sailoverloadLzz8operatorz0z1zJz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadLzz8operatorz0z1zjz981ebe433e26f9e2dfa2a9d2c7f4fe1f4.tex}}}} + + \newcommand{\sailvalbitvectorLength}{\saildoclabelled{sailzbitvectorzylength}{\saildocval{}{\lstinputlisting[language=sail]{out/valzbitvector_lengthcd74a5cced7567d19500671e4b6e1031.tex}}}} + + \newcommand{\sailvalvectorLength}{\saildoclabelled{sailzvectorzylength}{\saildocval{}{\lstinputlisting[language=sail]{out/valzvector_length9ee541b308cdfd9738d44bfb3dff4b46.tex}}}} + +-\newcommand{\sailvalvectorInit}{\saildoclabelled{sailzvectorzyinit}{\saildocval{}{\lstinputlisting[language=sail]{out/valzvector_inita510fd0ead8056bd52754fbb56c09b98.tex}}}} +- +-\newcommand{\sailoverloadAlength}{\saildoclabelled{sailoverloadAzlength}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzlength469e3f917f7b24f4691faf3caf842eba.tex}}}} ++\newcommand{\sailoverloadMlength}{\saildoclabelled{sailoverloadMzlength}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadMzlength469e3f917f7b24f4691faf3caf842eba.tex}}}} + + \newcommand{\sailvalcountLeadingZeros}{\saildoclabelled{sailzcountzyleadingzyzzeros}{\saildocval{}{\lstinputlisting[language=sail]{out/valzcount_leading_zzeros315ae28f559df1d42a7d2ca4cfff2905.tex}}}} + +@@ -121,11 +95,11 @@ + + \newcommand{\sailvalsailZeroExtend}{\saildoclabelled{sailzsailzyzzerozyextend}{\saildocval{}{\lstinputlisting[language=sail]{out/valzsail_zzero_extend411875c18d3b332113845d17151890c2.tex}}}} + +-\newcommand{\sailvaltruncate}{\saildoclabelled{sailztruncate}{\saildocval{\lstinline{sail_zero_extend}\lstinline`(v, n)` truncates \lstinline`v`, keeping only the \emph{least} significant \lstinline`n` bits. ++\newcommand{\sailvaltruncate}{\saildoclabelled{sailztruncate}{\saildocval{\lstinline{truncate}\lstinline`(v, n)` truncates \lstinline`v`, keeping only the \emph{least} significant \lstinline`n` bits. + + }{\lstinputlisting[language=sail]{out/valztruncatea666e28ae0c8ca7327a2b3fcd1ed4ec7.tex}}}} + +-\newcommand{\sailvaltruncateLSB}{\saildoclabelled{sailztruncateLSB}{\saildocval{\lstinline{truncate}\lstinline`(v, n)` truncates \lstinline`v`, keeping only the \emph{most} significant \lstinline`n` bits. ++\newcommand{\sailvaltruncateLSB}{\saildoclabelled{sailztruncateLSB}{\saildocval{\lstinline{truncateLSB}\lstinline`(v, n)` truncates \lstinline`v`, keeping only the \emph{most} significant \lstinline`n` bits. + + }{\lstinputlisting[language=sail]{out/valztruncatelsb4d124c6ec672453343dc0b20d295e82d.tex}}}} + +@@ -133,11 +107,11 @@ + + \newcommand{\sailfnsailMask}{\saildoclabelled{sailfnzsailzymask}{\saildocfn{}{\lstinputlisting[language=sail]{out/fnzsail_maske146b73afc824e90813dd8234bfa3053.tex}}}} + +-\newcommand{\sailoverloadAzEightoperatorzZerozQzNine}{\saildoclabelled{sailoverloadAzz8operatorz0zQz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzz8operatorz0zqz9ccbd65071d8f0fbb9677c7f6e86d3527.tex}}}} ++\newcommand{\sailoverloadNzEightoperatorzZerozQzNine}{\saildoclabelled{sailoverloadNzz8operatorz0zQz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadNzz8operatorz0zqz9ccbd65071d8f0fbb9677c7f6e86d3527.tex}}}} + + \newcommand{\sailvalbitvectorConcat}{\saildoclabelled{sailzbitvectorzyconcat}{\saildocval{}{\lstinputlisting[language=sail]{out/valzbitvector_concat6176f8be1468d8779ee8370fd3b4a6e0.tex}}}} + +-\newcommand{\sailoverloadAappend}{\saildoclabelled{sailoverloadAzappend}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzappend88575169e0ec1639b6ae3851df999710.tex}}}} ++\newcommand{\sailoverloadOappend}{\saildoclabelled{sailoverloadOzappend}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadOzappend88575169e0ec1639b6ae3851df999710.tex}}}} + + \newcommand{\sailvalappendSixFour}{\saildoclabelled{sailzappendzy64}{\saildocval{}{\lstinputlisting[language=sail]{out/valzappend_6433ef192058d4bf5f092d6f8b6d97f4c4.tex}}}} + +@@ -145,19 +119,19 @@ + + \newcommand{\sailvalplainVectorAccess}{\saildoclabelled{sailzplainzyvectorzyaccess}{\saildocval{}{\lstinputlisting[language=sail]{out/valzplain_vector_access792547dd734d4ff2e6078cbb88967469.tex}}}} + +-\newcommand{\sailoverloadAvectorAccess}{\saildoclabelled{sailoverloadAzvectorzyaccess}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzvector_accessbe81ec250d2df2ebadde393ea37a85a4.tex}}}} ++\newcommand{\sailoverloadPvectorAccess}{\saildoclabelled{sailoverloadPzvectorzyaccess}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadPzvector_accessbe81ec250d2df2ebadde393ea37a85a4.tex}}}} + + \newcommand{\sailvalbitvectorUpdate}{\saildoclabelled{sailzbitvectorzyupdate}{\saildocval{}{\lstinputlisting[language=sail]{out/valzbitvector_update20826799a1ff3ff40895206db0df14bb.tex}}}} + + \newcommand{\sailvalplainVectorUpdate}{\saildoclabelled{sailzplainzyvectorzyupdate}{\saildocval{}{\lstinputlisting[language=sail]{out/valzplain_vector_updateb31d67bfe51b1a6f79983347dfc57da0.tex}}}} + +-\newcommand{\sailoverloadAvectorUpdate}{\saildoclabelled{sailoverloadAzvectorzyupdate}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzvector_updateb14d5207ae01ed7fc9d9882c9cc3ebef.tex}}}} ++\newcommand{\sailoverloadQvectorUpdate}{\saildoclabelled{sailoverloadQzvectorzyupdate}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadQzvector_updateb14d5207ae01ed7fc9d9882c9cc3ebef.tex}}}} + + \newcommand{\sailvaladdBits}{\saildoclabelled{sailzaddzybits}{\saildocval{}{\lstinputlisting[language=sail]{out/valzadd_bits24373ffc11f289d5bb648df2f4f41b25.tex}}}} + + \newcommand{\sailvaladdBitsInt}{\saildoclabelled{sailzaddzybitszyint}{\saildocval{}{\lstinputlisting[language=sail]{out/valzadd_bits_inta5424052402522ff4653275c899f7543.tex}}}} + +-\newcommand{\sailoverloadAzEightoperatorzZerozBzNine}{\saildoclabelled{sailoverloadAzz8operatorz0zBz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzz8operatorz0zbz9a2d0168f574b152e5f31357e86602c16.tex}}}} ++\newcommand{\sailoverloadRzEightoperatorzZerozBzNine}{\saildoclabelled{sailoverloadRzz8operatorz0zBz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadRzz8operatorz0zbz9a2d0168f574b152e5f31357e86602c16.tex}}}} + + \newcommand{\sailvalsubBits}{\saildoclabelled{sailzsubzybits}{\saildocval{}{\lstinputlisting[language=sail]{out/valzsub_bitsf0dc4fc3429d45517c523db21af72127.tex}}}} + +@@ -165,21 +139,21 @@ + + \newcommand{\sailvalandVec}{\saildoclabelled{sailzandzyvec}{\saildocval{}{\lstinputlisting[language=sail]{out/valzand_vec99be3fe45d23194b597520c9e407ad35.tex}}}} + +-\newcommand{\sailoverloadBzEightoperatorzZerozSixzNine}{\saildoclabelled{sailoverloadBzz8operatorz0z6z9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadBzz8operatorz0z6z9d3731bb9b1c9d765858778ad48ba6b3a.tex}}}} ++\newcommand{\sailoverloadSzEightoperatorzZerozSixzNine}{\saildoclabelled{sailoverloadSzz8operatorz0z6z9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadSzz8operatorz0z6z9d3731bb9b1c9d765858778ad48ba6b3a.tex}}}} + + \newcommand{\sailvalorVec}{\saildoclabelled{sailzorzyvec}{\saildocval{}{\lstinputlisting[language=sail]{out/valzor_vec467c7a3f74be27085fe1b2aa3651ffe7.tex}}}} + +-\newcommand{\sailoverloadBzEightoperatorzZerozUzNine}{\saildoclabelled{sailoverloadBzz8operatorz0zUz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadBzz8operatorz0zuz99af95b281314726fa91893b57fc290dc.tex}}}} ++\newcommand{\sailoverloadTzEightoperatorzZerozUzNine}{\saildoclabelled{sailoverloadTzz8operatorz0zUz9}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadTzz8operatorz0zuz99af95b281314726fa91893b57fc290dc.tex}}}} + + \newcommand{\sailvalxorVec}{\saildoclabelled{sailzxorzyvec}{\saildocval{}{\lstinputlisting[language=sail]{out/valzxor_vecdacd54acc32f073fb01d1c188177bc8c.tex}}}} + + \newcommand{\sailvalsubrangeBits}{\saildoclabelled{sailzsubrangezybits}{\saildocval{}{\lstinputlisting[language=sail]{out/valzsubrange_bits6c497c14df4f4754bd345a6c56ca2aad.tex}}}} + +-\newcommand{\sailoverloadAvectorSubrange}{\saildoclabelled{sailoverloadAzvectorzysubrange}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzvector_subrange270c799ffa6c20b5244f22c64fba0367.tex}}}} ++\newcommand{\sailoverloadUvectorSubrange}{\saildoclabelled{sailoverloadUzvectorzysubrange}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadUzvector_subrange270c799ffa6c20b5244f22c64fba0367.tex}}}} + + \newcommand{\sailvalupdateSubrangeBits}{\saildoclabelled{sailzupdatezysubrangezybits}{\saildocval{}{\lstinputlisting[language=sail]{out/valzupdate_subrange_bitsb5ffe862b26310b45a779cd45bbf041e.tex}}}} + +-\newcommand{\sailoverloadAvectorUpdateSubrange}{\saildoclabelled{sailoverloadAzvectorzyupdatezysubrange}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadAzvector_update_subrangeb77be803268d55f5f112399f9d0dfbc2.tex}}}} ++\newcommand{\sailoverloadVvectorUpdateSubrange}{\saildoclabelled{sailoverloadVzvectorzyupdatezysubrange}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadVzvector_update_subrangeb77be803268d55f5f112399f9d0dfbc2.tex}}}} + + \newcommand{\sailvalsailShiftleft}{\saildoclabelled{sailzsailzyshiftleft}{\saildocval{}{\lstinputlisting[language=sail]{out/valzsail_shiftlefta7bc10407d10355c4e981688c9926084.tex}}}} + +@@ -215,22 +189,13 @@ + + }{\lstinputlisting[language=sail]{out/valzsigned36d2317f34f1dacb4e465e6e56b185e6.tex}}}} + +-\newcommand{\sailoverloadBSizze}{\saildoclabelled{sailoverloadBzzyzysizze}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadBz__sizze5b2e36a5dbb42eaba80b4d164e45d3ae.tex}}}} ++\newcommand{\sailoverloadWSizze}{\saildoclabelled{sailoverloadWzzyzysizze}{\saildocoverload{}{\lstinputlisting[language=sail]{out/overloadWz__sizze5b2e36a5dbb42eaba80b4d164e45d3ae.tex}}}} + + \newcommand{\sailtypecapUpermsWidth}{\saildoclabelled{sailtypezcapzyupermszywidth}{\saildoctype{}{\lstinputlisting[language=sail]{out/typezcap_uperms_widthf6dfed0942499b0c2d58b90971faca40.tex}}}} + + \newcommand{\sailletcapUpermsWidth}{\saildoclabelled{sailletzcapzyupermszywidth}{\saildoclet{}{\lstinputlisting[language=sail]{out/letzcap_uperms_widthf6dfed0942499b0c2d58b90971faca40.tex}}}} + +-\newcommand{\sailvalmain}{\saildoclabelled{sailzmain}{\saildocval{\begin{itemize} +-\item Ref to \hyperref[sailzcapzyupermszywidth]{\lstinline{cap_uperms_width}} +-\item Ref to \hyperref[sailzcapzyupermszywidth]{description} +-\item Ref to \hyperref[sailztypez0capzyupermszywidth]{type description} +-\item Ref to % FIXME: this should be using type\_description \hyperref[sailztypezycapzyupermszywidth]{type_description} +-\item Ref to \sailreftype{cap\_uperms\_width}{uperms\_width} +-\item Ref to \sailreftype{cap\_uperms\_width}{uperms\_width} +- +-\end{itemize} +-}{\lstinputlisting[language=sail]{out/valzmaine3ee21bf8f1dbb3fd716a5a1803d7e24.tex}}}} ++\newcommand{\sailvalmain}{\saildoclabelled{sailzmain}{\saildocval{}{\lstinputlisting[language=sail]{out/valzmaine3ee21bf8f1dbb3fd716a5a1803d7e24.tex}}}} + + \newcommand{\sailfnmain}{\saildoclabelled{sailfnzmain}{\saildocfn{\begin{itemize} + \item Ref to \hyperref[sailzcapzyupermszywidth]{\lstinline{cap_uperms_width}} +@@ -239,20 +204,10 @@ + \item Ref to % FIXME: this should be using type\_description \hyperref[sailztypezycapzyupermszywidth]{type_description} + \item Ref to \sailreftype{cap\_uperms\_width}{uperms\_width} + \item Ref to \sailreftype{cap\_uperms\_width}{uperms\_width} +- + \end{itemize} + }{\lstinputlisting[language=sail]{out/fnzmaine3ee21bf8f1dbb3fd716a5a1803d7e24.tex}}}} + +-\newcommand{\sailvalfunctionWithUnderscores}{\saildoclabelled{sailzfunctionzywithzyunderscores}{\saildocval{\begin{itemize} +-\item \hyperref[sailzmain]{\lstinline{main}} +-\item \hyperref[sailzmain]{\lstinline{main}} +-\item \hyperref[sailzNOTz0main]{main} +-\item \hyperref[sailzNOTz0\lstinline{main}]{\lstinline{main}} +-\item \hyperref[sailzmain]{NOT main} +-\item \hyperref[sailzmain]{NOT \lstinline{main}} +- +-\end{itemize} +-}{\lstinputlisting[language=sail]{out/valzfunction_with_underscores6e195bff96b3fe3d60b356f28519989f.tex}}}} ++\newcommand{\sailvalfunctionWithUnderscores}{\saildoclabelled{sailzfunctionzywithzyunderscores}{\saildocval{}{\lstinputlisting[language=sail]{out/valzfunction_with_underscores6e195bff96b3fe3d60b356f28519989f.tex}}}} + + \newcommand{\sailfnfunctionWithUnderscores}{\saildoclabelled{sailfnzfunctionzywithzyunderscores}{\saildocfn{\begin{itemize} + \item \hyperref[sailzfunction\_with\_underscores]{\lstinline{function\_with\_underscores}} +@@ -261,14 +216,9 @@ + \item \hyperref[sailzNOTz0\lstinline{function_with_underscores}]{\lstinline{function_with_underscores}} + \item \hyperref[sailzfunction\_with\_underscores]{NOT function\_with\_underscores} + \item \hyperref[sailzfunctionzywithzyunderscores]{NOT \lstinline{function_with_underscores}} +- + \end{itemize} + }{\lstinputlisting[language=sail]{out/fnzfunction_with_underscores6e195bff96b3fe3d60b356f28519989f.tex}}}} + +-\newcommand{\sailvalinitializzeRegisters}{\saildoclabelled{sailzinitializzezyregisters}{\saildocval{}{\lstinputlisting[language=sail]{out/valzinitializze_registerscd0d92787ce5f32f7391468692054f16.tex}}}} +- +-\newcommand{\sailfninitializzeRegisters}{\saildoclabelled{sailfnzinitializzezyregisters}{\saildocfn{}{\lstinputlisting[language=sail]{out/fnzinitializze_registerscd0d92787ce5f32f7391468692054f16.tex}}}} +- + \newcommand{\sailval}[1]{ + \ifstrequal{#1}{__deref}{\sailvalDeref}{}% + \ifstrequal{#1}{\_\_deref}{\sailvalDeref}{}% +@@ -314,10 +264,6 @@ + \ifstrequal{#1}{gt\_int}{\sailvalgtInt}{}% + \ifstrequal{#1}{gteq_int}{\sailvalgteqInt}{}% + \ifstrequal{#1}{gteq\_int}{\sailvalgteqInt}{}% +- \ifstrequal{#1}{initialize_registers}{\sailvalinitializzeRegisters}{}% +- \ifstrequal{#1}{initialize\_registers}{\sailvalinitializzeRegisters}{}% +- \ifstrequal{#1}{internal_pick}{\sailvalinternalPick}{}% +- \ifstrequal{#1}{internal\_pick}{\sailvalinternalPick}{}% + \ifstrequal{#1}{lt_int}{\sailvalltInt}{}% + \ifstrequal{#1}{lt\_int}{\sailvalltInt}{}% + \ifstrequal{#1}{lteq_int}{\sailvallteqInt}{}% +@@ -377,33 +323,9 @@ + \ifstrequal{#1}{subrange\_bits}{\sailvalsubrangeBits}{}% + \ifstrequal{#1}{truncate}{\sailvaltruncate}{}% + \ifstrequal{#1}{truncateLSB}{\sailvaltruncateLSB}{}% +- \ifstrequal{#1}{undefined_bit}{\sailvalundefinedBit}{}% +- \ifstrequal{#1}{undefined\_bit}{\sailvalundefinedBit}{}% +- \ifstrequal{#1}{undefined_bitvector}{\sailvalundefinedBitvector}{}% +- \ifstrequal{#1}{undefined\_bitvector}{\sailvalundefinedBitvector}{}% +- \ifstrequal{#1}{undefined_bool}{\sailvalundefinedBool}{}% +- \ifstrequal{#1}{undefined\_bool}{\sailvalundefinedBool}{}% +- \ifstrequal{#1}{undefined_int}{\sailvalundefinedInt}{}% +- \ifstrequal{#1}{undefined\_int}{\sailvalundefinedInt}{}% +- \ifstrequal{#1}{undefined_list}{\sailvalundefinedList}{}% +- \ifstrequal{#1}{undefined\_list}{\sailvalundefinedList}{}% +- \ifstrequal{#1}{undefined_nat}{\sailvalundefinedNat}{}% +- \ifstrequal{#1}{undefined\_nat}{\sailvalundefinedNat}{}% +- \ifstrequal{#1}{undefined_range}{\sailvalundefinedRange}{}% +- \ifstrequal{#1}{undefined\_range}{\sailvalundefinedRange}{}% +- \ifstrequal{#1}{undefined_real}{\sailvalundefinedReal}{}% +- \ifstrequal{#1}{undefined\_real}{\sailvalundefinedReal}{}% +- \ifstrequal{#1}{undefined_string}{\sailvalundefinedString}{}% +- \ifstrequal{#1}{undefined\_string}{\sailvalundefinedString}{}% +- \ifstrequal{#1}{undefined_unit}{\sailvalundefinedUnit}{}% +- \ifstrequal{#1}{undefined\_unit}{\sailvalundefinedUnit}{}% +- \ifstrequal{#1}{undefined_vector}{\sailvalundefinedVector}{}% +- \ifstrequal{#1}{undefined\_vector}{\sailvalundefinedVector}{}% + \ifstrequal{#1}{unsigned}{\sailvalunsigned}{}% + \ifstrequal{#1}{update_subrange_bits}{\sailvalupdateSubrangeBits}{}% + \ifstrequal{#1}{update\_subrange\_bits}{\sailvalupdateSubrangeBits}{}% +- \ifstrequal{#1}{vector_init}{\sailvalvectorInit}{}% +- \ifstrequal{#1}{vector\_init}{\sailvalvectorInit}{}% + \ifstrequal{#1}{vector_length}{\sailvalvectorLength}{}% + \ifstrequal{#1}{vector\_length}{\sailvalvectorLength}{}% + \ifstrequal{#1}{xor_vec}{\sailvalxorVec}{}% +@@ -454,10 +376,6 @@ + \ifstrequal{#1}{gt\_int}{\hyperref[sailzgtzyint]{#2}}{}% + \ifstrequal{#1}{gteq_int}{\hyperref[sailzgteqzyint]{#2}}{}% + \ifstrequal{#1}{gteq\_int}{\hyperref[sailzgteqzyint]{#2}}{}% +- \ifstrequal{#1}{initialize_registers}{\hyperref[sailzinitializzezyregisters]{#2}}{}% +- \ifstrequal{#1}{initialize\_registers}{\hyperref[sailzinitializzezyregisters]{#2}}{}% +- \ifstrequal{#1}{internal_pick}{\hyperref[sailzinternalzypick]{#2}}{}% +- \ifstrequal{#1}{internal\_pick}{\hyperref[sailzinternalzypick]{#2}}{}% + \ifstrequal{#1}{lt_int}{\hyperref[sailzltzyint]{#2}}{}% + \ifstrequal{#1}{lt\_int}{\hyperref[sailzltzyint]{#2}}{}% + \ifstrequal{#1}{lteq_int}{\hyperref[sailzlteqzyint]{#2}}{}% +@@ -517,33 +435,9 @@ + \ifstrequal{#1}{subrange\_bits}{\hyperref[sailzsubrangezybits]{#2}}{}% + \ifstrequal{#1}{truncate}{\hyperref[sailztruncate]{#2}}{}% + \ifstrequal{#1}{truncateLSB}{\hyperref[sailztruncateLSB]{#2}}{}% +- \ifstrequal{#1}{undefined_bit}{\hyperref[sailzundefinedzybit]{#2}}{}% +- \ifstrequal{#1}{undefined\_bit}{\hyperref[sailzundefinedzybit]{#2}}{}% +- \ifstrequal{#1}{undefined_bitvector}{\hyperref[sailzundefinedzybitvector]{#2}}{}% +- \ifstrequal{#1}{undefined\_bitvector}{\hyperref[sailzundefinedzybitvector]{#2}}{}% +- \ifstrequal{#1}{undefined_bool}{\hyperref[sailzundefinedzybool]{#2}}{}% +- \ifstrequal{#1}{undefined\_bool}{\hyperref[sailzundefinedzybool]{#2}}{}% +- \ifstrequal{#1}{undefined_int}{\hyperref[sailzundefinedzyint]{#2}}{}% +- \ifstrequal{#1}{undefined\_int}{\hyperref[sailzundefinedzyint]{#2}}{}% +- \ifstrequal{#1}{undefined_list}{\hyperref[sailzundefinedzylist]{#2}}{}% +- \ifstrequal{#1}{undefined\_list}{\hyperref[sailzundefinedzylist]{#2}}{}% +- \ifstrequal{#1}{undefined_nat}{\hyperref[sailzundefinedzynat]{#2}}{}% +- \ifstrequal{#1}{undefined\_nat}{\hyperref[sailzundefinedzynat]{#2}}{}% +- \ifstrequal{#1}{undefined_range}{\hyperref[sailzundefinedzyrange]{#2}}{}% +- \ifstrequal{#1}{undefined\_range}{\hyperref[sailzundefinedzyrange]{#2}}{}% +- \ifstrequal{#1}{undefined_real}{\hyperref[sailzundefinedzyreal]{#2}}{}% +- \ifstrequal{#1}{undefined\_real}{\hyperref[sailzundefinedzyreal]{#2}}{}% +- \ifstrequal{#1}{undefined_string}{\hyperref[sailzundefinedzystring]{#2}}{}% +- \ifstrequal{#1}{undefined\_string}{\hyperref[sailzundefinedzystring]{#2}}{}% +- \ifstrequal{#1}{undefined_unit}{\hyperref[sailzundefinedzyunit]{#2}}{}% +- \ifstrequal{#1}{undefined\_unit}{\hyperref[sailzundefinedzyunit]{#2}}{}% +- \ifstrequal{#1}{undefined_vector}{\hyperref[sailzundefinedzyvector]{#2}}{}% +- \ifstrequal{#1}{undefined\_vector}{\hyperref[sailzundefinedzyvector]{#2}}{}% + \ifstrequal{#1}{unsigned}{\hyperref[sailzunsigned]{#2}}{}% + \ifstrequal{#1}{update_subrange_bits}{\hyperref[sailzupdatezysubrangezybits]{#2}}{}% + \ifstrequal{#1}{update\_subrange\_bits}{\hyperref[sailzupdatezysubrangezybits]{#2}}{}% +- \ifstrequal{#1}{vector_init}{\hyperref[sailzvectorzyinit]{#2}}{}% +- \ifstrequal{#1}{vector\_init}{\hyperref[sailzvectorzyinit]{#2}}{}% + \ifstrequal{#1}{vector_length}{\hyperref[sailzvectorzylength]{#2}}{}% + \ifstrequal{#1}{vector\_length}{\hyperref[sailzvectorzylength]{#2}}{}% + \ifstrequal{#1}{xor_vec}{\hyperref[sailzxorzyvec]{#2}}{}% +@@ -556,8 +450,6 @@ + \ifstrequal{#1}{eq\_unit}{\sailfneqUnit}{}% + \ifstrequal{#1}{function_with_underscores}{\sailfnfunctionWithUnderscores}{}% + \ifstrequal{#1}{function\_with\_underscores}{\sailfnfunctionWithUnderscores}{}% +- \ifstrequal{#1}{initialize_registers}{\sailfninitializzeRegisters}{}% +- \ifstrequal{#1}{initialize\_registers}{\sailfninitializzeRegisters}{}% + \ifstrequal{#1}{main}{\sailfnmain}{}% + \ifstrequal{#1}{neq_bits}{\sailfnneqBits}{}% + \ifstrequal{#1}{neq\_bits}{\sailfnneqBits}{}% +@@ -579,8 +471,6 @@ + \ifstrequal{#1}{eq\_unit}{\hyperref[sailfnzeqzyunit]{#2}}{}% + \ifstrequal{#1}{function_with_underscores}{\hyperref[sailfnzfunctionzywithzyunderscores]{#2}}{}% + \ifstrequal{#1}{function\_with\_underscores}{\hyperref[sailfnzfunctionzywithzyunderscores]{#2}}{}% +- \ifstrequal{#1}{initialize_registers}{\hyperref[sailfnzinitializzezyregisters]{#2}}{}% +- \ifstrequal{#1}{initialize\_registers}{\hyperref[sailfnzinitializzezyregisters]{#2}}{}% + \ifstrequal{#1}{main}{\hyperref[sailfnzmain]{#2}}{}% + \ifstrequal{#1}{neq_bits}{\hyperref[sailfnzneqzybits]{#2}}{}% + \ifstrequal{#1}{neq\_bits}{\hyperref[sailfnzneqzybits]{#2}}{}% +Generating LaTeX for reference-type.sail: output is different +Building LaTeX for reference-type.sail: latexmk not installed +Files /tmp/tmp.TVbNa7qJdt/out/commands.tex and reg.commands.tex.exp differ +--- /tmp/tmp.TVbNa7qJdt/out/commands.tex 2024-07-29 15:49:32.427277970 +0800 ++++ reg.commands.tex.exp 2024-07-26 09:11:18.863870876 +0800 +@@ -9,101 +9,21 @@ + \providecommand\saildoclet[2]{#1 #2} + \providecommand\saildocregister[2]{#1 #2} + +-\newcommand{\sailvalinternalPick}{\saildoclabelled{sailzinternalzypick}{\saildocval{}{\lstinputlisting[language=sail]{out/valzinternal_pick0eb5adfbcccbb1785fa494f00459100d.tex}}}} +- +-\newcommand{\sailvalundefinedBool}{\saildoclabelled{sailzundefinedzybool}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_bool243ac67bbc90a729a829b61aebdfb100.tex}}}} +- +-\newcommand{\sailvalundefinedBit}{\saildoclabelled{sailzundefinedzybit}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_bitda1641f2d65bcfe8a6543bdf76182545.tex}}}} +- +-\newcommand{\sailvalundefinedInt}{\saildoclabelled{sailzundefinedzyint}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_intd4ae6556082aadeaaedb4f74f01376ce.tex}}}} +- +-\newcommand{\sailvalundefinedNat}{\saildoclabelled{sailzundefinedzynat}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_natd1f1df7de8df3f2d01791e80cbd35531.tex}}}} +- +-\newcommand{\sailvalundefinedReal}{\saildoclabelled{sailzundefinedzyreal}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_realc5ec14397a5a0720672cdd9ba3506589.tex}}}} +- +-\newcommand{\sailvalundefinedString}{\saildoclabelled{sailzundefinedzystring}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_stringe5c8a6af28b8ac03b9fd048eaa331eb8.tex}}}} +- +-\newcommand{\sailvalundefinedList}{\saildoclabelled{sailzundefinedzylist}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_list642d622904a8c0888aa4e72a844c6812.tex}}}} +- +-\newcommand{\sailvalundefinedRange}{\saildoclabelled{sailzundefinedzyrange}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_range78fb4a60a699f8333068f57d526860fa.tex}}}} +- +-\newcommand{\sailvalundefinedVector}{\saildoclabelled{sailzundefinedzyvector}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_vector7dcc506a79e97a89a0d66bc54b515466.tex}}}} +- +-\newcommand{\sailvalundefinedBitvector}{\saildoclabelled{sailzundefinedzybitvector}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_bitvectorc0153f961b53b1b17bf36adcf5409590.tex}}}} +- +-\newcommand{\sailvalundefinedUnit}{\saildoclabelled{sailzundefinedzyunit}{\saildocval{}{\lstinputlisting[language=sail]{out/valzundefined_unitd751910db26c6cf7ec5d02a503ad4f9e.tex}}}} +- + \newcommand{\sailregistersmall}{\saildoclabelled{sailregisterzsmall}{\saildocregister{}{\lstinputlisting[language=sail]{out/registerzsmall1f2dadee7c54a6dda75948109cacc9d5.tex}}}} + + \newcommand{\sailregisterbig}{\saildoclabelled{sailregisterzbig}{\saildocregister{}{\lstinputlisting[language=sail]{out/registerzbig1066534ae1b23930893efa3da0ce3b60.tex}}}} + +-\newcommand{\sailvalinitializzeRegisters}{\saildoclabelled{sailzinitializzezyregisters}{\saildocval{}{\lstinputlisting[language=sail]{out/valzinitializze_registerscd0d92787ce5f32f7391468692054f16.tex}}}} +- +-\newcommand{\sailfninitializzeRegisters}{\saildoclabelled{sailfnzinitializzezyregisters}{\saildocfn{}{\lstinputlisting[language=sail]{out/fnzinitializze_registerscd0d92787ce5f32f7391468692054f16.tex}}}} +- + \newcommand{\sailval}[1]{ +- \ifstrequal{#1}{initialize_registers}{\sailvalinitializzeRegisters}{}% +- \ifstrequal{#1}{initialize\_registers}{\sailvalinitializzeRegisters}{}% +- \ifstrequal{#1}{internal_pick}{\sailvalinternalPick}{}% +- \ifstrequal{#1}{internal\_pick}{\sailvalinternalPick}{}% +- \ifstrequal{#1}{undefined_bit}{\sailvalundefinedBit}{}% +- \ifstrequal{#1}{undefined\_bit}{\sailvalundefinedBit}{}% +- \ifstrequal{#1}{undefined_bitvector}{\sailvalundefinedBitvector}{}% +- \ifstrequal{#1}{undefined\_bitvector}{\sailvalundefinedBitvector}{}% +- \ifstrequal{#1}{undefined_bool}{\sailvalundefinedBool}{}% +- \ifstrequal{#1}{undefined\_bool}{\sailvalundefinedBool}{}% +- \ifstrequal{#1}{undefined_int}{\sailvalundefinedInt}{}% +- \ifstrequal{#1}{undefined\_int}{\sailvalundefinedInt}{}% +- \ifstrequal{#1}{undefined_list}{\sailvalundefinedList}{}% +- \ifstrequal{#1}{undefined\_list}{\sailvalundefinedList}{}% +- \ifstrequal{#1}{undefined_nat}{\sailvalundefinedNat}{}% +- \ifstrequal{#1}{undefined\_nat}{\sailvalundefinedNat}{}% +- \ifstrequal{#1}{undefined_range}{\sailvalundefinedRange}{}% +- \ifstrequal{#1}{undefined\_range}{\sailvalundefinedRange}{}% +- \ifstrequal{#1}{undefined_real}{\sailvalundefinedReal}{}% +- \ifstrequal{#1}{undefined\_real}{\sailvalundefinedReal}{}% +- \ifstrequal{#1}{undefined_string}{\sailvalundefinedString}{}% +- \ifstrequal{#1}{undefined\_string}{\sailvalundefinedString}{}% +- \ifstrequal{#1}{undefined_unit}{\sailvalundefinedUnit}{}% +- \ifstrequal{#1}{undefined\_unit}{\sailvalundefinedUnit}{}% +- \ifstrequal{#1}{undefined_vector}{\sailvalundefinedVector}{}% +- \ifstrequal{#1}{undefined\_vector}{\sailvalundefinedVector}{}} ++ } + + \newcommand{\sailrefval}[2]{ +- \ifstrequal{#1}{initialize_registers}{\hyperref[sailzinitializzezyregisters]{#2}}{}% +- \ifstrequal{#1}{initialize\_registers}{\hyperref[sailzinitializzezyregisters]{#2}}{}% +- \ifstrequal{#1}{internal_pick}{\hyperref[sailzinternalzypick]{#2}}{}% +- \ifstrequal{#1}{internal\_pick}{\hyperref[sailzinternalzypick]{#2}}{}% +- \ifstrequal{#1}{undefined_bit}{\hyperref[sailzundefinedzybit]{#2}}{}% +- \ifstrequal{#1}{undefined\_bit}{\hyperref[sailzundefinedzybit]{#2}}{}% +- \ifstrequal{#1}{undefined_bitvector}{\hyperref[sailzundefinedzybitvector]{#2}}{}% +- \ifstrequal{#1}{undefined\_bitvector}{\hyperref[sailzundefinedzybitvector]{#2}}{}% +- \ifstrequal{#1}{undefined_bool}{\hyperref[sailzundefinedzybool]{#2}}{}% +- \ifstrequal{#1}{undefined\_bool}{\hyperref[sailzundefinedzybool]{#2}}{}% +- \ifstrequal{#1}{undefined_int}{\hyperref[sailzundefinedzyint]{#2}}{}% +- \ifstrequal{#1}{undefined\_int}{\hyperref[sailzundefinedzyint]{#2}}{}% +- \ifstrequal{#1}{undefined_list}{\hyperref[sailzundefinedzylist]{#2}}{}% +- \ifstrequal{#1}{undefined\_list}{\hyperref[sailzundefinedzylist]{#2}}{}% +- \ifstrequal{#1}{undefined_nat}{\hyperref[sailzundefinedzynat]{#2}}{}% +- \ifstrequal{#1}{undefined\_nat}{\hyperref[sailzundefinedzynat]{#2}}{}% +- \ifstrequal{#1}{undefined_range}{\hyperref[sailzundefinedzyrange]{#2}}{}% +- \ifstrequal{#1}{undefined\_range}{\hyperref[sailzundefinedzyrange]{#2}}{}% +- \ifstrequal{#1}{undefined_real}{\hyperref[sailzundefinedzyreal]{#2}}{}% +- \ifstrequal{#1}{undefined\_real}{\hyperref[sailzundefinedzyreal]{#2}}{}% +- \ifstrequal{#1}{undefined_string}{\hyperref[sailzundefinedzystring]{#2}}{}% +- \ifstrequal{#1}{undefined\_string}{\hyperref[sailzundefinedzystring]{#2}}{}% +- \ifstrequal{#1}{undefined_unit}{\hyperref[sailzundefinedzyunit]{#2}}{}% +- \ifstrequal{#1}{undefined\_unit}{\hyperref[sailzundefinedzyunit]{#2}}{}% +- \ifstrequal{#1}{undefined_vector}{\hyperref[sailzundefinedzyvector]{#2}}{}% +- \ifstrequal{#1}{undefined\_vector}{\hyperref[sailzundefinedzyvector]{#2}}{}} ++ } + + \newcommand{\sailfn}[1]{ +- \ifstrequal{#1}{initialize_registers}{\sailfninitializzeRegisters}{}% +- \ifstrequal{#1}{initialize\_registers}{\sailfninitializzeRegisters}{}} ++ } + + \newcommand{\sailreffn}[2]{ +- \ifstrequal{#1}{initialize_registers}{\hyperref[sailfnzinitializzezyregisters]{#2}}{}% +- \ifstrequal{#1}{initialize\_registers}{\hyperref[sailfnzinitializzezyregisters]{#2}}{}} ++ } + + \newcommand{\sailtype}[1]{ + } +Generating LaTeX for reg.sail: output is different +Building LaTeX for reg.sail: latexmk not installed +LaTeX testing: Passed 1 out of 10 + + +========================================== +C tests +========================================== +Sail is /home/trdthg/repo/sail/sail +Sail dir is /home/trdthg/repo/sail +--------------------------------------------------------------------- +Testing unoptimized C with C options: Sail options: valgrind: False +--------------------------------------------------------------------- +fallthrough_exception.sail ............. ok +list_let.sail .......................... ok +fail_assert_mono_bug.sail .............. ok +and_block.sail ......................... ok +empty_list.sail ........................ ok +list_rec_functions2.sail ............... ok +issue136.sail .......................... ok +primop.sail ............................ ok +real.sail .............................. ok +reg_init_let.sail ...................... ok +anf_block.sail ......................... ok +pc_no_wildcard.sail .................... ok +gvector.sail ........................... ok +vector_subrange_pattern.sail ........... ok +read_write_ram.sail .................... ok +implicits.sail ......................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c lib_hex_bits.sail 1> lib_hex_bits.c +stdout: + +stderr: +Fatal error: exception Not_found + +get_slice_int.sail ..................... ok +foreach_none.sail ...................... ok +issue37.sail ........................... ok +vmatch.sail ............................ ok +toplevel_tyvar.sail .................... ok +nexp_simp_euclidian.sail ............... ok +int64_vector_literal.sail .............. ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c poly_mapping2.sail 1> poly_mapping2.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 409): +poly_mapping2.sail:17.47-67: +17 |mapping test1m : bits(3) <-> bits(5) = { v <-> zero_int_bits(2) @ v } +  | ^------------------^ +  | Invalid bitvector pattern +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize.bvc.(fun) in file "src/lib/pattern_completeness.ml", line 409, characters 27-86 +  | Called from Stdlib__List.fold_left2 in file "list.ml", line 161, characters 37-51 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 559, characters 54-93 +  | Called from Stdlib__List.map2 in file "list.ml", line 134, characters 15-22 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 555, characters 16-1023 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete in file "src/lib/pattern_completeness.ml", line 552, characters 10-1023 +  | Called from Libsail__Pattern_completeness.Make.is_complete_matrixs.(fun) in file "src/lib/pattern_completeness.ml", line 987, characters 16-47 +  | Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +Failed: /home/trdthg/repo/sail/sail -no_warn -c rv_format.sail 1> rv_format.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +rv_format.sail:32.79-108: +32 | 0b0 @ opcode : bits(4) @ rd : regidx @ r1 : regidx @ r2 : regidx <-> AType(struct { opcode, rd, r1, r2 }), +  | ^---------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1059, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 96, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1059, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +enum_tup_match.sail .................... ok +either.sail ............................ ok +unconstructed_type_mono.sail ........... ok +single_arg.sail ........................ ok +struct_fn_arg.sail ..................... ok +split.sail ............................. ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c rv_format2.sail 1> rv_format2.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +rv_format2.sail:32.79-108: +32 | 0b0 @ opcode : bits(4) @ rd : regidx @ r1 : regidx @ r2 : regidx <-> AType(struct { opcode, rd, r1, r2 }), +  | ^---------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1059, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 96, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1059, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +nested_fields.sail ..................... ok +bitvector_update.sail .................. ok +list_mut.sail .......................... ok +varswap.sail ........................... ok +unused_poly_ctor.sail .................. ok +anf_as_pattern.sail .................... ok +custom_flow.sail ....................... ok +list_test.sail ......................... ok +tuple_conversion.sail .................. ok +int_struct.sail ........................ ok +set_struct2.sail ....................... ok +xlen32.sail ............................ ok +bool_bits_mapping.sail ................. ok +fail_exception.sail .................... ok +small_slice.sail ....................... ok +for_shadow.sail ........................ ok +prelude.sail ........................... ok +special_annot.sail ..................... ok +poly_union_rev.sail .................... ok +xlen_val.sail .......................... ok +rv_duopod_bug.sail ..................... ok +fast_signed.sail ....................... ok +cheri128_hsb.sail ...................... ok +return_leak.sail ....................... ok +list_scope.sail ........................ ok +undefined_nat.sail ..................... ok +issue401.sail .......................... ok +pattern_concat_nest.sail ............... ok +tl_let.sail ............................ ok +real_prop.sail ......................... ok +cheri_capreg.sail ...................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c issue232_2.sail 1> issue232_2.c +stdout: + +stderr: +Fatal error: exception Not_found + +gvectorlit.sail ........................ ok +either_rvbug.sail ...................... ok +config_register.sail ................... ok +simple_bitmanip.sail ................... ok +struct_mapping.sail .................... ok +enum_functions.sail .................... ok +two_mapping.sail ....................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c lib_valid_hex_bits.sail 1> lib_valid_hex_bits.c +stdout: + +stderr: +Fatal error: exception Not_found + +undefined_union.sail ................... ok +anon_rec.sail .......................... ok +nonexistent_pragma.sail ................ ok +list_cons_cons.sail .................... ok +bitvector_update2.sail ................. ok +large_bitvector.sail ................... ok +type_if_bits.sail ...................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c zeros_mapping.sail 1> zeros_mapping.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 409): +zeros_mapping.sail:17.50-87: +17 |mapping clause encdec = Add(dest, src1, src2) <-> zeros_16() @ dest @ src1 @ src2 @ 0b1 +  | ^-----------------------------------^ +  | Invalid bitvector pattern +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize.bvc.(fun) in file "src/lib/pattern_completeness.ml", line 409, characters 27-86 +  | Called from Stdlib__List.fold_left2 in file "list.ml", line 161, characters 37-51 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 559, characters 54-93 +  | Called from Stdlib__List.map2 in file "list.ml", line 134, characters 15-22 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 555, characters 16-1023 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete in file "src/lib/pattern_completeness.ml", line 552, characters 10-1023 +  | Called from Libsail__Pattern_completeness.Make.is_complete_matrixs.(fun) in file "src/lib/pattern_completeness.ml", line 987, characters 16-47 +  | Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +tuple_union.sail ....................... ok +shadow_cleanup.sail .................... ok +pointer_assign.sail .................... ok +tuple_fun.sail ......................... ok +spc_mappings.sail ...................... ok +flow_restrict.sail ..................... ok +constructor247.sail .................... ok +reg_ref.sail ........................... ok +set_struct.sail ........................ ok +enum_map.sail .......................... ok +rv_memop.sail .......................... ok +global_let_shadow.sail ................. ok +fvector_update.sail .................... ok +if_opt_typ.sail ........................ ok +poly_mapping.sail ...................... ok +issue362.sail .......................... ok +cheri_capstruct_order.sail ............. ok +fail_issue203.sail ..................... ok +try_return.sail ........................ ok +double_option.sail ..................... ok +let_option_shadow.sail ................. ok +let_option.sail ........................ ok +dead_branch.sail ....................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c mapping_compose.sail 1> mapping_compose.c +stdout: + +stderr: +Fatal error: exception Not_found + +enum_match.sail ........................ ok +eq_struct.sail ......................... ok +tl_pat.sail ............................ ok +string_literal_type.sail ............... ok +extend_simple.sail ..................... ok +poly_int_record.sail ................... ok +downcast_fn.sail ....................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c lib_hex_bits_signed.sail 1> lib_hex_bits_signed.c +stdout: + +stderr: +Fatal error: exception Not_found + +assign_rename_bug.sail ................. ok +string_of_bits.sail .................... ok +poly_outcome.sail ...................... ok +return_register_ref.sail ............... ok +list_rec_functions1.sail ............... ok +overload_mapping.sail .................. ok +reg_32_64.sail ......................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c issue243_fixed.sail 1> issue243_fixed.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +issue243_fixed.sail:17.22-49: +17 |mapping f_bits = { FE(struct { e1 = e1, v1 = v1 }) <-> e_pair_bits(e1,EB) @ v1 } +  | ^-------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1053, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 93, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1053, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +poly_pair.sail ......................... ok +hello_world.sail ....................... ok +mapping.sail ........................... ok +match_bind.sail ........................ ok +pr194.sail ............................. ok +list_torture.sail ...................... ok +all_even_vector_length.sail ............ ok +list_scope2.sail ....................... ok +infix_include.sail ..................... ok +stack_struct.sail ...................... ok +struct_pattern.sail .................... ok +issue429.sail .......................... ok +nexp_synonym.sail ...................... ok +shadow_let.sail ........................ ok +inc_tests.sail ......................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c issue232.sail 1> issue232.c +stdout: + +stderr: +Fatal error: exception Not_found + +short_circuit.sail ..................... ok +single_guard.sail ...................... ok +reg_ref_nb.sail ........................ ok +warl.sail .............................. ok +exn_hello_world.sail ................... ok +zero_length_bv.sail .................... ok +encdec_subrange.sail ................... ok +poly_tup.sail .......................... ok +warl2.sail ............................. ok +struct.sail ............................ ok +scattered_mapping.sail ................. ok +pow2.sail .............................. ok +nested_mapping.sail .................... ok +new_bitfields.sail ..................... ok +vector_example.sail .................... ok +config.sail ............................ ok +poly_union.sail ........................ ok +non_unique.sail ........................ ok +poly_record.sail ....................... ok +int_struct_constrained.sail ............ ok +string_take.sail ....................... ok +letbind.sail ........................... ok +concurrency_interface.sail ............. ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c encdec.sail 1> encdec.c +stdout: + +stderr: +Fatal error: exception Not_found + +bitvector.sail ......................... ok +tl_poly_match.sail ..................... ok +option.sail ............................ ok +struct_pattern_partial.sail ............ ok +option_nest.sail ....................... ok +list_scope3.sail ....................... ok +cfold_reg.sail ......................... ok +poly_simple.sail ....................... ok +bv_literal.sail ........................ ok +option_option.sail ..................... ok +issue202_1.sail ........................ ok +vector_init.sail ....................... ok +string_of_bits2.sail ................... ok +outcome_impl.sail ...................... ok +loop_exception.sail .................... ok +164 passes and 12 failures +-------------------------------------------------------------------------------------------- +Testing unoptimized C with C++ compiler with C options: -xc++ Sail options: valgrind: False +-------------------------------------------------------------------------------------------- +fallthrough_exception.sail ............. ok +empty_list.sail ........................ ok +list_let.sail .......................... ok +and_block.sail ......................... ok +primop.sail ............................ ok +fail_assert_mono_bug.sail .............. ok +list_rec_functions2.sail ............... ok +issue136.sail .......................... ok +anf_block.sail ......................... ok +pc_no_wildcard.sail .................... ok +vector_subrange_pattern.sail ........... ok +implicits.sail ......................... ok +real.sail .............................. ok +reg_init_let.sail ...................... ok +gvector.sail ........................... ok +read_write_ram.sail .................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c lib_hex_bits.sail 1> lib_hex_bits.c +stdout: + +stderr: +Fatal error: exception Not_found + +issue37.sail ........................... ok +foreach_none.sail ...................... ok +vmatch.sail ............................ ok +get_slice_int.sail ..................... ok +nexp_simp_euclidian.sail ............... ok +toplevel_tyvar.sail .................... ok +int64_vector_literal.sail .............. ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c poly_mapping2.sail 1> poly_mapping2.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 409): +poly_mapping2.sail:17.47-67: +17 |mapping test1m : bits(3) <-> bits(5) = { v <-> zero_int_bits(2) @ v } +  | ^------------------^ +  | Invalid bitvector pattern +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize.bvc.(fun) in file "src/lib/pattern_completeness.ml", line 409, characters 27-86 +  | Called from Stdlib__List.fold_left2 in file "list.ml", line 161, characters 37-51 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 559, characters 54-93 +  | Called from Stdlib__List.map2 in file "list.ml", line 134, characters 15-22 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 555, characters 16-1023 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete in file "src/lib/pattern_completeness.ml", line 552, characters 10-1023 +  | Called from Libsail__Pattern_completeness.Make.is_complete_matrixs.(fun) in file "src/lib/pattern_completeness.ml", line 987, characters 16-47 +  | Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +Failed: /home/trdthg/repo/sail/sail -no_warn -c rv_format.sail 1> rv_format.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +rv_format.sail:32.79-108: +32 | 0b0 @ opcode : bits(4) @ rd : regidx @ r1 : regidx @ r2 : regidx <-> AType(struct { opcode, rd, r1, r2 }), +  | ^---------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1059, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 96, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1059, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +either.sail ............................ ok +enum_tup_match.sail .................... ok +single_arg.sail ........................ ok +unconstructed_type_mono.sail ........... ok +struct_fn_arg.sail ..................... ok +split.sail ............................. ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c rv_format2.sail 1> rv_format2.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +rv_format2.sail:32.79-108: +32 | 0b0 @ opcode : bits(4) @ rd : regidx @ r1 : regidx @ r2 : regidx <-> AType(struct { opcode, rd, r1, r2 }), +  | ^---------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1059, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 96, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1059, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +unused_poly_ctor.sail .................. ok +custom_flow.sail ....................... ok +bitvector_update.sail .................. ok +nested_fields.sail ..................... ok +varswap.sail ........................... ok +anf_as_pattern.sail .................... ok +list_mut.sail .......................... ok +tuple_conversion.sail .................. ok +list_test.sail ......................... ok +set_struct2.sail ....................... ok +small_slice.sail ....................... ok +bool_bits_mapping.sail ................. ok +int_struct.sail ........................ ok +xlen32.sail ............................ ok +fail_exception.sail .................... ok +prelude.sail ........................... ok +for_shadow.sail ........................ ok +cheri128_hsb.sail ...................... ok +poly_union_rev.sail .................... ok +special_annot.sail ..................... ok +xlen_val.sail .......................... ok +rv_duopod_bug.sail ..................... ok +fast_signed.sail ....................... ok +return_leak.sail ....................... ok +tl_let.sail ............................ ok +list_scope.sail ........................ ok +issue401.sail .......................... ok +cheri_capreg.sail ...................... ok +undefined_nat.sail ..................... ok +pattern_concat_nest.sail ............... ok +real_prop.sail ......................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c issue232_2.sail 1> issue232_2.c +stdout: + +stderr: +Fatal error: exception Not_found + +simple_bitmanip.sail ................... ok +config_register.sail ................... ok +gvectorlit.sail ........................ ok +either_rvbug.sail ...................... ok +struct_mapping.sail .................... ok +enum_functions.sail .................... ok +two_mapping.sail ....................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c lib_valid_hex_bits.sail 1> lib_valid_hex_bits.c +stdout: + +stderr: +Fatal error: exception Not_found + +undefined_union.sail ................... ok +list_cons_cons.sail .................... ok +type_if_bits.sail ...................... ok +anon_rec.sail .......................... ok +bitvector_update2.sail ................. ok +nonexistent_pragma.sail ................ ok +large_bitvector.sail ................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c zeros_mapping.sail 1> zeros_mapping.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 409): +zeros_mapping.sail:17.50-87: +17 |mapping clause encdec = Add(dest, src1, src2) <-> zeros_16() @ dest @ src1 @ src2 @ 0b1 +  | ^-----------------------------------^ +  | Invalid bitvector pattern +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize.bvc.(fun) in file "src/lib/pattern_completeness.ml", line 409, characters 27-86 +  | Called from Stdlib__List.fold_left2 in file "list.ml", line 161, characters 37-51 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 559, characters 54-93 +  | Called from Stdlib__List.map2 in file "list.ml", line 134, characters 15-22 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 555, characters 16-1023 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete in file "src/lib/pattern_completeness.ml", line 552, characters 10-1023 +  | Called from Libsail__Pattern_completeness.Make.is_complete_matrixs.(fun) in file "src/lib/pattern_completeness.ml", line 987, characters 16-47 +  | Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +tuple_fun.sail ......................... ok +pointer_assign.sail .................... ok +shadow_cleanup.sail .................... ok +tuple_union.sail ....................... ok +spc_mappings.sail ...................... ok +flow_restrict.sail ..................... ok +constructor247.sail .................... ok +fvector_update.sail .................... ok +if_opt_typ.sail ........................ ok +rv_memop.sail .......................... ok +enum_map.sail .......................... ok +reg_ref.sail ........................... ok +global_let_shadow.sail ................. ok +set_struct.sail ........................ ok +poly_mapping.sail ...................... ok +cheri_capstruct_order.sail ............. ok +issue362.sail .......................... ok +dead_branch.sail ....................... ok +double_option.sail ..................... ok +let_option.sail ........................ ok +try_return.sail ........................ ok +let_option_shadow.sail ................. ok +fail_issue203.sail ..................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c mapping_compose.sail 1> mapping_compose.c +stdout: + +stderr: +Fatal error: exception Not_found + +Failed: c++ -xc++ tl_pat.c /home/trdthg/repo/sail/lib/*.c -lgmp -lz -I /home/trdthg/repo/sail/lib -o tl_pat.bin +stdout: + +stderr: +tl_pat.c:58:31: error: ‘zX::::::zX’ has the same name as the class in which it is declared + 58 | union {struct { sail_string zX; };}; + | ^~ +tl_pat.c: In function ‘void create_zX(zX*)’: +tl_pat.c:63:28: error: invalid use of ‘zX::zX’ + 63 | CREATE(sail_string)(&op->zX); + | ^~ +tl_pat.c: In function ‘void kill_zX(zX*)’: +tl_pat.c:72:28: error: invalid use of ‘zX::zX’ + 72 | KILL(sail_string)(&op->zX); + | ^~ +tl_pat.c: In function ‘void copy_zX(zX*, zX)’: +tl_pat.c:78:29: error: invalid use of ‘zX::zX’ + 78 | KILL(sail_string)(&rop->zX); + | ^~ +tl_pat.c:82:31: error: invalid use of ‘zX::zX’ + 82 | CREATE(sail_string)(&rop->zX); COPY(sail_string)(&rop->zX, op.zX); + | ^~ +tl_pat.c:82:60: error: invalid use of ‘zX::zX’ + 82 | CREATE(sail_string)(&rop->zX); COPY(sail_string)(&rop->zX, op.zX); + | ^~ +tl_pat.c:82:67: error: invalid use of ‘zX::zX’ + 82 | CREATE(sail_string)(&rop->zX); COPY(sail_string)(&rop->zX, op.zX); + | ^~ +tl_pat.c: In function ‘bool eq_zX(zX, zX)’: +tl_pat.c:88:35: error: invalid use of ‘zX::zX’ + 88 | return EQUAL(sail_string)(op1.zX, op2.zX); + | ^~ +tl_pat.c:88:43: error: invalid use of ‘zX::zX’ + 88 | return EQUAL(sail_string)(op1.zX, op2.zX); + | ^~ +tl_pat.c: In function ‘void zX(zX*, const_sail_string)’: +tl_pat.c:94:29: error: invalid use of ‘zX::zX’ + 94 | KILL(sail_string)(&rop->zX); + | ^~ +tl_pat.c:97:29: error: invalid use of ‘zX::zX’ + 97 | CREATE(sail_string)(&rop->zX); + | ^~ +tl_pat.c:98:27: error: invalid use of ‘zX::zX’ + 98 | COPY(sail_string)(&rop->zX, op); + | ^~ +tl_pat.c: In function ‘void zf(char**, zX)’: +tl_pat.c:112:35: error: invalid use of ‘zX::zX’ + 112 | COPY(sail_string)(&zstr, zgsz30.zX); + | ^~ + +eq_struct.sail ......................... ok +downcast_fn.sail ....................... ok +enum_match.sail ........................ ok +string_literal_type.sail ............... ok +poly_int_record.sail ................... ok +extend_simple.sail ..................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c lib_hex_bits_signed.sail 1> lib_hex_bits_signed.c +stdout: + +stderr: +Fatal error: exception Not_found + +return_register_ref.sail ............... ok +poly_outcome.sail ...................... ok +string_of_bits.sail .................... ok +assign_rename_bug.sail ................. ok +overload_mapping.sail .................. ok +list_rec_functions1.sail ............... ok +reg_32_64.sail ......................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c issue243_fixed.sail 1> issue243_fixed.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +issue243_fixed.sail:17.22-49: +17 |mapping f_bits = { FE(struct { e1 = e1, v1 = v1 }) <-> e_pair_bits(e1,EB) @ v1 } +  | ^-------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1053, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 93, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1053, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +pr194.sail ............................. ok +hello_world.sail ....................... ok +poly_pair.sail ......................... ok +match_bind.sail ........................ ok +mapping.sail ........................... ok +all_even_vector_length.sail ............ ok +list_torture.sail ...................... ok +stack_struct.sail ...................... ok +nexp_synonym.sail ...................... ok +list_scope2.sail ....................... ok +infix_include.sail ..................... ok +struct_pattern.sail .................... ok +shadow_let.sail ........................ ok +issue429.sail .......................... ok +inc_tests.sail ......................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c issue232.sail 1> issue232.c +stdout: + +stderr: +Fatal error: exception Not_found + +short_circuit.sail ..................... ok +exn_hello_world.sail ................... ok +single_guard.sail ...................... ok +reg_ref_nb.sail ........................ ok +warl.sail .............................. ok +zero_length_bv.sail .................... ok +encdec_subrange.sail ................... ok +poly_tup.sail .......................... ok +struct.sail ............................ ok +warl2.sail ............................. ok +scattered_mapping.sail ................. ok +pow2.sail .............................. ok +new_bitfields.sail ..................... ok +nested_mapping.sail .................... ok +vector_example.sail .................... ok +poly_record.sail ....................... ok +config.sail ............................ ok +poly_union.sail ........................ ok +non_unique.sail ........................ ok +string_take.sail ....................... ok +int_struct_constrained.sail ............ ok +letbind.sail ........................... ok +concurrency_interface.sail ............. ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c encdec.sail 1> encdec.c +stdout: + +stderr: +Fatal error: exception Not_found + +list_scope3.sail ....................... ok +bitvector.sail ......................... ok +option_nest.sail ....................... ok +struct_pattern_partial.sail ............ ok +tl_poly_match.sail ..................... ok +option.sail ............................ ok +cfold_reg.sail ......................... ok +bv_literal.sail ........................ ok +string_of_bits2.sail ................... ok +poly_simple.sail ....................... ok +option_option.sail ..................... ok +issue202_1.sail ........................ ok +vector_init.sail ....................... ok +outcome_impl.sail ...................... ok +loop_exception.sail .................... ok +163 passes and 12 failures (1 expected failures) +----------------------------------------------------------------------- +Testing optimized C with C options: -O2 Sail options: -O valgrind: True +----------------------------------------------------------------------- +skipping because no valgrind found +0 passes and 0 failures +----------------------------------------------------------------------------------------------- +Testing optimized C with C++ compiler with C options: -xc++ -O2 Sail options: -O valgrind: True +----------------------------------------------------------------------------------------------- +skipping because no valgrind found +0 passes and 0 failures +--------------------------------------------------------------------------------------- +Testing constant folding with C options: Sail options: -Oconstant_fold valgrind: False +--------------------------------------------------------------------------------------- +empty_list.sail ........................ ok +list_let.sail .......................... ok +and_block.sail ......................... ok +fallthrough_exception.sail ............. ok +fail_assert_mono_bug.sail .............. ok +list_rec_functions2.sail ............... ok +primop.sail ............................ ok +issue136.sail .......................... ok +anf_block.sail ......................... ok +real.sail .............................. ok +vector_subrange_pattern.sail ........... ok +reg_init_let.sail ...................... ok +pc_no_wildcard.sail .................... ok +read_write_ram.sail .................... ok +implicits.sail ......................... ok +gvector.sail ........................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -Oconstant_fold lib_hex_bits.sail 1> lib_hex_bits.c +stdout: + +stderr: +Fatal error: exception Not_found + +vmatch.sail ............................ ok +issue37.sail ........................... ok +foreach_none.sail ...................... ok +get_slice_int.sail ..................... ok +toplevel_tyvar.sail .................... ok +nexp_simp_euclidian.sail ............... ok +int64_vector_literal.sail .............. ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -Oconstant_fold poly_mapping2.sail 1> poly_mapping2.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 409): +poly_mapping2.sail:17.47-67: +17 |mapping test1m : bits(3) <-> bits(5) = { v <-> zero_int_bits(2) @ v } +  | ^------------------^ +  | Invalid bitvector pattern +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize.bvc.(fun) in file "src/lib/pattern_completeness.ml", line 409, characters 27-86 +  | Called from Stdlib__List.fold_left2 in file "list.ml", line 161, characters 37-51 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 559, characters 54-93 +  | Called from Stdlib__List.map2 in file "list.ml", line 134, characters 15-22 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 555, characters 16-1023 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete in file "src/lib/pattern_completeness.ml", line 552, characters 10-1023 +  | Called from Libsail__Pattern_completeness.Make.is_complete_matrixs.(fun) in file "src/lib/pattern_completeness.ml", line 987, characters 16-47 +  | Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +Failed: /home/trdthg/repo/sail/sail -no_warn -c -Oconstant_fold rv_format.sail 1> rv_format.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +rv_format.sail:32.79-108: +32 | 0b0 @ opcode : bits(4) @ rd : regidx @ r1 : regidx @ r2 : regidx <-> AType(struct { opcode, rd, r1, r2 }), +  | ^---------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1059, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 96, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1059, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +unconstructed_type_mono.sail ........... ok +enum_tup_match.sail .................... ok +either.sail ............................ ok +single_arg.sail ........................ ok +split.sail ............................. ok +struct_fn_arg.sail ..................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -Oconstant_fold rv_format2.sail 1> rv_format2.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +rv_format2.sail:32.79-108: +32 | 0b0 @ opcode : bits(4) @ rd : regidx @ r1 : regidx @ r2 : regidx <-> AType(struct { opcode, rd, r1, r2 }), +  | ^---------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1059, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 96, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1059, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +varswap.sail ........................... ok +list_mut.sail .......................... ok +unused_poly_ctor.sail .................. ok +anf_as_pattern.sail .................... ok +bitvector_update.sail .................. ok +nested_fields.sail ..................... ok +custom_flow.sail ....................... ok +tuple_conversion.sail .................. ok +int_struct.sail ........................ ok +list_test.sail ......................... ok +bool_bits_mapping.sail ................. ok +set_struct2.sail ....................... ok +xlen32.sail ............................ ok +fail_exception.sail .................... ok +small_slice.sail ....................... ok +rv_duopod_bug.sail ..................... ok +for_shadow.sail ........................ ok +poly_union_rev.sail .................... ok +xlen_val.sail .......................... ok +special_annot.sail ..................... ok +prelude.sail ........................... ok +fast_signed.sail ....................... ok +cheri128_hsb.sail ...................... ok +return_leak.sail ....................... ok +tl_let.sail ............................ ok +issue401.sail .......................... ok +list_scope.sail ........................ ok +undefined_nat.sail ..................... ok +pattern_concat_nest.sail ............... ok +real_prop.sail ......................... ok +cheri_capreg.sail ...................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -Oconstant_fold issue232_2.sail 1> issue232_2.c +stdout: + +stderr: +Fatal error: exception Not_found + +simple_bitmanip.sail ................... ok +config_register.sail ................... ok +gvectorlit.sail ........................ ok +either_rvbug.sail ...................... ok +struct_mapping.sail .................... ok +enum_functions.sail .................... ok +two_mapping.sail ....................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -Oconstant_fold lib_valid_hex_bits.sail 1> lib_valid_hex_bits.c +stdout: + +stderr: +Fatal error: exception Not_found + +nonexistent_pragma.sail ................ ok +bitvector_update2.sail ................. ok +list_cons_cons.sail .................... ok +undefined_union.sail ................... ok +anon_rec.sail .......................... ok +large_bitvector.sail ................... ok +type_if_bits.sail ...................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -Oconstant_fold zeros_mapping.sail 1> zeros_mapping.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 409): +zeros_mapping.sail:17.50-87: +17 |mapping clause encdec = Add(dest, src1, src2) <-> zeros_16() @ dest @ src1 @ src2 @ 0b1 +  | ^-----------------------------------^ +  | Invalid bitvector pattern +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize.bvc.(fun) in file "src/lib/pattern_completeness.ml", line 409, characters 27-86 +  | Called from Stdlib__List.fold_left2 in file "list.ml", line 161, characters 37-51 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 559, characters 54-93 +  | Called from Stdlib__List.map2 in file "list.ml", line 134, characters 15-22 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 555, characters 16-1023 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete in file "src/lib/pattern_completeness.ml", line 552, characters 10-1023 +  | Called from Libsail__Pattern_completeness.Make.is_complete_matrixs.(fun) in file "src/lib/pattern_completeness.ml", line 987, characters 16-47 +  | Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +pointer_assign.sail .................... ok +tuple_fun.sail ......................... ok +shadow_cleanup.sail .................... ok +spc_mappings.sail ...................... ok +tuple_union.sail ....................... ok +flow_restrict.sail ..................... ok +constructor247.sail .................... ok +rv_memop.sail .......................... ok +fvector_update.sail .................... ok +reg_ref.sail ........................... ok +global_let_shadow.sail ................. ok +enum_map.sail .......................... ok +set_struct.sail ........................ ok +if_opt_typ.sail ........................ ok +poly_mapping.sail ...................... ok +cheri_capstruct_order.sail ............. ok +try_return.sail ........................ ok +issue362.sail .......................... ok +let_option_shadow.sail ................. ok +fail_issue203.sail ..................... ok +double_option.sail ..................... ok +let_option.sail ........................ ok +dead_branch.sail ....................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -Oconstant_fold mapping_compose.sail 1> mapping_compose.c +stdout: + +stderr: +Fatal error: exception Not_found + +tl_pat.sail ............................ ok +eq_struct.sail ......................... ok +string_literal_type.sail ............... ok +downcast_fn.sail ....................... ok +enum_match.sail ........................ ok +extend_simple.sail ..................... ok +poly_int_record.sail ................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -Oconstant_fold lib_hex_bits_signed.sail 1> lib_hex_bits_signed.c +stdout: + +stderr: +Fatal error: exception Not_found + +string_of_bits.sail .................... ok +return_register_ref.sail ............... ok +assign_rename_bug.sail ................. ok +reg_32_64.sail ......................... ok +poly_outcome.sail ...................... ok +list_rec_functions1.sail ............... ok +overload_mapping.sail .................. ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -Oconstant_fold issue243_fixed.sail 1> issue243_fixed.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +issue243_fixed.sail:17.22-49: +17 |mapping f_bits = { FE(struct { e1 = e1, v1 = v1 }) <-> e_pair_bits(e1,EB) @ v1 } +  | ^-------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1053, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 93, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1053, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +poly_pair.sail ......................... ok +hello_world.sail ....................... ok +pr194.sail ............................. ok +match_bind.sail ........................ ok +all_even_vector_length.sail ............ ok +list_torture.sail ...................... ok +mapping.sail ........................... ok +nexp_synonym.sail ...................... ok +struct_pattern.sail .................... ok +stack_struct.sail ...................... ok +list_scope2.sail ....................... ok +infix_include.sail ..................... ok +shadow_let.sail ........................ ok +inc_tests.sail ......................... ok +issue429.sail .......................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -Oconstant_fold issue232.sail 1> issue232.c +stdout: + +stderr: +Fatal error: exception Not_found + +short_circuit.sail ..................... ok +exn_hello_world.sail ................... ok +reg_ref_nb.sail ........................ ok +zero_length_bv.sail .................... ok +single_guard.sail ...................... ok +warl.sail .............................. ok +encdec_subrange.sail ................... ok +poly_tup.sail .......................... ok +struct.sail ............................ ok +scattered_mapping.sail ................. ok +warl2.sail ............................. ok +new_bitfields.sail ..................... ok +nested_mapping.sail .................... ok +vector_example.sail .................... ok +pow2.sail .............................. ok +poly_record.sail ....................... ok +poly_union.sail ........................ ok +config.sail ............................ ok +non_unique.sail ........................ ok +string_take.sail ....................... ok +int_struct_constrained.sail ............ ok +concurrency_interface.sail ............. ok +letbind.sail ........................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -Oconstant_fold encdec.sail 1> encdec.c +stdout: + +stderr: +Fatal error: exception Not_found + +option_nest.sail ....................... ok +struct_pattern_partial.sail ............ ok +bitvector.sail ......................... ok +cfold_reg.sail ......................... ok +option.sail ............................ ok +list_scope3.sail ....................... ok +tl_poly_match.sail ..................... ok +bv_literal.sail ........................ ok +poly_simple.sail ....................... ok +issue202_1.sail ........................ ok +string_of_bits2.sail ................... ok +loop_exception.sail .................... ok +option_option.sail ..................... ok +vector_init.sail ....................... ok +outcome_impl.sail ...................... ok +164 passes and 12 failures +-------------------------------------------------------------------------------------------------------------- +Testing undefined behavior sanitised with C options: -O2 -fsanitize=undefined Sail options: -O valgrind: False +-------------------------------------------------------------------------------------------------------------- +and_block.sail ......................... ok +list_let.sail .......................... ok +fail_assert_mono_bug.sail .............. ok +fallthrough_exception.sail ............. ok +empty_list.sail ........................ ok +list_rec_functions2.sail ............... ok +issue136.sail .......................... ok +primop.sail ............................ ok +anf_block.sail ......................... ok +reg_init_let.sail ...................... ok +real.sail .............................. ok +pc_no_wildcard.sail .................... ok +vector_subrange_pattern.sail ........... ok +gvector.sail ........................... ok +implicits.sail ......................... ok +read_write_ram.sail .................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -O lib_hex_bits.sail 1> lib_hex_bits.c +stdout: + +stderr: +Fatal error: exception Not_found + +vmatch.sail ............................ ok +issue37.sail ........................... ok +foreach_none.sail ...................... ok +toplevel_tyvar.sail .................... ok +get_slice_int.sail ..................... ok +nexp_simp_euclidian.sail ............... ok +int64_vector_literal.sail .............. ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -O poly_mapping2.sail 1> poly_mapping2.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 409): +poly_mapping2.sail:17.47-67: +17 |mapping test1m : bits(3) <-> bits(5) = { v <-> zero_int_bits(2) @ v } +  | ^------------------^ +  | Invalid bitvector pattern +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize.bvc.(fun) in file "src/lib/pattern_completeness.ml", line 409, characters 27-86 +  | Called from Stdlib__List.fold_left2 in file "list.ml", line 161, characters 37-51 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 559, characters 54-93 +  | Called from Stdlib__List.map2 in file "list.ml", line 134, characters 15-22 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 555, characters 16-1023 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete in file "src/lib/pattern_completeness.ml", line 552, characters 10-1023 +  | Called from Libsail__Pattern_completeness.Make.is_complete_matrixs.(fun) in file "src/lib/pattern_completeness.ml", line 987, characters 16-47 +  | Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +Failed: /home/trdthg/repo/sail/sail -no_warn -c -O rv_format.sail 1> rv_format.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +rv_format.sail:32.79-108: +32 | 0b0 @ opcode : bits(4) @ rd : regidx @ r1 : regidx @ r2 : regidx <-> AType(struct { opcode, rd, r1, r2 }), +  | ^---------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1059, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 96, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1059, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +either.sail ............................ ok +unconstructed_type_mono.sail ........... ok +enum_tup_match.sail .................... ok +struct_fn_arg.sail ..................... ok +single_arg.sail ........................ ok +split.sail ............................. ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -O rv_format2.sail 1> rv_format2.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +rv_format2.sail:32.79-108: +32 | 0b0 @ opcode : bits(4) @ rd : regidx @ r1 : regidx @ r2 : regidx <-> AType(struct { opcode, rd, r1, r2 }), +  | ^---------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1059, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 96, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1059, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +custom_flow.sail ....................... ok +unused_poly_ctor.sail .................. ok +nested_fields.sail ..................... ok +list_mut.sail .......................... ok +bitvector_update.sail .................. ok +varswap.sail ........................... ok +anf_as_pattern.sail .................... ok +tuple_conversion.sail .................. ok +set_struct2.sail ....................... ok +int_struct.sail ........................ ok +bool_bits_mapping.sail ................. ok +list_test.sail ......................... ok +xlen32.sail ............................ ok +small_slice.sail ....................... ok +fail_exception.sail .................... ok +for_shadow.sail ........................ ok +poly_union_rev.sail .................... ok +xlen_val.sail .......................... ok +rv_duopod_bug.sail ..................... ok +special_annot.sail ..................... ok +prelude.sail ........................... ok +cheri128_hsb.sail ...................... ok +fast_signed.sail ....................... ok +return_leak.sail ....................... ok +tl_let.sail ............................ ok +list_scope.sail ........................ ok +undefined_nat.sail ..................... ok +issue401.sail .......................... ok +cheri_capreg.sail ...................... ok +real_prop.sail ......................... ok +pattern_concat_nest.sail ............... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -O issue232_2.sail 1> issue232_2.c +stdout: + +stderr: +Fatal error: exception Not_found + +either_rvbug.sail ...................... ok +gvectorlit.sail ........................ ok +struct_mapping.sail .................... ok +config_register.sail ................... ok +simple_bitmanip.sail ................... ok +enum_functions.sail .................... ok +two_mapping.sail ....................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -O lib_valid_hex_bits.sail 1> lib_valid_hex_bits.c +stdout: + +stderr: +Fatal error: exception Not_found + +bitvector_update2.sail ................. ok +anon_rec.sail .......................... ok +nonexistent_pragma.sail ................ ok +undefined_union.sail ................... ok +list_cons_cons.sail .................... ok +large_bitvector.sail ................... ok +type_if_bits.sail ...................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -O zeros_mapping.sail 1> zeros_mapping.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 409): +zeros_mapping.sail:17.50-87: +17 |mapping clause encdec = Add(dest, src1, src2) <-> zeros_16() @ dest @ src1 @ src2 @ 0b1 +  | ^-----------------------------------^ +  | Invalid bitvector pattern +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize.bvc.(fun) in file "src/lib/pattern_completeness.ml", line 409, characters 27-86 +  | Called from Stdlib__List.fold_left2 in file "list.ml", line 161, characters 37-51 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 559, characters 54-93 +  | Called from Stdlib__List.map2 in file "list.ml", line 134, characters 15-22 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 555, characters 16-1023 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete in file "src/lib/pattern_completeness.ml", line 552, characters 10-1023 +  | Called from Libsail__Pattern_completeness.Make.is_complete_matrixs.(fun) in file "src/lib/pattern_completeness.ml", line 987, characters 16-47 +  | Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +tuple_fun.sail ......................... ok +shadow_cleanup.sail .................... ok +pointer_assign.sail .................... ok +tuple_union.sail ....................... ok +flow_restrict.sail ..................... ok +spc_mappings.sail ...................... ok +constructor247.sail .................... ok +global_let_shadow.sail ................. ok +set_struct.sail ........................ ok +if_opt_typ.sail ........................ ok +reg_ref.sail ........................... ok +fvector_update.sail .................... ok +rv_memop.sail .......................... ok +enum_map.sail .......................... ok +poly_mapping.sail ...................... ok +fail_issue203.sail ..................... ok +dead_branch.sail ....................... ok +issue362.sail .......................... ok +cheri_capstruct_order.sail ............. ok +double_option.sail ..................... ok +let_option_shadow.sail ................. ok +let_option.sail ........................ ok +try_return.sail ........................ ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -O mapping_compose.sail 1> mapping_compose.c +stdout: + +stderr: +Fatal error: exception Not_found + +extend_simple.sail ..................... ok +enum_match.sail ........................ ok +string_literal_type.sail ............... ok +tl_pat.sail ............................ ok +eq_struct.sail ......................... ok +downcast_fn.sail ....................... ok +poly_int_record.sail ................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -O lib_hex_bits_signed.sail 1> lib_hex_bits_signed.c +stdout: + +stderr: +Fatal error: exception Not_found + +string_of_bits.sail .................... ok +return_register_ref.sail ............... ok +poly_outcome.sail ...................... ok +assign_rename_bug.sail ................. ok +overload_mapping.sail .................. ok +list_rec_functions1.sail ............... ok +reg_32_64.sail ......................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -O issue243_fixed.sail 1> issue243_fixed.c +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +issue243_fixed.sail:17.22-49: +17 |mapping f_bits = { FE(struct { e1 = e1, v1 = v1 }) <-> e_pair_bits(e1,EB) @ v1 } +  | ^-------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1053, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 93, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1053, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +match_bind.sail ........................ ok +pr194.sail ............................. ok +poly_pair.sail ......................... ok +hello_world.sail ....................... ok +mapping.sail ........................... ok +all_even_vector_length.sail ............ ok +list_torture.sail ...................... ok +struct_pattern.sail .................... ok +nexp_synonym.sail ...................... ok +stack_struct.sail ...................... ok +infix_include.sail ..................... ok +issue429.sail .......................... ok +shadow_let.sail ........................ ok +list_scope2.sail ....................... ok +inc_tests.sail ......................... ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -O issue232.sail 1> issue232.c +stdout: + +stderr: +Fatal error: exception Not_found + +exn_hello_world.sail ................... ok +single_guard.sail ...................... ok +short_circuit.sail ..................... ok +reg_ref_nb.sail ........................ ok +warl.sail .............................. ok +zero_length_bv.sail .................... ok +encdec_subrange.sail ................... ok +poly_tup.sail .......................... ok +struct.sail ............................ ok +warl2.sail ............................. ok +scattered_mapping.sail ................. ok +nested_mapping.sail .................... ok +pow2.sail .............................. ok +new_bitfields.sail ..................... ok +vector_example.sail .................... ok +non_unique.sail ........................ ok +int_struct_constrained.sail ............ ok +poly_union.sail ........................ ok +poly_record.sail ....................... ok +string_take.sail ....................... ok +config.sail ............................ ok +letbind.sail ........................... ok +concurrency_interface.sail ............. ok +Failed: /home/trdthg/repo/sail/sail -no_warn -c -O encdec.sail 1> encdec.c +stdout: + +stderr: +Fatal error: exception Not_found + +list_scope3.sail ....................... ok +option.sail ............................ ok +option_nest.sail ....................... ok +struct_pattern_partial.sail ............ ok +tl_poly_match.sail ..................... ok +bitvector.sail ......................... ok +cfold_reg.sail ......................... ok +option_option.sail ..................... ok +string_of_bits2.sail ................... ok +poly_simple.sail ....................... ok +bv_literal.sail ........................ ok +issue202_1.sail ........................ ok +vector_init.sail ....................... ok +outcome_impl.sail ...................... ok +loop_exception.sail .................... ok +164 passes and 12 failures +------------------- +Testing interpreter +------------------- +and_block.sail ......................... ok +fallthrough_exception.sail ............. ok +issue136.sail .......................... ok +primop.sail ............................ ok +list_let.sail .......................... ok +fail_assert_mono_bug.sail .............. ok +empty_list.sail ........................ ok +list_rec_functions2.sail ............... ok +anf_block.sail ......................... ok +real.sail .............................. ok +reg_init_let.sail ...................... ok +pc_no_wildcard.sail .................... ok +implicits.sail ......................... ok +vector_subrange_pattern.sail ........... ok +gvector.sail ........................... ok +read_write_ram.sail .................... ok +vmatch.sail ............................ ok +issue37.sail ........................... ok +Failed: /home/trdthg/repo/sail/sail -undefined_gen -is execute.isail -iout lib_hex_bits.iresult lib_hex_bits.sail +stdout: + +stderr: +Fatal error: exception Not_found + +toplevel_tyvar.sail .................... ok +foreach_none.sail ...................... ok +get_slice_int.sail ..................... ok +nexp_simp_euclidian.sail ............... ok +int64_vector_literal.sail .............. ok +Failed: /home/trdthg/repo/sail/sail -undefined_gen -is execute.isail -iout poly_mapping2.iresult poly_mapping2.sail +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 409): +poly_mapping2.sail:17.47-67: +17 |mapping test1m : bits(3) <-> bits(5) = { v <-> zero_int_bits(2) @ v } +  | ^------------------^ +  | Invalid bitvector pattern +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize.bvc.(fun) in file "src/lib/pattern_completeness.ml", line 409, characters 27-86 +  | Called from Stdlib__List.fold_left2 in file "list.ml", line 161, characters 37-51 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 559, characters 54-93 +  | Called from Stdlib__List.map2 in file "list.ml", line 134, characters 15-22 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 555, characters 16-1023 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete in file "src/lib/pattern_completeness.ml", line 552, characters 10-1023 +  | Called from Libsail__Pattern_completeness.Make.is_complete_matrixs.(fun) in file "src/lib/pattern_completeness.ml", line 987, characters 16-47 +  | Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +unconstructed_type_mono.sail ........... ok +either.sail ............................ ok +single_arg.sail ........................ ok +enum_tup_match.sail .................... ok +struct_fn_arg.sail ..................... ok +Failed: /home/trdthg/repo/sail/sail -undefined_gen -is execute.isail -iout rv_format.iresult rv_format.sail +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +rv_format.sail:32.79-108: +32 | 0b0 @ opcode : bits(4) @ rd : regidx @ r1 : regidx @ r2 : regidx <-> AType(struct { opcode, rd, r1, r2 }), +  | ^---------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1059, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 96, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1059, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +split.sail ............................. ok +bitvector_update.sail .................. ok +nested_fields.sail ..................... ok +unused_poly_ctor.sail .................. ok +varswap.sail ........................... ok +list_mut.sail .......................... ok +anf_as_pattern.sail .................... ok +Failed: /home/trdthg/repo/sail/sail -undefined_gen -is execute.isail -iout rv_format2.iresult rv_format2.sail +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +rv_format2.sail:32.79-108: +32 | 0b0 @ opcode : bits(4) @ rd : regidx @ r1 : regidx @ r2 : regidx <-> AType(struct { opcode, rd, r1, r2 }), +  | ^---------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1059, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 96, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1059, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +custom_flow.sail ....................... ok +tuple_conversion.sail .................. ok +list_test.sail ......................... ok +set_struct2.sail ....................... ok +int_struct.sail ........................ ok +bool_bits_mapping.sail ................. ok +xlen32.sail ............................ ok +fail_exception.sail .................... ok +small_slice.sail ....................... ok +special_annot.sail ..................... ok +poly_union_rev.sail .................... ok +prelude.sail ........................... ok +for_shadow.sail ........................ ok +xlen_val.sail .......................... ok +fast_signed.sail ....................... ok +rv_duopod_bug.sail ..................... ok +cheri128_hsb.sail ...................... ok +tl_let.sail ............................ ok +list_scope.sail ........................ ok +issue401.sail .......................... ok +return_leak.sail ....................... ok +undefined_nat.sail ..................... ok +pattern_concat_nest.sail ............... ok +cheri_capreg.sail ...................... ok +real_prop.sail ......................... ok +gvectorlit.sail ........................ ok +config_register.sail ................... ok +simple_bitmanip.sail ................... ok +either_rvbug.sail ...................... ok +Failed: /home/trdthg/repo/sail/sail -undefined_gen -is execute.isail -iout issue232_2.iresult issue232_2.sail +stdout: + +stderr: +Warning: Incomplete pattern match statement at issue232_2.sail:6.0-7: +6 |mapping e_pair_bits : (E,E) <-> bits(2) = +  |^-----^ +  | +The following expression is unmatched: (EB, EA) + +Fatal error: exception Not_found + +enum_functions.sail .................... ok +struct_mapping.sail .................... ok +two_mapping.sail ....................... ok +undefined_union.sail ................... ok +nonexistent_pragma.sail ................ ok +large_bitvector.sail ................... ok +anon_rec.sail .......................... ok +bitvector_update2.sail ................. ok +list_cons_cons.sail .................... ok +Failed: /home/trdthg/repo/sail/sail -undefined_gen -is execute.isail -iout lib_valid_hex_bits.iresult lib_valid_hex_bits.sail +stdout: + +stderr: +Fatal error: exception Not_found + +type_if_bits.sail ...................... ok +pointer_assign.sail .................... ok +tuple_fun.sail ......................... ok +shadow_cleanup.sail .................... ok +constructor247.sail .................... ok +Failed: /home/trdthg/repo/sail/sail -undefined_gen -is execute.isail -iout zeros_mapping.iresult zeros_mapping.sail +stdout: + +stderr: +Warning: Incomplete pattern match statement at zeros_mapping.sail:7.0-7: +7 |mapping zeros_16 : unit <-> bits(16) = { () <-> 0x0000 } +  |^-----^ +  | +The following expression is unmatched: 0xffff + +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 409): +zeros_mapping.sail:17.50-87: +17 |mapping clause encdec = Add(dest, src1, src2) <-> zeros_16() @ dest @ src1 @ src2 @ 0b1 +  | ^-----------------------------------^ +  | Invalid bitvector pattern +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize.bvc.(fun) in file "src/lib/pattern_completeness.ml", line 409, characters 27-86 +  | Called from Stdlib__List.fold_left2 in file "list.ml", line 161, characters 37-51 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 559, characters 54-93 +  | Called from Stdlib__List.map2 in file "list.ml", line 134, characters 15-22 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 555, characters 16-1023 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete in file "src/lib/pattern_completeness.ml", line 552, characters 10-1023 +  | Called from Libsail__Pattern_completeness.Make.is_complete_matrixs.(fun) in file "src/lib/pattern_completeness.ml", line 987, characters 16-47 +  | Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +flow_restrict.sail ..................... ok +spc_mappings.sail ...................... ok +tuple_union.sail ....................... ok +if_opt_typ.sail ........................ ok +global_let_shadow.sail ................. ok +rv_memop.sail .......................... ok +fvector_update.sail .................... ok +set_struct.sail ........................ ok +reg_ref.sail ........................... ok +poly_mapping.sail ...................... ok +enum_map.sail .......................... ok +cheri_capstruct_order.sail ............. ok +issue362.sail .......................... ok +double_option.sail ..................... ok +try_return.sail ........................ ok +fail_issue203.sail ..................... ok +let_option.sail ........................ ok +dead_branch.sail ....................... ok +let_option_shadow.sail ................. ok +tl_pat.sail ............................ ok +downcast_fn.sail ....................... ok +string_literal_type.sail ............... ok +eq_struct.sail ......................... ok +enum_match.sail ........................ ok +Failed: /home/trdthg/repo/sail/sail -undefined_gen -is execute.isail -iout mapping_compose.iresult mapping_compose.sail +stdout: + +stderr: +Fatal error: exception Not_found + +poly_int_record.sail ................... ok +extend_simple.sail ..................... ok +return_register_ref.sail ............... ok +poly_outcome.sail ...................... ok +string_of_bits.sail .................... ok +assign_rename_bug.sail ................. ok +Failed: /home/trdthg/repo/sail/sail -undefined_gen -is execute.isail -iout lib_hex_bits_signed.iresult lib_hex_bits_signed.sail +stdout: + +stderr: +Fatal error: exception Not_found + +reg_32_64.sail ......................... ok +overload_mapping.sail .................. ok +list_rec_functions1.sail ............... ok +poly_pair.sail ......................... ok +hello_world.sail ....................... ok +match_bind.sail ........................ ok +pr194.sail ............................. ok +all_even_vector_length.sail ............ ok +list_torture.sail ...................... ok +Failed: /home/trdthg/repo/sail/sail -undefined_gen -is execute.isail -iout issue243_fixed.iresult issue243_fixed.sail +stdout: + +stderr: +Warning: Incomplete pattern match statement at issue243_fixed.sail:6.0-7: +6 |mapping e_pair_bits : (E,E) <-> bits(2) = +  |^-----^ +  | +The following expression is unmatched: (EB, EA) + +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +issue243_fixed.sail:17.22-49: +17 |mapping f_bits = { FE(struct { e1 = e1, v1 = v1 }) <-> e_pair_bits(e1,EB) @ v1 } +  | ^-------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1053, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 93, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1053, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +mapping.sail ........................... ok +stack_struct.sail ...................... ok +infix_include.sail ..................... ok +shadow_let.sail ........................ ok +nexp_synonym.sail ...................... ok +list_scope2.sail ....................... ok +struct_pattern.sail .................... ok +inc_tests.sail ......................... ok +issue429.sail .......................... ok +reg_ref_nb.sail ........................ ok +single_guard.sail ...................... ok +short_circuit.sail ..................... ok +zero_length_bv.sail .................... ok +exn_hello_world.sail ................... ok +warl.sail .............................. ok +Failed: /home/trdthg/repo/sail/sail -undefined_gen -is execute.isail -iout issue232.iresult issue232.sail +stdout: + +stderr: +Warning: Incomplete pattern match statement at issue232.sail:6.0-7: +6 |mapping e_pair_bits : (E,E) <-> bits(2) = +  |^-----^ +  | +The following expression is unmatched: (EB, EA) + +Fatal error: exception Not_found + +encdec_subrange.sail ................... ok +struct.sail ............................ ok +poly_tup.sail .......................... ok +pow2.sail .............................. ok +nested_mapping.sail .................... ok +new_bitfields.sail ..................... ok +warl2.sail ............................. ok +scattered_mapping.sail ................. ok +vector_example.sail .................... ok +poly_record.sail ....................... ok +poly_union.sail ........................ ok +config.sail ............................ ok +non_unique.sail ........................ ok +string_take.sail ....................... ok +int_struct_constrained.sail ............ ok +letbind.sail ........................... ok +concurrency_interface.sail ............. ok +option_nest.sail ....................... ok +bitvector.sail ......................... ok +option.sail ............................ ok +cfold_reg.sail ......................... ok +tl_poly_match.sail ..................... ok +Failed: /home/trdthg/repo/sail/sail -undefined_gen -is execute.isail -iout encdec.iresult encdec.sail +stdout: + +stderr: +Warning: Deprecated encdec.sail:30.24-82: +30 |val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg} +  | ^--------------------------------------------------------^ +  | +Explicit effect annotations are deprecated. They are no longer used and can be removed. + +Warning: Incomplete pattern match statement at encdec.sail:11.0-7: +11 |mapping decenc_p : bits(2) <-> pred = { +  |^-----^ +  | +The following expression is unmatched: 0b10 + +Fatal error: exception Not_found + +struct_pattern_partial.sail ............ ok +list_scope3.sail ....................... ok +bv_literal.sail ........................ ok +poly_simple.sail ....................... ok +string_of_bits2.sail ................... ok +option_option.sail ..................... ok +outcome_impl.sail ...................... ok +issue202_1.sail ........................ ok +vector_init.sail ....................... ok +loop_exception.sail .................... ok +164 passes and 12 failures +------------- +Testing OCaml +------------- +and_block.sail ......................... ok +list_let.sail .......................... ok +fallthrough_exception.sail ............. ok +empty_list.sail ........................ ok +issue136.sail .......................... ok +primop.sail ............................ ok +fail_assert_mono_bug.sail .............. ok +list_rec_functions2.sail ............... ok +real.sail .............................. ok +anf_block.sail ......................... ok +reg_init_let.sail ...................... ok +read_write_ram.sail .................... ok +pc_no_wildcard.sail .................... ok +gvector.sail ........................... ok +vector_subrange_pattern.sail ........... ok +implicits.sail ......................... ok +Failed: /home/trdthg/repo/sail/sail -ocaml -ocaml_build_dir _sbuild_lib_hex_bits -o lib_hex_bits_ocaml lib_hex_bits.sail +stdout: + +stderr: +Fatal error: exception Not_found + +nexp_simp_euclidian.sail ............... ok +issue37.sail ........................... ok +foreach_none.sail ...................... ok +vmatch.sail ............................ ok +get_slice_int.sail ..................... ok +toplevel_tyvar.sail .................... ok +int64_vector_literal.sail .............. ok +Failed: /home/trdthg/repo/sail/sail -ocaml -ocaml_build_dir _sbuild_poly_mapping2 -o poly_mapping2_ocaml poly_mapping2.sail +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 409): +poly_mapping2.sail:17.47-67: +17 |mapping test1m : bits(3) <-> bits(5) = { v <-> zero_int_bits(2) @ v } +  | ^------------------^ +  | Invalid bitvector pattern +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize.bvc.(fun) in file "src/lib/pattern_completeness.ml", line 409, characters 27-86 +  | Called from Stdlib__List.fold_left2 in file "list.ml", line 161, characters 37-51 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 559, characters 54-93 +  | Called from Stdlib__List.map2 in file "list.ml", line 134, characters 15-22 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 555, characters 16-1023 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete in file "src/lib/pattern_completeness.ml", line 552, characters 10-1023 +  | Called from Libsail__Pattern_completeness.Make.is_complete_matrixs.(fun) in file "src/lib/pattern_completeness.ml", line 987, characters 16-47 +  | Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +Failed: /home/trdthg/repo/sail/sail -ocaml -ocaml_build_dir _sbuild_rv_format -o rv_format_ocaml rv_format.sail +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +rv_format.sail:32.79-108: +32 | 0b0 @ opcode : bits(4) @ rd : regidx @ r1 : regidx @ r2 : regidx <-> AType(struct { opcode, rd, r1, r2 }), +  | ^---------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1059, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 96, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1059, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +either.sail ............................ ok +unconstructed_type_mono.sail ........... ok +enum_tup_match.sail .................... ok +single_arg.sail ........................ ok +struct_fn_arg.sail ..................... ok +split.sail ............................. ok +Failed: /home/trdthg/repo/sail/sail -ocaml -ocaml_build_dir _sbuild_rv_format2 -o rv_format2_ocaml rv_format2.sail +stdout: + +stderr: +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +rv_format2.sail:32.79-108: +32 | 0b0 @ opcode : bits(4) @ rd : regidx @ r1 : regidx @ r2 : regidx <-> AType(struct { opcode, rd, r1, r2 }), +  | ^---------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1059, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 96, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1059, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +list_mut.sail .......................... ok +varswap.sail ........................... ok +custom_flow.sail ....................... ok +nested_fields.sail ..................... ok +bitvector_update.sail .................. ok +unused_poly_ctor.sail .................. ok +anf_as_pattern.sail .................... ok +tuple_conversion.sail .................. ok +list_test.sail ......................... ok +bool_bits_mapping.sail ................. ok +int_struct.sail ........................ ok +fail_exception.sail .................... ok +set_struct2.sail ....................... ok +small_slice.sail ....................... ok +xlen32.sail ............................ ok +special_annot.sail ..................... ok +for_shadow.sail ........................ ok +xlen_val.sail .......................... ok +poly_union_rev.sail .................... ok +rv_duopod_bug.sail ..................... ok +prelude.sail ........................... ok +fast_signed.sail ....................... ok +cheri128_hsb.sail ...................... ok +tl_let.sail ............................ ok +return_leak.sail ....................... ok +pattern_concat_nest.sail ............... ok +issue401.sail .......................... ok +undefined_nat.sail ..................... ok +list_scope.sail ........................ ok +cheri_capreg.sail ...................... ok +real_prop.sail ......................... ok +Failed: /home/trdthg/repo/sail/sail -ocaml -ocaml_build_dir _sbuild_issue232_2 -o issue232_2_ocaml issue232_2.sail +stdout: + +stderr: +Warning: Incomplete pattern match statement at issue232_2.sail:6.0-7: +6 |mapping e_pair_bits : (E,E) <-> bits(2) = +  |^-----^ +  | +The following expression is unmatched: (EB, EA) + +Fatal error: exception Not_found + +gvectorlit.sail ........................ ok +config_register.sail ................... ok +either_rvbug.sail ...................... ok +simple_bitmanip.sail ................... ok +struct_mapping.sail .................... ok +enum_functions.sail .................... ok +two_mapping.sail ....................... ok +Failed: /home/trdthg/repo/sail/sail -ocaml -ocaml_build_dir _sbuild_lib_valid_hex_bits -o lib_valid_hex_bits_ocaml lib_valid_hex_bits.sail +stdout: + +stderr: +Fatal error: exception Not_found + +undefined_union.sail ................... ok +bitvector_update2.sail ................. ok +anon_rec.sail .......................... ok +large_bitvector.sail ................... ok +list_cons_cons.sail .................... ok +nonexistent_pragma.sail ................ ok +type_if_bits.sail ...................... ok +Failed: /home/trdthg/repo/sail/sail -ocaml -ocaml_build_dir _sbuild_zeros_mapping -o zeros_mapping_ocaml zeros_mapping.sail +stdout: + +stderr: +Warning: Incomplete pattern match statement at zeros_mapping.sail:7.0-7: +7 |mapping zeros_16 : unit <-> bits(16) = { () <-> 0x0000 } +  |^-----^ +  | +The following expression is unmatched: 0xffff + +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 409): +zeros_mapping.sail:17.50-87: +17 |mapping clause encdec = Add(dest, src1, src2) <-> zeros_16() @ dest @ src1 @ src2 @ 0b1 +  | ^-----------------------------------^ +  | Invalid bitvector pattern +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize.bvc.(fun) in file "src/lib/pattern_completeness.ml", line 409, characters 27-86 +  | Called from Stdlib__List.fold_left2 in file "list.ml", line 161, characters 37-51 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 559, characters 54-93 +  | Called from Stdlib__List.map2 in file "list.ml", line 134, characters 15-22 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete.(fun) in file "src/lib/pattern_completeness.ml", line 555, characters 16-1023 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.simple_matrix_is_complete in file "src/lib/pattern_completeness.ml", line 552, characters 10-1023 +  | Called from Libsail__Pattern_completeness.Make.is_complete_matrixs.(fun) in file "src/lib/pattern_completeness.ml", line 987, characters 16-47 +  | Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +pointer_assign.sail .................... ok +flow_restrict.sail ..................... ok +tuple_union.sail ....................... ok +constructor247.sail .................... ok +tuple_fun.sail ......................... ok +shadow_cleanup.sail .................... ok +spc_mappings.sail ...................... ok +global_let_shadow.sail ................. ok +if_opt_typ.sail ........................ ok +set_struct.sail ........................ ok +rv_memop.sail .......................... ok +poly_mapping.sail ...................... ok +fvector_update.sail .................... ok +enum_map.sail .......................... ok +reg_ref.sail ........................... ok +cheri_capstruct_order.sail ............. ok +issue362.sail .......................... ok +fail_issue203.sail ..................... ok +let_option_shadow.sail ................. ok +try_return.sail ........................ ok +dead_branch.sail ....................... ok +double_option.sail ..................... ok +let_option.sail ........................ ok +Failed: /home/trdthg/repo/sail/sail -ocaml -ocaml_build_dir _sbuild_mapping_compose -o mapping_compose_ocaml mapping_compose.sail +stdout: + +stderr: +Fatal error: exception Not_found + +tl_pat.sail ............................ ok +eq_struct.sail ......................... ok +downcast_fn.sail ....................... ok +enum_match.sail ........................ ok +string_literal_type.sail ............... ok +poly_int_record.sail ................... ok +extend_simple.sail ..................... ok +Failed: /home/trdthg/repo/sail/sail -ocaml -ocaml_build_dir _sbuild_lib_hex_bits_signed -o lib_hex_bits_signed_ocaml lib_hex_bits_signed.sail +stdout: + +stderr: +Fatal error: exception Not_found + +string_of_bits.sail .................... ok +assign_rename_bug.sail ................. ok +reg_32_64.sail ......................... ok +overload_mapping.sail .................. ok +return_register_ref.sail ............... ok +list_rec_functions1.sail ............... ok +poly_outcome.sail ...................... ok +Failed: /home/trdthg/repo/sail/sail -ocaml -ocaml_build_dir _sbuild_issue243_fixed -o issue243_fixed_ocaml issue243_fixed.sail +stdout: + +stderr: +Warning: Incomplete pattern match statement at issue243_fixed.sail:6.0-7: +6 |mapping e_pair_bits : (E,E) <-> bits(2) = +  |^-----^ +  | +The following expression is unmatched: (EB, EA) + +Internal error: Unreachable code (at "src/lib/pattern_completeness.ml" line 479): +issue243_fixed.sail:17.22-49: +17 |mapping f_bits = { FE(struct { e1 = e1, v1 = v1 }) <-> e_pair_bits(e1,EB) @ v1 } +  | ^-------------------------^ +  | P_struct pattern with non-struct type +  | +  | Raised by primitive operation at Libsail__Reporting.err_unreachable in file "src/lib/reporting.ml", line 211, characters 18-62 +  | Called from Libsail__Reporting.unreachable in file "src/lib/reporting.ml" (inlined), line 219, characters 34-61 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 479, characters 17-88 +  | Called from Stdlib__List.map in file "list.ml", line 83, characters 15-19 +  | Called from Libsail__Pattern_completeness.Make.generalize in file "src/lib/pattern_completeness.ml", line 426, characters 28-63 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded.(fun) in file "src/lib/pattern_completeness.ml", line 1053, characters 73-103 +  | Called from Stdlib__List.mapi in file "list.ml", line 93, characters 15-21 +  | Called from Stdlib__List.mapi in file "list.ml" (inlined), line 100, characters 15-25 +  | Called from Libsail__Pattern_completeness.Make.is_complete_mapcls_wildcarded in file "src/lib/pattern_completeness.ml", line 1053, characters 11-113 +  | Called from Libsail__Type_check.check_mapdef_completeness in file "src/lib/type_check.ml", line 4571, characters 8-63 +  | Called from Libsail__Type_check.check_mapdef in file "src/lib/type_check.ml", line 4622, characters 9-57 +  | Called from Libsail__Type_check.check_defs_progress.aux in file "src/lib/type_check.ml", line 5160, characters 20-37 +  | +  | Please report this as an issue on GitHub at https://github.com/rems-project/sail/issues + +hello_world.sail ....................... ok +poly_pair.sail ......................... ok +all_even_vector_length.sail ............ ok +pr194.sail ............................. ok +match_bind.sail ........................ ok +mapping.sail ........................... ok +list_torture.sail ...................... ok +stack_struct.sail ...................... ok +struct_pattern.sail .................... ok +issue429.sail .......................... ok +list_scope2.sail ....................... ok +nexp_synonym.sail ...................... ok +shadow_let.sail ........................ ok +infix_include.sail ..................... ok +inc_tests.sail ......................... ok +Failed: /home/trdthg/repo/sail/sail -ocaml -ocaml_build_dir _sbuild_issue232 -o issue232_ocaml issue232.sail +stdout: + +stderr: +Warning: Incomplete pattern match statement at issue232.sail:6.0-7: +6 |mapping e_pair_bits : (E,E) <-> bits(2) = +  |^-----^ +  | +The following expression is unmatched: (EB, EA) + +Fatal error: exception Not_found + +short_circuit.sail ..................... ok +single_guard.sail ...................... ok +reg_ref_nb.sail ........................ ok +exn_hello_world.sail ................... ok +zero_length_bv.sail .................... ok +warl.sail .............................. ok +encdec_subrange.sail ................... ok +struct.sail ............................ ok +poly_tup.sail .......................... ok +warl2.sail ............................. ok +scattered_mapping.sail ................. ok +new_bitfields.sail ..................... ok +nested_mapping.sail .................... ok +pow2.sail .............................. ok +vector_example.sail .................... ok +poly_record.sail ....................... ok +non_unique.sail ........................ ok +poly_union.sail ........................ ok +config.sail ............................ ok +string_take.sail ....................... ok +letbind.sail ........................... ok +int_struct_constrained.sail ............ ok +concurrency_interface.sail ............. ok +Failed: /home/trdthg/repo/sail/sail -ocaml -ocaml_build_dir _sbuild_encdec -o encdec_ocaml encdec.sail +stdout: + +stderr: +Warning: Deprecated encdec.sail:30.24-82: +30 |val main : unit -> unit effect {barr, eamem, escape, exmem, rmem, rreg, wmv, wreg} +  | ^--------------------------------------------------------^ +  | +Explicit effect annotations are deprecated. They are no longer used and can be removed. + +Warning: Incomplete pattern match statement at encdec.sail:11.0-7: +11 |mapping decenc_p : bits(2) <-> pred = { +  |^-----^ +  | +The following expression is unmatched: 0b10 + +Fatal error: exception Not_found + +option_nest.sail ....................... ok +option.sail ............................ ok +struct_pattern_partial.sail ............ ok +tl_poly_match.sail ..................... ok +bitvector.sail ......................... ok +cfold_reg.sail ......................... ok +list_scope3.sail ....................... ok +string_of_bits2.sail ................... ok +poly_simple.sail ....................... ok +issue202_1.sail ........................ ok +vector_init.sail ....................... ok +bv_literal.sail ........................ ok +option_option.sail ..................... ok +loop_exception.sail .................... ok +outcome_impl.sail ...................... ok +164 passes and 12 failures + +========================================== +SMT tests +========================================== + +========================================== +Builtins tests +========================================== +Sail is /home/trdthg/repo/sail/sail +Sail dir is /home/trdthg/repo/sail +---------------------------------------------------- +Testing builtins: C, No optimisations Sail options: +---------------------------------------------------- +zeros.sail ok +replicate_bits.sail ok +div_int.sail ok +unsigned6.sail ok +slice_mask.sail ok +div_int2.sail ok +unsigned3.sail ok +set_slice_bits.sail ok +not_bool.sail ok +hex_str.sail ok +get_slice_int.sail ok +unsigned1.sail ok +clz.sail ok +vector_update_subrange.sail ok +sub_int.sail ok +unsigned4.sail ok +vector_update.sail ok +divmod.sail ok +unsigned7.sail ok +unsigned5.sail ok +count_leading_zeros.sail ok +shl_int.sail ok +shift.sail ok +add_bits.sail ok +append.sail ok +unsigned8.sail ok +mult_int.sail ok +unsigned2.sail ok +signed.sail ok +29 passes and 0 failures +--------------------------------------------------- +Testing builtins: C, Optimisations Sail options: -O +--------------------------------------------------- +zeros.sail ok +replicate_bits.sail ok +div_int.sail ok +unsigned6.sail ok +slice_mask.sail ok +div_int2.sail ok +unsigned3.sail ok +set_slice_bits.sail ok +not_bool.sail ok +hex_str.sail ok +get_slice_int.sail ok +unsigned1.sail ok +clz.sail ok +vector_update_subrange.sail ok +sub_int.sail ok +unsigned4.sail ok +vector_update.sail ok +divmod.sail ok +unsigned7.sail ok +unsigned5.sail ok +count_leading_zeros.sail ok +shift.sail ok +shl_int.sail ok +add_bits.sail ok +append.sail ok +unsigned8.sail ok +mult_int.sail ok +unsigned2.sail ok +signed.sail ok +29 passes and 0 failures +------------------------------------------------------------------- +Testing builtins: C, Constant folding Sail options: -Oconstant_fold +------------------------------------------------------------------- +replicate_bits.sail ok +zeros.sail ok +unsigned6.sail ok +div_int.sail ok +slice_mask.sail ok +set_slice_bits.sail ok +unsigned3.sail ok +div_int2.sail ok +hex_str.sail ok +not_bool.sail ok +get_slice_int.sail ok +unsigned1.sail ok +clz.sail ok +vector_update_subrange.sail ok +sub_int.sail ok +unsigned4.sail ok +vector_update.sail ok +divmod.sail ok +unsigned5.sail ok +unsigned7.sail ok +count_leading_zeros.sail ok +shift.sail ok +shl_int.sail ok +add_bits.sail ok +append.sail ok +mult_int.sail ok +unsigned2.sail ok +unsigned8.sail ok +signed.sail ok +29 passes and 0 failures +-------------------------------------- +Testing builtins: OCaml Sail options: +-------------------------------------- +zeros.sail ok +replicate_bits.sail ok +div_int.sail ok +unsigned6.sail ok +slice_mask.sail ok +div_int2.sail ok +set_slice_bits.sail ok +unsigned3.sail ok +not_bool.sail ok +hex_str.sail ok +get_slice_int.sail ok +unsigned1.sail ok +clz.sail ok +vector_update_subrange.sail ok +sub_int.sail ok +unsigned4.sail ok +vector_update.sail ok +divmod.sail ok +unsigned7.sail ok +unsigned5.sail ok +shift.sail ok +shl_int.sail ok +count_leading_zeros.sail ok +add_bits.sail ok +append.sail ok +mult_int.sail ok +unsigned8.sail ok +unsigned2.sail ok +signed.sail ok +29 passes and 0 failures + +========================================== +ARM spec tests +========================================== +Compiling specification... +compiled no_vector specification: ok +ran test.elf: ok +ran test_O1.elf: ok +ran test_O2.elf: ok +ran test_Og.elf: ok + +Loading specification into interpreter... +loaded no_vector specification: ok +interpreter success: ok +ARM generated spec tests: Passed 7 out of 7 + diff --git a/test/sailcov/Makefile b/test/sailcov/Makefile index 48002c701..183832699 100644 --- a/test/sailcov/Makefile +++ b/test/sailcov/Makefile @@ -1,14 +1,17 @@ -basename="nested_mapping" -filename="nested_mapping.sail" +basename="nested_mapping4" +filename="${basename}.sail" sail="/home/trdthg/repo/sail/sail" sail_dir="/home/trdthg/repo/sail" sailcov="/home/trdthg/repo/sail/sailcov/sailcov" -all: clear build_sail all_branch build_model taken cov diff +all: clear build_sail build_sailcov all_branch build_model taken cov diff build_and_run_c: build_model taken build_sail: - cd ${sail_dir} && make -f ${sail_dir}/Makefile + cd ${sail_dir} && make + +build_sailcov: + cd ${sail_dir}/sailcov && make all_branch: ${sail} -no_warn -no_memo_z3 -c -c_include sail_coverage.h -c_coverage ${basename}.branches ${filename} -o ${basename} @@ -26,4 +29,4 @@ diff: diff ${basename}.html ${basename}.expect clear: - rm -f ${basename}.taken ${basename}.bin ${basename}.branches + rm -f ${basename}.taken ${basename}.bin ${basename}.branches ${basename}.html ${basename}.c diff --git a/test/sailcov/nested_mapping.expect b/test/sailcov/nested_mapping.expect new file mode 100644 index 000000000..fd06fdfb3 --- /dev/null +++ b/test/sailcov/nested_mapping.expect @@ -0,0 +1,33 @@ + + + + +nested_mapping + +

nested_mapping.sail (2/6) 33%

+ +default Order dec
+$include <prelude.sail>
+
+union ast = {
+  B : (bool),
+  Z : unit
+}
+
+mapping bool_not_bits2 : bool <-> bits(2) = {
+  true   <-> 0b10,
+  false  <-> 0b11
+}
+mapping encdec  : bits(2) <->  ast = {
+  0b00 <-> Z(),
+  0b01 <-> Z(),
+  bool_not_bits2(s) <-> B(s),
+}
+
+val main : unit -> unit
+function main() = {
+    let encdec_value = encdec(0b00)
+}
+ + + \ No newline at end of file diff --git a/test/sailcov/nested_mapping1.expect b/test/sailcov/nested_mapping1.expect new file mode 100644 index 000000000..749307487 --- /dev/null +++ b/test/sailcov/nested_mapping1.expect @@ -0,0 +1,32 @@ + + + + +nested_mapping1 + +

nested_mapping1.sail (4/5) 80%

+ +default Order dec
+$include <prelude.sail>
+
+union ast = {
+  B : (bool),
+  Z : unit
+}
+
+mapping bool_not_bits2 : bool <-> bits(2) = {
+  true   <-> 0b10,
+  false  <-> 0b11
+}
+mapping encdec  : bits(2) <->  ast = {
+  0b01 if true <-> Z(),
+  0b00 <-> Z(),
+}
+
+val main : unit -> unit
+function main() = {
+    let encdec_value = encdec(0b00)
+}
+ + + \ No newline at end of file diff --git a/test/sailcov/nested_mapping1.sail b/test/sailcov/nested_mapping1.sail new file mode 100644 index 000000000..8aeafae2e --- /dev/null +++ b/test/sailcov/nested_mapping1.sail @@ -0,0 +1,28 @@ +default Order dec +$include + +union ast = { + B : (bool), + Z : unit +} + +mapping bool_not_bits : bool <-> bits(1) = { + true <-> 0b0, + false <-> 0b1, +} + +let false_val = false +let false_2 = false == true + +mapping encdec : bits(2) <-> ast = { + 0b1 @ bool_not_bits(s) <-> B(s), + 0b01 if true <-> Z(), + 0b00 if false_val <-> Z(), + 0b00 if false_val == true <-> Z(), + 0b00 <-> Z(), +} + +val main : unit -> unit +function main() = { + let encdec_value = encdec(0b00) +} \ No newline at end of file diff --git a/test/sailcov/nested_mapping2.expect b/test/sailcov/nested_mapping2.expect new file mode 100644 index 000000000..03f62f450 --- /dev/null +++ b/test/sailcov/nested_mapping2.expect @@ -0,0 +1,33 @@ + + + + +nested_mapping2 + +

nested_mapping2.sail (2/5) 40%

+ +default Order dec
+$include <prelude.sail>
+
+union ast = {
+  B : (bool),
+  Z : unit,
+}
+
+mapping bool_not_bits : bool <-> bits(1) = {
+  true   <-> 0b0,
+  false  <-> 0b1,
+}
+
+mapping encdec  : bits(2) <->  ast = {
+  0b00 <-> Z(),
+  0b1 @ bool_not_bits(s) <-> B(s),
+}
+
+val main : unit -> unit
+function main() = {
+    let _ = encdec(0b00)
+}
+ + + \ No newline at end of file diff --git a/test/sailcov/nested_mapping2.sail b/test/sailcov/nested_mapping2.sail new file mode 100644 index 000000000..ffd363578 --- /dev/null +++ b/test/sailcov/nested_mapping2.sail @@ -0,0 +1,22 @@ +default Order dec +$include + +union ast = { + B : (bool), + Z : unit, +} + +mapping bool_not_bits : bool <-> bits(1) = { + true <-> 0b0, + false <-> 0b1, +} + +mapping encdec : bits(2) <-> ast = { + 0b00 <-> Z(), + 0b1 @ bool_not_bits(s) <-> B(s), +} + +val main : unit -> unit +function main() = { + let _ = encdec(0b00) +} \ No newline at end of file diff --git a/test/sailcov/nested_mapping3.expect b/test/sailcov/nested_mapping3.expect new file mode 100644 index 000000000..ddf631bcc --- /dev/null +++ b/test/sailcov/nested_mapping3.expect @@ -0,0 +1,33 @@ + + + + +nested_mapping3 + +

nested_mapping3.sail (3/5) 60%

+ +default Order dec
+$include <prelude.sail>
+
+union ast = {
+  B : (bool),
+  Z : unit,
+}
+
+mapping bool_not_bits : bool <-> bits(1) = {
+  true   <-> 0b0,
+  false  <-> 0b1,
+}
+
+mapping encdec  : bits(2) <->  ast = {
+  0b1 @ bool_not_bits(s) <-> B(s),
+  0b00 <-> Z(),
+}
+
+val main : unit -> unit
+function main() = {
+    let _ = encdec(0b00)
+}
+ + + \ No newline at end of file diff --git a/test/sailcov/nested_mapping3.sail b/test/sailcov/nested_mapping3.sail new file mode 100644 index 000000000..c35579316 --- /dev/null +++ b/test/sailcov/nested_mapping3.sail @@ -0,0 +1,22 @@ +default Order dec +$include + +union ast = { + B : (bool), + Z : unit, +} + +mapping bool_not_bits : bool <-> bits(1) = { + true <-> 0b0, + false <-> 0b1, +} + +mapping encdec : bits(2) <-> ast = { + 0b1 @ bool_not_bits(s) <-> B(s), + 0b00 <-> Z(), +} + +val main : unit -> unit +function main() = { + let _ = encdec(0b00) +} \ No newline at end of file diff --git a/test/sailcov/nested_mapping4.sail b/test/sailcov/nested_mapping4.sail new file mode 100644 index 000000000..7a0f24aea --- /dev/null +++ b/test/sailcov/nested_mapping4.sail @@ -0,0 +1,22 @@ +default Order dec +$include + +union ast = { + B : (bool), + Z : unit +} + +mapping bool_not_bits : bool <-> bits(1) = { + true <-> 0b0, + false <-> 0b1 +} + +mapping encdec : bits(2) <-> ast = { + 0b1 @ bool_not_bits(s) if true <-> B(s), + 0b00 <-> Z() +} + +val main : unit -> unit +function main() = { + let _ = encdec(0b00) +} \ No newline at end of file diff --git a/test/sailcov/nested_mapping5.sail b/test/sailcov/nested_mapping5.sail new file mode 100644 index 000000000..54692e61b --- /dev/null +++ b/test/sailcov/nested_mapping5.sail @@ -0,0 +1,29 @@ +default Order dec +$include + +union ast = { + B : (bool), + Z : unit, +} + +mapping bool_not_bits : bool <-> bits(1) = { + true <-> 0b0, + false <-> 0b1, +} + +let false_val = false +let false_2 = false == true + +mapping encdec : bits(2) <-> ast = { + 0b1 @ bool_not_bits(s) <-> B(s), + 0b01 if true <-> Z(), + 0b00 if false_val <-> Z(), + 0b00 if false_val == true <-> Z(), + 0b0 @ bool_not_bits(s) if true <-> B(s), + 0b00 <-> Z(), +} + +val main : unit -> unit +function main() = { + let _ = encdec(0b00) +} \ No newline at end of file diff --git a/test/sailcov/nested_mapping_demo.full_branches b/test/sailcov/nested_mapping_demo.full_branches new file mode 100644 index 000000000..2ef0f9df4 --- /dev/null +++ b/test/sailcov/nested_mapping_demo.full_branches @@ -0,0 +1,27 @@ +$[complete] +function encdec_forwards arg# = let head_exp# = arg# in + $[complete] $[mapping_match] match $[complete] match head_exp# { + v__0 if and_bool( + let mapping0# : bitvector(1) = + $[overloaded { "name" = "vector_subrange", "is_infix" = false }] subrange_bits(v__0, 0, 0) + in + bool_not_bits_backwards_matches(mapping0#), + $[overloaded { "name" = "==", "is_infix" = true }] + eq_bits( + $[overloaded { "name" = "vector_subrange", "is_infix" = false }] + subrange_bits(v__0, 1, 1), [bitone]) + ) => + let mapping0# : bitvector(1) = + $[overloaded { "name" = "vector_subrange", "is_infix" = false }] subrange_bits(v__0, 0, 0) + in + $[complete] match bool_not_bits_backwards(mapping0#) { + s => Some(B(s)), + _ => None() + }, + _ => None() + } { + Some(result) => result, + None(_) => $[incomplete] match head_exp# { + b__0 if $[overloaded { "name" = "==", "is_infix" = true }] eq_bits(b__0, [bitzero, bitzero]) => Z() + } + } diff --git a/test/sailcov/nested_mapping_demo.sail b/test/sailcov/nested_mapping_demo.sail new file mode 100644 index 000000000..c35579316 --- /dev/null +++ b/test/sailcov/nested_mapping_demo.sail @@ -0,0 +1,22 @@ +default Order dec +$include + +union ast = { + B : (bool), + Z : unit, +} + +mapping bool_not_bits : bool <-> bits(1) = { + true <-> 0b0, + false <-> 0b1, +} + +mapping encdec : bits(2) <-> ast = { + 0b1 @ bool_not_bits(s) <-> B(s), + 0b00 <-> Z(), +} + +val main : unit -> unit +function main() = { + let _ = encdec(0b00) +} \ No newline at end of file