Commits · 8fb416d303b987a89cd0e45a4e932145d92f753f · Why3 / why3 · GitLab

16 Sep, 2014 1 commit
- updated sessions using the new combined checksum for theories · 8fb416d3
  MARCHE Claude authored Sep 16, 2014
  
  8fb416d3
15 Sep, 2014 1 commit
- [session] theory checksum is now the combination of checksums of its subtasks. · d9855c53
  MARCHE Claude authored Sep 15, 2014
  
  d9855c53
12 Sep, 2014 1 commit
- [compute] a simple additional test · cde46567
  MARCHE Claude authored Sep 12, 2014
  
  cde46567
11 Sep, 2014 8 commits
- mini-compiler:bisect · 253b4a7b
  Léon Gondelman authored Sep 11, 2014
  
  253b4a7b
- Mlw_ty: add a missing check to eff_full_inst · 13585337
  Andrei Paskevich authored Sep 11, 2014
```
This fixes a soundness bug in WhyML typechecking.
See bench/programs/bad-typing/alias6.mlw for an example
of illegal alias that would go uncatched until now.
```
  13585337
- mini-compiler: proved (4 goals by coq) · 693db5a7
  Léon Gondelman authored Sep 11, 2014
  
  693db5a7
- [run strategy] allow the user to provide callbacks · 057b8d9f
  MARCHE Claude authored Sep 11, 2014
  
  057b8d9f
- Ity: effect instantiation · 853deb85
  Andrei Paskevich authored Sep 11, 2014
  
  853deb85
- Mini-compiler: loop in progress · e017894d
  Martin Clochard authored Sep 11, 2014
  
  e017894d
- Added missing "loop" keyword to why3.lang · b041d198
  Martin Clochard authored Sep 11, 2014
  
  b041d198
- mini-compiler: aexpr & bexpr proved · c87c1e9a
  Léon Gondelman authored Sep 11, 2014
  
  c87c1e9a
10 Sep, 2014 10 commits
- Ity: forbid using a tvsymbol both as a type variable and a region variable · 5fd9aede
  Andrei Paskevich authored Sep 10, 2014
  
  5fd9aede
- mini-compiler:new version of compiler with aexpr proverd · 20e00b94
  Léon Gondelman authored Sep 10, 2014
  
  20e00b94
- mini-compiler:wip · 8921730c
  Léon Gondelman authored Sep 10, 2014
  
  8921730c
- Makefile: fix installation rules · 636415cf
  Andrei Paskevich authored Sep 10, 2014
  
  636415cf
- Ity: store full refresh in effects · 15a4e420
  Andrei Paskevich authored Sep 10, 2014
  
  15a4e420
- [bench, extraction] allow to pass any number of arguments · 490a3fca
  MARCHE Claude authored Sep 10, 2014
  
  490a3fca
- [compute] simplify quantified formulas if possible · 0d5fa281
  MARCHE Claude authored Sep 10, 2014
  
  0d5fa281
- [ide] display warnings also on stderr, synchronously · 678c869b
  MARCHE Claude authored Sep 10, 2014
  
  678c869b
- fixed eliminate_if with inductive definitions · b41b7a20
  Jean-Christophe Filliatre authored Sep 10, 2014
  
  b41b7a20
- removed one OCaml warning · 390383ee
  Jean-Christophe Filliatre authored Sep 10, 2014
  
  390383ee
09 Sep, 2014 8 commits
- Ity: refresh effects · c34adb3b
  Andrei Paskevich authored Sep 10, 2014
  
  c34adb3b
- [compute] maximal number of steps can be given with meta compute_max_steps · 6a3b6896
  MARCHE Claude authored Sep 09, 2014
  
  6a3b6896
- [compute] (in progress) make the maximal number of steps as a parameter · fb63f8ba
  MARCHE Claude authored Sep 09, 2014
  
  fb63f8ba
- Ity: tentative merge of refresh effects · bde193f5
  Andrei Paskevich authored Sep 09, 2014
  
  bde193f5
- allow rewrite rules with a builtin symbol or a defined symbol, or a constructor · fad54f38
  MARCHE Claude authored Sep 09, 2014
```
as root of the left-hand side
```
  fad54f38
- details · 1eb08942
  MARCHE Claude authored Sep 09, 2014
  
  1eb08942
- Beta-reduction: reduce higher-order predicate application · 1478a689
  Martin Clochard authored Sep 09, 2014
  
  1478a689
- Transformation compute: reduce partial function application · eda26846
  Martin Clochard authored Sep 09, 2014
  
  eda26846
08 Sep, 2014 8 commits
- [compute] support for lambda-expressions · 5e54ace2
  MARCHE Claude authored Sep 08, 2014
  
  5e54ace2
- Ity: effects and assignment · 642cb2b3
  Andrei Paskevich authored Sep 08, 2014
  
  642cb2b3
- mini-copmiler: wip bexpr · ba24fca9
  Léon Gondelman authored Sep 08, 2014
  
  ba24fca9
- Proof of aexpr_natural · e3c4a040
  Martin Clochard authored Sep 08, 2014
  
  e3c4a040
- mini-compiler: a natural soundness lemma for compile_aexpr (to be proved) · 3cb17d16
  Jean-Christophe Filliatre authored Sep 08, 2014
  
  3cb17d16
- mini-compiler : fully automatic proof of compilation for arithmetic expressions · 92211e8b
  Léon Gondelman authored Sep 08, 2014
  
  92211e8b
- Ity: more checks in create_itysymbol · 1469c893
  Andrei Paskevich authored Sep 08, 2014
  
  1469c893
- Mini-compiler example: some changes · 7ec4d574
  Martin Clochard authored Sep 08, 2014
  
  7ec4d574
07 Sep, 2014 3 commits
- Ity: keep more information about itysymbol's · 31539eb2
  Andrei Paskevich authored Sep 07, 2014
  
  31539eb2
- why3 session html: more detailed output · 128257f4
  MARCHE Claude authored Sep 07, 2014
  
  128257f4
- session: refined the "verified" boolean status into a float option · 5517c9ed
  MARCHE Claude authored Sep 07, 2014
  
  5517c9ed