FFI: Add test for runtime errors

This commit is contained in:
Bretton 2022-08-11 17:23:37 -07:00
parent 8a274d08b1
commit 4fd7e175d9
4 changed files with 49 additions and 0 deletions

View File

@ -0,0 +1,10 @@
#include <stddef.h>
#include <stdint.h>
uint8_t f(size_t n, uint8_t *p) {
return n == 0;
}
uint8_t g(uint8_t x) {
return x;
}

View File

@ -0,0 +1,2 @@
foreign f : {n} (fin n, n >= 2^^64) => [n - 2^^64][8] -> Bit
foreign g : Bit -> Bit

View File

@ -0,0 +1,9 @@
:! make -s ffi-runtime-errors
:l ffi-runtime-errors.cry
f []
:prove g
:sat g
:safe g
:eval g

View File

@ -0,0 +1,28 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
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.