Commit 7012fc39 authored by MARCHE Claude's avatar MARCHE Claude

bench: add bad-bts files

new file for issue 166
parent 5c406a3a
...@@ -253,6 +253,7 @@ goods bench/programs/bad-typing --parse-only ...@@ -253,6 +253,7 @@ goods bench/programs/bad-typing --parse-only
bads bench/typing/bad --type-only bads bench/typing/bad --type-only
bads bench/programs/bad-typing --type-only bads bench/programs/bad-typing --type-only
goods bench/typing/x-bad --type-only goods bench/typing/x-bad --type-only
bads examples/bad-bts
echo "" echo ""
echo "=== Checking good files ===" echo "=== Checking good files ==="
......
type t
constant a : t
val function f t : int
use ref.Ref
let test (x:ref int) : unit = x := f a
module A
use int.Int
use mach.int.Int63
let test (x:int63) : int63
requires { x < 100 }
= x+1
end
(*
module A
use import int.Int
use import mach.int.Int63
val add (x y:int63) : int63
requires { int63'minInt <= int63'int x + int63'int y <= int63'maxInt }
ensures { int63'int result = int63'int x + int63'int y }
let test (x:int63) : int63
requires { int63'int x < 100 }
= add x (1:int63)
end
*)
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment