diff options
| author | Enrico Tassi | 2015-02-07 18:40:18 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-02-07 18:54:42 +0100 |
| commit | 861ec0bdbe8be5e327b5082102c646882cd23383 (patch) | |
| tree | e70d59d5936d267397a48df40e76032eb7e4d097 /stm | |
| parent | a71aec672bc66a0e19752fa15d55bc2bd75ef3bc (diff) | |
STM: tolerate simple side effects in async proofs (Close: 4006)
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 05c59720b1..3a57d85bab 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1580,6 +1580,7 @@ let collect_proof keep cur hd brkind id = let view = VCS.visit id in match view.step with | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next + | `Sideff (`Ast (x,_)) -> collect (Some (id,x)) (id::accn) view.next (* An Alias could jump everywhere... we hope we can ignore it*) | `Alias _ -> `Sync (no_name,None,`Alias) | `Fork((_,_,_,_::_::_), _) -> |