mirror of
https://github.com/yugr/Implib.so
synced 2026-06-08 18:33:41 +00:00
Yury Gribov
32 lines
486 B
INI
32 lines
486 B
INI
SPECIFICATION
|
|
Spec
|
|
|
|
(*
|
|
TODO: more invariants
|
|
*)
|
|
|
|
INVARIANT
|
|
TypeInvariant
|
|
LockInvariant
|
|
LoadBeforeUse
|
|
LoadBeforeUse2
|
|
LibHandleCorrectness
|
|
|
|
PROPERTIES
|
|
Termination
|
|
NoLibResets
|
|
NoShimResets
|
|
|
|
CONSTANTS
|
|
\* Concurrent threads
|
|
THREADS = {1, 2}
|
|
NoThread = 0
|
|
\* Library functions
|
|
FUNS = {"foo", "bar"}
|
|
\* Number of calls in each thread and in library ctor
|
|
CALLS = 2
|
|
\* Max callstack size
|
|
MAX_DEPTH = 2
|
|
\* Max number of recursive mutex locks
|
|
MAX_LOCK = 3
|