Commit 861f1302 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp+kernel] Prepare ChangeLog

parent 03865276
......@@ -21,6 +21,7 @@ Open Source Release <next-release>
transition, and use such variables in subsequent guards.
- Kernel [2020-10-09] Add option -print-config-json, to output Frama-C
configuration data in JSON format.
- Logic [2020-10-XX] '\from' now accepts '&v' expressions
- Metrics [2020-10-01] Distinguish between undefined but specified functions
and functions with neither definition nor specification.
-* Eva [2020-09-28] Improved string builtins on wide strings: crash fixed,
......@@ -26,6 +26,12 @@ Plugin WP <next-release>
- WP [2020-10-07] New tactic Bit-Test range
- WP [2020-09-21] Added support for Why3 interactive prover (Coq)
- WP [2020-10-XX] New warning "pedantic-assigns". WP needs precise
'assigns ... \from ...' specification about out
pointers (\result and assigned pointers) to generate
precise proof hypotheses.
- WP [2020-10-XX] Hypotheses: out pointers (\result + written pointers)
- WP [2020-09-21] Added support for Why3 Coq interactive prover
- WP [2020-09-21] New option -wp-interactive <mode>
- WP [2020-09-21] New option -wp-interactive-timeout <seconds>
- WP [2020-09-17] New experimental option: -wp-check-model-hypotheses
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment