-
Notifications
You must be signed in to change notification settings - Fork 42
Open
Description
frontend/tests/cases/positive/security/level_pos3.gr
Checking frontend/tests/cases/positive/security/level_pos3.gr...
Type checking failed: frontend/tests/cases/positive/security/level_pos3.gr:
Counter example: frontend/tests/cases/positive/security/level_pos3.gr:9:1:
The following constraint associated with `incr` is false:
(((1 : Level) ∨ (prom_[9:34]0 * ((1 : Level) ∨ (1 : Level)))) ∨ ((Private ∨ (l * (1 : Level))) ∨ (1 : Level)) ≤ Dunno) ∧ (((1 : Level) ∨ (prom_[9:34]0 * ((1 : Level) ∨ (1 : Level)))) ∨ ((Private ∨ (l * (1 : Level))) ∨ (1 : Level)) ≤ (1 : Level)) ∧ (prom_[9:34]0 * (1 : Level) ≤ l) ∧ ((prom_[9:34]0 * (1 : Level)) + (l * (1 : Level)) ≤ l) ∧ (l ≤ prom_[9:34]0) ∧ (prom_[9:34]0 ≤ l)
Counter-example:
l = Public :: Level
Metadata
Metadata
Assignees
Labels
No labels