1. 05 Apr, 2017 3 commits
    • Johannes Kanig's avatar
      P802-016 fix pop-ups for prover crashes · c77024ba
      Johannes Kanig authored
      We set the error mode in the why3 server. This has two effects:
      - disable pop-ups in case of crashes of why3server;
      - inherit this setting to all spawned prover processes.
      
      * server-win.c
      (main): call SetErrorMode
      
      Change-Id: I93862d51aebe1d4639ab1d463c08366f79375a7a
      c77024ba
    • Johannes Kanig's avatar
      Q301-016 update why3 maps to ocaml 4.04 maps · 410d4b48
      Johannes Kanig authored
      The extmap.ml file was taken (and extended) from ocaml 3.12 and has not
      been updated since. Since then, ocaml map.ml has evolved and contains
      some space optimizations.
      
      The commit contains more changes than strictly needed. The objective is
      to be as close as possible to map.ml from ocaml 4.04. After this patch,
      the 'diff' wrt. map.ml  contains almost exclusively additions, and no
      other changes.
      
      Change-Id: I3e31f6068562e5e1c48f8426efc9ce4e2f5b6010
      410d4b48
    • MARCHE Claude's avatar
      e532edfe
  2. 31 Mar, 2017 1 commit
  3. 30 Mar, 2017 3 commits
  4. 23 Mar, 2017 1 commit
  5. 21 Mar, 2017 3 commits
  6. 20 Mar, 2017 1 commit
  7. 17 Mar, 2017 5 commits
  8. 14 Mar, 2017 1 commit
  9. 09 Mar, 2017 2 commits
  10. 08 Mar, 2017 2 commits
  11. 07 Mar, 2017 12 commits
  12. 06 Mar, 2017 4 commits
  13. 01 Mar, 2017 1 commit
  14. 28 Feb, 2017 1 commit
    • Clément Fumex's avatar
      Add the ability to · f0547868
      Clément Fumex authored
      * declare range types and float types,
      * use integer (resp. real) literals for those types through casting,
      * specify how to print them in drivers.
      
      Change in syntax
      * use
      
        type t = < range 1 2 >   (* integers from 1 to 2 *)
        type t' = < float 4 12 > (* float with 4 bits in exponent and 12 in mantissa *)
      
        the two projections :
        t'int
        t''real
      
        and the predicate :
        t''isFinite
      
      * Restrict the use of "'" in whyml:
        Users are not allowed to introduce names where a quote symbol
        is followed by a letter. Thus, the following identifiers are
        valid:
      
        t'
        toto'0''
        toto'_phi
      
        whereas toto'phi is not.
      
      Note: we do not yet support negative numbers in range declaration
      and casting of a literal.
      f0547868