Skip to content

Commit f629592

Browse files
authored
Merge pull request #2480 from GaloisInc/crucible-T1445-submodule-bump
Bump `crucible`, `mir-json` submodule to bring in custom DST support
2 parents ac08070 + 23621d4 commit f629592

File tree

5 files changed

+6
-7
lines changed

5 files changed

+6
-7
lines changed

crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.good

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ failures:
55
---- basic_err_fewer_args/<DISAMB>::test[0] counterexamples ----
66
[Crux] Found counterexample for verification goal
77
[Crux] test/symb_eval/cryptol/basic_err_fewer_args.rs:8:35: 8:65: error: in basic_err_fewer_args/<DISAMB>::test[0]
8-
[Crux] error loading "addByte": not enough arguments: Cryptol function signature [8] -> [8] -> [8] has 2 arguments, but Rust signature (u8, u8, u8) -> u8 [RustAbi] requires 3
8+
[Crux] error loading "addByte": not enough arguments: Cryptol function signature [8] -> [8] -> [8] has 2 arguments, but Rust signature (u8, u8, u8) -> u8 [RustAbi] requires 3
99

1010
[Crux] Overall status: Invalid.

deps/mir-json

saw-central/src/SAWCentral/Crucible/MIR/ResolveSetupValue.hs

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1360,7 +1360,6 @@ data FnSigView = FnSigView {
13601360
_fsvarg_tys :: ![TyView]
13611361
, _fsvreturn_ty :: !TyView
13621362
, _fsvabi :: Mir.Abi
1363-
, _fsvspreadarg :: Maybe Int
13641363
}
13651364
deriving Eq
13661365

@@ -1423,8 +1422,8 @@ substsView (Mir.Substs tys) = SubstsView (map tyView tys)
14231422

14241423
-- | Convert a 'Mir.FnSig' value to a 'FnSigView' value.
14251424
fnSigView :: Mir.FnSig -> FnSigView
1426-
fnSigView (Mir.FnSig argTys retTy abi spreadarg) =
1427-
FnSigView (map tyView argTys) (tyView retTy) abi spreadarg
1425+
fnSigView (Mir.FnSig argTys retTy abi) =
1426+
FnSigView (map tyView argTys) (tyView retTy) abi
14281427

14291428
-- | Read the value out of a 'MaybeType' expression that is assumed to be
14301429
-- assigned to a value. If this assumption does not hold (i.e., if the value is

saw-central/src/SAWCentral/Crucible/MIR/TypeShape.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -275,7 +275,7 @@ tyToShape col = go
275275
goRef ty ty' mutbl | Some tpr <- tyToRepr col ty' = Some $ RefShape ty ty' mutbl tpr
276276

277277
goFnPtr :: M.Ty -> M.FnSig -> Some TypeShape
278-
goFnPtr ty (M.FnSig args ret _abi _spread) =
278+
goFnPtr ty (M.FnSig args ret _abi) =
279279
tyListToCtx col args $ \argsr ->
280280
tyToReprCont col ret $ \retr ->
281281
Some (FnPtrShape ty argsr retr)

0 commit comments

Comments
 (0)