blob: 8208fd3fab492ac19386ca8afadbf293e1ea8b25 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
type S = (
[typestate Uninitialized, Connected, Closed]
int socket [when Connected]
int bytes_sent [when Connected,Closed]
)
# or
type S = private [typestate Uninitialized, Connected, Closed]
type S = (
int socket [when Connected]
int bytes_sent [when Connected,Closed]
)
# more:
func work(int i [!= 0]) return int [!= 0]
{
int j [< i] = blabla(i)
cond [j != 4]
return i - j
}
# since constraint validation is cumbersome, it could be done as follows:
# - statically at compile time, when requested
# - statically at compile time, when there could be UB (how to detect this?)
# - at runtime, when requested at compile time (like clang's sanitizers) - statically at compile time,
# which conditions should be supported? perhaps these:
# - typestates
# - the following for non-var (and non-shared?) values?
# - enum in / not in / = / !=
# - elementary type = / !=
# - integer < > <= >= = !=
|
