1. 02 Feb, 2018 1 commit
  2. 22 Jan, 2018 1 commit
  3. 17 Jan, 2018 2 commits
    • Jean-Christophe Filliâtre's avatar
      fixed 'make bench' · 544987d5
      Jean-Christophe Filliâtre authored
      new directory bench/typing/x-bad containing bugs not yet fixed
      544987d5
    • Stefan Berghofer's avatar
      Improved checking of realizations for Isabelle · 96f69b5e
      Stefan Berghofer authored
      Rather than using pre-generated files, the *.xml files describing the
      Why3 theories to be realized are generated again before compiling the
      corresponding Isabelle theories. Instead of the generated *.xml files,
      we use a file containing their hash values to detect changes in the
      realizations. Since there may be different realizations for different
      versions of Isabelle, we provide a file with hash values for every
      supported version of Isabelle. The files containing the hash values
      can be updated via the update-isabelle target.
      
      (cherry picked from commit 039e0f0a321c36ea3bea231e4376f5833cd2ad8a)
      96f69b5e
  4. 13 Jan, 2018 1 commit
  5. 26 Dec, 2017 2 commits
  6. 22 Dec, 2017 1 commit
  7. 15 Dec, 2017 1 commit
  8. 22 Nov, 2017 2 commits
  9. 07 Nov, 2017 1 commit
  10. 06 Nov, 2017 1 commit
  11. 31 Oct, 2017 1 commit
  12. 02 Sep, 2017 1 commit
  13. 25 Aug, 2017 1 commit
  14. 24 Aug, 2017 1 commit
  15. 17 Aug, 2017 1 commit
  16. 19 Jul, 2017 1 commit
  17. 14 Jul, 2017 1 commit
  18. 30 Jun, 2017 1 commit
    • MARCHE Claude's avatar
      few improvements in CE bench · a229dcf0
      MARCHE Claude authored
      * time limit set to 1 sec. Quicker, and results are the same !
      
      * use Stdlib whenever possible
      
      * FIXME: the use of StringMap.bindings should not be useful, and wastes time and memory
      a229dcf0
  19. 28 Jun, 2017 3 commits
  20. 25 Jun, 2017 1 commit
  21. 23 Jun, 2017 1 commit
  22. 21 Jun, 2017 2 commits
  23. 13 Jun, 2017 1 commit
    • Andrei Paskevich's avatar
      Expr: execute abstract blocks and whiteboxes with unfiltered effect · f9ff4e02
      Andrei Paskevich authored
      This commit also contains a fix for a curious exploit of our type
      system which was made possible by a combination of local exceptions
      and a special treatment of abstract blocks and whiteboxes.
      
      Local exceptions allow us to exploit the type inference mechanism
      and to force the same regions onto unrelated expressions. This is due
      to the fact that local exceptions are region-monomorphic (this may be
      relaxed in future). Of course, this was always possible via the API,
      and the false aliases do not threaten the soundness of the system,
      thanks to the following critical invariant:
      
        An allocation of a new mutable value always has an associated reset
        effect which invalidates the existing variables of the same type.
      
      So, if two variables share a region, then exactly one of three
      conditions must hold:
      
      1. They are actually aliased, and modification of one must change
         the other in the VC.
      
      2. They are not aliased, but the newer one invalidates the other:
         this is a case of false alias made benign by the reset effect.
      
      3. The shared region is not actually reachable from the newer one:
              let x = if true then None else Some r
         this is another false alias, without an associated reset effect,
         yet still benign since the shared region is not reachable from x.
      
      However, the type system and the VC generator must have the exact
      same view on who's who's alias. If the VCgen encounters in the
      same control flow two variables with a shared region in the type,
      then the type system must have ensured one of the three conditions
      above. Prior to this commit, there were two cases which violated
      this:
      
      - An exception raised in an abstract block that does not have
        an exceptional postcondition for it, escapes into the main
        control flow.
      
      - A whitebox, by its nature, is fully handled inside the main
        control flow.
      
      The violation came from the fact that abstract blocks and whiteboxes
      are stored as cexps and so their effect is filtered by Ity.create_cty
      in order to hide effects on variables allocated and collected inside
      the block. This is a useful and necessary feature, except when the
      VC of the block escapes into the main control flow and the forced
      false aliases -- unchecked by the type system -- are seen by VCgen.
      The implemented fix resolves the issue by restoring the hidden
      effects for abstract blocks and whiteboxes.
      
      Check bench/programs/bad-typing/false_alias*.mlw for two concrete
      examples.
      f9ff4e02
  24. 11 Jun, 2017 1 commit
  25. 09 Jun, 2017 3 commits
  26. 08 Jun, 2017 1 commit
  27. 04 Jun, 2017 1 commit
    • Andrei Paskevich's avatar
      bench: typecheck the gallery before extraction/execution · 85074baf
      Andrei Paskevich authored
      I know that extraction and execution are much more fun than
      the boring "can we even parse WhyML at all?" question, but
      you see, if our parsing/typechecking is broken, then the fun
      stuff is broken, too. And I really prefer to get the error
      messages about the typechecking being broken from the typechecking
      part of the bench, and not from the test-api or extraction part.
      Merci pour votre compréhension.
      85074baf
  28. 01 Jun, 2017 1 commit
  29. 23 May, 2017 2 commits
  30. 22 May, 2017 1 commit
  31. 16 May, 2017 1 commit