Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
fc4eaa70
Commit
fc4eaa70
authored
May 31, 2011
by
Jean-Christophe Filliâtre
Browse files
more tests in 'make bench'
parent
295ccce2
Changes
2
Hide whitespace changes
Inline
Side-by-side
bench/programs/bad-typing/at1.mlw
0 → 100644
View file @
fc4eaa70
module M
use import int.Int
use import module ref.Ref
let test (a: (ref int, int)) =
{}
let (r,_) = a in r := !r + 1
{ let (x, _) = a in !x = (old !x) + 1 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/bad-typing/at1"
End:
*)
bench/programs/good/labels.mlw
0 → 100644
View file @
fc4eaa70
module Labels
use import int.Int
use import module ref.Ref
logic fst (x: ('a, 'b)) : 'a = let (x1, _) = x in x1
let test (a: (ref int, int)) =
{}
let (r,_) = a in r := !r + 1
{ !(fst a) = (old !(fst a)) + 1 }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../../.. bench/programs/good/labels"
End:
*)
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment