Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

  1. 16 Apr, 2015 1 commit
  2. 15 Apr, 2015 8 commits
  3. 14 Apr, 2015 1 commit
  4. 13 Apr, 2015 6 commits
  5. 12 Apr, 2015 2 commits
  6. 11 Apr, 2015 2 commits
    • Andrei Paskevich's avatar
      examples/vstte10_queens: strong updates · 340ffc11
      Andrei Paskevich authored
      1. Strong region updates can only work with direct assignments, e.g.
           r.contents <- something_completely_different
         but not with functions such as (:=) : ref 'a -> 'a -> unit
         Why3 requires 'a to be instantiated with one concrete type,
         not with a bunch of types that differ in their regions.
      2. Strong region updates will restrict the updated regions to their
         covers. However, in the current implementation, Why3 does not know
         if the region corresponding to the field "contents" is the only
         cover for 'a in the type [ref 'a] or if there is a way to retrieve
         'a from [ref 'a] without going through "contents". Therefore, to
         ensure soundness, a strong update of r.contents will forbid to
         use r itself. A solution consists in writing an adhoc "reference"
         type, where the mutable contents (O.t in this case) is explicitly
         given in the type definition. Then the strong update of the field
         containing O.t will preserve the covering "reference".
         This problem is fixed in the "new system", where mutable types
         carry information about the access paths of the type variables.
         There, "r.contents <- something_different" preserves r.
    • Jean-Christophe Filliâtre's avatar
  7. 10 Apr, 2015 2 commits
  8. 09 Apr, 2015 1 commit
  9. 08 Apr, 2015 6 commits
  10. 07 Apr, 2015 2 commits
  11. 05 Apr, 2015 2 commits
  12. 03 Apr, 2015 2 commits
  13. 02 Apr, 2015 5 commits