1. 11 Jan, 2018 1 commit
  2. 24 May, 2017 1 commit
    • MARCHE Claude's avatar
      allow relative pathnames for drivers stored in the Why3 config file · eb751c1b
      MARCHE Claude authored
      If drivers in why3.conf are simple names like "alt_ergo", then the driver file
      is search as <datadir>/drivers/alt_ergo.drv
      
      This behavior is now the same as when a driver is given with option -D on the
      command line for why3prove, why3replay or why3extract
      
      Reminder: the datadir is either given as
      1) the environment variable WHY3DATA
      2) the field "datadir" of the [main] section of the
         why3 config file if exists
      3) or by default the compile-time datadir
      eb751c1b
  3. 12 Apr, 2017 1 commit
  4. 26 Jul, 2016 1 commit
  5. 19 Jul, 2016 1 commit
    • Johannes Kanig's avatar
      Allow to keep unmatched theories · 4c744eba
      Johannes Kanig authored
      When Why3 is run on a file where some theories have been suppressed, it
      will delete the corresponding theories from the session file.  We now
      add an option keep_unmatched_theories to Session.update_session, which
      keeps all theories. In this commit, this option is always disabled.
      
      This is useful for SPARK, which sometimes only generates part of the
      Why3 file for efficiency reasons, but doesn't want the session file to
      be damaged because of that.
      
      * session.ml
      (import_theory)
      (import_goal)
      (import_proof_attempt)
      (import_transf): new functions to copy a session tree from an old
        session file
      (merge_file): keep old theories when keep_unmatched_theories is true
      * session_scheduler.ml
      (update_session): pass keep_unmatched_theories
      * why3session_lib.ml
      (read_update_session): pass keep_unmatched_theories
      4c744eba
  6. 14 Apr, 2016 1 commit
  7. 15 Mar, 2016 2 commits
  8. 08 Mar, 2016 1 commit
  9. 10 Dec, 2015 1 commit
  10. 20 Mar, 2015 1 commit
  11. 19 Mar, 2015 1 commit
  12. 15 Sep, 2014 1 commit
  13. 31 Aug, 2014 1 commit
  14. 29 Aug, 2014 1 commit
  15. 25 Aug, 2014 1 commit
  16. 28 Jun, 2014 1 commit
  17. 14 Mar, 2014 1 commit
  18. 07 Feb, 2014 1 commit
  19. 06 Mar, 2013 1 commit
  20. 30 Jan, 2013 1 commit
    • Andrei Paskevich's avatar
      reorganize examples/ · 4b1bc2b0
      Andrei Paskevich authored
      - all programs with sessions are in examples/
      - all programs without sessions are in examples/in_progress/
        (if you have private sessions for those, just move them there)
      - all pure logical problems are in logic/
        (to simplify bench scripts and gallery building; they are few anyway)
      - all OCaml programs are in examples/use_api/
      - all strange stuff is in examples/misc/
        (most of it should probably go)
      - Claude's solutions for Foveoos 2011 are in examples/foveoos11-cm/
        (why do we need two sets of solutions for quite simple problems?)
      - hoare_logic, bitvectors, vacid_0_binary_heaps are in examples/
      
      Bench scripts and documentation are updated.
      Also, bench/bench is simplified a little bit.
      4b1bc2b0
  21. 09 Nov, 2012 1 commit