Commits · d5ad016626d4d520e10c77623b4ab14611ace81e · Why3 / why3

21 Mar, 2019 2 commits
- C driver: precedences for fxp, correct integer suffixes · d5ad0166
  Raphael Rieu-Helft authored Mar 21, 2019
  
  d5ad0166
- C extraction: print appropriate suffixes on integer constants · 15509bd7
  Raphael Rieu-Helft authored Mar 21, 2019
  
  15509bd7
20 Mar, 2019 3 commits
- Normalize the size of sqrt remainder · ef6e98c8
  Raphael Rieu-Helft authored Mar 20, 2019
  
  ef6e98c8
- Tighten precedence requirements inside logical shifts (avoid Wparentheses) · ee116440
  Raphael Rieu-Helft authored Mar 20, 2019
  
  ee116440
- Add square root to extraction · 3bee3018
  Raphael Rieu-Helft authored Mar 20, 2019
  
  3bee3018
19 Mar, 2019 1 commit
- Finish square root proof · 0fde67d6
  Raphael Rieu-Helft authored Mar 19, 2019
  
  0fde67d6
14 Mar, 2019 1 commit
- sqrtrem: wip (and rebase) · b9405b26
  Raphael Rieu-Helft authored Mar 14, 2019
  
  b9405b26
13 Mar, 2019 19 commits
- sqrt normalization wrapper: wip · c424daef
  Raphael Rieu-Helft authored Feb 28, 2019
  
  c424daef
- dc_sqrtrem: complete proof · 2ecd4020
  Raphael Rieu-Helft authored Feb 26, 2019
  
  2ecd4020
- sqrt: wip · d8136223
  Raphael Rieu-Helft authored Feb 25, 2019
  
  d8136223
- Partial proof of sqrt general case · a3fd268a
  Raphael Rieu-Helft authored Feb 22, 2019
  
  a3fd268a
- Simplify sqrt proof · a93167a2
  Raphael Rieu-Helft authored Jan 31, 2019
  
  a93167a2
- Complete square root proof · 9bb0a1d1
  Raphael Rieu-Helft authored Jan 17, 2019
  
  9bb0a1d1
- Use some better-looking assertions. · e7394e20
  Guillaume Melquiond authored Jan 16, 2019
  
  e7394e20
- Change ghost into pure to make it possible to use a coercion. · 115ac8a6
  Guillaume Melquiond authored Jan 16, 2019
  
  115ac8a6
- Prove the main error bound. · 717697a1
  Guillaume Melquiond authored Jan 16, 2019
  
  717697a1
- C extraction: use ML types more consistently · 1a0e9e92
  Raphael Rieu-Helft authored Jan 16, 2019
  
  1a0e9e92
- Add square root tests · 5ca3f3f9
  Raphael Rieu-Helft authored Jan 15, 2019
  
  5ca3f3f9
- Add square root to extracted library · 4e093781
  Raphael Rieu-Helft authored Jan 15, 2019
  
  4e093781
- Add remainder computation and fix a magic constant · f2843199
  Raphael Rieu-Helft authored Jan 15, 2019
  
  f2843199
- Remove useless error term. · 794079fa
  Guillaume Melquiond authored Jan 14, 2019
  
  794079fa
- Verify a few more conditions. · 014f0f73
  Guillaume Melquiond authored Jan 14, 2019
  
  014f0f73
- Add early version of square root algorithm. · bb95fc9f
  Guillaume Melquiond authored Jan 14, 2019
  
  bb95fc9f
- Add support for fixed-point arithmetic to the Gappa driver. · e2c99a74
  Guillaume Melquiond authored Jan 14, 2019
```
As many computations as possible are now performed in Why3, so that the
parameters of the "fixed" rounding operator are literals once sent to
Gappa.
```
  e2c99a74
- Add a minimal theory for fixed-point arithmetic. · e2134bf9
  Guillaume Melquiond authored Jan 14, 2019
  
  e2134bf9
- Add transformation to perform computations in the whole task. · 5cf2e819
  Guillaume Melquiond authored Jan 14, 2019
```
This transformation also substitutes using all the equalities of the form
"f x... = t" with f an unrecognized symbol.
```
  5cf2e819
12 Mar, 2019 1 commit
- Merge branch 'simp_cast_projections' into 'master' · 06c4cb7c
  Raphaël Rieu-Helft authored Mar 12, 2019
```
Simplify projections applied to casted literals in VCs

See merge request !51
```
  06c4cb7c
11 Mar, 2019 3 commits
- Merge branch 'ocaml_printer_precedences' into 'master' · 6fb58a7a
  Raphaël Rieu-Helft authored Mar 11, 2019
```
Move the Ocaml printer to a precedence-based system

Closes #284

See merge request !104
```
  6fb58a7a
- Fix indentation of nested let-ins · 81369020
  Raphael Rieu-Helft authored Mar 11, 2019
  
  81369020
- Indentation fixes · 82c5ab5d
  Raphael Rieu-Helft authored Mar 11, 2019
  
  82c5ab5d
08 Mar, 2019 9 commits
- Fix indentation, remove spurious begin/end around blocks · 16368d2f
  Raphael Rieu-Helft authored Mar 08, 2019
  
  16368d2f
- Remove spurious spaces, fix precedences · 43ac5bd0
  Raphael Rieu-Helft authored Mar 08, 2019
  
  43ac5bd0
- update sessions (except logic/genealogy which depends on Isabelle) · 4508d668
  Andrei Paskevich authored Mar 08, 2019
  
  4508d668
- Remove some begin/end, fix some protect checks · 9e916c2e
  Raphael Rieu-Helft authored Mar 08, 2019
  
  9e916c2e
- Fix a session · 3356006b
  Raphael Rieu-Helft authored Mar 08, 2019
  
  3356006b
- Vc: fix the "circular dependency" error · b7159d49
  Andrei Paskevich authored Mar 04, 2019
  
  b7159d49
- Vc: call simp_cast_projections after eval_match · dc856605
  Andrei Paskevich authored Dec 21, 2018
  
  dc856605
- Update sessions · b5db1999
  Raphael Rieu-Helft authored Oct 26, 2018
  
  b5db1999
- Simplify t'int (c:t) -> c in VCs · 9fedeaf3
  Raphael Rieu-Helft authored Oct 24, 2018
  
  9fedeaf3
07 Mar, 2019 1 commit
- fixed 'make bench' · efecb614
  Jean-Christophe Filliâtre authored Mar 07, 2019
  
  efecb614