test-pgm-jcf.mlw 366 Bytes
Newer Older
1

2 3
module P

4
  use import int.Int
5
  use import module stdlib.Ref
6

7 8 9 10 11
(* let create sz = *)
(*   { 0 <= sz <= maxlen } *)
(*   ref (SA (malloc sz) (malloc sz) (malloc sz) sz 0) *)
(*   { invariant_ result and *)
(*     sa_sz result = sz and forall i:int. model result i = default } *)
12
end
13

14 15
(*
Local Variables: 
16
compile-command: "unset LANG; make -C .. testl-ide"
17 18
End: 
*)