File tree 1 file changed +6
-5
lines changed 1 file changed +6
-5
lines changed Original file line number Diff line number Diff line change @@ -132,9 +132,10 @@ the array **dest** with the given value.
132
132
__CPROVER_bool __CPROVER_enum_is_in_range();
133
133
```
134
134
135
- The function ** \_\_ CPROVER\_ enum\_ is\_ in\_ range** returns true
136
- if their one argument (an ` enum ` ) is one of the defined values for
137
- the enumeration. For example
135
+ The function ** \_\_ CPROVER\_ enum\_ is\_ in\_ range** is used to check
136
+ that an enumeration has one of the defined enumeration values. In
137
+ the following example ` __CPROVER_enum_is_in_range(ev1) ` will return
138
+ true and the assertion will pass
138
139
``` C
139
140
enum my_enum { first, second };
140
141
@@ -144,7 +145,7 @@ int main()
144
145
assert (__CPROVER_enum_is_in_range (ev1));
145
146
}
146
147
```
147
- would return true, while the following example
148
+ However, in the example below the assertion will fail
148
149
```C
149
150
enum my_enum { first, second };
150
151
@@ -154,7 +155,7 @@ int main()
154
155
assert(__CPROVER_enum_is_in_range(ev1));
155
156
}
156
157
```
157
- would return false.
158
+
158
159
159
160
#### Uninterpreted Functions
160
161
You can’t perform that action at this time.
0 commit comments