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
commitf59bbf0b942cd888c798c06ba6841bf94562a438 (patch)
tree64c89f63745865e9d0e443dc8cc8ecc2cac7900b /src/settings.sig
parent1607362ff628b9a1476679fbf9146b66ce92a3ee (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