Skip to content

Instantly share code, notes, and snippets.

@RyanGlScott
Created March 21, 2023 14:40
Show Gist options
  • Save RyanGlScott/ba57ccfd36553d7f0540d1c965af70c9 to your computer and use it in GitHub Desktop.
Save RyanGlScott/ba57ccfd36553d7f0540d1c965af70c9 to your computer and use it in GitHub Desktop.
crux-mir test suite progress
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: FAIL (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: FAIL (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: FAIL (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: FAIL (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: FAIL (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: FAIL (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: FAIL (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: FAIL (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: FAIL (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: FAIL (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: FAIL (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: FAIL (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: FAIL (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: FAIL (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: FAIL (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: FAIL (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: FAIL (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: FAIL (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]