|
| 1 | +const effects_key_string = """ |
| 2 | +## Key for `show` output of Effects: |
| 3 | +
|
| 4 | +The output represents the state of different effect properties in the following order: |
| 5 | +
|
| 6 | +1. `consistent` (`c`): |
| 7 | + - `+c` (green): `ALWAYS_TRUE` |
| 8 | + - `-c` (red): `ALWAYS_FALSE` |
| 9 | + - `?c` (yellow): `CONSISTENT_IF_NOTRETURNED` and/or `CONSISTENT_IF_INACCESSIBLEMEMONLY` |
| 10 | +2. `effect_free` (`e`): |
| 11 | + - `+e` (green): `ALWAYS_TRUE` |
| 12 | + - `-e` (red): `ALWAYS_FALSE` |
| 13 | + - `?e` (yellow): `EFFECT_FREE_IF_INACCESSIBLEMEMONLY` |
| 14 | +3. `nothrow` (`n`): |
| 15 | + - `+n` (green): `true` |
| 16 | + - `-n` (red): `false` |
| 17 | +4. `terminates` (`t`): |
| 18 | + - `+t` (green): `true` |
| 19 | + - `-t` (red): `false` |
| 20 | +5. `notaskstate` (`s`): |
| 21 | + - `+s` (green): `true` |
| 22 | + - `-s` (red): `false` |
| 23 | +6. `inaccessiblememonly` (`m`): |
| 24 | + - `+m` (green): `ALWAYS_TRUE` |
| 25 | + - `-m` (red): `ALWAYS_FALSE` |
| 26 | + - `?m` (yellow): `INACCESSIBLEMEM_OR_ARGMEMONLY` |
| 27 | +7. `noub` (`u`): |
| 28 | + - `+u` (green): `true` |
| 29 | + - `-u` (red): `false` |
| 30 | + - `?u` (yellow): `NOUB_IF_NOINBOUNDS` |
| 31 | +8. `:nonoverlayed` (`o`): |
| 32 | + - `+o` (green): `ALWAYS_TRUE` |
| 33 | + - `-o` (red): `ALWAYS_FALSE` |
| 34 | + - `?o` (yellow): `CONSISTENT_OVERLAY` |
| 35 | +9. `:nortcall` (`r`): |
| 36 | + - `+r` (green): `true` |
| 37 | + - `-r` (red): `false` |
| 38 | +""" |
| 39 | + |
1 | 40 | """ |
2 | 41 | effects::Effects |
3 | 42 |
|
@@ -74,42 +113,8 @@ initialized with `ALWAYS_TRUE`/`true` and then transitioned towards `ALWAYS_FALS |
74 | 113 | Note that within the current flow-insensitive analysis design, effects detected by local |
75 | 114 | analysis on each statement usually taint the global conclusion conservatively. |
76 | 115 |
|
77 | | -## Key for `show` output of Effects: |
78 | 116 |
|
79 | | -The output represents the state of different effect properties in the following order: |
80 | | -
|
81 | | -1. `consistent` (`c`): |
82 | | - - `+c` (green): `ALWAYS_TRUE` |
83 | | - - `-c` (red): `ALWAYS_FALSE` |
84 | | - - `?c` (yellow): `CONSISTENT_IF_NOTRETURNED` and/or `CONSISTENT_IF_INACCESSIBLEMEMONLY` |
85 | | -2. `effect_free` (`e`): |
86 | | - - `+e` (green): `ALWAYS_TRUE` |
87 | | - - `-e` (red): `ALWAYS_FALSE` |
88 | | - - `?e` (yellow): `EFFECT_FREE_IF_INACCESSIBLEMEMONLY` |
89 | | -3. `nothrow` (`n`): |
90 | | - - `+n` (green): `true` |
91 | | - - `-n` (red): `false` |
92 | | -4. `terminates` (`t`): |
93 | | - - `+t` (green): `true` |
94 | | - - `-t` (red): `false` |
95 | | -5. `notaskstate` (`s`): |
96 | | - - `+s` (green): `true` |
97 | | - - `-s` (red): `false` |
98 | | -6. `inaccessiblememonly` (`m`): |
99 | | - - `+m` (green): `ALWAYS_TRUE` |
100 | | - - `-m` (red): `ALWAYS_FALSE` |
101 | | - - `?m` (yellow): `INACCESSIBLEMEM_OR_ARGMEMONLY` |
102 | | -7. `noub` (`u`): |
103 | | - - `+u` (green): `true` |
104 | | - - `-u` (red): `false` |
105 | | - - `?u` (yellow): `NOUB_IF_NOINBOUNDS` |
106 | | -8. `:nonoverlayed` (`o`): |
107 | | - - `+o` (green): `ALWAYS_TRUE` |
108 | | - - `-o` (red): `ALWAYS_FALSE` |
109 | | - - `?o` (yellow): `CONSISTENT_OVERLAY` |
110 | | -9. `:nortcall` (`r`): |
111 | | - - `+r` (green): `true` |
112 | | - - `-r` (red): `false` |
| 117 | +$(effects_key_string) |
113 | 118 | """ |
114 | 119 | struct Effects |
115 | 120 | consistent::UInt8 |
|
0 commit comments