Created
March 21, 2023 14:40
-
-
Save RyanGlScott/ba57ccfd36553d7f0540d1c965af70c9 to your computer and use it in GitHub Desktop.
crux-mir test suite progress
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| crux-mir | |
| crux concrete | |
| refs | |
| promoted_imm: OK (0.15s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 0 | |
| Crux output: 0 | |
| mut_raw: OK (0.15s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 123 | |
| Crux output: 123 | |
| mut_nested: OK (0.15s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () | |
| Crux output: () | |
| fn_ptr_mut: OK (1.40s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (1.25s) | |
| Crux output: 1 | |
| never: OK (1.45s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 1 (1.29s) | |
| Crux output: 1 | |
| mut_ref: OK (1.38s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 1 (1.24s) | |
| Crux output: 1 | |
| temp: FAIL (1.44s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 1 (1.30s) | |
| Crux output: | |
| failures: | |
| ---- temp/d7844d21::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/refs/temp.rs:4:13: 4:16: error: in temp/d7844d21::crux_test[0] | |
| [Crux] Translation error in temp/d7844d21::crux_test[0]: cannot find static variable alloc$1/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/temp/' to rerun this test only. | |
| mut_arg: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (1.27s) | |
| Crux output: 1 | |
| fn_ptr: OK (1.41s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (1.27s) | |
| Crux output: 1 | |
| promoted_mut: FAIL (1.49s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 0 (1.35s) | |
| Crux output: | |
| failures: | |
| ---- promoted_mut/2f6ad8be::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/refs/promoted_mut.rs:4:27: 4:34: error: in promoted_mut/2f6ad8be::crux_test[0] | |
| [Crux] Translation error in promoted_mut/2f6ad8be::crux_test[0]: cannot find static variable alloc$0/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/promoted_mut/' to rerun this test only. | |
| never_mut: OK (1.44s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 1 (1.28s) | |
| Crux output: 1 | |
| mut_tuple_field: FAIL (1.49s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.34s) | |
| Crux output: | |
| failures: | |
| ---- mut_tuple_field/5c4d5845::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/refs/mut_tuple_field.rs:10:19: 10:25: error: in mut_tuple_field/5c4d5845::f[0] | |
| [Crux] Translation error in mut_tuple_field/5c4d5845::f[0]: cannot find static variable alloc$0/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/mut_tuple_field/' to rerun this test only. | |
| imm_raw: OK (1.41s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 123 (1.25s) | |
| Crux output: 123 | |
| static_mut: OK (1.43s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 2 (1.28s) | |
| Crux output: 2 | |
| imm_ref: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 123 (1.27s) | |
| Crux output: 123 | |
| imm_arg: OK (1.44s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 1 (1.30s) | |
| Crux output: 1 | |
| hash_map | |
| insert_multi: FAIL (2.39s) | |
| Compiling and running oracle program (0.19s) | |
| Oracle output: 100 (2.20s) | |
| vtable signature mismatch for vtable core/4066fdba::ops[0]::function[0]::FnMut[0]::_vtblc2e637e13369cbd5[0] of trait core/4066fdba::ops[0]::function[0]::FnMut[0]::_trait35b29a8a4ae9e473[0] : StructRepr [FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] BoolRepr, FunctionHandleRepr [AnyRepr, BVRepr 32] BoolRepr] != StructRepr [FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] BoolRepr, FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] BoolRepr] | |
| CallStack (from HasCallStack): | |
| error, called at src/Mir/Trans.hs:904:20 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| mkTraitObject, called at src/Mir/Trans.hs:747:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast', called at src/Mir/Trans.hs:878:5 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast, called at src/Mir/Trans.hs:930:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalRval, called at src/Mir/Trans.hs:1142:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transStatement, called at src/Mir/Trans.hs:1740:68 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| translateBlockBody, called at src/Mir/Trans.hs:1749:28 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| registerBlock, called at src/Mir/Trans.hs:1789:10 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| genFn, called at src/Mir/Trans.hs:1835:24 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transDefine, called at src/Mir/Trans.hs:2272:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transCollection, called at src/Mir/Generate.hs:225:26 in crux-mir-0.6.0.99-inplace:Mir.Generate | |
| translateMIR, called at src/Mir/Language.hs:252:16 in crux-mir-0.6.0.99-inplace:Mir.Language | |
| Use -p '/insert_multi/' to rerun this test only. | |
| insert_remove: FAIL (2.51s) | |
| Compiling and running oracle program (0.18s) | |
| Oracle output: 12 (2.33s) | |
| vtable signature mismatch for vtable core/4066fdba::ops[0]::function[0]::FnMut[0]::_vtblc2e637e13369cbd5[0] of trait core/4066fdba::ops[0]::function[0]::FnMut[0]::_trait35b29a8a4ae9e473[0] : StructRepr [FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] BoolRepr, FunctionHandleRepr [AnyRepr, BVRepr 32] BoolRepr] != StructRepr [FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] BoolRepr, FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] BoolRepr] | |
| CallStack (from HasCallStack): | |
| error, called at src/Mir/Trans.hs:904:20 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| mkTraitObject, called at src/Mir/Trans.hs:747:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast', called at src/Mir/Trans.hs:878:5 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast, called at src/Mir/Trans.hs:930:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalRval, called at src/Mir/Trans.hs:1142:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transStatement, called at src/Mir/Trans.hs:1740:68 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| translateBlockBody, called at src/Mir/Trans.hs:1749:28 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| registerBlock, called at src/Mir/Trans.hs:1789:10 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| genFn, called at src/Mir/Trans.hs:1835:24 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transDefine, called at src/Mir/Trans.hs:2272:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transCollection, called at src/Mir/Generate.hs:225:26 in crux-mir-0.6.0.99-inplace:Mir.Generate | |
| translateMIR, called at src/Mir/Language.hs:252:16 in crux-mir-0.6.0.99-inplace:Mir.Language | |
| Use -p '/insert_remove/' to rerun this test only. | |
| insert_iter: FAIL (2.37s) | |
| Compiling and running oracle program (0.19s) | |
| Oracle output: [11, 12] (2.19s) | |
| vtable signature mismatch for vtable core/4066fdba::ops[0]::function[0]::FnMut[0]::_vtblc2e637e13369cbd5[0] of trait core/4066fdba::ops[0]::function[0]::FnMut[0]::_trait35b29a8a4ae9e473[0] : StructRepr [FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] BoolRepr, FunctionHandleRepr [AnyRepr, BVRepr 32] BoolRepr] != StructRepr [FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] BoolRepr, FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] BoolRepr] | |
| CallStack (from HasCallStack): | |
| error, called at src/Mir/Trans.hs:904:20 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| mkTraitObject, called at src/Mir/Trans.hs:747:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast', called at src/Mir/Trans.hs:878:5 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast, called at src/Mir/Trans.hs:930:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalRval, called at src/Mir/Trans.hs:1142:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transStatement, called at src/Mir/Trans.hs:1740:68 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| translateBlockBody, called at src/Mir/Trans.hs:1749:28 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| registerBlock, called at src/Mir/Trans.hs:1789:10 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| genFn, called at src/Mir/Trans.hs:1835:24 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transDefine, called at src/Mir/Trans.hs:2272:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transCollection, called at src/Mir/Generate.hs:225:26 in crux-mir-0.6.0.99-inplace:Mir.Generate | |
| translateMIR, called at src/Mir/Language.hs:252:16 in crux-mir-0.6.0.99-inplace:Mir.Language | |
| Use -p '/insert_iter/' to rerun this test only. | |
| insert_get: FAIL (2.48s) | |
| Compiling and running oracle program (0.18s) | |
| Oracle output: (11, 12) (2.30s) | |
| vtable signature mismatch for vtable core/4066fdba::ops[0]::function[0]::FnMut[0]::_vtblc2e637e13369cbd5[0] of trait core/4066fdba::ops[0]::function[0]::FnMut[0]::_trait35b29a8a4ae9e473[0] : StructRepr [FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] BoolRepr, FunctionHandleRepr [AnyRepr, BVRepr 32] BoolRepr] != StructRepr [FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] BoolRepr, FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] BoolRepr] | |
| CallStack (from HasCallStack): | |
| error, called at src/Mir/Trans.hs:904:20 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| mkTraitObject, called at src/Mir/Trans.hs:747:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast', called at src/Mir/Trans.hs:878:5 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast, called at src/Mir/Trans.hs:930:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalRval, called at src/Mir/Trans.hs:1142:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transStatement, called at src/Mir/Trans.hs:1740:68 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| translateBlockBody, called at src/Mir/Trans.hs:1749:28 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| registerBlock, called at src/Mir/Trans.hs:1789:10 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| genFn, called at src/Mir/Trans.hs:1835:24 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transDefine, called at src/Mir/Trans.hs:2272:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transCollection, called at src/Mir/Generate.hs:225:26 in crux-mir-0.6.0.99-inplace:Mir.Generate | |
| translateMIR, called at src/Mir/Language.hs:252:16 in crux-mir-0.6.0.99-inplace:Mir.Language | |
| Use -p '/insert_get/' to rerun this test only. | |
| traits | |
| params: OK (1.46s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 25 (1.30s) | |
| Crux output: 25 | |
| generic3: FAIL (1.46s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: () (1.30s) | |
| Crux output: | |
| failures: | |
| ---- generic3/114e3374::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in generic3/114e3374::f[0] | |
| [Crux] Translation error in generic3/114e3374::f[0]: error building variant core/4066fdba::option[0]::Option[0]::Some[0]: not enough expressions -- [] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/generic3/' to rerun this test only. | |
| static_three: OK (1.46s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.31s) | |
| Crux output: 2 | |
| generic1: FAIL (1.46s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: () (1.30s) | |
| Crux output: | |
| failures: | |
| ---- generic1/b404ba2b::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in generic1/b404ba2b::f[0] | |
| [Crux] Translation error in generic1/b404ba2b::f[0]: error building variant core/4066fdba::option[0]::Option[0]::Some[0]: not enough expressions -- [] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/generic1/' to rerun this test only. | |
| subtrait: OK (1.44s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 73 (1.29s) | |
| Crux output: 73 | |
| gen_trait: OK (1.49s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: -69 (1.33s) | |
| Crux output: -69 | |
| dynamic_branch: FAIL (0.18s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (0.03s) | |
| user error (Error 101 while running mir-json on test/conc_eval/traits/dynamic_branch.rs) | |
| Use -p '/dynamic_branch/' to rerun this test only. | |
| static_two: OK (1.40s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 1 (1.26s) | |
| Crux output: 1 | |
| tyfam5: OK (1.41s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.26s) | |
| Crux output: () | |
| generic2: FAIL (1.41s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.27s) | |
| Crux output: | |
| failures: | |
| ---- generic2/3de970d6::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in generic2/3de970d6::f[0] | |
| [Crux] Translation error in generic2/3de970d6::f[0]: error building variant core/4066fdba::option[0]::Option[0]::Some[0]: not enough expressions -- [] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/generic2/' to rerun this test only. | |
| assoc3: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.26s) | |
| Crux output: () | |
| tyfam4: OK (1.40s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 0 (1.24s) | |
| Crux output: 0 | |
| static_self: OK (1.41s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 42 (1.27s) | |
| Crux output: 42 | |
| conv: OK (1.40s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 1 (1.26s) | |
| Crux output: 1 | |
| dynamic_poly: FAIL (0.17s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 3 (0.03s) | |
| user error (Error 101 while running mir-json on test/conc_eval/traits/dynamic_poly.rs) | |
| Use -p '/dynamic_poly/' to rerun this test only. | |
| dynamic_simple: OK (1.40s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (1.25s) | |
| Crux output: 1 | |
| gen_trait_poly: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 12 (1.27s) | |
| Crux output: 12 | |
| default: OK (1.54s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 12 (1.39s) | |
| Crux output: 12 | |
| assoc1: OK (1.49s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: () (1.34s) | |
| Crux output: () | |
| subtrait2: OK (1.39s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 64 (1.25s) | |
| Crux output: 64 | |
| bounds1: FAIL (1.49s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: () (1.33s) | |
| Crux output: | |
| failures: | |
| ---- bounds1/7fe6450b::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in bounds1/7fe6450b::f[0] | |
| [Crux] Translation error in bounds1/7fe6450b::f[0]: error building variant core/4066fdba::option[0]::Option[0]::Some[0]: not enough expressions -- [] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/bounds1/' to rerun this test only. | |
| bounds3: FAIL (1.49s) | |
| Compiling and running oracle program (0.17s) | |
| Oracle output: () (1.33s) | |
| Crux output: | |
| failures: | |
| ---- bounds3/7d1bd76d::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in bounds3/7d1bd76d::f[0] | |
| [Crux] Translation error in bounds3/7d1bd76d::f[0]: error building variant core/4066fdba::option[0]::Option[0]::Some[0]: not enough expressions -- [] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/bounds3/' to rerun this test only. | |
| static_eq: OK (1.41s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: true (1.26s) | |
| Crux output: true | |
| tyfam3: OK (1.37s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 23 (1.22s) | |
| Crux output: 23 | |
| dict_med: OK (1.40s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 42 (1.26s) | |
| Crux output: 42 | |
| basics1: OK (1.37s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.23s) | |
| Crux output: () | |
| assoc2: OK (1.46s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.31s) | |
| Crux output: () | |
| dict_polymem: OK (1.47s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 4 (1.32s) | |
| Crux output: 4 | |
| bounds2: FAIL (1.49s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.34s) | |
| Crux output: | |
| failures: | |
| ---- bounds2/9cd2482f::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in bounds2/9cd2482f::f[0] | |
| [Crux] Translation error in bounds2/9cd2482f::f[0]: error building variant core/4066fdba::option[0]::Option[0]::Some[0]: not enough expressions -- [] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/bounds2/' to rerun this test only. | |
| intoiter: OK (1.51s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 0 (1.36s) | |
| Crux output: 0 | |
| static: OK (1.45s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 42 (1.29s) | |
| Crux output: 42 | |
| dynamic_two: FAIL (0.18s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (0.03s) | |
| user error (Error 101 while running mir-json on test/conc_eval/traits/dynamic_two.rs) | |
| Use -p '/dynamic_two/' to rerun this test only. | |
| bounds4: FAIL (1.58s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: () (1.41s) | |
| Crux output: | |
| failures: | |
| ---- bounds4/4b079270::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in bounds4/4b079270::f[0] | |
| [Crux] Translation error in bounds4/4b079270::f[0]: error building variant core/4066fdba::option[0]::Option[0]::Some[0]: not enough expressions -- [] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/bounds4/' to rerun this test only. | |
| dict_poly: OK (1.44s) | |
| Compiling and running oracle program (0.18s) | |
| Oracle output: 1 (1.26s) | |
| Crux output: 1 | |
| dict_simple: OK (1.37s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 32 (1.22s) | |
| Crux output: 32 | |
| tyfam: OK (1.37s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 23 (1.23s) | |
| Crux output: 23 | |
| bounds5: FAIL (1.37s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.23s) | |
| Crux output: | |
| failures: | |
| ---- bounds5/e0f4424e::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in bounds5/e0f4424e::f[0] | |
| [Crux] Translation error in bounds5/e0f4424e::f[0]: error building variant core/4066fdba::option[0]::Option[0]::Some[0]: not enough expressions -- [] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/bounds5/' to rerun this test only. | |
| tyfam2: OK (1.41s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 23 (1.27s) | |
| Crux output: 23 | |
| dynamic_med: FAIL (0.17s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (0.03s) | |
| user error (Error 101 while running mir-json on test/conc_eval/traits/dynamic_med.rs) | |
| Use -p '/dynamic_med/' to rerun this test only. | |
| intTest | |
| test0039: OK (1.40s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 7 (1.24s) | |
| Crux output: 7 | |
| test0038: FAIL (1.43s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.29s) | |
| Crux output: | |
| failures: | |
| ---- test0038/e095a59c::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/ptr/mut_ptr.rs:52:37: 52:52: error: in core/4066fdba::ptr[0]::mut_ptr[0]::{impl#0}[0]::is_null[0]::_inst5dab88813bb37c92[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::mut_ptr[0]::{impl#0}[0]::is_null[0]::_inst5dab88813bb37c92[0]: unimplemented cast: Misc | |
| [Crux] ty: TyRawPtr (TyArray (TyInt B32) 4) Mut | |
| [Crux] as: TyRawPtr (TyUint B8) Mut | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/test0038/' to rerun this test only. | |
| tuple | |
| clone_rec: FAIL (1.39s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.25s) | |
| Crux output: | |
| failures: | |
| ---- clone_rec/ecd17fa9::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/tuple/clone_rec.rs:4:17: 4:28: error: in clone_rec/ecd17fa9::f[0] | |
| [Crux] Translation error in clone_rec/ecd17fa9::f[0]: fail or unimp constant: TyTuple [TyInt B32,TyInt B32] (StructRepr [MaybeRepr (BVRepr 32), MaybeRepr (BVRepr 32)]) ConstTuple [ConstInt (I32 3),ConstInt (I32 4)] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/clone_rec/' to rerun this test only. | |
| clone: OK (1.36s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.22s) | |
| Crux output: () | |
| clone_from: FAIL (1.42s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.27s) | |
| Crux output: | |
| failures: | |
| ---- clone_from/9126dd62::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/clone.rs:136:17: 136:31: error: in core/4066fdba::clone[0]::Clone[0]::clone_from[0]::_insta1f0a334420ce0e0[0] | |
| [Crux] Translation error in core/4066fdba::clone[0]::Clone[0]::clone_from[0]::_insta1f0a334420ce0e0[0]: don't know how to generate CloneShim for unknown method core/4066fdba::clone[0]::Clone[0]::clone[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/clone_from/' to rerun this test only. | |
| clone_struct: FAIL (1.39s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.24s) | |
| Crux output: | |
| failures: | |
| ---- clone_struct/52a24041::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/tuple/clone_struct.rs:8:13: 8:22: error: in clone_struct/52a24041::f[0] | |
| [Crux] Translation error in clone_struct/52a24041::f[0]: don't know how to generate CloneShim for unknown method core/4066fdba::clone[0]::Clone[0]::clone[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/clone_struct/' to rerun this test only. | |
| iter | |
| for: FAIL (1.41s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 47 (1.27s) | |
| Crux output: | |
| failures: | |
| ---- for/c15c4981::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:470:54: 470:57 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:921:5: 922:101: error: in core/4066fdba::num[0]::{impl#9}[0]::unchecked_add[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#9}[0]::unchecked_add[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::unchecked_add[0]::_instc5e93708b8ca6e2a[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/iter.for/' to rerun this test only. | |
| sum: FAIL (1.46s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.31s) | |
| Crux output: | |
| failures: | |
| ---- sum/4e872c6b::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/ptr/const_ptr.rs:53:37: 53:54: error: in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::is_null[0]::_instaffa7a8b1157c078[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::is_null[0]::_instaffa7a8b1157c078[0]: unimplemented cast: Misc | |
| [Crux] ty: TyRawPtr (TyUint USize) Immut | |
| [Crux] as: TyRawPtr (TyUint B8) Immut | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/sum/' to rerun this test only. | |
| filter_chain: OK (1.51s) | |
| Compiling and running oracle program (0.17s) | |
| Oracle output: 0 (1.35s) | |
| Crux output: 0 | |
| from_fn: OK (1.38s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.23s) | |
| Crux output: () | |
| peek: FAIL (1.46s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 3 (1.31s) | |
| Crux output: | |
| failures: | |
| ---- peek/13c8e595::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/ptr/const_ptr.rs:53:37: 53:54: error: in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::is_null[0]::_instaffa7a8b1157c078[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::is_null[0]::_instaffa7a8b1157c078[0]: unimplemented cast: Misc | |
| [Crux] ty: TyRawPtr (TyUint USize) Immut | |
| [Crux] as: TyRawPtr (TyUint B8) Immut | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/peek/' to rerun this test only. | |
| zip: FAIL (1.44s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.29s) | |
| Crux output: | |
| failures: | |
| ---- zip/4543a512::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/ptr/const_ptr.rs:53:37: 53:54: error: in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::is_null[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::is_null[0]::_inst1e2825177cd3b608[0]: unimplemented cast: Misc | |
| [Crux] ty: TyRawPtr (TyInt B32) Immut | |
| [Crux] as: TyRawPtr (TyUint B8) Immut | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/zip/' to rerun this test only. | |
| loop: OK (1.34s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 2 (1.20s) | |
| Crux output: 2 | |
| cloned: FAIL (1.40s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 6 (1.25s) | |
| Crux output: | |
| failures: | |
| ---- cloned/da08d733::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/ptr/const_ptr.rs:53:37: 53:54: error: in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::is_null[0]::_instaffa7a8b1157c078[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::is_null[0]::_instaffa7a8b1157c078[0]: unimplemented cast: Misc | |
| [Crux] ty: TyRawPtr (TyUint USize) Immut | |
| [Crux] as: TyRawPtr (TyUint B8) Immut | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/cloned/' to rerun this test only. | |
| str | |
| format_hex: FAIL (1.82s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: true (1.67s) | |
| Crux output: | |
| failures: | |
| ---- format_hex/b88e4167::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/format_hex/' to rerun this test only. | |
| format_int: FAIL (1.82s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: true (1.67s) | |
| Crux output: | |
| failures: | |
| ---- format_int/4a875cdd::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/format_int/' to rerun this test only. | |
| format_struct: FAIL (1.91s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: true (1.75s) | |
| Crux output: | |
| failures: | |
| ---- format_struct/183ba7d2::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/format_struct/' to rerun this test only. | |
| format: FAIL (1.85s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: true (1.70s) | |
| Crux output: | |
| failures: | |
| ---- format/e7c20613::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '$0=="crux-mir.crux concrete..str.format"' to rerun this test only. | |
| to_owned: FAIL (1.40s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: true (1.25s) | |
| Crux output: | |
| failures: | |
| ---- to_owned/bf0d6fd2::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/str/mod.rs:327:33: 327:37: error: in core/4066fdba::str[0]::{impl#0}[0]::as_bytes[0] | |
| [Crux] Translation error in core/4066fdba::str[0]::{impl#0}[0]::as_bytes[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::transmute[0]::_instf78f029a53f4941f[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/to_owned/' to rerun this test only. | |
| string_push: FAIL (1.89s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: true (1.73s) | |
| Crux output: | |
| failures: | |
| ---- string_push/186270ac::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/string_push/' to rerun this test only. | |
| format_array: FAIL (1.93s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: true (1.77s) | |
| Crux output: | |
| failures: | |
| ---- format_array/386388ff::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/format_array/' to rerun this test only. | |
| sync | |
| mutex: FAIL (2.09s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (1.94s) | |
| standalone use of `dyn` is not supported: TyDynamic core/4066fdba::error[0]::Error[0]::_trait56353a7b840403b4[0] | |
| CallStack (from HasCallStack): | |
| error, called at src/Mir/TransTy.hs:230:25 in crux-mir-0.6.0.99-inplace:Mir.TransTy | |
| tyToRepr, called at src/Mir/Trans.hs:810:12 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast', called at src/Mir/Trans.hs:878:5 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast, called at src/Mir/Trans.hs:930:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalRval, called at src/Mir/Trans.hs:1142:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transStatement, called at src/Mir/Trans.hs:1740:68 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| translateBlockBody, called at src/Mir/Trans.hs:1749:28 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| registerBlock, called at src/Mir/Trans.hs:1789:10 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| genFn, called at src/Mir/Trans.hs:1835:24 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transDefine, called at src/Mir/Trans.hs:2272:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transCollection, called at src/Mir/Generate.hs:225:26 in crux-mir-0.6.0.99-inplace:Mir.Generate | |
| translateMIR, called at src/Mir/Language.hs:252:16 in crux-mir-0.6.0.99-inplace:Mir.Language | |
| Use -p '$0=="crux-mir.crux concrete..sync.mutex"' to rerun this test only. | |
| arc_cell: FAIL (1.51s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 4 (1.35s) | |
| Crux output: | |
| failures: | |
| ---- arc_cell/f5026f6d::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:89:31: 89:47 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:965:5: 970:27: error: in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::ctpop[0]::_inst11a9dd2a3cfdbd73[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/arc_cell/' to rerun this test only. | |
| arc: FAIL (1.47s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (1.32s) | |
| Crux output: | |
| failures: | |
| ---- arc/38b1a234::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:89:31: 89:47 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:965:5: 970:27: error: in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::ctpop[0]::_inst11a9dd2a3cfdbd73[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '$0=="crux-mir.crux concrete..sync.arc"' to rerun this test only. | |
| atomic_add: FAIL (1.44s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 6 (1.29s) | |
| Crux output: | |
| failures: | |
| ---- atomic_add/e6bcffed::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/sync/atomic_add.rs:8:22: 8:66: error: in atomic_add/e6bcffed::crux_test[0] | |
| [Crux] Translation error in atomic_add/e6bcffed::crux_test[0]: cannot find static variable alloc$0/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/atomic_add/' to rerun this test only. | |
| rwlock: FAIL (2.11s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.96s) | |
| standalone use of `dyn` is not supported: TyDynamic core/4066fdba::error[0]::Error[0]::_trait56353a7b840403b4[0] | |
| CallStack (from HasCallStack): | |
| error, called at src/Mir/TransTy.hs:230:25 in crux-mir-0.6.0.99-inplace:Mir.TransTy | |
| tyToRepr, called at src/Mir/Trans.hs:810:12 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast', called at src/Mir/Trans.hs:878:5 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast, called at src/Mir/Trans.hs:930:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalRval, called at src/Mir/Trans.hs:1142:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transStatement, called at src/Mir/Trans.hs:1740:68 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| translateBlockBody, called at src/Mir/Trans.hs:1749:28 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| registerBlock, called at src/Mir/Trans.hs:1789:10 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| genFn, called at src/Mir/Trans.hs:1835:24 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transDefine, called at src/Mir/Trans.hs:2272:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transCollection, called at src/Mir/Generate.hs:225:26 in crux-mir-0.6.0.99-inplace:Mir.Generate | |
| translateMIR, called at src/Mir/Language.hs:252:16 in crux-mir-0.6.0.99-inplace:Mir.Language | |
| Use -p '$0=="crux-mir.crux concrete..sync.rwlock"' to rerun this test only. | |
| atomic_cxchg: FAIL (1.46s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 6 (1.31s) | |
| Crux output: | |
| failures: | |
| ---- atomic_cxchg/0014ab56::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/sync/atomic_cxchg.rs:8:22: 8:66: error: in atomic_cxchg/0014ab56::crux_test[0] | |
| [Crux] Translation error in atomic_cxchg/0014ab56::crux_test[0]: cannot find static variable alloc$0/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/atomic_cxchg/' to rerun this test only. | |
| arc_clone: FAIL (1.49s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.34s) | |
| Crux output: | |
| failures: | |
| ---- arc_clone/18ee29b1::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:89:31: 89:47 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:965:5: 970:27: error: in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::ctpop[0]::_inst11a9dd2a3cfdbd73[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/arc_clone/' to rerun this test only. | |
| atomic_swap: FAIL (1.40s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: (2, 1) (1.26s) | |
| Crux output: | |
| failures: | |
| ---- atomic_swap/a9057abb::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/sync/atomic.rs:3010:60: 3010:63: error: in core/4066fdba::sync[0]::atomic[0]::atomic_store[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Translation error in core/4066fdba::sync[0]::atomic[0]::atomic_store[0]::_inst1e2825177cd3b608[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::atomic_store_seqcst[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/atomic_swap/' to rerun this test only. | |
| rwlock_multi: FAIL (2.19s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 3 (2.04s) | |
| standalone use of `dyn` is not supported: TyDynamic core/4066fdba::error[0]::Error[0]::_trait56353a7b840403b4[0] | |
| CallStack (from HasCallStack): | |
| error, called at src/Mir/TransTy.hs:230:25 in crux-mir-0.6.0.99-inplace:Mir.TransTy | |
| tyToRepr, called at src/Mir/Trans.hs:810:12 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast', called at src/Mir/Trans.hs:878:5 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast, called at src/Mir/Trans.hs:930:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalRval, called at src/Mir/Trans.hs:1142:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transStatement, called at src/Mir/Trans.hs:1740:68 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| translateBlockBody, called at src/Mir/Trans.hs:1749:28 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| registerBlock, called at src/Mir/Trans.hs:1789:10 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| genFn, called at src/Mir/Trans.hs:1835:24 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transDefine, called at src/Mir/Trans.hs:2272:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transCollection, called at src/Mir/Generate.hs:225:26 in crux-mir-0.6.0.99-inplace:Mir.Generate | |
| translateMIR, called at src/Mir/Language.hs:252:16 in crux-mir-0.6.0.99-inplace:Mir.Language | |
| Use -p '/rwlock_multi/' to rerun this test only. | |
| atomic_fence: FAIL (1.45s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.30s) | |
| Crux output: | |
| failures: | |
| ---- atomic_fence/49ba31f4::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/sync/atomic.rs:3010:60: 3010:63: error: in core/4066fdba::sync[0]::atomic[0]::atomic_store[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Translation error in core/4066fdba::sync[0]::atomic[0]::atomic_store[0]::_inst1e2825177cd3b608[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::atomic_store_seqcst[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/atomic_fence/' to rerun this test only. | |
| mutex_multi: FAIL (2.16s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 3 (2.01s) | |
| standalone use of `dyn` is not supported: TyDynamic core/4066fdba::error[0]::Error[0]::_trait56353a7b840403b4[0] | |
| CallStack (from HasCallStack): | |
| error, called at src/Mir/TransTy.hs:230:25 in crux-mir-0.6.0.99-inplace:Mir.TransTy | |
| tyToRepr, called at src/Mir/Trans.hs:810:12 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast', called at src/Mir/Trans.hs:878:5 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast, called at src/Mir/Trans.hs:930:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalRval, called at src/Mir/Trans.hs:1142:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transStatement, called at src/Mir/Trans.hs:1740:68 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| translateBlockBody, called at src/Mir/Trans.hs:1749:28 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| registerBlock, called at src/Mir/Trans.hs:1789:10 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| genFn, called at src/Mir/Trans.hs:1835:24 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transDefine, called at src/Mir/Trans.hs:2272:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transCollection, called at src/Mir/Generate.hs:225:26 in crux-mir-0.6.0.99-inplace:Mir.Generate | |
| translateMIR, called at src/Mir/Language.hs:252:16 in crux-mir-0.6.0.99-inplace:Mir.Language | |
| Use -p '/mutex_multi/' to rerun this test only. | |
| consts | |
| struct_val: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: Foo { x: true } (1.27s) | |
| Crux output: Foo { x: true } | |
| struct_unit: FAIL (1.37s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: Err(Foo { x: () }) (1.23s) | |
| Crux output: | |
| failures: | |
| ---- struct_unit/7e69aa53::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in struct_unit/7e69aa53::crux_test[0] | |
| [Crux] Translation error in struct_unit/7e69aa53::crux_test[0]: error building variant core/4066fdba::result[0]::Result[0]::Err[0]: not enough expressions -- [] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/struct_unit/' to rerun this test only. | |
| local_key: FAIL (1.37s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (1.23s) | |
| Crux output: | |
| failures: | |
| ---- local_key/66e3d1ae::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/consts/local_key.rs:22:78: 22:93: error: in local_key/66e3d1ae::crux_test[0] | |
| [Crux] Translation error in local_key/66e3d1ae::crux_test[0]: cannot find static variable alloc$0/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/local_key/' to rerun this test only. | |
| fn_def: FAIL (1.36s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 1 (1.22s) | |
| user error (JSON Decoding of test/conc_eval/consts/fn_def.all.mir failed: Error in $.fns[0].body.blocks[0].block.terminator.func.data.rendered: parseJSON - bad rendered constant kind: Just (String "fn_ptr")) | |
| Use -p '/fn_def/' to rerun this test only. | |
| enum_val: OK (1.37s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: None (1.23s) | |
| Crux output: None | |
| crypto | |
| add: FAIL (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: true (1.26s) | |
| Crux output: | |
| failures: | |
| ---- add/a2fc467c::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/num/uint_macros.rs:470:54: 470:57 !lib/core/src/num/mod.rs:965:5: 970:27: error: in core/4066fdba::num[0]::{impl#12}[0]::unchecked_add[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#12}[0]::unchecked_add[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::unchecked_add[0]::_instaffa7a8b1157c078[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '$0=="crux-mir.crux concrete..crypto.add"' to rerun this test only. | |
| add_noL: FAIL (1.41s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: false (1.26s) | |
| Crux output: | |
| failures: | |
| ---- add_noL/2a0c8b5c::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/num/uint_macros.rs:470:54: 470:57 !lib/core/src/num/mod.rs:965:5: 970:27: error: in core/4066fdba::num[0]::{impl#12}[0]::unchecked_add[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#12}[0]::unchecked_add[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::unchecked_add[0]::_instaffa7a8b1157c078[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/add_noL/' to rerun this test only. | |
| cell | |
| cell: FAIL (1.38s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.24s) | |
| Crux output: | |
| failures: | |
| ---- cell/653a630d::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/cell.rs:413:57: 413:60: error: in core/4066fdba::cell[0]::{impl#9}[0]::replace[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Translation error in core/4066fdba::cell[0]::{impl#9}[0]::replace[0]::_inst1e2825177cd3b608[0]: callExp: Don't know how to call core/4066fdba::mem[0]::replace[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/cell.cell/' to rerun this test only. | |
| ref_cell: FAIL (1.80s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.65s) | |
| Crux output: | |
| failures: | |
| ---- ref_cell/4742eea6::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '$0=="crux-mir.crux concrete..cell.ref_cell"' to rerun this test only. | |
| ref_cell2: FAIL (1.91s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 2 (1.76s) | |
| Crux output: | |
| failures: | |
| ---- ref_cell2/0327967a::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/ref_cell2/' to rerun this test only. | |
| fnptr | |
| call: OK (1.47s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.32s) | |
| Crux output: 2 | |
| field: OK (1.50s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.35s) | |
| Crux output: 2 | |
| make: OK (1.49s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 0 (1.34s) | |
| Crux output: 0 | |
| custom: rustc compilation failed for custom | |
| error output: | |
| error[E0432]: unresolved import `core` | |
| --> test/conc_eval/fnptr/custom.rs:2:5 | |
| | | |
| 2 | use core::mem; | |
| | ^^^^ maybe a missing crate `core`? | |
| | | |
| = help: consider adding `extern crate core` to use the `core` crate | |
| error: aborting due to previous error | |
| For more information about this error, try `rustc --explain E0432`. | |
| FAIL (expected: taking address of an overridden function) (0.06s) | |
| Compiling and running oracle program (0.06s) | |
| test/Test.hs:109: | |
| failed to compile and run | |
| (expected failure) | |
| num | |
| overflow: FAIL (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.27s) | |
| Crux output: | |
| failures: | |
| ---- overflow/3147857b::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/num/overflow.rs:5:40: 5:50: error: in overflow/3147857b::crux_test[0] | |
| [Crux] Translation error in overflow/3147857b::crux_test[0]: cannot find static variable alloc$0/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/num.overflow/' to rerun this test only. | |
| from_bytes: FAIL (1.43s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.28s) | |
| Crux output: | |
| failures: | |
| ---- from_bytes/0b010b9d::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:2417:37: 2417:42 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:890:5: 891:49: error: in core/4066fdba::num[0]::{impl#8}[0]::from_ne_bytes[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#8}[0]::from_ne_bytes[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::transmute[0]::_inst850c595be4adc72f[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/from_bytes/' to rerun this test only. | |
| saturate: FAIL (1.43s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.28s) | |
| Crux output: | |
| failures: | |
| ---- saturate/c73def0d::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:1022:46: 1022:49 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:305:5: 306:27: error: in core/4066fdba::num[0]::{impl#7}[0]::saturating_add[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#7}[0]::saturating_add[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::saturating_add[0]::_instaddce72e1232152c[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/saturate/' to rerun this test only. | |
| prim | |
| bool: OK (1.35s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: false (1.21s) | |
| Crux output: false | |
| shift3: OK (1.43s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: -9223372036854775808 (1.28s) | |
| Crux output: -9223372036854775808 | |
| div: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 4 (1.27s) | |
| Crux output: 4 | |
| ge: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: true (1.27s) | |
| Crux output: true | |
| add1: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.27s) | |
| Crux output: 2 | |
| shift_exceeding: rustc compilation failed for shift_exceeding | |
| error output: | |
| error[E0425]: cannot find function `catch_unwind` in module `panic` | |
| --> test/conc_eval/prim/shift_exceeding.rs:14:25 | |
| | | |
| 14 | let result = panic::catch_unwind(|| { | |
| | ^^^^^^^^^^^^ not found in `panic` | |
| | | |
| help: consider importing this function | |
| | | |
| 3 | use std::panic::catch_unwind; | |
| | | |
| help: if you import `catch_unwind`, refer to it directly | |
| | | |
| 14 - let result = panic::catch_unwind(|| { | |
| 14 + let result = catch_unwind(|| { | |
| | | |
| warning: lint `exceeding_bitshifts` has been renamed to `arithmetic_overflow` | |
| --> test/conc_eval/prim/shift_exceeding.rs:4:9 | |
| | | |
| 4 | #[allow(exceeding_bitshifts)] | |
| | ^^^^^^^^^^^^^^^^^^^ help: use the new name: `arithmetic_overflow` | |
| | | |
| = note: `#[warn(renamed_and_removed_lints)]` on by default | |
| error: aborting due to previous error; 1 warning emitted | |
| For more information about this error, try `rustc --explain E0425`. | |
| FAIL (expected: Should panic, but doesn't) (0.06s) | |
| Compiling and running oracle program (0.06s) | |
| test/Test.hs:109: | |
| failed to compile and run | |
| (expected failure) | |
| char_from_u32: FAIL (1.41s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 'A' (1.26s) | |
| Crux output: | |
| failures: | |
| ---- char_from_u32/36585810::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/char/convert.rs:215:31: 215:32: error: in core/4066fdba::char[0]::convert[0]::char_try_from_u32[0] | |
| [Crux] Translation error in core/4066fdba::char[0]::convert[0]::char_try_from_u32[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::transmute[0]::_instdc3291f36c45d6de[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/char_from_u32/' to rerun this test only. | |
| ffs: FAIL (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: true (1.27s) | |
| Crux output: | |
| failures: | |
| ---- ffs/c5114da4::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/int_macros.rs:460:54: 460:57 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:251:5: 253:45: error: in core/4066fdba::num[0]::{impl#3}[0]::unchecked_add[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#3}[0]::unchecked_add[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::unchecked_add[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/prim.ffs/' to rerun this test only. | |
| mut_arg: OK (1.35s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 1 (1.21s) | |
| Crux output: 1 | |
| litstring: FAIL (1.36s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: true (1.22s) | |
| Crux output: | |
| failures: | |
| ---- litstring/3e92e693::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/str/mod.rs:327:33: 327:37: error: in core/4066fdba::str[0]::{impl#0}[0]::as_bytes[0] | |
| [Crux] Translation error in core/4066fdba::str[0]::{impl#0}[0]::as_bytes[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::transmute[0]::_instf78f029a53f4941f[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/litstring/' to rerun this test only. | |
| lit: FAIL (1.38s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: false (1.24s) | |
| Crux output: | |
| failures: | |
| ---- lit/f7ce1583::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in lit/f7ce1583::crux_test[0] | |
| [Crux] Translation error in lit/f7ce1583::crux_test[0]: fail or unimp constant: TyTuple [TyBool,TyBool] (StructRepr [MaybeRepr BoolRepr, MaybeRepr BoolRepr]) ConstTuple [ConstBool True,ConstBool True] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '$0=="crux-mir.crux concrete..prim.lit"' to rerun this test only. | |
| litbstring: OK (1.36s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: true (1.22s) | |
| Crux output: true | |
| shift1: OK (1.35s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 2 (1.21s) | |
| Crux output: 2 | |
| shift2: OK (1.34s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 2 (1.20s) | |
| Crux output: 2 | |
| shift4: OK (1.37s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: -9223372036854775808 (1.23s) | |
| Crux output: -9223372036854775808 | |
| mut: OK (1.36s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 14 (1.22s) | |
| Crux output: 14 | |
| wrapping_sub: OK (1.35s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: true (1.21s) | |
| Crux output: true | |
| impl | |
| self: OK (1.36s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 42 (1.22s) | |
| Crux output: 42 | |
| simple: OK (1.35s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 42 (1.21s) | |
| Crux output: 42 | |
| self_mut: OK (1.37s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 42 (1.23s) | |
| Crux output: 42 | |
| box | |
| new: FAIL (1.47s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.33s) | |
| Crux output: | |
| failures: | |
| ---- new/7ae66e33::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:89:31: 89:47 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:965:5: 970:27: error: in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::ctpop[0]::_inst11a9dd2a3cfdbd73[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/box.new/' to rerun this test only. | |
| mut_ref: FAIL (1.49s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.34s) | |
| Crux output: | |
| failures: | |
| ---- mut_ref/f78a34e7::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:89:31: 89:47 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:965:5: 970:27: error: in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::ctpop[0]::_inst11a9dd2a3cfdbd73[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/box.mut_ref/' to rerun this test only. | |
| mut: FAIL (1.48s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.33s) | |
| Crux output: | |
| failures: | |
| ---- mut/edd70056::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:89:31: 89:47 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:965:5: 970:27: error: in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::ctpop[0]::_inst11a9dd2a3cfdbd73[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '$0=="crux-mir.crux concrete..box.mut"' to rerun this test only. | |
| unsize: FAIL (1.49s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.35s) | |
| Crux output: | |
| failures: | |
| ---- unsize/ef9e0d91::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:89:31: 89:47 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:965:5: 970:27: error: in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::ctpop[0]::_inst11a9dd2a3cfdbd73[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/box.unsize/' to rerun this test only. | |
| struct: FAIL (1.49s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (1.34s) | |
| Crux output: | |
| failures: | |
| ---- struct/8fded446::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:89:31: 89:47 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:965:5: 970:27: error: in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::ctpop[0]::_inst11a9dd2a3cfdbd73[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/box.struct/' to rerun this test only. | |
| ptr | |
| is_null_slice: FAIL (expected: can't unsize null pointers) (1.43s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: (false, true) (1.28s) | |
| Crux output: | |
| failures: | |
| ---- is_null_slice/31fc8c0c::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/ptr/is_null_slice.rs:6:13: 6:20: error: in is_null_slice/31fc8c0c::crux_test[0] | |
| [Crux] Translation error in is_null_slice/31fc8c0c::crux_test[0]: cannot find static variable alloc$0/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| (expected failure) | |
| struct_eq: OK (1.41s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.27s) | |
| Crux output: () | |
| read_write: OK (1.45s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: [1, 3, 1] (1.30s) | |
| Crux output: [1, 3, 1] | |
| offset_mut: FAIL (1.42s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 3 (1.28s) | |
| Crux output: | |
| failures: | |
| ---- offset_mut/bb64cc5d::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/ptr/mut_ptr.rs:487:43: 487:48: error: in core/4066fdba::ptr[0]::mut_ptr[0]::{impl#0}[0]::offset[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::mut_ptr[0]::{impl#0}[0]::offset[0]::_inst1e2825177cd3b608[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::offset[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/offset_mut/' to rerun this test only. | |
| copy: OK (1.44s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: [1, 2, 3, 1, 2, 3] (1.29s) | |
| Crux output: [1, 2, 3, 1, 2, 3] | |
| unsize_slice: FAIL (1.42s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: (1, 2) (1.28s) | |
| Crux output: | |
| failures: | |
| ---- unsize_slice/2aa7d255::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/ptr/const_ptr.rs:473:43: 473:48: error: in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::offset[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::offset[0]::_inst1e2825177cd3b608[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::offset[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/unsize_slice/' to rerun this test only. | |
| dangling_eq: FAIL (1.43s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.29s) | |
| Crux output: | |
| failures: | |
| ---- dangling_eq/fd9e920d::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/ptr/mod.rs:599:29: 599:33: error: in core/4066fdba::ptr[0]::invalid_mut[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::invalid_mut[0]::_inst1e2825177cd3b608[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::transmute[0]::_inst102627303ebf2823[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/dangling_eq/' to rerun this test only. | |
| cast_eq: OK (1.41s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.26s) | |
| Crux output: () | |
| offset_from: FAIL (1.42s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: -2 (1.28s) | |
| Crux output: | |
| failures: | |
| ---- offset_from/2e67629b::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/ptr/const_ptr.rs:706:52: 706:58: error: in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::offset_from[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::offset_from[0]::_inst1e2825177cd3b608[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::ptr_offset_from[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/offset_from/' to rerun this test only. | |
| null_eq: FAIL (1.46s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (1.31s) | |
| Crux output: | |
| failures: | |
| ---- null_eq/0c1db7ec::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/ptr/mod.rs:568:29: 568:33: error: in core/4066fdba::ptr[0]::invalid[0]::_instf59dc84daa91a404[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::invalid[0]::_instf59dc84daa91a404[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::transmute[0]::_insta5d0a99e3b08f3bd[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/null_eq/' to rerun this test only. | |
| coerce_unsized: FAIL (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: (1, 2) (1.28s) | |
| Crux output: | |
| failures: | |
| ---- coerce_unsized/ba12a486::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/ptr/const_ptr.rs:473:43: 473:48: error: in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::offset[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::offset[0]::_inst1e2825177cd3b608[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::offset[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/coerce_unsized/' to rerun this test only. | |
| offset: FAIL (1.43s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 3 (1.29s) | |
| Crux output: | |
| failures: | |
| ---- offset/10e9df14::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/ptr/const_ptr.rs:473:43: 473:48: error: in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::offset[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::offset[0]::_inst1e2825177cd3b608[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::offset[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '$0=="crux-mir.crux concrete..ptr.offset"' to rerun this test only. | |
| is_null: FAIL (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: (false, true) (1.28s) | |
| Crux output: | |
| failures: | |
| ---- is_null/b0e382ce::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/ptr/is_null.rs:5:13: 5:15: error: in is_null/b0e382ce::crux_test[0] | |
| [Crux] Translation error in is_null/b0e382ce::crux_test[0]: cannot find static variable alloc$0/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '$0=="crux-mir.crux concrete..ptr.is_null"' to rerun this test only. | |
| valid_eq: OK (1.41s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.27s) | |
| Crux output: () | |
| ops | |
| deref2: OK (1.44s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.30s) | |
| Crux output: () | |
| index2: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.27s) | |
| Crux output: () | |
| arith1: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.27s) | |
| Crux output: () | |
| index3: OK (1.45s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.30s) | |
| Crux output: () | |
| deref1: OK (1.43s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.28s) | |
| Crux output: () | |
| index1: OK (1.41s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.26s) | |
| Crux output: () | |
| deref3: OK (1.45s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.30s) | |
| Crux output: () | |
| statics | |
| promoted_fn: FAIL (1.50s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (1.35s) | |
| Crux output: | |
| failures: | |
| ---- promoted_fn/e7dbfe54::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/statics/promoted_fn.rs:4:13: 4:16: error: in promoted_fn/e7dbfe54::crux_test[0] | |
| [Crux] Translation error in promoted_fn/e7dbfe54::crux_test[0]: cannot find static variable alloc$1/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/promoted_fn/' to rerun this test only. | |
| promoted_static: OK (1.48s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (1.32s) | |
| Crux output: 1 | |
| io | |
| cursor_write2: FAIL (2.17s) | |
| Compiling and running oracle program (0.17s) | |
| Oracle output: 0 (2.00s) | |
| standalone use of `dyn` is not supported: TyDynamic core/4066fdba::error[0]::Error[0]::_trait56353a7b840403b4[0] | |
| CallStack (from HasCallStack): | |
| error, called at src/Mir/TransTy.hs:230:25 in crux-mir-0.6.0.99-inplace:Mir.TransTy | |
| tyToRepr, called at src/Mir/Trans.hs:810:12 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast', called at src/Mir/Trans.hs:878:5 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast, called at src/Mir/Trans.hs:930:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalRval, called at src/Mir/Trans.hs:1142:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transStatement, called at src/Mir/Trans.hs:1740:68 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| translateBlockBody, called at src/Mir/Trans.hs:1749:28 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| registerBlock, called at src/Mir/Trans.hs:1789:10 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| genFn, called at src/Mir/Trans.hs:1835:24 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transDefine, called at src/Mir/Trans.hs:2272:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transCollection, called at src/Mir/Generate.hs:225:26 in crux-mir-0.6.0.99-inplace:Mir.Generate | |
| translateMIR, called at src/Mir/Language.hs:252:16 in crux-mir-0.6.0.99-inplace:Mir.Language | |
| Use -p '/cursor_write2/' to rerun this test only. | |
| cursor_write: FAIL (1.90s) | |
| Compiling and running oracle program (0.17s) | |
| Oracle output: 0 (1.72s) | |
| standalone use of `dyn` is not supported: TyDynamic core/4066fdba::error[0]::Error[0]::_trait56353a7b840403b4[0] | |
| CallStack (from HasCallStack): | |
| error, called at src/Mir/TransTy.hs:230:25 in crux-mir-0.6.0.99-inplace:Mir.TransTy | |
| tyToRepr, called at src/Mir/Trans.hs:810:12 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast', called at src/Mir/Trans.hs:878:5 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast, called at src/Mir/Trans.hs:930:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalRval, called at src/Mir/Trans.hs:1142:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transStatement, called at src/Mir/Trans.hs:1740:68 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| translateBlockBody, called at src/Mir/Trans.hs:1749:28 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| registerBlock, called at src/Mir/Trans.hs:1789:10 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| genFn, called at src/Mir/Trans.hs:1835:24 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transDefine, called at src/Mir/Trans.hs:2272:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transCollection, called at src/Mir/Generate.hs:225:26 in crux-mir-0.6.0.99-inplace:Mir.Generate | |
| translateMIR, called at src/Mir/Language.hs:252:16 in crux-mir-0.6.0.99-inplace:Mir.Language | |
| Use -p '$0=="crux-mir.crux concrete..io.cursor_write"' to rerun this test only. | |
| cursor_read: FAIL (1.88s) | |
| Compiling and running oracle program (0.17s) | |
| Oracle output: 0 (1.71s) | |
| standalone use of `dyn` is not supported: TyDynamic core/4066fdba::error[0]::Error[0]::_trait56353a7b840403b4[0] | |
| CallStack (from HasCallStack): | |
| error, called at src/Mir/TransTy.hs:230:25 in crux-mir-0.6.0.99-inplace:Mir.TransTy | |
| tyToRepr, called at src/Mir/Trans.hs:810:12 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast', called at src/Mir/Trans.hs:878:5 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast, called at src/Mir/Trans.hs:930:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalRval, called at src/Mir/Trans.hs:1142:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transStatement, called at src/Mir/Trans.hs:1740:68 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| translateBlockBody, called at src/Mir/Trans.hs:1749:28 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| registerBlock, called at src/Mir/Trans.hs:1789:10 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| genFn, called at src/Mir/Trans.hs:1835:24 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transDefine, called at src/Mir/Trans.hs:2272:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transCollection, called at src/Mir/Generate.hs:225:26 in crux-mir-0.6.0.99-inplace:Mir.Generate | |
| translateMIR, called at src/Mir/Language.hs:252:16 in crux-mir-0.6.0.99-inplace:Mir.Language | |
| Use -p '/io.cursor_read/' to rerun this test only. | |
| mem | |
| maybe_uninit: FAIL (1.46s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (1.31s) | |
| Crux output: | |
| failures: | |
| ---- maybe_uninit/779fc73a::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in core/4066fdba::mem[0]::maybe_uninit[0]::{impl#2}[0]::assume_init[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Translation error in core/4066fdba::mem[0]::maybe_uninit[0]::{impl#2}[0]::assume_init[0]::_inst1e2825177cd3b608[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::assert_inhabited[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '$0=="crux-mir.crux concrete..mem.maybe_uninit"' to rerun this test only. | |
| maybe_uninit_array_cast: FAIL (1.48s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: [1, 2] (1.32s) | |
| Crux output: | |
| failures: | |
| ---- maybe_uninit_array_cast/de5c39f6::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/ptr/mut_ptr.rs:487:43: 487:48: error: in core/4066fdba::ptr[0]::mut_ptr[0]::{impl#0}[0]::offset[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::mut_ptr[0]::{impl#0}[0]::offset[0]::_inst1e2825177cd3b608[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::offset[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/maybe_uninit_array_cast/' to rerun this test only. | |
| time | |
| instant: FAIL (2.11s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.96s) | |
| standalone use of `dyn` is not supported: TyDynamic core/4066fdba::error[0]::Error[0]::_trait56353a7b840403b4[0] | |
| CallStack (from HasCallStack): | |
| error, called at src/Mir/TransTy.hs:230:25 in crux-mir-0.6.0.99-inplace:Mir.TransTy | |
| tyToRepr, called at src/Mir/Trans.hs:810:12 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast', called at src/Mir/Trans.hs:878:5 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast, called at src/Mir/Trans.hs:930:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalRval, called at src/Mir/Trans.hs:1142:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transStatement, called at src/Mir/Trans.hs:1740:68 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| translateBlockBody, called at src/Mir/Trans.hs:1749:28 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| registerBlock, called at src/Mir/Trans.hs:1789:10 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| genFn, called at src/Mir/Trans.hs:1835:24 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transDefine, called at src/Mir/Trans.hs:2272:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transCollection, called at src/Mir/Generate.hs:225:26 in crux-mir-0.6.0.99-inplace:Mir.Generate | |
| translateMIR, called at src/Mir/Language.hs:252:16 in crux-mir-0.6.0.99-inplace:Mir.Language | |
| Use -p '/instant/' to rerun this test only. | |
| struct | |
| field_order: OK (1.44s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.29s) | |
| Crux output: () | |
| arg: OK (1.44s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 42 (1.28s) | |
| Crux output: 42 | |
| tup: OK (1.44s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: () (1.28s) | |
| Crux output: () | |
| proj: OK (1.38s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 42 (1.23s) | |
| Crux output: 42 | |
| ret: OK (1.37s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: S { x: 42, y: 120 } (1.23s) | |
| Crux output: S { x: 42, y: 120 } | |
| repr_transparent: FAIL (1.48s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 6 (1.32s) | |
| Crux output: | |
| failures: | |
| ---- repr_transparent/a1914669::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/ptr/const_ptr.rs:61:9: 61:18: error: in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::cast[0]::_inst1fe84093a10a77db[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::cast[0]::_inst1fe84093a10a77db[0]: unimplemented cast: Misc | |
| [Crux] ty: TyRawPtr (TyInt B32) Immut | |
| [Crux] as: TyRawPtr (TyArray (TyInt B32) 2) Immut | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '$0=="crux-mir.crux concrete..struct.repr_transparent"' to rerun this test only. | |
| repr_transparent_const: OK (1.43s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 124 (1.28s) | |
| Crux output: 124 | |
| dyn | |
| assoc_ty: OK (1.36s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 100 (1.22s) | |
| Crux output: 100 | |
| trait_param: OK (1.36s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 100 (1.22s) | |
| Crux output: 100 | |
| plain_trait: OK (1.37s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 100 (1.23s) | |
| Crux output: 100 | |
| inherit: FAIL (1.40s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 4 (1.26s) | |
| Crux output: | |
| failures: | |
| ---- inherit/d1d6a53b::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/dyn/inherit.rs:20:13: 20:16: error: in inherit/d1d6a53b::crux_test[0] | |
| [Crux] Translation error in inherit/d1d6a53b::crux_test[0]: cannot find static variable alloc$0/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/inherit/' to rerun this test only. | |
| stdlib | |
| option: OK (1.38s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: true (1.23s) | |
| Crux output: true | |
| option2: OK (1.41s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 0 (1.27s) | |
| Crux output: 0 | |
| result: OK (1.38s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 27 (1.24s) | |
| Crux output: 27 | |
| default: OK (1.38s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: true (1.24s) | |
| Crux output: true | |
| cvt: OK (1.34s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 0 (1.20s) | |
| Crux output: 0 | |
| range: OK (1.35s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 10 (1.21s) | |
| Crux output: 10 | |
| poly: OK (1.36s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 1 (1.22s) | |
| Crux output: 1 | |
| result_interior: OK (1.38s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 3 (1.24s) | |
| Crux output: 3 | |
| default_impl: OK (1.34s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.20s) | |
| Crux output: () | |
| option3: OK (1.37s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 27 (1.23s) | |
| Crux output: 27 | |
| teq: OK (1.37s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: false (1.23s) | |
| Crux output: false | |
| array | |
| wick2: OK (1.46s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: true (1.32s) | |
| Crux output: true | |
| arg: OK (1.44s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.29s) | |
| Crux output: 2 | |
| iter: FAIL (1.46s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 3 (1.31s) | |
| Crux output: | |
| failures: | |
| ---- iter/794350c6::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/ptr/const_ptr.rs:53:37: 53:54: error: in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::is_null[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::is_null[0]::_inst1e2825177cd3b608[0]: unimplemented cast: Misc | |
| [Crux] ty: TyRawPtr (TyInt B32) Immut | |
| [Crux] as: TyRawPtr (TyUint B8) Immut | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/array.iter/' to rerun this test only. | |
| mk_and_proj: OK (1.39s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 42 (1.24s) | |
| Crux output: 42 | |
| wick3: FAIL (expected: needs Vec data structure from stdlib) (0.22s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: true (0.07s) | |
| user error (Error 101 while running mir-json on test/conc_eval/array/wick3.rs) | |
| (expected failure) | |
| clone: FAIL (1.39s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.24s) | |
| Crux output: | |
| failures: | |
| ---- clone/077ae3ab::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/ptr/const_ptr.rs:61:9: 61:18: error: in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::cast[0]::_inst6cd22c7344b2c333[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::const_ptr[0]::{impl#0}[0]::cast[0]::_inst6cd22c7344b2c333[0]: unimplemented cast: Misc | |
| [Crux] ty: TyRawPtr (TyInt B32) Immut | |
| [Crux] as: TyRawPtr (TyArray (TyInt B32) 3) Immut | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/array.clone/' to rerun this test only. | |
| wick1: FAIL (expected: needs Vec data structure from stdlib) (0.20s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: true (0.04s) | |
| user error (Error 101 while running mir-json on test/conc_eval/array/wick1.rs) | |
| (expected failure) | |
| mut_index: FAIL (1.82s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 7 (1.68s) | |
| Crux output: | |
| failures: | |
| ---- mut_index/66ce1f11::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/mut_index/' to rerun this test only. | |
| mut_arg: OK (1.38s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 42 (1.24s) | |
| Crux output: 42 | |
| const: OK (1.42s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 1 (1.28s) | |
| Crux output: 1 | |
| from_slice: FAIL (2.00s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.86s) | |
| Crux output: | |
| failures: | |
| ---- from_slice/fd42c804::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/array.from_slice/' to rerun this test only. | |
| const_impl: OK (1.44s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 5 (1.29s) | |
| Crux output: 5 | |
| enum | |
| match: OK (1.43s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 42 (1.27s) | |
| Crux output: 42 | |
| field_order: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.27s) | |
| Crux output: () | |
| mixed_discrs: OK (1.45s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: () (1.28s) | |
| Crux output: () | |
| arg: OK (1.38s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 0 (1.22s) | |
| Crux output: 0 | |
| arg2: rustc compilation failed for arg2 | |
| error output: | |
| error[E0518]: attribute should be applied to function or closure | |
| --> test/conc_eval/enum/arg2.rs:3:5 | |
| | | |
| 3 | #[inline(never)] | |
| | ^^^^^^^^^^^^^^^^ | |
| 4 | A(u8), | |
| | ----- not a function or closure | |
| error[E0518]: attribute should be applied to function or closure | |
| --> test/conc_eval/enum/arg2.rs:5:5 | |
| | | |
| 5 | #[inline(never)] | |
| | ^^^^^^^^^^^^^^^^ | |
| 6 | B(i32,i32), | |
| | ---------- not a function or closure | |
| error: aborting due to 2 previous errors | |
| For more information about this error, try `rustc --explain E0518`. | |
| FAIL (0.05s) | |
| Compiling and running oracle program (0.05s) | |
| test/Test.hs:109: | |
| failed to compile and run | |
| Use -p '/arg2/' to rerun this test only. | |
| cow: FAIL (1.42s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 200 (1.27s) | |
| Crux output: | |
| failures: | |
| ---- cow/f55da345::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/enum/cow.rs:6:35: 6:50: error: in cow/f55da345::crux_test[0] | |
| [Crux] Translation error in cow/f55da345::crux_test[0]: callExp: Don't know how to call alloc/2e88dd27::slice[0]::{impl#0}[0]::to_vec[0]::_instaddce72e1232152c[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/cow/' to rerun this test only. | |
| ret: OK (1.43s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: (A(42), B { x: 42 }, C) (1.28s) | |
| Crux output: (A(42), B { x: 42 }, C) | |
| eq: FAIL (1.44s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.29s) | |
| Crux output: | |
| failures: | |
| ---- eq/4dddd583::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/enum/eq.rs:9:17: 9:21: error: in eq/4dddd583::f[0] | |
| [Crux] Translation error in eq/4dddd583::f[0]: cannot find static variable alloc$0/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/enum.eq/' to rerun this test only. | |
| cmp: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: -23 (1.27s) | |
| Crux output: -23 | |
| inner: OK (1.41s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 4 (1.27s) | |
| Crux output: 4 | |
| vec | |
| drop: FAIL (1.53s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.38s) | |
| Crux output: | |
| failures: | |
| ---- drop/5fda7f30::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:89:31: 89:47 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:965:5: 970:27: error: in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::ctpop[0]::_inst11a9dd2a3cfdbd73[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/drop/' to rerun this test only. | |
| set_len: FAIL (1.54s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.39s) | |
| Crux output: | |
| failures: | |
| ---- set_len/0d570f4f::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:89:31: 89:47 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:965:5: 970:27: error: in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::ctpop[0]::_inst11a9dd2a3cfdbd73[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/set_len/' to rerun this test only. | |
| push: FAIL (1.68s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: (1, 2) (1.52s) | |
| Crux output: | |
| failures: | |
| ---- push/1e1dd999::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in alloc/2e88dd27::raw_vec[0]::{impl#2}[0]::grow_amortized[0]::_inst6708c5c8c5ed40f8[0] | |
| [Crux] Translation error in alloc/2e88dd27::raw_vec[0]::{impl#2}[0]::grow_amortized[0]::_inst6708c5c8c5ed40f8[0]: callExp: Don't know how to call core/4066fdba::option[0]::{impl#0}[0]::ok_or[0]::_instb640de1649d04e9b[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/vec.push/' to rerun this test only. | |
| extend: FAIL (0.30s) | |
| Compiling and running oracle program (0.17s) | |
| Oracle output: (1, 10) (0.13s) | |
| Crux output: | |
| failures: | |
| ---- extend/de992584::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in alloc/2e88dd27::raw_vec[0]::{impl#2}[0]::grow_amortized[0]::_inst6708c5c8c5ed40f8[0] | |
| [Crux] Translation error in alloc/2e88dd27::raw_vec[0]::{impl#2}[0]::grow_amortized[0]::_inst6708c5c8c5ed40f8[0]: callExp: Don't know how to call core/4066fdba::option[0]::{impl#0}[0]::ok_or[0]::_instb640de1649d04e9b[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '$0=="crux-mir.crux concrete..vec.extend"' to rerun this test only. | |
| collect: FAIL (2.40s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 45 (2.23s) | |
| Crux output: | |
| failures: | |
| ---- collect/d16176b5::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/collect/' to rerun this test only. | |
| extend_trusted_len: FAIL (2.10s) | |
| Compiling and running oracle program (0.17s) | |
| Oracle output: (1, 10) (1.93s) | |
| Crux output: | |
| failures: | |
| ---- extend_trusted_len/4a68c13a::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/extend_trusted_len/' to rerun this test only. | |
| from_elem_zero: FAIL (0.21s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 0 (0.06s) | |
| user error (Error 101 while running mir-json on test/conc_eval/vec/from_elem_zero.rs) | |
| Use -p '/from_elem_zero/' to rerun this test only. | |
| clos | |
| promoted: FAIL (1.38s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 33 (1.24s) | |
| Crux output: | |
| failures: | |
| ---- promoted/19368140::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/clos/promoted.rs:15:9: 15:11: error: in promoted/19368140::f[0] | |
| [Crux] Translation error in promoted/19368140::f[0]: cannot find static variable alloc$0/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/clos.promoted/' to rerun this test only. | |
| as_fn_ptr: FAIL (expected: ClosureFnPointer cast) (1.40s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 1 (1.26s) | |
| Crux output: | |
| failures: | |
| ---- as_fn_ptr/bc1221dd::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/clos/as_fn_ptr.rs:9:13: 9:19: error: in as_fn_ptr/bc1221dd::crux_test[0] | |
| [Crux] Translation error in as_fn_ptr/bc1221dd::crux_test[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [], _fsreturn_ty = TyInt B32, _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| (expected failure) | |
| fnptr_fnmut: OK (1.43s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 4 (1.28s) | |
| Crux output: 4 | |
| direct_fnonce: OK (1.45s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 2 (1.30s) | |
| Crux output: 2 | |
| conv_fnonce_fnmut: OK (1.43s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.29s) | |
| Crux output: 2 | |
| fn_static_poly: OK (1.43s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 3 (1.28s) | |
| Crux output: 3 | |
| fnptr_fnonce: OK (1.42s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 4 (1.27s) | |
| Crux output: 4 | |
| fn_static: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 3 (1.28s) | |
| Crux output: 3 | |
| fn_dyn: FAIL (expected: call_once shim (in `dyn Fn` vtable)) (0.19s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 3 (0.03s) | |
| user error (Error 101 while running mir-json on test/conc_eval/clos/fn_dyn.rs) | |
| (expected failure) | |
| fnonce: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: false (1.27s) | |
| Crux output: false | |
| conv_fnmut_fn: OK (1.40s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.26s) | |
| Crux output: 2 | |
| direct_fnmut2: OK (1.39s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 7 (1.24s) | |
| Crux output: 7 | |
| fo: OK (1.37s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 29 (1.23s) | |
| Crux output: 29 | |
| unique_borrow: OK (1.43s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 3 (1.27s) | |
| Crux output: 3 | |
| conv_fnonce_fn: OK (1.41s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2 (1.26s) | |
| Crux output: 2 | |
| fnptr_fn: OK (1.36s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 4 (1.22s) | |
| Crux output: 4 | |
| direct_fnmut: OK (1.38s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 7 (1.24s) | |
| Crux output: 7 | |
| dispatch_fnmut: FAIL (1.43s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 7 (1.29s) | |
| Crux output: | |
| failures: | |
| ---- dispatch_fnmut/35585cbd::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/clos/dispatch_fnmut.rs:7:7: 7:9: error: in dispatch_fnmut/35585cbd::call_it2[0]::_inst15715dbe1d0521ca[0] | |
| [Crux] Translation error in dispatch_fnmut/35585cbd::call_it2[0]::_inst15715dbe1d0521ca[0]: cannot find static variable alloc$0/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/dispatch_fnmut/' to rerun this test only. | |
| poly: OK (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 3 (1.27s) | |
| Crux output: 3 | |
| direct_fn: OK (1.41s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: 2 (1.26s) | |
| Crux output: 2 | |
| fnptr_closure: FAIL (1.41s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 7 (1.27s) | |
| Crux output: | |
| failures: | |
| ---- fnptr_closure/761e489a::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/conc_eval/clos/fnptr_closure.rs:7:7: 7:9: error: in fnptr_closure/761e489a::call_it2[0]::_inste366449525d6d5d6[0] | |
| [Crux] Translation error in fnptr_closure/761e489a::call_it2[0]::_inste366449525d6d5d6[0]: cannot find static variable alloc$0/3a1fbbbh | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/fnptr_closure/' to rerun this test only. | |
| fnonce1: OK (1.37s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 3 (1.22s) | |
| Crux output: 3 | |
| ref_fnmut: OK (1.39s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 7 (1.25s) | |
| Crux output: 7 | |
| vec_deque | |
| pop: FAIL (1.95s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: [5, 4, 3, 1, 2] (1.80s) | |
| Crux output: | |
| failures: | |
| ---- pop/92eddffa::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/vec_deque.pop/' to rerun this test only. | |
| iter_clone: FAIL (2.03s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: [1, 2, 3, 2, 3] (1.87s) | |
| Crux output: | |
| failures: | |
| ---- iter_clone/0b924872::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/iter_clone/' to rerun this test only. | |
| push: FAIL (2.00s) | |
| Compiling and running oracle program (0.19s) | |
| Oracle output: [4, 1, 2, 3, 5] (1.81s) | |
| Crux output: | |
| failures: | |
| ---- push/ea8085e1::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/vec_deque.push/' to rerun this test only. | |
| retain: FAIL (2.00s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: [1, 4] (1.84s) | |
| Crux output: | |
| failures: | |
| ---- retain/e5cffc67::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/retain/' to rerun this test only. | |
| rotate_left: FAIL (2.06s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: [3, 4, 5, 1, 2] (1.90s) | |
| Crux output: | |
| failures: | |
| ---- rotate_left/c8f21bf2::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/rotate_left/' to rerun this test only. | |
| rotate_right: FAIL (2.00s) | |
| Compiling and running oracle program (0.16s) | |
| Oracle output: [4, 5, 1, 2, 3] (1.84s) | |
| Crux output: | |
| failures: | |
| ---- rotate_right/61f4f78a::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/rotate_right/' to rerun this test only. | |
| slice | |
| len: OK (1.35s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 5 (1.20s) | |
| Crux output: 5 | |
| mut_range: FAIL (1.77s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 86 (1.62s) | |
| Crux output: | |
| failures: | |
| ---- mut_range/e18d91dc::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/mut_range/' to rerun this test only. | |
| range_len: FAIL (1.81s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (1.66s) | |
| Crux output: | |
| failures: | |
| ---- range_len/36c67780::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '$0=="crux-mir.crux concrete..slice.range_len"' to rerun this test only. | |
| range_len_mut: FAIL (1.77s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 1 (1.63s) | |
| Crux output: | |
| failures: | |
| ---- range_len_mut/92ec4e52::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/range_len_mut/' to rerun this test only. | |
| mk_and_proj: OK (1.38s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 42 (1.24s) | |
| Crux output: 42 | |
| swap: OK (1.41s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 2001 (1.26s) | |
| Crux output: 2001 | |
| eq: FAIL (1.39s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: () (1.25s) | |
| Crux output: | |
| failures: | |
| ---- eq/3e30bdc6::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/mem/mod.rs:338:38: 338:41: error: in core/4066fdba::mem[0]::size_of_val[0]::_inst55af81a2cef2701c[0] | |
| [Crux] Translation error in core/4066fdba::mem[0]::size_of_val[0]::_inst55af81a2cef2701c[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::size_of_val[0]::_inst55af81a2cef2701c[0] | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/slice.eq/' to rerun this test only. | |
| iter_mut: FAIL (1.42s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: () (1.27s) | |
| Crux output: | |
| failures: | |
| ---- iter_mut/b5359b52::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/ptr/mut_ptr.rs:52:37: 52:52: error: in core/4066fdba::ptr[0]::mut_ptr[0]::{impl#0}[0]::is_null[0]::_inst1e2825177cd3b608[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::mut_ptr[0]::{impl#0}[0]::is_null[0]::_inst1e2825177cd3b608[0]: unimplemented cast: Misc | |
| [Crux] ty: TyRawPtr (TyInt B32) Mut | |
| [Crux] as: TyRawPtr (TyUint B8) Mut | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/iter_mut/' to rerun this test only. | |
| get: FAIL (1.40s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: true (1.26s) | |
| Crux output: | |
| failures: | |
| ---- get/f53e085a::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/ptr/metadata.rs:98:14: 98:40: error: in core/4066fdba::ptr[0]::metadata[0]::metadata[0]::_inst1743054c4d18d3c5[0] | |
| [Crux] Translation error in core/4066fdba::ptr[0]::metadata[0]::metadata[0]::_inst1743054c4d18d3c5[0]: evalPlace (PField, Union) NYI | |
| [Crux] Overall status: Invalid. | |
| test/Test.hs:126: | |
| crux doesn't match oracle | |
| Use -p '/slice.get/' to rerun this test only. | |
| mut: OK (1.40s) | |
| Compiling and running oracle program (0.15s) | |
| Oracle output: 42 (1.26s) | |
| Crux output: 42 | |
| last: OK (1.39s) | |
| Compiling and running oracle program (0.14s) | |
| Oracle output: 3 (1.24s) | |
| Crux output: 3 | |
| crux symbolic | |
| Output testing | |
| mux_init_mut: [0KFAIL (1.24s) | |
| files test/symb_eval/refs/mux_init_mut.good and test/symb_eval/refs/mux_init_mut.out differ; test/symb_eval/refs/mux_init_mut.out contains: | |
| test mux_init_mut/23803b55::crux_test[0]: FAILED | |
| failures: | |
| ---- mux_init_mut/23803b55::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/symb_eval/refs/mux_init_mut.rs:6:22: 6:23: error: in mux_init_mut/23803b55::crux_test[0] | |
| [Crux] Translation error in mux_init_mut/23803b55::crux_test[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#0}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/mux_init_mut/' to rerun this test only. | |
| mux_init_imm: [0KFAIL (1.21s) | |
| files test/symb_eval/refs/mux_init_imm.good and test/symb_eval/refs/mux_init_imm.out differ; test/symb_eval/refs/mux_init_imm.out contains: | |
| test mux_init_imm/c6487fd6::crux_test[0]: FAILED | |
| failures: | |
| ---- mux_init_imm/c6487fd6::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/symb_eval/refs/mux_init_imm.rs:7:15: 7:16: error: in mux_init_imm/c6487fd6::crux_test[0] | |
| [Crux] Translation error in mux_init_imm/c6487fd6::crux_test[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#0}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/mux_init_imm/' to rerun this test only. | |
| early_fail: [0K[0KFAIL (1.30s) | |
| files test/symb_eval/crux/early_fail.good and test/symb_eval/crux/early_fail.out differ; test/symb_eval/crux/early_fail.out contains: | |
| test early_fail/ce52f3be::fail1[0]: FAILED | |
| test early_fail/ce52f3be::fail2[0]: FAILED | |
| failures: | |
| ---- early_fail/ce52f3be::fail1[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/symb_eval/crux/early_fail.rs:11:12: 11:19: error: in early_fail/ce52f3be::fail1[0] | |
| [Crux] Translation error in early_fail/ce52f3be::fail1[0]: cannot find static variable alloc$0/3a1fbbbh | |
| ---- early_fail/ce52f3be::fail2[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in early_fail/ce52f3be::fail2[0] | |
| [Crux] Translation error in early_fail/ce52f3be::fail2[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#1}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/early_fail/' to rerun this test only. | |
| mixed_fail: [0K[0K[0K[0KFAIL (1.29s) | |
| files test/symb_eval/crux/mixed_fail.good and test/symb_eval/crux/mixed_fail.out differ; test/symb_eval/crux/mixed_fail.out contains: | |
| test mixed_fail/e2b2e711::fail1[0]: FAILED | |
| test mixed_fail/e2b2e711::fail2[0]: FAILED | |
| test mixed_fail/e2b2e711::pass1[0]: FAILED | |
| test mixed_fail/e2b2e711::pass2[0]: FAILED | |
| failures: | |
| ---- mixed_fail/e2b2e711::fail1[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in mixed_fail/e2b2e711::fail1[0] | |
| [Crux] Translation error in mixed_fail/e2b2e711::fail1[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#1}[0]::symbolic[0] | |
| ---- mixed_fail/e2b2e711::fail2[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in mixed_fail/e2b2e711::fail2[0] | |
| [Crux] Translation error in mixed_fail/e2b2e711::fail2[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#1}[0]::symbolic[0] | |
| ---- mixed_fail/e2b2e711::pass1[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in mixed_fail/e2b2e711::pass1[0] | |
| [Crux] Translation error in mixed_fail/e2b2e711::pass1[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#1}[0]::symbolic[0] | |
| ---- mixed_fail/e2b2e711::pass2[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in mixed_fail/e2b2e711::pass2[0] | |
| [Crux] Translation error in mixed_fail/e2b2e711::pass2[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#1}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/mixed_fail/' to rerun this test only. | |
| multi: [0K[0K[0KFAIL (1.29s) | |
| files test/symb_eval/crux/multi.good and test/symb_eval/crux/multi.out differ; test/symb_eval/crux/multi.out contains: | |
| test multi/cd95a197::fail1[0]: FAILED | |
| test multi/cd95a197::fail2[0]: FAILED | |
| test multi/cd95a197::fail3[0]: FAILED | |
| failures: | |
| ---- multi/cd95a197::fail1[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in multi/cd95a197::fail1[0] | |
| [Crux] Translation error in multi/cd95a197::fail1[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#1}[0]::symbolic[0] | |
| ---- multi/cd95a197::fail2[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in multi/cd95a197::fail2[0] | |
| [Crux] Translation error in multi/cd95a197::fail2[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#1}[0]::symbolic[0] | |
| ---- multi/cd95a197::fail3[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in multi/cd95a197::fail3[0] | |
| [Crux] Translation error in multi/cd95a197::fail3[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#1}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/Output testing.multi/' to rerun this test only. | |
| fail_return: [0K[0KFAIL (1.21s) | |
| files test/symb_eval/crux/fail_return.good and test/symb_eval/crux/fail_return.out differ; test/symb_eval/crux/fail_return.out contains: | |
| test fail_return/9725aa3c::fail1[0]: FAILED | |
| test fail_return/9725aa3c::fail2[0]: FAILED | |
| failures: | |
| ---- fail_return/9725aa3c::fail1[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in fail_return/9725aa3c::fail1[0] | |
| [Crux] Translation error in fail_return/9725aa3c::fail1[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#1}[0]::symbolic[0] | |
| ---- fail_return/9725aa3c::fail2[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in fail_return/9725aa3c::fail2[0] | |
| [Crux] Translation error in fail_return/9725aa3c::fail2[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#1}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/fail_return/' to rerun this test only. | |
| no_conc: [0KFAIL (1.20s) | |
| files test/symb_eval/concretize/no_conc.good and test/symb_eval/concretize/no_conc.out differ; test/symb_eval/concretize/no_conc.out contains: | |
| test no_conc/b49ef5bb::crux_test[0]: FAILED | |
| failures: | |
| ---- no_conc/b49ef5bb::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in no_conc/b49ef5bb::crux_test[0] | |
| [Crux] Translation error in no_conc/b49ef5bb::crux_test[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#1}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/no_conc/' to rerun this test only. | |
| conc: [0KFAIL (1.28s) | |
| files test/symb_eval/concretize/conc.good and test/symb_eval/concretize/conc.out differ; test/symb_eval/concretize/conc.out contains: | |
| test conc/f9138415::crux_test[0]: FAILED | |
| failures: | |
| ---- conc/f9138415::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in conc/f9138415::crux_test[0] | |
| [Crux] Translation error in conc/f9138415::crux_test[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#1}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '$0=="crux-mir.crux symbolic.Output testing.conc"' to rerun this test only. | |
| array: [0KFAIL (1.38s) | |
| files test/symb_eval/concretize/array.good and test/symb_eval/concretize/array.out differ; test/symb_eval/concretize/array.out contains: | |
| test array/216ad3e7::crux_test[0]: FAILED | |
| failures: | |
| ---- array/216ad3e7::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '$0=="crux-mir.crux symbolic.Output testing.array"' to rerun this test only. | |
| assert_ok: [0KFAIL (1.70s) | |
| files test/symb_eval/concretize/assert_ok.good and test/symb_eval/concretize/assert_ok.out differ; test/symb_eval/concretize/assert_ok.out contains: | |
| test assert_ok/dc64ceb2::crux_test[0]: FAILED | |
| failures: | |
| ---- assert_ok/dc64ceb2::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/assert_ok/' to rerun this test only. | |
| assert: [0KFAIL (1.73s) | |
| files test/symb_eval/concretize/assert.good and test/symb_eval/concretize/assert.out differ; test/symb_eval/concretize/assert.out contains: | |
| test assert/efbb0209::crux_test[0]: FAILED | |
| failures: | |
| ---- assert/efbb0209::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '$0=="crux-mir.crux symbolic.Output testing.assert"' to rerun this test only. | |
| bytes2: [0KFAIL (1.24s) | |
| files test/symb_eval/crypto/bytes2.good and test/symb_eval/crypto/bytes2.out differ; test/symb_eval/crypto/bytes2.out contains: | |
| test bytes2/b6d594d6::f[0]: FAILED | |
| failures: | |
| ---- bytes2/b6d594d6::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/symb_eval/crypto/bytes2.rs:74:17: 74:26: error: in bytes2/b6d594d6::f[0] | |
| [Crux] Translation error in bytes2/b6d594d6::f[0]: callExp: Don't know how to call crucible/55e82edd::crucible_u8[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/bytes2/' to rerun this test only. | |
| double: [0KFAIL (1.20s) | |
| files test/symb_eval/crypto/double.good and test/symb_eval/crypto/double.out differ; test/symb_eval/crypto/double.out contains: | |
| test double/854ab6a5::f[0]: FAILED | |
| failures: | |
| ---- double/854ab6a5::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in double/854ab6a5::f[0] | |
| [Crux] Translation error in double/854ab6a5::f[0]: callExp: Don't know how to call crucible/55e82edd::crucible_u32[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/double/' to rerun this test only. | |
| ffs: [0KFAIL (1.23s) | |
| files test/symb_eval/crypto/ffs.good and test/symb_eval/crypto/ffs.out differ; test/symb_eval/crypto/ffs.out contains: | |
| test ffs/cb6f0f07::f[0]: FAILED | |
| failures: | |
| ---- ffs/cb6f0f07::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in ffs/cb6f0f07::f[0] | |
| [Crux] Translation error in ffs/cb6f0f07::f[0]: callExp: Don't know how to call crucible/55e82edd::crucible_u32[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/Output testing.ffs/' to rerun this test only. | |
| bytes: [0KFAIL (1.26s) | |
| files test/symb_eval/crypto/bytes.good and test/symb_eval/crypto/bytes.out differ; test/symb_eval/crypto/bytes.out contains: | |
| test bytes/6c18198b::f[0]: FAILED | |
| failures: | |
| ---- bytes/6c18198b::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in bytes/6c18198b::f[0] | |
| [Crux] Translation error in bytes/6c18198b::f[0]: callExp: Don't know how to call crucible/55e82edd::crucible_u64[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '$0=="crux-mir.crux symbolic.Output testing.bytes"' to rerun this test only. | |
| bad_symb1: [0KFAIL (1.25s) | |
| files test/symb_eval/overrides/bad_symb1.good and test/symb_eval/overrides/bad_symb1.out differ; test/symb_eval/overrides/bad_symb1.out contains: | |
| test bad_symb1/3801f553::crux_test[0]: FAILED | |
| failures: | |
| ---- bad_symb1/3801f553::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in bad_symb1/3801f553::crux_test[0] | |
| [Crux] Translation error in bad_symb1/3801f553::crux_test[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#0}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/bad_symb1/' to rerun this test only. | |
| bad_symb2: [0KFAIL (1.24s) | |
| files test/symb_eval/overrides/bad_symb2.good and test/symb_eval/overrides/bad_symb2.out differ; test/symb_eval/overrides/bad_symb2.out contains: | |
| test bad_symb2/6b7da1d6::crux_test[0]: FAILED | |
| failures: | |
| ---- bad_symb2/6b7da1d6::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in bad_symb2/6b7da1d6::crux_test[0] | |
| [Crux] Translation error in bad_symb2/6b7da1d6::crux_test[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#1}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/bad_symb2/' to rerun this test only. | |
| override3: [0KFAIL (1.26s) | |
| files test/symb_eval/overrides/override3.good and test/symb_eval/overrides/override3.out differ; test/symb_eval/overrides/override3.out contains: | |
| test override3/99deca29::f[0]: FAILED | |
| failures: | |
| ---- override3/99deca29::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in override3/99deca29::f[0] | |
| [Crux] Translation error in override3/99deca29::f[0]: callExp: Don't know how to call crucible/55e82edd::crucible_i8[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/override3/' to rerun this test only. | |
| override1: [0KFAIL (1.27s) | |
| files test/symb_eval/overrides/override1.good and test/symb_eval/overrides/override1.out differ; test/symb_eval/overrides/override1.out contains: | |
| test override1/1b30b055::f[0]: FAILED | |
| failures: | |
| ---- override1/1b30b055::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/symb_eval/overrides/override1.rs:9:5: 9:6: error: in override1/1b30b055::f[0] | |
| [Crux] Translation error in override1/1b30b055::f[0]: callExp: Don't know how to call crucible/55e82edd::one[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/override1/' to rerun this test only. | |
| override4: [0KFAIL (1.25s) | |
| files test/symb_eval/overrides/override4.good and test/symb_eval/overrides/override4.out differ; test/symb_eval/overrides/override4.out contains: | |
| test override4/2e2f9c61::f[0]: FAILED | |
| failures: | |
| ---- override4/2e2f9c61::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in override4/2e2f9c61::f[0] | |
| [Crux] Translation error in override4/2e2f9c61::f[0]: callExp: Don't know how to call crucible/55e82edd::crucible_i8[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/override4/' to rerun this test only. | |
| override_rust: [0KFAIL (1.26s) | |
| files test/symb_eval/overrides/override_rust.good and test/symb_eval/overrides/override_rust.out differ; test/symb_eval/overrides/override_rust.out contains: | |
| test override_rust/c056eda2::crux_test[0]: FAILED | |
| failures: | |
| ---- override_rust/c056eda2::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/override_rust/' to rerun this test only. | |
| override2: [0KFAIL (1.25s) | |
| files test/symb_eval/overrides/override2.good and test/symb_eval/overrides/override2.out differ; test/symb_eval/overrides/override2.out contains: | |
| test override2/e3ba454a::f[0]: FAILED | |
| failures: | |
| ---- override2/e3ba454a::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in override2/e3ba454a::f[0] | |
| [Crux] Translation error in override2/e3ba454a::f[0]: callExp: Don't know how to call crucible/55e82edd::crucible_i8[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/override2/' to rerun this test only. | |
| override5: [0KFAIL (1.29s) | |
| files test/symb_eval/overrides/override5.good and test/symb_eval/overrides/override5.out differ; test/symb_eval/overrides/override5.out contains: | |
| test override5/4478e731::f[0]: FAILED | |
| failures: | |
| ---- override5/4478e731::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in override5/4478e731::f[0] | |
| [Crux] Translation error in override5/4478e731::f[0]: callExp: Don't know how to call crucible/55e82edd::crucible_u64[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/override5/' to rerun this test only. | |
| mux: [0KFAIL (1.30s) | |
| files test/symb_eval/fnptr/mux.good and test/symb_eval/fnptr/mux.out differ; test/symb_eval/fnptr/mux.out contains: | |
| test mux/13339a38::crux_test[0]: FAILED | |
| failures: | |
| ---- mux/13339a38::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in mux/13339a38::crux_test[0] | |
| [Crux] Translation error in mux/13339a38::crux_test[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#0}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '$0=="crux-mir.crux symbolic.Output testing.mux"' to rerun this test only. | |
| checked_mul_signed: FAIL (0.05s) | |
| test/symb_eval/num/checked_mul_signed.out: withFile: user error (Error 101 while running mir-json on test/symb_eval/num/checked_mul_signed.rs) | |
| Use -p '/checked_mul_signed/' to rerun this test only. | |
| checked_mul: FAIL (0.04s) | |
| test/symb_eval/num/checked_mul.out: withFile: user error (Error 101 while running mir-json on test/symb_eval/num/checked_mul.rs) | |
| Use -p '$0=="crux-mir.crux symbolic.Output testing.checked_mul"' to rerun this test only. | |
| checked_div: [0KFAIL (1.36s) | |
| files test/symb_eval/num/checked_div.good and test/symb_eval/num/checked_div.out differ; test/symb_eval/num/checked_div.out contains: | |
| test checked_div/7574440c::crux_test[0]: returned 65, FAILED | |
| failures: | |
| ---- checked_div/7574440c::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/symb_eval/num/checked_div.rs:3:5: 3:10: error: in checked_div/7574440c::div_signed[0] | |
| [Crux] attempt to compute `_3 / _4`, which would overflow | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/symb_eval/num/checked_div.rs:3:5: 3:10: error: in checked_div/7574440c::div_signed[0] | |
| [Crux] attempt to divide `_3` by zero | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/symb_eval/num/checked_div.rs:8:5: 8:10: error: in checked_div/7574440c::div_unsigned[0] | |
| [Crux] attempt to divide `_3` by zero | |
| [Crux] Overall status: Invalid. | |
| Use -p '/checked_div/' to rerun this test only. | |
| checked_add: FAIL (0.05s) | |
| test/symb_eval/num/checked_add.out: withFile: user error (Error 101 while running mir-json on test/symb_eval/num/checked_add.rs) | |
| Use -p '/checked_add/' to rerun this test only. | |
| test1: FAIL (0.08s) | |
| test/symb_eval/scalar/test1.out: withFile: user error (Error 101 while running mir-json on test/symb_eval/scalar/test1.rs) | |
| Use -p '/test1/' to rerun this test only. | |
| pop: [0KFAIL (1.46s) | |
| files test/symb_eval/vector/pop.good and test/symb_eval/vector/pop.out differ; test/symb_eval/vector/pop.out contains: | |
| test pop/77e609b5::f[0]: FAILED | |
| failures: | |
| ---- pop/77e609b5::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/Output testing.pop/' to rerun this test only. | |
| as_mut_slice: [0KFAIL (1.38s) | |
| files test/symb_eval/vector/as_mut_slice.good and test/symb_eval/vector/as_mut_slice.out differ; test/symb_eval/vector/as_mut_slice.out contains: | |
| test as_mut_slice/02620ec7::f[0]: FAILED | |
| failures: | |
| ---- as_mut_slice/02620ec7::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/as_mut_slice/' to rerun this test only. | |
| push: [0KFAIL (1.38s) | |
| files test/symb_eval/vector/push.good and test/symb_eval/vector/push.out differ; test/symb_eval/vector/push.out contains: | |
| test push/332ef752::f[0]: FAILED | |
| failures: | |
| ---- push/332ef752::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/Output testing.push/' to rerun this test only. | |
| copy_from_slice: [0KFAIL (1.34s) | |
| files test/symb_eval/vector/copy_from_slice.good and test/symb_eval/vector/copy_from_slice.out differ; test/symb_eval/vector/copy_from_slice.out contains: | |
| test copy_from_slice/160e2de5::f[0]: FAILED | |
| failures: | |
| ---- copy_from_slice/160e2de5::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/copy_from_slice/' to rerun this test only. | |
| new: [0KFAIL (1.43s) | |
| files test/symb_eval/vector/new.good and test/symb_eval/vector/new.out differ; test/symb_eval/vector/new.out contains: | |
| test new/ad2cd4cd::f[0]: FAILED | |
| failures: | |
| ---- new/ad2cd4cd::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '$0=="crux-mir.crux symbolic.Output testing.new"' to rerun this test only. | |
| mut: [0KFAIL (1.38s) | |
| files test/symb_eval/vector/mut.good and test/symb_eval/vector/mut.out differ; test/symb_eval/vector/mut.out contains: | |
| test mut/45011252::f[0]: FAILED | |
| failures: | |
| ---- mut/45011252::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/Output testing.mut/' to rerun this test only. | |
| concat: [0KFAIL (1.36s) | |
| files test/symb_eval/vector/concat.good and test/symb_eval/vector/concat.out differ; test/symb_eval/vector/concat.out contains: | |
| test concat/32baab4e::f[0]: FAILED | |
| failures: | |
| ---- concat/32baab4e::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/concat/' to rerun this test only. | |
| split_at: [0KFAIL (1.43s) | |
| files test/symb_eval/vector/split_at.good and test/symb_eval/vector/split_at.out differ; test/symb_eval/vector/split_at.out contains: | |
| test split_at/b857b600::f[0]: FAILED | |
| failures: | |
| ---- split_at/b857b600::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/split_at/' to rerun this test only. | |
| replicate: [0KFAIL (1.32s) | |
| files test/symb_eval/vector/replicate.good and test/symb_eval/vector/replicate.out differ; test/symb_eval/vector/replicate.out contains: | |
| test replicate/ea0c868b::f[0]: FAILED | |
| failures: | |
| ---- replicate/ea0c868b::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/replicate/' to rerun this test only. | |
| as_slice: [0KFAIL (1.27s) | |
| files test/symb_eval/vector/as_slice.good and test/symb_eval/vector/as_slice.out differ; test/symb_eval/vector/as_slice.out contains: | |
| test as_slice/3739377a::f[0]: FAILED | |
| failures: | |
| ---- as_slice/3739377a::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/as_slice/' to rerun this test only. | |
| array_mut: [0KFAIL (1.20s) | |
| files test/symb_eval/mux/array_mut.good and test/symb_eval/mux/array_mut.out differ; test/symb_eval/mux/array_mut.out contains: | |
| test array_mut/d50e5231::crux_test[0]: FAILED | |
| failures: | |
| ---- array_mut/d50e5231::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/symb_eval/mux/array_mut.rs:8:20: 8:26: error: in array_mut/d50e5231::crux_test[0] | |
| [Crux] Translation error in array_mut/d50e5231::crux_test[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#0}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/array_mut/' to rerun this test only. | |
| array: [0KFAIL (1.21s) | |
| files test/symb_eval/mux/array.good and test/symb_eval/mux/array.out differ; test/symb_eval/mux/array.out contains: | |
| test array/8beb8706::crux_test[0]: FAILED | |
| failures: | |
| ---- array/8beb8706::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/symb_eval/mux/array.rs:8:16: 8:22: error: in array/8beb8706::crux_test[0] | |
| [Crux] Translation error in array/8beb8706::crux_test[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#0}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '$0=="crux-mir.crux symbolic.Output testing.array"' to rerun this test only. | |
| extend_bytes: FAIL (0.03s) | |
| test/symb_eval/bytes/extend_bytes.out: withFile: user error (Error 101 while running mir-json on test/symb_eval/bytes/extend_bytes.rs) | |
| Use -p '/extend_bytes/' to rerun this test only. | |
| put: FAIL | |
| test/symb_eval/bytes/put.out: withFile: user error (Error 101 while running mir-json on test/symb_eval/bytes/put.rs) | |
| Use -p '$0=="crux-mir.crux symbolic.Output testing.put"' to rerun this test only. | |
| split_to: FAIL (0.04s) | |
| test/symb_eval/bytes/split_to.out: withFile: user error (Error 101 while running mir-json on test/symb_eval/bytes/split_to.rs) | |
| Use -p '/split_to/' to rerun this test only. | |
| new: FAIL | |
| test/symb_eval/bytes/new.out: withFile: user error (Error 101 while running mir-json on test/symb_eval/bytes/new.rs) | |
| Use -p '$0=="crux-mir.crux symbolic.Output testing.new"' to rerun this test only. | |
| split_off: FAIL | |
| test/symb_eval/bytes/split_off.out: withFile: user error (Error 101 while running mir-json on test/symb_eval/bytes/split_off.rs) | |
| Use -p '/split_off/' to rerun this test only. | |
| sym_len: FAIL | |
| test/symb_eval/bytes/sym_len.out: withFile: user error (Error 101 while running mir-json on test/symb_eval/bytes/sym_len.rs) | |
| Use -p '/sym_len/' to rerun this test only. | |
| put_overflow: FAIL (0.03s) | |
| test/symb_eval/bytes/put_overflow.out: withFile: user error (Error 101 while running mir-json on test/symb_eval/bytes/put_overflow.rs) | |
| Use -p '/put_overflow/' to rerun this test only. | |
| vec_cursor_read: FAIL (1.84s) | |
| standalone use of `dyn` is not supported: TyDynamic core/4066fdba::error[0]::Error[0]::_trait56353a7b840403b4[0] | |
| CallStack (from HasCallStack): | |
| error, called at src/Mir/TransTy.hs:230:25 in crux-mir-0.6.0.99-inplace:Mir.TransTy | |
| tyToRepr, called at src/Mir/Trans.hs:810:12 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast', called at src/Mir/Trans.hs:878:5 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast, called at src/Mir/Trans.hs:930:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalRval, called at src/Mir/Trans.hs:1142:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transStatement, called at src/Mir/Trans.hs:1740:68 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| translateBlockBody, called at src/Mir/Trans.hs:1749:28 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| registerBlock, called at src/Mir/Trans.hs:1789:10 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| genFn, called at src/Mir/Trans.hs:1835:24 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transDefine, called at src/Mir/Trans.hs:2272:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transCollection, called at src/Mir/Generate.hs:225:26 in crux-mir-0.6.0.99-inplace:Mir.Generate | |
| translateMIR, called at src/Mir/Language.hs:252:16 in crux-mir-0.6.0.99-inplace:Mir.Language | |
| Use -p '/vec_cursor_read/' to rerun this test only. | |
| vec_write: FAIL (1.70s) | |
| standalone use of `dyn` is not supported: TyDynamic core/4066fdba::error[0]::Error[0]::_trait56353a7b840403b4[0] | |
| CallStack (from HasCallStack): | |
| error, called at src/Mir/TransTy.hs:230:25 in crux-mir-0.6.0.99-inplace:Mir.TransTy | |
| tyToRepr, called at src/Mir/Trans.hs:810:12 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast', called at src/Mir/Trans.hs:878:5 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalCast, called at src/Mir/Trans.hs:930:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| evalRval, called at src/Mir/Trans.hs:1142:11 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transStatement, called at src/Mir/Trans.hs:1740:68 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| translateBlockBody, called at src/Mir/Trans.hs:1749:28 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| registerBlock, called at src/Mir/Trans.hs:1789:10 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| genFn, called at src/Mir/Trans.hs:1835:24 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transDefine, called at src/Mir/Trans.hs:2272:30 in crux-mir-0.6.0.99-inplace:Mir.Trans | |
| transCollection, called at src/Mir/Generate.hs:225:26 in crux-mir-0.6.0.99-inplace:Mir.Generate | |
| translateMIR, called at src/Mir/Language.hs:252:16 in crux-mir-0.6.0.99-inplace:Mir.Language | |
| Use -p '/vec_write/' to rerun this test only. | |
| write: FAIL | |
| test/symb_eval/byteorder/write.out: withFile: user error (Error 101 while running mir-json on test/symb_eval/byteorder/write.rs) | |
| Use -p '/Output testing.write/' to rerun this test only. | |
| read: FAIL | |
| test/symb_eval/byteorder/read.out: withFile: user error (Error 101 while running mir-json on test/symb_eval/byteorder/read.rs) | |
| Use -p '/Output testing.read/' to rerun this test only. | |
| slice_mut: [0KFAIL (1.37s) | |
| files test/symb_eval/array/slice_mut.good and test/symb_eval/array/slice_mut.out differ; test/symb_eval/array/slice_mut.out contains: | |
| test slice_mut/44122423::crux_test[0]: FAILED | |
| failures: | |
| ---- slice_mut/44122423::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/slice_mut/' to rerun this test only. | |
| basic: [0KFAIL (1.32s) | |
| files test/symb_eval/array/basic.good and test/symb_eval/array/basic.out differ; test/symb_eval/array/basic.out contains: | |
| test basic/2989ddae::crux_test[0]: FAILED | |
| failures: | |
| ---- basic/2989ddae::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/Output testing.basic/' to rerun this test only. | |
| slice: [0KFAIL (1.31s) | |
| files test/symb_eval/array/slice.good and test/symb_eval/array/slice.out differ; test/symb_eval/array/slice.out contains: | |
| test slice/769f2857::crux_test[0]: FAILED | |
| failures: | |
| ---- slice/769f2857::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '$0=="crux-mir.crux symbolic.Output testing.slice"' to rerun this test only. | |
| mux_slice: [0KFAIL (1.35s) | |
| files test/symb_eval/array/mux_slice.good and test/symb_eval/array/mux_slice.out differ; test/symb_eval/array/mux_slice.out contains: | |
| test mux_slice/f44157bb::crux_test[0]: FAILED | |
| failures: | |
| ---- mux_slice/f44157bb::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/mux_slice/' to rerun this test only. | |
| mux: [0KFAIL (1.23s) | |
| files test/symb_eval/enum/mux.good and test/symb_eval/enum/mux.out differ; test/symb_eval/enum/mux.out contains: | |
| test mux/7b886b72::test[0]: FAILED | |
| failures: | |
| ---- mux/7b886b72::test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in mux/7b886b72::test[0] | |
| [Crux] Translation error in mux/7b886b72::test[0]: callExp: Don't know how to call crucible/55e82edd::crucible_u8[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '$0=="crux-mir.crux symbolic.Output testing.mux"' to rerun this test only. | |
| uninit_read: [0KFAIL (1.35s) | |
| files test/symb_eval/alloc/uninit_read.good and test/symb_eval/alloc/uninit_read.out differ; test/symb_eval/alloc/uninit_read.out contains: | |
| test uninit_read/38f8f06e::crux_test[0]: FAILED | |
| failures: | |
| ---- uninit_read/38f8f06e::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/uninit_read/' to rerun this test only. | |
| valid_read: [0KFAIL (1.38s) | |
| files test/symb_eval/alloc/valid_read.good and test/symb_eval/alloc/valid_read.out differ; test/symb_eval/alloc/valid_read.out contains: | |
| test valid_read/1ae1e678::crux_test[0]: FAILED | |
| failures: | |
| ---- valid_read/1ae1e678::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/valid_read/' to rerun this test only. | |
| out_of_bounds: [0KFAIL (1.38s) | |
| files test/symb_eval/alloc/out_of_bounds.good and test/symb_eval/alloc/out_of_bounds.out differ; test/symb_eval/alloc/out_of_bounds.out contains: | |
| test out_of_bounds/3c7234c3::crux_test[0]: FAILED | |
| failures: | |
| ---- out_of_bounds/3c7234c3::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/out_of_bounds/' to rerun this test only. | |
| zero_length: [0KFAIL (1.33s) | |
| files test/symb_eval/alloc/zero_length.good and test/symb_eval/alloc/zero_length.out differ; test/symb_eval/alloc/zero_length.out contains: | |
| test zero_length/42c5ba2a::crux_test[0]: FAILED | |
| failures: | |
| ---- zero_length/42c5ba2a::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/zero_length/' to rerun this test only. | |
| downcast: [0KFAIL (1.33s) | |
| files test/symb_eval/any/downcast.good and test/symb_eval/any/downcast.out differ; test/symb_eval/any/downcast.out contains: | |
| test downcast/1a0f60fe::crux_test[0]: FAILED | |
| failures: | |
| ---- downcast/1a0f60fe::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '$0=="crux-mir.crux symbolic.Output testing.downcast"' to rerun this test only. | |
| downcast_fail: [0KFAIL (1.28s) | |
| files test/symb_eval/any/downcast_fail.good and test/symb_eval/any/downcast_fail.out differ; test/symb_eval/any/downcast_fail.out contains: | |
| test downcast_fail/f7cfd85b::crux_test[0]: FAILED | |
| failures: | |
| ---- downcast_fail/f7cfd85b::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/downcast_fail/' to rerun this test only. | |
| conditional: FAIL | |
| test/symb_eval/any/conditional.out: withFile: user error (Error 101 while running mir-json on test/symb_eval/any/conditional.rs) | |
| Use -p '/conditional/' to rerun this test only. | |
| literals: [0KFAIL (1.32s) | |
| files test/symb_eval/bitvector/literals.good and test/symb_eval/bitvector/literals.out differ; test/symb_eval/bitvector/literals.out contains: | |
| test literals/4f4d111c::crux_test[0]: FAILED | |
| failures: | |
| ---- literals/4f4d111c::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/crucible/bitvector.rs:91:29: 91:30 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/crucible/bitvector.rs:125:1: 125:53: error: in crucible/55e82edd::bitvector[0]::{impl#27}[0]::from[0]::_inst9ea2f935eda83dab[0] | |
| [Crux] Translation error in crucible/55e82edd::bitvector[0]::{impl#27}[0]::from[0]::_inst9ea2f935eda83dab[0]: BUG: invalid arguments to bv_convert: [$31: AnyRepr] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/literals/' to rerun this test only. | |
| arith: [0KFAIL (1.29s) | |
| files test/symb_eval/bitvector/arith.good and test/symb_eval/bitvector/arith.out differ; test/symb_eval/bitvector/arith.out contains: | |
| test arith/b506105a::crux_test[0]: FAILED | |
| failures: | |
| ---- arith/b506105a::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] test/symb_eval/bitvector/arith.rs:20:9: 20:10: error: in arith/b506105a::test_binop[0]::_inst34be60c65b9c0bef[0] | |
| [Crux] Translation error in arith/b506105a::test_binop[0]::_inst34be60c65b9c0bef[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#4}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/Output testing.arith/' to rerun this test only. | |
| leading_zeros: [0KFAIL (1.26s) | |
| files test/symb_eval/bitvector/leading_zeros.good and test/symb_eval/bitvector/leading_zeros.out differ; test/symb_eval/bitvector/leading_zeros.out contains: | |
| test leading_zeros/ea71a47d::crux_test[0]: FAILED | |
| failures: | |
| ---- leading_zeros/ea71a47d::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in leading_zeros/ea71a47d::crux_test[0] | |
| [Crux] Translation error in leading_zeros/ea71a47d::crux_test[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#4}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/leading_zeros/' to rerun this test only. | |
| overflowing_sub: [0KFAIL (1.30s) | |
| files test/symb_eval/bitvector/overflowing_sub.good and test/symb_eval/bitvector/overflowing_sub.out differ; test/symb_eval/bitvector/overflowing_sub.out contains: | |
| test overflowing_sub/8fb0bcd3::crux_test[0]: FAILED | |
| failures: | |
| ---- overflowing_sub/8fb0bcd3::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in overflowing_sub/8fb0bcd3::crux_test[0] | |
| [Crux] Translation error in overflowing_sub/8fb0bcd3::crux_test[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#4}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/overflowing_sub/' to rerun this test only. | |
| cmp: [0KFAIL (1.32s) | |
| files test/symb_eval/bitvector/cmp.good and test/symb_eval/bitvector/cmp.out differ; test/symb_eval/bitvector/cmp.out contains: | |
| test cmp/e4bc424b::crux_test[0]: FAILED | |
| failures: | |
| ---- cmp/e4bc424b::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/crucible/symbolic.rs:116:43: 116:47 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/crucible/symbolic.rs:124:1: 138:2: error: in crucible/55e82edd::symbolic[0]::{impl#48}[0]::symbolic[0]::_inst21661be9becebe1c[0] | |
| [Crux] Translation error in crucible/55e82edd::symbolic[0]::{impl#48}[0]::symbolic[0]::_inst21661be9becebe1c[0]: callExp: Don't know how to call crucible/55e82edd::symbolic[0]::{impl#4}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/Output testing.cmp/' to rerun this test only. | |
| symbolic: [0KFAIL (1.32s) | |
| files test/symb_eval/bitvector/symbolic.good and test/symb_eval/bitvector/symbolic.out differ; test/symb_eval/bitvector/symbolic.out contains: | |
| test symbolic/819762eb::crux_test[0]: FAILED | |
| failures: | |
| ---- symbolic/819762eb::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/crucible/bitvector.rs:251:26: 251:30: error: in crucible/55e82edd::bitvector[0]::{impl#11}[0]::symbolic[0]::_inst9ea2f935eda83dab[0] | |
| [Crux] Translation error in crucible/55e82edd::bitvector[0]::{impl#11}[0]::symbolic[0]::_inst9ea2f935eda83dab[0]: callExp: Don't know how to call crucible/55e82edd::bitvector[0]::{impl#1}[0]::make_symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/Output testing.symbolic/' to rerun this test only. | |
| from_to: [0KFAIL (1.31s) | |
| files test/symb_eval/bitvector/from_to.good and test/symb_eval/bitvector/from_to.out differ; test/symb_eval/bitvector/from_to.out contains: | |
| test from_to/3b2687fb::crux_test[0]: FAILED | |
| failures: | |
| ---- from_to/3b2687fb::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/crucible/bitvector.rs:103:29: 103:30 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/crucible/bitvector.rs:125:1: 125:53: error: in crucible/55e82edd::bitvector[0]::{impl#21}[0]::from[0]::_inst9ea2f935eda83dab[0] | |
| [Crux] Translation error in crucible/55e82edd::bitvector[0]::{impl#21}[0]::from[0]::_inst9ea2f935eda83dab[0]: BUG: invalid arguments to bv_convert: [$27: BVRepr 64] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/from_to/' to rerun this test only. | |
| clone: [0KFAIL (1.54s) | |
| files test/symb_eval/vec/clone.good and test/symb_eval/vec/clone.out differ; test/symb_eval/vec/clone.out contains: | |
| test clone/ebdb3d5e::f[0]: FAILED | |
| failures: | |
| ---- clone/ebdb3d5e::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:89:31: 89:47 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:965:5: 970:27: error: in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::ctpop[0]::_inst11a9dd2a3cfdbd73[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/Output testing.clone/' to rerun this test only. | |
| sort_by_key: [0KFAIL (2.07s) | |
| files test/symb_eval/vec/sort_by_key.good and test/symb_eval/vec/sort_by_key.out differ; test/symb_eval/vec/sort_by_key.out contains: | |
| test sort_by_key/17326fc3::f[0]: FAILED | |
| failures: | |
| ---- sort_by_key/17326fc3::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/sort_by_key/' to rerun this test only. | |
| into_iter: [0KFAIL (1.87s) | |
| files test/symb_eval/vec/into_iter.good and test/symb_eval/vec/into_iter.out differ; test/symb_eval/vec/into_iter.out contains: | |
| test into_iter/9f90cc90::f[0]: FAILED | |
| failures: | |
| ---- into_iter/9f90cc90::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] lib/core/src/fmt/mod.rs:316:65: 320:2: error: in core/4066fdba::fmt[0]::USIZE_MARKER[0] | |
| [Crux] Translation error in core/4066fdba::fmt[0]::USIZE_MARKER[0]: unimplemented cast: ClosureFnPointer | |
| [Crux] ty: TyClosure [] | |
| [Crux] as: TyFnPtr (FnSig {_fsarg_tys = [TyRef (TyUint USize) Immut,TyRef (TyAdt core/4066fdba::fmt[0]::Formatter[0]::_adtbd21306cbe4f0b9b[0] core/4066fdba::fmt[0]::Formatter[0] (Substs [TyLifetime])) Mut], _fsreturn_ty = TyAdt core/4066fdba::result[0]::Result[0]::_adtb3f4e538b15dbdda[0] core/4066fdba::result[0]::Result[0] (Substs [TyTuple [],TyAdt core/4066fdba::fmt[0]::Error[0]::_adtb7803c2264daf0ec[0] core/4066fdba::fmt[0]::Error[0] (Substs [])]), _fsabi = RustAbi, _fsspreadarg = Nothing}) | |
| [Crux] Overall status: Invalid. | |
| Use -p '/into_iter/' to rerun this test only. | |
| macro: [0KFAIL (1.36s) | |
| files test/symb_eval/vec/macro.good and test/symb_eval/vec/macro.out differ; test/symb_eval/vec/macro.out contains: | |
| test macro/9fcec95b::f[0]: FAILED | |
| failures: | |
| ---- macro/9fcec95b::f[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] /home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/uint_macros.rs:89:31: 89:47 !/home/rscott/Documents/Hacking/Haskell/sandbox/crucible-chainsaw/crux-mir/lib/core/src/num/mod.rs:965:5: 970:27: error: in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0] | |
| [Crux] Translation error in core/4066fdba::num[0]::{impl#12}[0]::count_ones[0]: callExp: Don't know how to call core/4066fdba::intrinsics[0]::{extern#0}[0]::ctpop[0]::_inst11a9dd2a3cfdbd73[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/Output testing.macro/' to rerun this test only. | |
| construct: [0KFAIL (1.37s) | |
| files test/symb_eval/sym_bytes/construct.good and test/symb_eval/sym_bytes/construct.out differ; test/symb_eval/sym_bytes/construct.out contains: | |
| test construct/16df3000::crux_test[0]: FAILED | |
| failures: | |
| ---- construct/16df3000::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in construct/16df3000::crux_test[0] | |
| [Crux] Translation error in construct/16df3000::crux_test[0]: callExp: Don't know how to call crucible/55e82edd::sym_bytes[0]::{impl#0}[0]::zeroed[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/construct/' to rerun this test only. | |
| deserialize: [0KFAIL (1.35s) | |
| files test/symb_eval/sym_bytes/deserialize.good and test/symb_eval/sym_bytes/deserialize.out differ; test/symb_eval/sym_bytes/deserialize.out contains: | |
| test deserialize/503f6b1e::crux_test[0]: FAILED | |
| failures: | |
| ---- deserialize/503f6b1e::crux_test[0] counterexamples ---- | |
| [Crux] Found counterexample for verification goal | |
| [Crux] internal: error: in deserialize/503f6b1e::crux_test[0] | |
| [Crux] Translation error in deserialize/503f6b1e::crux_test[0]: callExp: Don't know how to call crucible/55e82edd::sym_bytes[0]::{impl#0}[0]::symbolic[0] | |
| [Crux] Overall status: Invalid. | |
| Use -p '/deserialize/' to rerun this test only. | |
| crux coverage | |
| Output testing | |
| coverage_dual: warning: trailing semicolon in macro used in expression position | |
| --> src/main.rs:45:46 | |
| | | |
| 45 | return Err(format!($($args)*).into()); | |
| | ^ | |
| ... | |
| 309 | _ => die!("unknown tag {:?} for branch", tag), | |
| | ---------------------------------------- in this macro invocation | |
| | | |
| = warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release! | |
| = note: for more information, see issue #79813 <https://github.com/rust-lang/rust/issues/79813> | |
| = note: `#[warn(semicolon_in_expressions_from_macros)]` on by default | |
| = note: this warning originates in the macro `die` (in Nightly builds, run with -Z macro-backtrace for more info) | |
| [0K[0KOK (7.48s) | |
| coverage: warning: trailing semicolon in macro used in expression position | |
| --> src/main.rs:45:46 | |
| | | |
| 45 | return Err(format!($($args)*).into()); | |
| | ^ | |
| ... | |
| 309 | _ => die!("unknown tag {:?} for branch", tag), | |
| | ---------------------------------------- in this macro invocation | |
| | | |
| = warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release! | |
| = note: for more information, see issue #79813 <https://github.com/rust-lang/rust/issues/79813> | |
| = note: `#[warn(semicolon_in_expressions_from_macros)]` on by default | |
| = note: this warning originates in the macro `die` (in Nightly builds, run with -Z macro-backtrace for more info) | |
| [0KFAIL (1.30s) | |
| files test/coverage/coverage.good and test/coverage/coverage.out differ; test/coverage/coverage.out contains: | |
| Use -p '$0=="crux-mir.crux coverage.Output testing.coverage"' to rerun this test only. | |
| coverage_try: warning: trailing semicolon in macro used in expression position | |
| --> src/main.rs:45:46 | |
| | | |
| 45 | return Err(format!($($args)*).into()); | |
| | ^ | |
| ... | |
| 309 | _ => die!("unknown tag {:?} for branch", tag), | |
| | ---------------------------------------- in this macro invocation | |
| | | |
| = warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release! | |
| = note: for more information, see issue #79813 <https://github.com/rust-lang/rust/issues/79813> | |
| = note: `#[warn(semicolon_in_expressions_from_macros)]` on by default | |
| = note: this warning originates in the macro `die` (in Nightly builds, run with -Z macro-backtrace for more info) | |
| [0KFAIL (1.34s) | |
| files test/coverage/coverage_try.good and test/coverage/coverage_try.out differ; test/coverage/coverage_try.out contains: | |
| Use -p '/coverage_try/' to rerun this test only. | |
| coverage_cond: warning: trailing semicolon in macro used in expression position | |
| --> src/main.rs:45:46 | |
| | | |
| 45 | return Err(format!($($args)*).into()); | |
| | ^ | |
| ... | |
| 309 | _ => die!("unknown tag {:?} for branch", tag), | |
| | ---------------------------------------- in this macro invocation | |
| | | |
| = warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release! | |
| = note: for more information, see issue #79813 <https://github.com/rust-lang/rust/issues/79813> | |
| = note: `#[warn(semicolon_in_expressions_from_macros)]` on by default | |
| = note: this warning originates in the macro `die` (in Nightly builds, run with -Z macro-backtrace for more info) | |
| [0KOK (1.35s) | |
| coverage_loop: warning: trailing semicolon in macro used in expression position | |
| --> src/main.rs:45:46 | |
| | | |
| 45 | return Err(format!($($args)*).into()); | |
| | ^ | |
| ... | |
| 309 | _ => die!("unknown tag {:?} for branch", tag), | |
| | ---------------------------------------- in this macro invocation | |
| | | |
| = warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release! | |
| = note: for more information, see issue #79813 <https://github.com/rust-lang/rust/issues/79813> | |
| = note: `#[warn(semicolon_in_expressions_from_macros)]` on by default | |
| = note: this warning originates in the macro `die` (in Nightly builds, run with -Z macro-backtrace for more info) | |
| [0KFAIL (1.35s) | |
| files test/coverage/coverage_loop.good and test/coverage/coverage_loop.out differ; test/coverage/coverage_loop.out contains: | |
| Use -p '/coverage_loop/' to rerun this test only. | |
| coverage_shortcircuit: warning: trailing semicolon in macro used in expression position | |
| --> src/main.rs:45:46 | |
| | | |
| 45 | return Err(format!($($args)*).into()); | |
| | ^ | |
| ... | |
| 309 | _ => die!("unknown tag {:?} for branch", tag), | |
| | ---------------------------------------- in this macro invocation | |
| | | |
| = warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release! | |
| = note: for more information, see issue #79813 <https://github.com/rust-lang/rust/issues/79813> | |
| = note: `#[warn(semicolon_in_expressions_from_macros)]` on by default | |
| = note: this warning originates in the macro `die` (in Nightly builds, run with -Z macro-backtrace for more info) | |
| [0KFAIL (1.33s) | |
| files test/coverage/coverage_shortcircuit.good and test/coverage/coverage_shortcircuit.out differ; test/coverage/coverage_shortcircuit.out contains: | |
| Use -p '/coverage_shortcircuit/' to rerun this test only. | |
| coverage_mono: warning: trailing semicolon in macro used in expression position | |
| --> src/main.rs:45:46 | |
| | | |
| 45 | return Err(format!($($args)*).into()); | |
| | ^ | |
| ... | |
| 309 | _ => die!("unknown tag {:?} for branch", tag), | |
| | ---------------------------------------- in this macro invocation | |
| | | |
| = warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release! | |
| = note: for more information, see issue #79813 <https://github.com/rust-lang/rust/issues/79813> | |
| = note: `#[warn(semicolon_in_expressions_from_macros)]` on by default | |
| = note: this warning originates in the macro `die` (in Nightly builds, run with -Z macro-backtrace for more info) | |
| [0KOK (1.31s) | |
| coverage_match: warning: trailing semicolon in macro used in expression position | |
| --> src/main.rs:45:46 | |
| | | |
| 45 | return Err(format!($($args)*).into()); | |
| | ^ | |
| ... | |
| 309 | _ => die!("unknown tag {:?} for branch", tag), | |
| | ---------------------------------------- in this macro invocation | |
| | | |
| = warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release! | |
| = note: for more information, see issue #79813 <https://github.com/rust-lang/rust/issues/79813> | |
| = note: `#[warn(semicolon_in_expressions_from_macros)]` on by default | |
| = note: this warning originates in the macro `die` (in Nightly builds, run with -Z macro-backtrace for more info) | |
| [0KFAIL (1.31s) | |
| files test/coverage/coverage_match.good and test/coverage/coverage_match.out differ; test/coverage/coverage_match.out contains: | |
| Use -p '/coverage_match/' to rerun this test only. | |
| coverage_macro: warning: trailing semicolon in macro used in expression position | |
| --> src/main.rs:45:46 | |
| | | |
| 45 | return Err(format!($($args)*).into()); | |
| | ^ | |
| ... | |
| 309 | _ => die!("unknown tag {:?} for branch", tag), | |
| | ---------------------------------------- in this macro invocation | |
| | | |
| = warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release! | |
| = note: for more information, see issue #79813 <https://github.com/rust-lang/rust/issues/79813> | |
| = note: `#[warn(semicolon_in_expressions_from_macros)]` on by default | |
| = note: this warning originates in the macro `die` (in Nightly builds, run with -Z macro-backtrace for more info) | |
| [0KFAIL (1.34s) | |
| files test/coverage/coverage_macro.good and test/coverage/coverage_macro.out differ; test/coverage/coverage_macro.out contains: | |
| Use -p '/coverage_macro/' to rerun this test only. | |
| 195 out of 339 tests failed (466.78s) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment