1. 07 Apr, 2013 40 commits
    • Andrei Paskevich's avatar
      whyml: reimplement verification of the ghost writes · 30c225b4
      Andrei Paskevich authored
      This fixes one bug and several deficiencies in the previous
      implementation, which was based on read effects. One caveat
      about the current version is that we treat all type variables
      in a polymorphic type as visible (= non-ghost) even if they
      only occur in the ghost fields. For example, the following
      code is rejected:
      
        type strange 'a = { ghost contents : 'a }
      
        let test () =
          let x = { contents = ref 0 } in
          x.contents := 42
      
      Even though the field [contents] is ghost and cannot be reached
      from the real-world code, the type of x is [strange (ref int)]
      and the region of the reference is considered to be visible.
      Thus the last assignment is seen as an illicit ghost write.
      
      On the other hand,
      
        type strange 'a = { ghost contents : ref 'a }
      
      and
      
        type strange 'a = { ghost mutable contents : 'a }
      
      permit ghost writes into [contents] without problem.
      Ghost writes into ghost variables are also okay.
      30c225b4
    • Andrei Paskevich's avatar
      4eb22501
  2. 06 Apr, 2013 40 commits
  3. 05 Apr, 2013 40 commits
  4. 03 Apr, 2013 40 commits
  5. 28 Mar, 2013 40 commits
  6. 27 Mar, 2013 40 commits
  7. 26 Mar, 2013 40 commits
  8. 25 Mar, 2013 40 commits
  9. 24 Mar, 2013 40 commits
  10. 23 Mar, 2013 40 commits
  11. 22 Mar, 2013 40 commits