Revision f51926b8
Added by Lélio Brun over 3 years ago
| src/spec_common.ml | ||
|---|---|---|
| 58 | 58 |
let a' = red a in |
| 59 | 59 |
let b' = red b in |
| 60 | 60 |
if a' = b' || is_false a' || is_true b' then True |
| 61 |
else if is_true a' && is_false b' then False
|
|
| 61 |
else if is_true a' then b'
|
|
| 62 | 62 |
else Imply (a', b') |
| 63 | 63 |
| Exists (x, p) -> ( |
| 64 | 64 |
let p' = red p in |
Also available in: Unified diff
no need to reschedule in order to "clock-protect" the unitialized state variables in ACSL !