Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

SDL2 MinGW fix #43

Open
wants to merge 15 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions contrib/SDL2/TEST/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,12 @@ CFLAGS_image += $(shell pkg-config SDL2_image --cflags)

######

PATSHOMERELOCQ="$(PATSHOMERELOC)"
CFLAGS0 += -I$(PATSHOMERELOCQ)/contrib
CFLAGS_image += -I$(PATSHOMERELOCQ)/contrib

######

LDFLAGS0 = $(LDFLAGS)
LDFLAGS_image = $(LDFLAGS)

Expand Down
12 changes: 11 additions & 1 deletion contrib/SDL2/TEST/test00.dats
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,11 @@ staload "./../SATS/SDL.sats"

(* ****** ****** *)

#define ATS_MAINATSFLAG 1
#define ATS_DYNLOADNAME "ats_dynload"

(* ****** ****** *)

val () = let
var ver: SDL_version
val () = SDL_VERSION (ver)
Expand All @@ -22,7 +27,12 @@ end // end of [val]

(* ****** ****** *)

implement main0 () = ()
%{$
int main(int argc, char *argv[]) {
ats_dynload();
return 0;
}
%}

(* ****** ****** *)

Expand Down
17 changes: 15 additions & 2 deletions contrib/SDL2/TEST/test01.dats
Original file line number Diff line number Diff line change
Expand Up @@ -13,12 +13,16 @@ staload "./../SATS/SDL.sats"

(* ****** ****** *)

#define ATS_MAINATSFLAG 1
#define ATS_DYNLOADNAME "ats_dynload"

(* ****** ****** *)

#define NULL the_null_ptr

(* ****** ****** *)

