@@ -37,18 +37,22 @@ class SignalCheckOperation extends EqualityOperation, GuardCondition {
37
37
)
38
38
}
39
39
40
+ ControlFlowNode getCheckedSuccessor ( ) {
41
+ result != errorSuccessor and result = this .getASuccessor ( )
42
+ }
43
+
40
44
ControlFlowNode getErrorSuccessor ( ) { result = errorSuccessor }
41
45
}
42
46
43
47
/**
44
48
* Models signal handlers that call signal() and return
45
49
*/
46
50
class SignalCallingHandler extends Function {
47
- SignalCall sh ;
51
+ SignalCall registration ;
48
52
49
53
SignalCallingHandler ( ) {
50
54
// is a signal handler
51
- this = sh .getArgument ( 1 ) .( FunctionAccess ) .getTarget ( ) and
55
+ this = registration .getArgument ( 1 ) .( FunctionAccess ) .getTarget ( ) and
52
56
// calls signal() on the handled signal
53
57
exists ( SignalCall sCall |
54
58
sCall .getEnclosingFunction ( ) = this and
@@ -63,18 +67,35 @@ class SignalCallingHandler extends Function {
63
67
)
64
68
}
65
69
66
- SignalCall getHandler ( ) { result = sh }
70
+ SignalCall getCall ( ) { result = registration }
71
+ }
72
+
73
+ /**
74
+ * CFG nodes preceeding `ErrnoRead`
75
+ */
76
+ ControlFlowNode preceedErrnoRead ( ErrnoRead er ) {
77
+ result = er
78
+ or
79
+ exists ( ControlFlowNode mid |
80
+ result = mid .getAPredecessor ( ) and
81
+ mid = preceedErrnoRead ( er ) and
82
+ // stop recursion on calls to `abort` and `_Exit`
83
+ not result .( FunctionCall ) .getTarget ( ) .hasGlobalName ( [ "abort" , "_Exit" ] ) and
84
+ // stop recursion on successful `SignalCheckOperation`
85
+ not result = any ( SignalCheckOperation o ) .getCheckedSuccessor ( )
86
+ )
67
87
}
68
88
69
- from ErrnoRead errno , SignalCall h
89
+ from ErrnoRead errno , SignalCall signal
70
90
where
71
91
not isExcluded ( errno , Contracts5Package:: doNotRelyOnIndeterminateValuesOfErrnoQuery ( ) ) and
72
- exists ( SignalCallingHandler sc | sc . getHandler ( ) = h |
73
- // errno read in the handler
74
- sc . calls * ( errno . getEnclosingFunction ( ) )
92
+ exists ( SignalCallingHandler handler |
93
+ // errno read after the handler returns
94
+ handler . getCall ( ) = signal
75
95
or
76
- // errno is read after the handle returns
77
- sc .getHandler ( ) = h and
78
- errno .getAPredecessor + ( ) = h
96
+ // errno read inside the handler
97
+ signal .getEnclosingFunction ( ) = handler
98
+ |
99
+ signal = preceedErrnoRead ( errno )
79
100
)
80
- select errno , "`errno` has indeterminate value after this $@." , h , h .toString ( )
101
+ select errno , "`errno` has indeterminate value after this $@." , signal , signal .toString ( )
0 commit comments