diff --git a/flake.lock b/flake.lock index 45c7906..21a435c 100644 --- a/flake.lock +++ b/flake.lock @@ -13,11 +13,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1736782668, - "narHash": "sha256-s2bUC/GDEjawaQCh/GE955uehSi/ACdT+1z2CMqIRow=", + "lastModified": 1738247409, + "narHash": "sha256-T4cRt5gSW4mpOePDWu/oaBkVJYgd04Fyn93qjw33CbI=", "owner": "aeneasverif", "repo": "charon", - "rev": "1c628d8a9704ee3ab0b9289c73b84848c508d26d", + "rev": "ab692757d7033908c89bcc0e94d5ab1380b4f856", "type": "github" }, "original": { @@ -177,16 +177,17 @@ ] }, "locked": { - "lastModified": 1736735482, - "narHash": "sha256-QOA4jCDyyUM9Y2Vba+HSZ/5LdtCMGaTE/7NkkUzBr50=", + "lastModified": 1737340068, + "narHash": "sha256-5UciRckNV+YOZ6y6ASBIb01cySB12whDxgFUK+EqT8g=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "cf960a1938ee91200fe0d2f7b2582fde2429d562", + "rev": "275c824ed9e90e7fd4f96d187bde3670062e721f", "type": "github" }, "original": { "owner": "oxalica", "repo": "rust-overlay", + "rev": "275c824ed9e90e7fd4f96d187bde3670062e721f", "type": "github" } }, diff --git a/flake.nix b/flake.nix index fcfa751..908f356 100644 --- a/flake.nix +++ b/flake.nix @@ -106,7 +106,8 @@ }; checks.default = packages.default.tests; devShells.ci = pkgs.mkShell { packages = [ pkgs.jq ]; }; - devShells.default = pkgs.mkShell { + devShells.default = (pkgs.mkShell.override { stdenv = pkgs.clangStdenv; }) { + OCAMLRUNPARAM = "b"; # Get backtrace on exception packages = [ pkgs.clang-tools # For clang-format pkgs.ocamlPackages.ocaml diff --git a/out/test-array2d/array2d.h b/out/test-array2d/array2d.h index 45677b2..e0cc097 100644 --- a/out/test-array2d/array2d.h +++ b/out/test-array2d/array2d.h @@ -27,9 +27,6 @@ void array2d_main(void); extern bool core_cmp_impls___core__cmp__PartialEq_u32__for_u32__24__eq(uint32_t *x0, uint32_t *x1); -extern bool -core_cmp_impls___core__cmp__PartialEq_u32__for_u32__24__ne(uint32_t *x0, uint32_t *x1); - #if defined(__cplusplus) } #endif diff --git a/out/test-nested_arrays/nested_arrays.h b/out/test-nested_arrays/nested_arrays.h index 029f0ed..4ecd065 100644 --- a/out/test-nested_arrays/nested_arrays.h +++ b/out/test-nested_arrays/nested_arrays.h @@ -25,21 +25,6 @@ typedef int8_t core_cmp_Ordering; extern bool core_cmp_impls___core__cmp__PartialEq_usize__for_usize__21__eq(size_t *x0, size_t *x1); -extern bool -core_cmp_impls___core__cmp__PartialEq_usize__for_usize__21__ne(size_t *x0, size_t *x1); - -extern bool -core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__ge(size_t *x0, size_t *x1); - -extern bool -core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__gt(size_t *x0, size_t *x1); - -extern bool -core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__le(size_t *x0, size_t *x1); - -extern bool -core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__lt(size_t *x0, size_t *x1); - #define core_option_None 0 #define core_option_Some 1 @@ -63,9 +48,6 @@ core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__partial_cmp( size_t *x1 ); -extern size_t -core_iter_range___core__iter__range__Step_for_usize__43__backward(size_t x0, size_t x1); - /** A monomorphic instance of core.option.Option with types size_t @@ -81,68 +63,12 @@ core_option_Option_08; extern core_option_Option_08 core_iter_range___core__iter__range__Step_for_usize__43__backward_checked(size_t x0, size_t x1); -extern size_t -core_iter_range___core__iter__range__Step_for_usize__43__backward_unchecked( - size_t x0, - size_t x1 -); - -extern size_t -core_iter_range___core__iter__range__Step_for_usize__43__forward(size_t x0, size_t x1); - extern core_option_Option_08 core_iter_range___core__iter__range__Step_for_usize__43__forward_checked(size_t x0, size_t x1); -extern size_t -core_iter_range___core__iter__range__Step_for_usize__43__forward_unchecked( - size_t x0, - size_t x1 -); - extern core_option_Option_08 core_iter_range___core__iter__range__Step_for_usize__43__steps_between(size_t *x0, size_t *x1); -/** -A monomorphic instance of core.num.nonzero.NonZero -with types size_t - -*/ -typedef size_t core_num_nonzero_NonZero_08; - -#define core_result_Ok 0 -#define core_result_Err 1 - -typedef uint8_t core_result_Result_eb_tags; - -/** -A monomorphic instance of core.result.Result -with types (), core_num_nonzero_NonZero size_t - -*/ -typedef struct core_result_Result_eb_s -{ - core_result_Result_eb_tags tag; - core_num_nonzero_NonZero_08 f0; -} -core_result_Result_eb; - -/** -A monomorphic instance of K. -with types size_t, core_option_Option size_t - -*/ -typedef struct tuple_04_s -{ - size_t fst; - core_option_Option_08 snd; -} -tuple_04; - -static inline core_num_nonzero_private_NonZeroUsizeInner -core_num_nonzero_private___core__clone__Clone_for_core__num__nonzero__private__NonZeroUsizeInner__26__clone( - core_num_nonzero_private_NonZeroUsizeInner *x0 -); - #define core_panicking_AssertKind_Eq 0 #define core_panicking_AssertKind_Ne 1 #define core_panicking_AssertKind_Match 2 diff --git a/out/test-symcrust/symcrust.h b/out/test-symcrust/symcrust.h index 46b5600..06ab6db 100644 --- a/out/test-symcrust/symcrust.h +++ b/out/test-symcrust/symcrust.h @@ -31,27 +31,9 @@ core_cmp_impls___core__cmp__Ord_for_u32__65__cmp(uint32_t *x0, uint32_t *x1); extern bool core_cmp_impls___core__cmp__PartialEq_u32__for_u32__24__eq(uint32_t *x0, uint32_t *x1); -extern bool -core_cmp_impls___core__cmp__PartialEq_u32__for_u32__24__ne(uint32_t *x0, uint32_t *x1); - extern bool core_cmp_impls___core__cmp__PartialEq_usize__for_usize__21__eq(size_t *x0, size_t *x1); -extern bool -core_cmp_impls___core__cmp__PartialEq_usize__for_usize__21__ne(size_t *x0, size_t *x1); - -extern bool -core_cmp_impls___core__cmp__PartialOrd_u32__for_u32__64__ge(uint32_t *x0, uint32_t *x1); - -extern bool -core_cmp_impls___core__cmp__PartialOrd_u32__for_u32__64__gt(uint32_t *x0, uint32_t *x1); - -extern bool -core_cmp_impls___core__cmp__PartialOrd_u32__for_u32__64__le(uint32_t *x0, uint32_t *x1); - -extern bool -core_cmp_impls___core__cmp__PartialOrd_u32__for_u32__64__lt(uint32_t *x0, uint32_t *x1); - #define core_option_None 0 #define core_option_Some 1 @@ -75,18 +57,6 @@ core_cmp_impls___core__cmp__PartialOrd_u32__for_u32__64__partial_cmp( uint32_t *x1 ); -extern bool -core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__ge(size_t *x0, size_t *x1); - -extern bool -core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__gt(size_t *x0, size_t *x1); - -extern bool -core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__le(size_t *x0, size_t *x1); - -extern bool -core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__lt(size_t *x0, size_t *x1); - extern core_option_Option_77 core_cmp_impls___core__cmp__PartialOrd_usize__for_usize__58__partial_cmp( size_t *x0, @@ -99,9 +69,6 @@ core_convert_num___core__convert__From_u16__for_u32__69__from(uint16_t x0); static inline uint64_t core_convert_num___core__convert__From_u32__for_u64__72__from(uint32_t x0); -extern size_t -core_iter_range___core__iter__range__Step_for_usize__43__backward(size_t x0, size_t x1); - /** A monomorphic instance of core.option.Option with types size_t @@ -117,68 +84,12 @@ core_option_Option_08; extern core_option_Option_08 core_iter_range___core__iter__range__Step_for_usize__43__backward_checked(size_t x0, size_t x1); -extern size_t -core_iter_range___core__iter__range__Step_for_usize__43__backward_unchecked( - size_t x0, - size_t x1 -); - -extern size_t -core_iter_range___core__iter__range__Step_for_usize__43__forward(size_t x0, size_t x1); - extern core_option_Option_08 core_iter_range___core__iter__range__Step_for_usize__43__forward_checked(size_t x0, size_t x1); -extern size_t -core_iter_range___core__iter__range__Step_for_usize__43__forward_unchecked( - size_t x0, - size_t x1 -); - extern core_option_Option_08 core_iter_range___core__iter__range__Step_for_usize__43__steps_between(size_t *x0, size_t *x1); -/** -A monomorphic instance of core.num.nonzero.NonZero -with types size_t - -*/ -typedef size_t core_num_nonzero_NonZero_08; - -#define core_result_Ok 0 -#define core_result_Err 1 - -typedef uint8_t core_result_Result_eb_tags; - -/** -A monomorphic instance of core.result.Result -with types (), core_num_nonzero_NonZero size_t - -*/ -typedef struct core_result_Result_eb_s -{ - core_result_Result_eb_tags tag; - core_num_nonzero_NonZero_08 f0; -} -core_result_Result_eb; - -/** -A monomorphic instance of K. -with types size_t, core_option_Option size_t - -*/ -typedef struct tuple_04_s -{ - size_t fst; - core_option_Option_08 snd; -} -tuple_04; - -static inline core_num_nonzero_private_NonZeroUsizeInner -core_num_nonzero_private___core__clone__Clone_for_core__num__nonzero__private__NonZeroUsizeInner__26__clone( - core_num_nonzero_private_NonZeroUsizeInner *x0 -); - static inline void core_num__u32_8__to_le_bytes(uint32_t x0, uint8_t x1[4U]); void diff --git a/scripts/update-charon-pin.sh b/scripts/update-charon-pin.sh index c04c5c3..7929cd0 100755 --- a/scripts/update-charon-pin.sh +++ b/scripts/update-charon-pin.sh @@ -1,12 +1,6 @@ #!/usr/bin/env bash -if ! which jq 2> /dev/null 1>&2; then - echo 'Error: command `jq` not found; please install it.' - exit 1 -fi - CHARON_DIR=./lib/charon CHARON_BRANCH="$(git -C "$CHARON_DIR" rev-parse --abbrev-ref HEAD)" CHARON_COMMIT="$(git -C "$CHARON_DIR" rev-parse HEAD)" echo 'Taking the commit from your local charon directory. The charon branch is `'"$CHARON_BRANCH"'`' nix flake lock --extra-experimental-features nix-command --extra-experimental-features flakes --override-input charon "github:aeneasverif/charon/$CHARON_COMMIT" -nix flake lock --extra-experimental-features nix-command --extra-experimental-features flakes --update-input charon/rust-overlay