@@ -37,18 +37,22 @@ class SignalCheckOperation extends EqualityOperation, GuardCondition {
3737 )
3838 }
3939
40+ ControlFlowNode getCheckedSuccessor ( ) {
41+ result != errorSuccessor and result = this .getASuccessor ( )
42+ }
43+
4044 ControlFlowNode getErrorSuccessor ( ) { result = errorSuccessor }
4145}
4246
4347/**
4448 * Models signal handlers that call signal() and return
4549 */
4650class SignalCallingHandler extends Function {
47- SignalCall sh ;
51+ SignalCall registration ;
4852
4953 SignalCallingHandler ( ) {
5054 // is a signal handler
51- this = sh .getArgument ( 1 ) .( FunctionAccess ) .getTarget ( ) and
55+ this = registration .getArgument ( 1 ) .( FunctionAccess ) .getTarget ( ) and
5256 // calls signal() on the handled signal
5357 exists ( SignalCall sCall |
5458 sCall .getEnclosingFunction ( ) = this and
@@ -63,18 +67,35 @@ class SignalCallingHandler extends Function {
6367 )
6468 }
6569
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+ )
6787}
6888
69- from ErrnoRead errno , SignalCall h
89+ from ErrnoRead errno , SignalCall signal
7090where
7191 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
7595 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 )
79100 )
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