FilesExpand file tree

 sauyon/java-spring-errors

/

Options.qll

Copy path

Blame

More file actions

Blame

More file actions

Latest commit

 

History

History

History

154 lines (137 loc) · 4.71 KB

 sauyon/java-spring-errors

/

Options.qll

Copy path

Top

File metadata and controls

• Code
• Blame

154 lines (137 loc) · 4.71 KB

Raw

Copy raw file

Download raw file

Open symbols panel

Edit and raw actions

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

38

39

40

41

42

43

44

45

46

47

48

49

50

51

52

53

54

55

56

57

58

59

60

61

62

63

64

65

66

67

68

69

70

71

72

73

74

75

76

77

78

79

80

81

82

83

84

85

86

87

88

89

90

91

92

93

94

95

96

97

98

99

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

/**

* Provides custom predicates that specify information about

* the behavior of the program being analyzed.

*

* By default they fall back to the reasonable defaults provided in

* `DefaultOptions.qll`, but by modifying this file, you can customize

* the standard analyses to give better results for your project.

*/

import cpp

/**

* Customizable predicates that specify information about

* the behavior of the program being analyzed.

*/

class CustomOptions extends Options {

/**

* Holds if we wish to override the "may return NULL" inference for this

* call. If this holds, then rather than trying to infer whether this

* call might return NULL, we will instead test whether `returnsNull`

* holds for it.

*

* By default, this handles the `Xstrdup` function used by the CVS

* project.

*/

override predicate overrideReturnsNull(Call call) { Options.super.overrideReturnsNull(call) }

/**

* Holds if this call may return NULL. This is only used if

* `overrideReturnsNull` holds for the call.

*

* By default, this handles the `Xstrdup` function used by the CVS

* project.

*/

override predicate returnsNull(Call call) { Options.super.returnsNull(call) }

/**

* Holds if a call to this function will never return.

*

* By default, this holds for `exit`, `_exit`, `abort`, `__assert_fail`,

* `longjmp`, `error`, `__builtin_unreachable` and any function with a

* `noreturn` attribute.

*/

override predicate exits(Function f) { Options.super.exits(f) }

/**

* Holds if evaluating expression `e` will never return, or can be assumed

* to never return. For example:

* ```

* __assume(0);

* ```

* (note that in this case if the hint is wrong and the expression is reached at

* runtime, the program's behaviour is undefined)

*/

override predicate exprExits(Expr e) { Options.super.exprExits(e) }

/**

* Holds if function `f` should always have its return value checked.

*

* By default holds only for `fgets`.

*/

override predicate alwaysCheckReturnValue(Function f) { Options.super.alwaysCheckReturnValue(f) }

/**

* Holds if it is reasonable to ignore the return value of function

* call `fc`.

*

* By default holds for calls to `select` where the first argument is

* `0` (commonly used as a way of sleeping), and any call inside a

* macro expansion.

*/

override predicate okToIgnoreReturnValue(FunctionCall fc) {

Options.super.okToIgnoreReturnValue(fc)

}

}

/**

* A type that acts as a mutex.

*/

class CustomMutexType extends MutexType {

CustomMutexType() { none() }

/**

* Holds if `fc` is a call that always locks mutex `arg`

* of this type.

*/

override predicate mustlockAccess(FunctionCall fc, Expr arg) { none() }

/**

* Holds if `fc` is a call that tries to lock mutex `arg`

* of this type, but may return without success.

*/

override predicate trylockAccess(FunctionCall fc, Expr arg) { none() }

/**

* Holds if `fc` is a call that unlocks mutex `arg`

* of this type.

*/

override predicate unlockAccess(FunctionCall fc, Expr arg) { none() }

}

/**

* DEPRECATED: customize `CustomOptions.overrideReturnsNull` instead.

*

* This predicate is required to support backwards compatibility for

* older `Options.qll` files. It should not be removed or modified by

* end users.

*/

predicate overrideReturnsNull(Call call) { none() }

/**

* DEPRECATED: customize `CustomOptions.returnsNull` instead.

*

* This predicate is required to support backwards compatibility for

* older `Options.qll` files. It should not be removed or modified by

* end users.

*/

predicate returnsNull(Call call) { none() }

/**

* DEPRECATED: customize `CustomOptions.exits` instead.

*

* This predicate is required to support backwards compatibility for

* older `Options.qll` files. It should not be removed or modified by

* end users.

*/

predicate exits(Function f) { none() }

/**

* DEPRECATED: customize `CustomOptions.exprExits` instead.

*

* This predicate is required to support backwards compatibility for

* older `Options.qll` files. It should not be removed or modified by

* end users.

*/

predicate exprExits(Expr e) { none() }

/**

* DEPRECATED: customize `CustomOptions.alwaysCheckReturnValue` instead.

*

* This predicate is required to support backwards compatibility for

* older `Options.qll` files. It should not be removed or modified by

* end users.

*/

predicate alwaysCheckReturnValue(Function f) { none() }

/**

* DEPRECATED: customize `CustomOptions.okToIgnoreReturnValue` instead.

*

* This predicate is required to support backwards compatibility for

* older `Options.qll` files. It should not be removed or modified by

* end users.

*/

predicate okToIgnoreReturnValue(FunctionCall fc) { none() }