|
| 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