• Andrei Paskevich's avatar
    Mlw_expr: fix potentially unsound pattern matching in programs · eda92a0b
    Andrei Paskevich authored
    split the ppat_ghost field in program patterns into two distinct
    conditions:
    - ppat_ghost, indicating that the pattern starts as ghost,
      meaning that all variables in it are ghost, too;
    - ppat_fail, meaning that the pattern contains a refutable
      ghost subpattern, which makes the match in the extracted code
      impossible, which makes the whole match expression ghost.
    
    Until now, the two conditions were disjunctively combined, making
    admissible the invalid pattern matching in bench/p/b-d/ghost4.mlw.
    eda92a0b
Name
Last commit
Last update
..
coq-tactic Loading commit data...
core Loading commit data...
driver Loading commit data...
ide Loading commit data...
jessie Loading commit data...
mlw Loading commit data...
parser Loading commit data...
printer Loading commit data...
session Loading commit data...
tools Loading commit data...
transform Loading commit data...
trywhy3 Loading commit data...
util Loading commit data...
why3doc Loading commit data...
why3session Loading commit data...
whyml Loading commit data...
config.sh.in Loading commit data...