implement
main0 () = () where
val () =
{
//
val err = SDL_Init (SDL_INIT_VIDEO)
Expand Down Expand Up @@ -56,4 +60,13 @@ val () = SDL_Quit ((*void*))

(* ****** ****** *)

%{$
int main(int argc, char *argv[]) {
ats_dynload();
return 0;
}
%}

(* ****** ****** *)

(* end of [test01.dats] *)
17 changes: 15 additions & 2 deletions contrib/SDL2/TEST/test02.dats
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,12 @@ staload "./../SATS/SDL_image.sats"

(* ****** ****** *)

implement
main0 () = () where
#define ATS_MAINATSFLAG 1
#define ATS_DYNLOADNAME "ats_dynload"

(* ****** ****** *)

val () =
{
//
val err = SDL_Init (SDL_INIT_VIDEO)
Expand Down Expand Up @@ -64,4 +68,13 @@ val () = SDL_Quit ((*void*))

(* ****** ****** *)

%{$
int main(int argc, char *argv[]) {
ats_dynload();
return 0;
}
%}

(* ****** ****** *)

(* end of [test02.dats] *)
137 changes: 137 additions & 0 deletions contrib/libats-/ashalkhakov/DATS/offset.dats
Original file line number Diff line number Diff line change
@@ -0,0 +1,137 @@
#include
"share/atspre_define.hats"
#include
"share/atspre_staload.hats"

(* ****** ****** *)

staload UN = "prelude/SATS/unsafe.sats"

(* ****** ****** *)

staload "./../SATS/offset.sats"

(* ****** ****** *)

local
//
dataprop offset_p (int, int, bool) =
| {n:int} offset_p_none (~1, n, false)
| {i,n:int | i >= 0; i < n} offset_p_some (i, n, true)
//
prfun
offset_p_sub {i:int} {n,m:int | n <= m} {b:bool} .< >.
(pf: offset_p (i, n, b)):<> offset_p (i, m, b) =
case+ pf of
| offset_p_none () => offset_p_none ()
| offset_p_some () => offset_p_some ()
// end of [offset_p_sub]
//
assume offset (a:vt@ype+, n:int, b:bool) =
[i:int] (offset_p (i, n, b) | int i)
//
in // in of [local]
//
primplement
offset_sizeof_lemma {a} {n} {b} () = ()
//
implement
offset_make {a} {n} (i) = (offset_p_some () | i)
//
implement
offset_cast {a} {n,m} (o) = (offset_p_sub o.0 | o.1)
//
implement
offset_elim {a} {n} (o) = o.1 where {
prval offset_p_some () = o.0
} (* end of [offset_elim] *)
//
implement
offset_make_nil {a} {n} () = (offset_p_none () | ~1)
//
implement
offset_is_some {a} {n} {b}
(o) = (
if o.1 = ~1 then let
prval offset_p_none () = o.0
in false end else let
prval offset_p_some () = o.0
in true end
) (* end of [offset_is_some] *)
//
implement{a}
offset_getopt {n} {b}
(arr, o, res) =
if offset_is_some (o) then let
val (pf_at, fpf | po) = offset2ptr<a> (view@arr | addr@arr, o)
val () = res := !po
prval () = opt_some {a} (res)
prval () = fpf (pf_at, view@arr)
in
true
end else let
prval () = opt_none {a} (res)
in
false
end
// end of [offset_getopt]
//
implement{a}
offset_get {n}
(arr, o, res) = let
val (pf_at, fpf | po) = offset2ptr<a> (view@arr | addr@arr, o)
val () = res := !po
prval () = fpf (pf_at, view@arr)
in
// empty
end // end of [offset_get]
//
implement{a}
offset_set {n}
(arr, o, x) = let
val (pf_at, fpf | po) = offset2ptr<a> (view@arr | addr@arr, o)
val () = !po := x
prval () = fpf (pf_at, view@arr)
in
// empty
end // end of [offset_set]
//
implement{a}
offset2ptropt {n} {l} {b} (
pf_arr
| p, o
) = (
if o.1 > ~1 then let
prval offset_p_some () = o.0
val (pf_at, fpf | po) = offset2ptr<a> (pf_arr | p, o)
prval () = __trustme (pf_at) where {
extern
prfun
__trustme {l:addr} (!a @ l): [l > null] void
} // end of [prval]
in
(Some_v @(pf_at, fpf) | po)
end else let
prval offset_p_none () = o.0
in
(None_v () | the_null_ptr)
end
) (* end of [offset2ptropt] *)
//
implement{a}
offset2ptr {n} {l}
(pf_arr | p_arr, o) = (pf, fpf | po) where {
prval offset_p_some () = o.0
val po = ptr_add<a> (p_arr, o.1)
prval (pf, fpf) = __trustme (pf_arr, po) where {
extern
prfun
__trustme {l1:addr}
(!array_v (a, l, n), ptr l1)
: (a @ l1, (a @ l1, !array_v (a, l, n)) -<lin,prf> void)
} // end of [prval]
} // end of [offset2ptr]
//
end // end of [local]
//
(* ****** end of [offset.dats] ****** *)
67 changes: 67 additions & 0 deletions contrib/libats-/ashalkhakov/DATS/rbuf.dats
Original file line number Diff line number Diff line change
@@ -0,0 +1,67 @@
(* ****** ****** *)

#include
"share/atspre_define.hats"
#include
"share/atspre_staload.hats"

(* ****** ****** *)

staload "./../SATS/rbuf.sats"

(* ****** ****** *)
//
local
//
// NB. the structure of the type closely follows
// the structure given in the interface; we are only
// allowed to refine the tuple elements, but not
// add some new elements, even if we only add proofs
// NB. we don't add a top-level constraint to the top (e.g. [n>=0])
assume rbuf_vt (a:t@ype, n:int, m:int, l:addr) = @(
(array_v (a, l, n), array_v (a, l + n*sizeof(a), m-n) | ptr (l + n*sizeof(a)))
, size_t (m-n)
) (* end of [buf_vt] *)
//
in (* of [local] *)
//
implement{a}
rbuf_make {n} {l} (pf_bytes | p, n, buf) = () where {
prval () = lemma_array_v_param {a} (pf_bytes)
prval () = $effmask_wrt (buf.0.0 := array_v_nil {a} ())
prval () = $effmask_wrt (buf.0.1 := pf_bytes)
val () = buf.0.2 := p
val () = buf.1 := n
} (* end of [rbuf_make] *)
//
implement{a}
rbuf_free {m,n} {l} (buf) = let
prval pf_arr = array_v_unsplit (buf.0.0, buf.0.1)
in
(pf_arr | ())
end // end of [rbuf_free]
//
implement{a}
rbuf_check {n,m} {l} (buf) = buf.1 > g1int2uint_int_size(0)
//
implement{a}
rbuf_rem {n,m} {l} (buf) = g1uint2int_size_int (buf.1)
//
implement{a}
rbuf_read {n,m} {l} (buf) = let
prval pf1_arr = buf.0.0
prval (pf1_at, pf2_arr) = array_v_uncons {a} {l+n*sizeof(a)} (buf.0.1)
val c = ptr_get<a> (pf1_at | buf.0.2)
val () = buf.0.2 := ptr1_succ (buf.0.2)
val () = buf.1 := pred (buf.1)
prval pf1_arr = array_v_extend (pf1_arr, pf1_at)
// why does it complain about wrt effect?
prval () = $effmask_wrt (buf.0.0 := pf1_arr)
prval () = $effmask_wrt (buf.0.1 := pf2_arr)
in
c
end // end of [rbuf_read]
//
end (* of [local] *)
//
(* ****** end of [rbuf.dats] ****** *)
Loading