Commits · d002cd0afc94f5070a2df3fca1de7daa161c1464 · Why3 / why3

25 May, 2020 3 commits
- cosmetic · d002cd0a
  MARCHE Claude authored May 25, 2020
  
  d002cd0a
- document error messages · c20dff94
  MARCHE Claude authored May 25, 2020
  
  c20dff94
- check for absence of invariant on a cycle. · 1b752111
  MARCHE Claude authored May 25, 2020
  
  1b752111
23 May, 2020 3 commits
- polished doc · a1517aca
  MARCHE Claude authored May 23, 2020
  
  a1517aca
- better cfg diagram · 80c78d75
  MARCHE Claude authored May 23, 2020
  
  80c78d75
- group consecutive invariants together · 6af319ea
  MARCHE Claude authored May 23, 2020
  
  6af319ea
21 May, 2020 1 commit
- fix syntax of var decl, allow ghost var · 019647ce
  MARCHE Claude authored May 21, 2020
  
  019647ce
20 May, 2020 2 commits
- improved syntax, doc completed · 31d776b9
  MARCHE Claude authored May 20, 2020
  
  31d776b9
- documentation · 81a0d5d9
  MARCHE Claude authored May 20, 2020
  
  81a0d5d9
19 May, 2020 7 commits
- a minor fix and a real example · 0ac3a7ec
  MARCHE Claude authored May 19, 2020
  
  0ac3a7ec
- no need for a return exception anymore · 6f77d846
  MARCHE Claude authored May 19, 2020
  
  6f77d846
- ignore termination · 54af3ec2
  MARCHE Claude authored May 19, 2020
  
  54af3ec2
- better translation scheme · fca0ab61
  MARCHE Claude authored May 19, 2020
  
  fca0ab61
- avoid infinite loop in CFG translation · c46553b1
  MARCHE Claude authored May 19, 2020
  
  c46553b1
- basic support for invariants · b6b769e2
  MARCHE Claude authored May 19, 2020
  
  b6b769e2
- translation of direct gotos · 4fcd288f
  MARCHE Claude authored May 19, 2020
  
  4fcd288f
14 May, 2020 1 commit
- more general ASTs for instructions · d18e38a3
  MARCHE Claude authored May 14, 2020
  
  d18e38a3
13 May, 2020 1 commit
- printing type errors as comments in the mlw output · 29a9d10f
  MARCHE Claude authored May 13, 2020
  
  29a9d10f
07 May, 2020 3 commits
- capture errors · 4bc3e63b
  MARCHE Claude authored May 07, 2020
  
  4bc3e63b
- first example, typing OK · a217d958
  MARCHE Claude authored May 07, 2020
  
  a217d958
- compilation complete, at last · 113d78e9
  MARCHE Claude authored May 07, 2020
  
  113d78e9
06 May, 2020 1 commit
- reorganize again parsers, works better like this · a3139b50
  MARCHE Claude authored May 06, 2020
  
  a3139b50
05 May, 2020 5 commits
- Merge branch 'split_parser' into cfg_lang · 2e1247a3
  MARCHE Claude authored May 05, 2020
```
# Conflicts:
#	Makefile.in
#	src/parser/parser.mly
```
  2e1247a3
- in progress · 5a3ff59f
  MARCHE Claude authored May 05, 2020
  
  5a3ff59f
- cfg parser in progress · e0218337
  MARCHE Claude authored May 04, 2020
  
  e0218337
- in progress, seems hard · 95f7b9c6
  MARCHE Claude authored May 05, 2020
  
  95f7b9c6
- split main parser in two parts (more to come) · e085acbe
  MARCHE Claude authored May 04, 2020
  
  e085acbe
01 May, 2020 4 commits
- modified example mutual_recursion · 11866d44
  Jean-Christophe Filliâtre authored May 01, 2020
  
  11866d44
- Pmodule: cloned functions may perform deep writes in added fields · b4202fbe
  Andrei Paskevich authored May 01, 2020
  
  b4202fbe
- examples of mutual recursion · 32ade6ee
  Jean-Christophe Filliâtre authored May 01, 2020
  
  32ade6ee
- stdlib: added a function length in mach.c.String · c84ba66b
  Jean-Christophe Filliâtre authored May 01, 2020
  
  c84ba66b
30 Apr, 2020 1 commit
- cfg minor · 6d44d3f3
  MARCHE Claude authored Apr 30, 2020
  
  6d44d3f3
29 Apr, 2020 3 commits
- example: swapping two integers · 3ae7cf75
  Jean-Christophe Filliâtre authored Apr 29, 2020
  
  3ae7cf75
- Do not ship .dockerignore. · 03533764
  Guillaume Melquiond authored Apr 29, 2020
  
  03533764
- Clean wmp.h a bit. · c52555e9
  Guillaume Melquiond authored Apr 29, 2020
  
  c52555e9
23 Apr, 2020 5 commits
- plugin for CFG-based input language · a0ba086c
  MARCHE Claude authored Apr 23, 2020
  
  a0ba086c
- Merge branch 'describe-ce-values' into 'master' · 3c3b7463
  Benedikt Becker authored Apr 23, 2020
```
Distinguish values of counterexamples for invariant preservation

See merge request !367
```
  3c3b7463
- Update oracle · c6da5555
  Benedikt Becker authored Apr 23, 2020
  
  c6da5555
- Update bench/ce · fc677465
  Benedikt Becker authored Apr 16, 2020
  
  fc677465
- Add bench/ce/loop_ce · 17bb76a2
  Benedikt Becker authored Apr 16, 2020
  
  17bb76a2