You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Wasn't sure if this was a bug or a basically satisfactory and intentional error message (either way it probably doesn't matter); think my code should have TESTPROP not TESTPROP().
(* ****** ****** *)
//
#include
"share/atspre_define.hats"
#include
"share/atspre_staload.hats"
//
(* ****** ****** *)
%{^
int do_adding() {
volatile unsigned int i = 1;
while(i >= 0) {
i = i + 1;
}
return -1;
}
%}
extern
fun do_adding():int = "mac#"
// Now with proofs:
dataprop TESTPROP() =
| TEST of ()
extern
fun do_adding_usepf(pf: TESTPROP):int = "mac#"
implement main0() = let
// val x = do_adding() and y = do_adding()
// same cpu usage as:
// val x = do_adding()
//prval a
//val x = do_adding1()
in
println!(x)
end
The text was updated successfully, but these errors were encountered:
Wasn't sure if this was a bug or a basically satisfactory and intentional error message (either way it probably doesn't matter); think my code should have TESTPROP not TESTPROP().
The text was updated successfully, but these errors were encountered: