summaryrefslogtreecommitdiff
path: root/src/settings.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-02-27 16:49:11 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-02-27 16:49:11 -0500
commit0c209d971e2813d9a5e3cac699f3f5c8ad278f7d (patch)
tree64c89f63745865e9d0e443dc8cc8ecc2cac7900b /src/settings.sig
parent3e9d47d0248f71983209f5a8640aa160bcf564a5 (diff)
benignEffectful
Diffstat (limited to 'src/settings.sig')
-rw-r--r--src/settings.sig4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/settings.sig b/src/settings.sig
index 348c47d4..3179c229 100644
--- a/src/settings.sig
+++ b/src/settings.sig
@@ -58,6 +58,10 @@ signature SETTINGS = sig
val setEffectful : ffi list -> unit
val isEffectful : ffi -> bool
+ (* Which FFI functions should not have their calls removed or reordered, but cause no lasting effects? *)
+ val setBenignEffectful : ffi list -> unit
+ val isBenignEffectful : ffi -> bool
+
(* Which FFI functions may only be run in clients? *)
val setClientOnly : ffi list -> unit
val isClientOnly : ffi -> bool