Running tests tests: constraint-guards: constant.icry: [Failed] 0a1 > ld: warning: -undefined dynamic_lookup may not work with chained fixups 18a20,22 > > Parse error at constant.icry:6:0, > unexpected: end of file # If output is OK: cp /Users/ur20980/src/cryptol/output/tests/constraint-guards/constant.icry.stdout \ /Users/ur20980/src/cryptol/tests/constraint-guards/constant.icry.stdout inits.icry: [OK] insert.icry: [OK] len.icry: [OK] mergesort.icry: [OK] nestMod.icry: [OK] noNested.icry: [OK] noPrim.icry: [OK] tail.icry: [OK] examples: allexamples.icry: [OK] ffi: ffi-header.icry: [OK] ffi-reload.icry: [Failed] 1a2,4 > ld: library not found for -lgmp > clang: error: linker command failed with exit code 1 (use -v to see invocation) > make: *** [ffi-reload.dylib] Error 1 4,5c7,17 < Loading dynamic library ffi-reload.dylib < False --- > > [error] Failed to load foreign implementations for module Main: > Could not load foreign source for module located at /Users/ur20980/src/cryptol/tests/ffi/ffi-reload.cry: > user error (dlopen: dlopen(/Users/ur20980/src/cryptol/tests/ffi/ffi-reload.dylib, 0x0002): tried: '/Users/ur20980/src/cryptol/tests/ffi/ffi-reload.dylib' (no such file)) > user error (dlopen: dlopen(/Users/ur20980/src/cryptol/tests/ffi/ffi-reload.so, 0x0002): tried: '/Users/ur20980/src/cryptol/tests/ffi/ffi-reload.so' (no such file)) > > [error] at ffi-reload.icry:9:1--9:5 > Value not in scope: test > ld: library not found for -lgmp > clang: error: linker command failed with exit code 1 (use -v to see invocation) > make: *** [ffi-reload.dylib] Error 1 8,9c20,27 < Loading dynamic library ffi-reload.dylib < True --- > > [error] Failed to load foreign implementations for module Main: > Could not load foreign source for module located at /Users/ur20980/src/cryptol/tests/ffi/ffi-reload.cry: > user error (dlopen: dlopen(/Users/ur20980/src/cryptol/tests/ffi/ffi-reload.dylib, 0x0002): tried: '/Users/ur20980/src/cryptol/tests/ffi/ffi-reload.dylib' (no such file)) > user error (dlopen: dlopen(/Users/ur20980/src/cryptol/tests/ffi/ffi-reload.so, 0x0002): tried: '/Users/ur20980/src/cryptol/tests/ffi/ffi-reload.so' (no such file)) > > [error] at ffi-reload.icry:21:1--21:5 > Value not in scope: test # If output is OK: cp /Users/ur20980/src/cryptol/output/tests/ffi/ffi-reload.icry.stdout \ /Users/ur20980/src/cryptol/tests/ffi/ffi-reload.icry.stdout.darwin ffi-runtime-errors.icry: [Failed] 1a2,4 > ld: library not found for -lgmp > clang: error: linker command failed with exit code 1 (use -v to see invocation) > make: *** [ffi-runtime-errors.dylib] Error 1 4d6 < Loading dynamic library ffi-runtime-errors.dylib 6,29c8,26 < numeric type argument to foreign function is too large: 18446744073709551616 < in type parameter n`899 of function Main::f < type arguments must fit in a C `size_t` < -- Backtrace -- < Main::f called at ffi-runtime-errors.icry:4:1--4:2 < < cannot call foreign function Main::g < FFI calls are not supported in this context < If you are trying to evaluate an expression, try rebuilding < Cryptol with FFI support enabled. < < cannot call foreign function Main::g < FFI calls are not supported in this context < If you are trying to evaluate an expression, try rebuilding < Cryptol with FFI support enabled. < < cannot call foreign function Main::g < FFI calls are not supported in this context < If you are trying to evaluate an expression, try rebuilding < Cryptol with FFI support enabled. < cannot call foreign function Main::g < FFI calls are not supported in this context < If you are trying to evaluate an expression, try rebuilding < Cryptol with FFI support enabled. --- > [error] Failed to load foreign implementations for module Main: > Could not load foreign source for module located at /Users/ur20980/src/cryptol/tests/ffi/ffi-runtime-errors.cry: > user error (dlopen: dlopen(/Users/ur20980/src/cryptol/tests/ffi/ffi-runtime-errors.dylib, 0x0002): tried: '/Users/ur20980/src/cryptol/tests/ffi/ffi-runtime-errors.dylib' (no such file)) > user error (dlopen: dlopen(/Users/ur20980/src/cryptol/tests/ffi/ffi-runtime-errors.so, 0x0002): tried: '/Users/ur20980/src/cryptol/tests/ffi/ffi-runtime-errors.so' (no such file)) > > [error] at ffi-runtime-errors.icry:4:1--4:2 > Value not in scope: f > > [error] at ffi-runtime-errors.icry:6:8--6:9 > Value not in scope: g > > [error] at ffi-runtime-errors.icry:7:6--7:7 > Value not in scope: g > > [error] at ffi-runtime-errors.icry:8:7--8:8 > Value not in scope: g > > [error] at ffi-runtime-errors.icry:9:7--9:8 > Value not in scope: g # If output is OK: cp /Users/ur20980/src/cryptol/output/tests/ffi/ffi-runtime-errors.icry.stdout \ /Users/ur20980/src/cryptol/tests/ffi/ffi-runtime-errors.icry.stdout.darwin ffi-type-errors.icry: [OK] test-ffi.icry: [Failed] 1a2,7 > In file included from test-ffi.c:6: > ./test-ffi.h:1:10: fatal error: 'gmp.h' file not found > #include > ^~~~~~~ > 1 error generated. > make: *** [test-ffi.dylib] Error 1 5,44c11,108 < Loading dynamic library test-ffi.dylib < 0x03 < 0x15b4 < 0x3a0f1880 < 0x00000002e90edc8f < 0x07 < 0x7 < 0x0 < False < 0x45.1eb8 < -0x1e61.c71de69ad5 < fpPosInf < fpNegInf < fpNaN < -0.0 < True < 0x00000037 < [0xb.cd, -0x9.0a, 0x6.78, -0x3.45, 0x1.23] < {a = (0x1234, 0x5678), < b = {c = [0x0000a, 0x00014, 0x0001e, 0x00028, 0x00032, 0x0003c, < 0x00046, 0x00050], < d = 0x09, < e = 0x0c}} < 0x12345678deadbeef < 0x00000000 < 0x00000037 < 0x02fb0408 < [0x01, 0x01, 0x02, 0x01, 0x02, 0x03, 0x01, 0x02, 0x03, 0x04, 0x01, < 0x02, 0x03, 0x04, 0x05] < [0x12.0, 0x38.0, 0x78.0] < [[[0x01, 0x02], [0x03, 0x04], [0x05, 0x06]], < [[0x07, 0x08], [0x09, 0x0a], [0x0b, 0x0c]], < [[0x0d, 0x0e], [0x0f, 0x10], [0x11, 0x12]], < [[0x13, 0x14], [0x15, 0x16], [0x17, 0x18]]] < (ratio 2 1) < [(ratio 4 1), (ratio 1 4)] < ((ratio 37 1), 72) < 2 < 0 < 1 --- > > [error] Failed to load foreign implementations for module Main: > Could not load foreign source for module located at /Users/ur20980/src/cryptol/tests/ffi/test-ffi.cry: > user error (dlopen: dlopen(/Users/ur20980/src/cryptol/tests/ffi/test-ffi.dylib, 0x0002): tried: '/Users/ur20980/src/cryptol/tests/ffi/test-ffi.dylib' (no such file)) > user error (dlopen: dlopen(/Users/ur20980/src/cryptol/tests/ffi/test-ffi.so, 0x0002): tried: '/Users/ur20980/src/cryptol/tests/ffi/test-ffi.so' (no such file)) > > [error] at test-ffi.icry:4:1--4:5 > Value not in scope: add8 > > [error] at test-ffi.icry:5:1--5:6 > Value not in scope: sub16 > > [error] at test-ffi.icry:6:1--6:6 > Value not in scope: mul32 > > [error] at test-ffi.icry:7:1--7:6 > Value not in scope: div64 > > [error] at test-ffi.icry:9:1--9:12 > Value not in scope: extendInput > > [error] at test-ffi.icry:10:1--10:11 > Value not in scope: maskOutput > > [error] at test-ffi.icry:11:1--11:7 > Value not in scope: noBits > > [error] at test-ffi.icry:13:1--13:4 > Value not in scope: not > > [error] at test-ffi.icry:15:1--15:11 > Value not in scope: addFloat32 > > [error] at test-ffi.icry:16:1--16:11 > Value not in scope: subFloat64 > > [error] at test-ffi.icry:17:1--17:14 > Value not in scope: specialFloats > > [error] at test-ffi.icry:18:1--18:14 > Value not in scope: specialFloats > > [error] at test-ffi.icry:19:1--19:14 > Value not in scope: specialFloats > > [error] at test-ffi.icry:20:1--20:14 > Value not in scope: specialFloats > > [error] at test-ffi.icry:22:1--22:16 > Value not in scope: usesTypeSynonym > > [error] at test-ffi.icry:24:1--24:6 > Value not in scope: sum10 > > [error] at test-ffi.icry:25:1--25:9 > Value not in scope: reverse5 > > [error] at test-ffi.icry:27:1--27:14 > Value not in scope: compoundTypes > > [error] at test-ffi.icry:29:1--29:12 > Value not in scope: typeToValue > > [error] at test-ffi.icry:30:1--30:8 > Value not in scope: sumPoly > > [error] at test-ffi.icry:31:1--31:8 > Value not in scope: sumPoly > > [error] at test-ffi.icry:32:1--32:8 > Value not in scope: sumPoly > > [error] at test-ffi.icry:33:1--33:6 > Value not in scope: inits > > [error] at test-ffi.icry:34:1--34:8 > Value not in scope: zipMul3 > > [error] at test-ffi.icry:36:1--36:10 > Value not in scope: nestedSeq > > [error] at test-ffi.icry:38:1--38:4 > Value not in scope: i2Q > > [error] at test-ffi.icry:39:1--39:5 > Value not in scope: i2Qs > > [error] at test-ffi.icry:40:1--40:6 > Value not in scope: iQ2Qi > > [error] at test-ffi.icry:41:1--41:5 > Value not in scope: i2Z5 > > [error] at test-ffi.icry:42:1--42:5 > Value not in scope: i2Z5 > > [error] at test-ffi.icry:43:1--43:4 > Value not in scope: i2Z # If output is OK: cp /Users/ur20980/src/cryptol/output/tests/ffi/test-ffi.icry.stdout \ /Users/ur20980/src/cryptol/tests/ffi/test-ffi.icry.stdout.darwin issues: T1179.icry: [OK] T146.icry: [OK] T820.icry: [OK] issue002.icry: [OK] issue006.icry: [OK] issue058.icry: [OK] issue066.icry: [OK] issue072.icry: [OK] issue073.icry: [OK] issue081.icry: [OK] issue083.icry: [OK] issue084.icry: [OK] issue086.icry: [OK] issue087.icry: [OK] issue090.icry: [OK] issue093.icry: [OK] issue094.icry: [OK] issue098.icry: [OK] issue101.icry: [OK] issue1024.icry: [OK] issue103.icry: [OK] issue104.icry: [OK] issue1040.icry: [OK] issue1044.icry: [OK] issue1049.icry: [OK] issue108.icry: [OK] issue1093.icry: [OK] issue1133.icry: [OK] issue116.icry: [OK] issue1191.icry: [OK] issue1210.icry: [OK] issue1240.icry: [OK] issue1253.icry: [OK] issue126.icry: [OK] issue127.icry: [OK] issue128.icry: [OK] issue130.icry: [OK] issue1322.icry: [OK] issue1324.icry: [OK] issue133.icry: [OK] issue1344.icry: [OK] issue135.icry: [OK] issue1359.icry: [OK] issue138.icry: [OK] issue141.icry: [OK] issue1415.icry: [OK] issue1435.icry: [OK] issue1441_a.icry: [OK] issue1441_b.icry: [OK] issue148.icry: [OK] issue149.icry: [OK] issue150.icry: [OK] issue152.icry: [OK] issue158.icry: [OK] issue160.icry: [OK] issue167.icry: [OK] issue171.icry: [OK] issue177.icry: [OK] issue184.icry: [OK] issue185.icry: [OK] issue187.icry: [OK] issue198.icry: [OK] issue202.icry: [OK] issue211.icry: [OK] issue212.icry: [OK] issue214.icry: [OK] issue220.icry: [OK] issue225.icry: [OK] issue226.icry: [OK] issue256.icry: [OK] issue268.icry: [OK] issue290.icry: [OK] issue290v2.icry: [OK] issue304.icry: [OK] issue306.icry: [OK] issue308.icry: [OK] issue312.icry: [OK] issue314.icry: [OK] issue322.icry: [OK] issue323.icry: [OK] issue325.icry: [OK] issue334.icry: [OK] issue335.icry: [OK] issue364.icry: [OK] issue368.icry: [OK] issue382.icry: [OK] issue389.icry: [OK] issue395.icry: [OK] issue406.icry: [OK] issue407.icry: [OK] issue408.icry: [OK] issue410.icry: [OK] issue413.icry: [OK] issue416.icry: [OK] issue463.icry: [OK] issue474.icry: [OK] issue485.icry: [OK] issue486.icry: [OK] issue494.icry: [OK] issue513.icry: [OK] issue533.icry: [OK] issue565.icry: [OK] issue567.icry: [OK] issue581.icry: [OK] issue582.icry: [OK] issue607.icry: [OK] issue614.icry: [OK] issue639.icry: [OK] issue640.icry: [OK] issue662.icry: [OK] issue664.icry: [OK] issue667.icry: [OK] issue670.icry: [OK] issue68.icry: [OK] issue702.icry: [OK] issue712.icry: [OK] issue713.icry: [OK] issue723.icry: [OK] issue725.icry: [OK] issue731.icry: [OK] issue734.icry: [OK] issue746.icry: [OK] issue78.icry: [OK] issue796.icry: [OK] issue805.icry: [OK] issue818.icry: [OK] issue826.icry: [OK] issue835.icry: [OK] issue838.icry: [OK] issue845.icry: [OK] issue848.icry: [OK] issue850.icry: [OK] issue851.icry: [OK] issue852.icry: [OK] issue861.icry: [OK] issue876.icry: [OK] issue877.icry: [OK] issue883.icry: [OK] issue883_A.icry: [OK] issue894.icry: [OK] issue910.icry: [OK] issue913.icry: [OK] issue933.icry: [OK] issue958.icry: [OK] issue962.icry: [OK] issue975.icry: [OK] padding.icry: [OK] trac133.icry: [OK] trac289.icry: [OK] transpose0.icry: [OK] modsys: T1.icry: [OK] T10.icry: [OK] T11.icry: [OK] T12.icry: [OK] T13.icry: [OK] T1330.icry: [OK] T14.icry: [OK] T15.icry: [OK] T16.icry: [OK] T17.icry: [OK] T18.icry: [OK] T2.icry: [OK] T3.icry: [OK] T4.icry: [OK] T5.icry: [OK] T6.icry: [OK] T7.icry: [OK] T8.icry: [OK] T9.icry: [OK] nested: T1.icry: [OK] T10.icry: [OK] T11.icry: [OK] T12.icry: [OK] T13.icry: [OK] T14.icry: [OK] T15.icry: [OK] T2.icry: [OK] T3.icry: [OK] T4.icry: [OK] T5.icry: [OK] T6.icry: [OK] T7.icry: [OK] T8.icry: [OK] T9.icry: [OK] relative-include: relative-include.icry: [OK] mono-binds: test01.icry: [OK] test02.icry: [OK] test03.icry: [OK] test04.icry: [OK] test05.icry: [OK] test06.icry: [OK] parser: T437.icry: [OK] docs.icry: [OK] infix-1.icry: [OK] infix-2.icry: [OK] infix-3.icry: [OK] multi-if-1.icry: [OK] unary-2.icry: [OK] unary.icry: [OK] regression: AES.icry: [OK] EvenMansour.icry: [OK] allsat.icry: [OK] array.icry: [OK] bitshift.icry: [OK] bvdiv.icry: [OK] check01.icry: [OK] check02.icry: [OK] check03.icry: [OK] check04.icry: [OK] check05.icry: [OK] check06.icry: [OK] check07.icry: [OK] check08.icry: [OK] check09.icry: [OK] check10.icry: [OK] check11.icry: [OK] check12.icry: [OK] check13.icry: [OK] check14.icry: [OK] check15.icry: [OK] check16-tab.icry: [OK] check16.icry: [OK] check17.icry: [OK] check18.icry: [OK] check19.icry: [OK] check20.icry: [OK] check21.icry: [OK] check22.icry: [OK] check229.icry: [OK] check23.icry: [OK] check24.icry: [OK] check25.icry: [OK] check26.icry: [OK] check27.icry: [OK] check28.icry: [OK] check29.icry: [OK] check30.icry: [OK] check31.icry: [OK] cplx.icry: [Failed] 1a2,3 > Warning: solver interaction failed with w4-cvc4 > user error (Could not find: cvc4) 15,19c17,19 < Q.E.D. < :prove cplxMulAssoc < Q.E.D. < :prove cplxMulDistrib < Q.E.D. --- > > What4 exception: > user error (Could not find: cvc4) 29,33c29,31 < Q.E.D. < :prove cplxMulAssoc < Counterexample < :prove cplxMulDistrib < Counterexample --- > > What4 exception: > user error (Could not find: cvc4) # If output is OK: cp /Users/ur20980/src/cryptol/output/tests/regression/cplx.icry.stdout \ /Users/ur20980/src/cryptol/tests/regression/cplx.icry.stdout dumptests.icry: [OK] explicit-strides.icry: [OK] f2polytest.icry: [OK] float.icry: [OK] frac_lit.icry: [OK] ignore-safe.icry: [OK] instance.icry: [OK] itreuse.icry: [OK] layout01.icry: [OK] layout02.icry: [OK] negshift.icry: [OK] poly.icry: [Failed] 1a2,3 > Warning: solver interaction failed with w4-cvc4 > user error (Could not find: cvc4) 13,17c15,17 < Q.E.D. < :prove polyAddEval < Q.E.D. < :prove polyMulEval < Q.E.D. --- > > What4 exception: > user error (Could not find: cvc4) # If output is OK: cp /Users/ur20980/src/cryptol/output/tests/regression/poly.icry.stdout \ /Users/ur20980/src/cryptol/tests/regression/poly.icry.stdout primes.icry: [OK] r01.icry: [OK] r02.icry: [OK] r03.icry: [OK] r04.icry: [OK] r05.icry: [OK] rational_properties.icry: [Failed] 51a52,53 > Warning: solver interaction failed with w4-cvc4 > user error (Could not find: cvc4) 53,99c55,57 < Q.E.D. < :prove QaddComm < Q.E.D. < :prove QaddAssoc < Q.E.D. < :prove Qneg < Q.E.D. < :prove QmulUnit < Q.E.D. < :prove QmulComm < Q.E.D. < :prove QmulAssoc < Q.E.D. < :prove Qdistrib < Q.E.D. < :prove Qrecip < Q.E.D. < :prove QdivisionEquiv < Q.E.D. < :prove QordEquiv1 < Q.E.D. < :prove QordEquiv2 < Q.E.D. < :prove QordTrans < Solver returned UNKNOWN < :prove QordIrreflexive < Q.E.D. < :prove QordExclusive < Q.E.D. < :prove Qtrichotomy < Q.E.D. < :prove QordCompatible < Q.E.D. < :prove QordPositive < Q.E.D. < :prove Qdense < Q.E.D. < :prove intDivDown < Q.E.D. < :prove floorCorrect1 < Q.E.D. < :prove floorCorrect2 < Q.E.D. < :prove ceilingCorrect1 < Q.E.D. < :prove ceilingCorrect2 < Q.E.D. --- > > What4 exception: > user error (Could not find: cvc4) # If output is OK: cp /Users/ur20980/src/cryptol/output/tests/regression/rational_properties.icry.stdout \ /Users/ur20980/src/cryptol/tests/regression/rational_properties.icry.stdout rec-update.icry: [OK] reference.icry: [OK] repeatFields.icry: [OK] repl-decls.icry: [OK] safety.icry: [OK] sort.icry: [OK] specialize.icry: [OK] superclass.icry: [OK] tc-errors.icry: [OK] twinmult.icry: [OK] word-update.icry: [OK] xor-precedence.icry: [OK] renamer: comp01.icry: [OK] comp02.icry: [OK] import01.icry: [OK] rename01.icry: [OK] suiteb: ECDSAKeyPair.icry: [OK] ECDSASigGen.icry: [OK] ECDSASigVerify.icry: [OK] aes-mct-ecb.icry: [OK] aes-vectors.icry: [OK] sha224-mct.icry: [OK] sha224-vectors-long.icry: [OK] sha224-vectors-short.icry: [OK] sha256-mct.icry: [OK] sha256-vectors-long.icry: [OK] sha256-vectors-short.icry: [OK] sha384-mct.icry: [OK] sha384-vectors-long.icry: [OK] sha384-vectors-short.icry: [OK] sha512-mct.icry: [OK] sha512-vectors-long.icry: [OK] sha512-vectors-short.icry: [OK] Test Cases Total Passed 299 299 Failed 7 7 Total 306 306