Merge requests · Why3 / why3 · GitLab

Mentions légales du service

UnboundSymbol exception and find_* now take expected kind as argument

!108 · created Mar 26, 2019 by DAILLER Sylvain
- Merged
updated Mar 26, 2019
Use syntax literal driver entries for C number constants

!107 · created Mar 25, 2019 by Raphaël Rieu-Helft
- Merged
- 2
updated Mar 25, 2019
GMP square root

!106 · created Mar 25, 2019 by Raphaël Rieu-Helft
- Merged
updated Mar 25, 2019
Imperative TagSet with iterators

!82 · created Jan 31, 2019 by François Bobot
- Merged
- 9
updated Mar 18, 2019
Fix Gtksourceview3 detection with new opam package

!105 · created Mar 12, 2019 by François Bobot
- Merged
- 14
updated Mar 18, 2019
Simplify projections applied to casted literals in VCs

!51 · created Oct 24, 2018 by Raphaël Rieu-Helft
- Merged
- 8
updated Mar 12, 2019
Move the Ocaml printer to a precedence-based system

!104 · created Mar 05, 2019 by Raphaël Rieu-Helft
- Merged
- 17
updated Mar 11, 2019
Precedence of extraction driver symbols (fix #223)

!73 · created Dec 07, 2018 by Raphaël Rieu-Helft 1.3.0
component: extraction component: provers component: syntax
- Merged
- 5
updated Mar 05, 2019
Extraction of C arrays

!88 · created Feb 08, 2019 by Raphaël Rieu-Helft
- Merged
updated Feb 19, 2019
Improve goals generated by the Gappa printer.

!103 · created Feb 19, 2019 by Guillaume Melquiond
component: provers
- Merged
updated Feb 19, 2019
Rework numerical constants.

!101 · created Feb 18, 2019 by Guillaume Melquiond 1.3.0
component: core
- Merged
updated Feb 18, 2019
Put the three_idem example in the examples folder

!99 · created Feb 15, 2019 by Quentin Garchery
- Merged
updated Feb 18, 2019
Factor abnormal transformation exceptions under is_fatal

!98 · created Feb 15, 2019 by DAILLER Sylvain
- Merged
updated Feb 18, 2019
Add the example about three-idempotent rings

!97 · created Feb 15, 2019 by Quentin Garchery
- Merged
updated Feb 15, 2019
fix #274

!96 · created Feb 15, 2019 by DAILLER Sylvain
- Merged
updated Feb 15, 2019
why3prove: Make the output of counterexamples readable by default

!94 · created Feb 13, 2019 by DAILLER Sylvain
- Merged
updated Feb 13, 2019
ce printing: Add breaking hint in array box. Also refactoring

!95 · created Feb 13, 2019 by DAILLER Sylvain
- Merged
updated Feb 13, 2019
Resolve "possible improvements in SMT-LIB driver"

!93 · created Feb 12, 2019 by DAILLER Sylvain
component: provers
- Merged
updated Feb 13, 2019
Resolve "Transformation apply failed: unbound variable"

!92 · created Feb 12, 2019 by DAILLER Sylvain
- Merged
updated Feb 12, 2019
Resolve "Removing Inline_trivial"

!91 · created Feb 12, 2019 by MARCHE Claude
component: provers component: transformations
- Merged
updated Feb 12, 2019

Prev
1
…
47
48
49
50
51
52
53
54
55
Next