- Jul 01, 2016
-
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
Kostyantyn Vorobyov authored
-
- Jun 27, 2016
-
-
Kostyantyn Vorobyov authored
-
- Jun 17, 2016
-
-
Julien Signoles authored
-
Kostyantyn Vorobyov authored
Fix issues with the new type system These issues were found by the Cfp plug-in. Consequently this MR and the upcoming one in CFP are required to fix OCI. This patch generates even less casts than before. See merge request !62
-
Boris Yakobowski authored
-
Julien Signoles authored
Add CfP and Security to continuous integration See merge request !60
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
fix function Translate.term_to_exp used by plug-in Cfp. This fix requires to call the type system with no context in some cases
-
- Jun 15, 2016
-
-
Boris Yakobowski authored
-
- Jun 13, 2016
-
-
Julien Signoles authored
-
- Jun 09, 2016
-
-
Kostyantyn Vorobyov authored
New type system This MR implements the new type system which is used to choose the best type for the generated integer expressions (in particular, either mpz or a standard C integral type). The core of the implementation follows Figures 3 & 4 of the following paper : http://julien.signoles.free.fr/publis/2015_jfla.pdf. Sorry it is in French, but the Figures are in an international mathematical language
. The main modification is the integration of a context in order to replace the 2 coercion rules (in order to transform a formal system in which more than 1 rule may be applied into an algorithm). It is probably not a good idea to read this MR commit by commit since interval.ml* are new files and typing.ml* were fully rewritten. It is probably much better to read these files from scratch and look at the differences between the last master commit and the last commit in this branch for the rest. See merge request !50 -
Kostyantyn Vorobyov authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
[typing] fix bug in on-the-fly typing when translating quantification [typing] update a few oracles
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-
Julien Signoles authored
-