Commit 9ac6d394 authored by Andrei Paskevich's avatar Andrei Paskevich

trywhy3: update syntax and add "5000 steps" option

parent 2ca226c7
...@@ -204,7 +204,6 @@ on linking described in file LICENSE. ...@@ -204,7 +204,6 @@ on linking described in file LICENSE.
<keyword>to</keyword> <keyword>to</keyword>
<keyword>try</keyword> <keyword>try</keyword>
<keyword>while</keyword> <keyword>while</keyword>
<keyword>loop</keyword>
<keyword>-&gt;</keyword> <keyword>-&gt;</keyword>
</context> </context>
<context id="spec" style-ref="spec-keyword"> <context id="spec" style-ref="spec-keyword">
......
...@@ -7,11 +7,13 @@ var TextHighlightRules = require("./text_highlight_rules").TextHighlightRules; ...@@ -7,11 +7,13 @@ var TextHighlightRules = require("./text_highlight_rules").TextHighlightRules;
var Why3HighlightRules = function() { var Why3HighlightRules = function() {
var keywords = ( var keywords = (
"and|as|assert|begin|do|done|downto|else|end|ensures|" + "abstract|axiom|by|clone|coinductive|constant|end|exception|" +
"exception|exists|for|forall|fun|function|goal|if|import|in|" + "export|function|goal|ghost|import|inductive|lemma|meta|mutable|" +
"invariant|let|match|module|mutable|predicate|" + "module|namespace|predicate|private|so|theory|type|use|val|with|" +
"rec|requires|then|theory|to|try|type|use|val|variant|" + "begin|do|done|downto|else|exists|for|forall|if|in|let|loop|match|" +
"while|with|diverges" "raise|rec|then|to|try|while|absurd|assert|assume|diverges|ensures|" +
"check|invariant|raises|reads|requires|result|returns|self|variant|" +
"writes"
); );
var builtinConstants = ("true|false"); var builtinConstants = ("true|false");
......
...@@ -61,10 +61,10 @@ ...@@ -61,10 +61,10 @@
<div class="why3-separator" style="width:2em;"></div> <div class="why3-separator" style="width:2em;"></div>
<div class="why3-button-group"> <div class="why3-button-group">
<button id="why3-button-compile" class="why3-button" title="Compile buffer"> <button id="why3-button-compile" class="why3-button" title="Verify">
<span class="fa-cogs"></span> <span class="fa-cogs"></span>
</button> </button>
<button id="why3-button-execute" class="why3-button" title="Execute buffer"> <button id="why3-button-execute" class="why3-button" title="Execute">
<span class="fa-arrow-circle-right"></span> <span class="fa-arrow-circle-right"></span>
</button> </button>
<button id="why3-button-stop" class="why3-button" title="Interrupt"> <button id="why3-button-stop" class="why3-button" title="Interrupt">
...@@ -127,6 +127,9 @@ ...@@ -127,6 +127,9 @@
<li id="why3-prove1000-menu-entry"><span class="fa-check-square <li id="why3-prove1000-menu-entry"><span class="fa-check-square
why3-icon"></span> why3-icon"></span>
Prove (1000 steps) </li> Prove (1000 steps) </li>
<li id="why3-prove5000-menu-entry"><span class="fa-check-square
why3-icon"></span>
Prove (5000 steps) </li>
<li id="why3-clean-menu-entry"><span class="fa-unlink why3-icon"></span> <li id="why3-clean-menu-entry"><span class="fa-unlink why3-icon"></span>
Clean </li> Clean </li>
</ul> </ul>
...@@ -163,7 +166,7 @@ ...@@ -163,7 +166,7 @@
<p>TryWhy3 is a Javascript based version of <p>TryWhy3 is a Javascript based version of
the <a href="http://why3.lri.fr/" target="_blank">Why3 the <a href="http://why3.lri.fr/" target="_blank">Why3
Verification Platform</a></p> Verification Platform</a></p>
<p>© 2010-2016, Inria - CNRS - Paris-Sud University<br/> <p>© 2010-2017, Inria - CNRS - Paris-Sud University<br/>
This software is distributed under the terms of the GNU Lesser This software is distributed under the terms of the GNU Lesser
General Public License version 2.1, with the special exception General Public License version 2.1, with the special exception
on linking described in the on linking described in the
......
...@@ -305,6 +305,7 @@ module ContextMenu = ...@@ -305,6 +305,7 @@ module ContextMenu =
let prove_menu_entry = getElement AsHtml.li "why3-prove-menu-entry" let prove_menu_entry = getElement AsHtml.li "why3-prove-menu-entry"
let prove100_menu_entry = getElement AsHtml.li "why3-prove100-menu-entry" let prove100_menu_entry = getElement AsHtml.li "why3-prove100-menu-entry"
let prove1000_menu_entry = getElement AsHtml.li "why3-prove1000-menu-entry" let prove1000_menu_entry = getElement AsHtml.li "why3-prove1000-menu-entry"
let prove5000_menu_entry = getElement AsHtml.li "why3-prove5000-menu-entry"
let clean_menu_entry = getElement AsHtml.li "why3-clean-menu-entry" let clean_menu_entry = getElement AsHtml.li "why3-clean-menu-entry"
let enabled = ref true let enabled = ref true
...@@ -1043,6 +1044,8 @@ let () = ...@@ -1043,6 +1044,8 @@ let () =
Controller.(why3_transform (`Prove(100)) ignore)); Controller.(why3_transform (`Prove(100)) ignore));
ContextMenu.(add_action prove1000_menu_entry ContextMenu.(add_action prove1000_menu_entry
Controller.(why3_transform (`Prove(1000)) ignore)); Controller.(why3_transform (`Prove(1000)) ignore));
ContextMenu.(add_action prove5000_menu_entry
Controller.(why3_transform (`Prove(5000)) ignore));
ContextMenu.(add_action clean_menu_entry ContextMenu.(add_action clean_menu_entry
Controller.(why3_transform (`Clean) TaskList.clean_task)); Controller.(why3_transform (`Clean) TaskList.clean_task));
Dialogs.(set_onchange input_num_threads Dialogs.(set_onchange input_num_threads
......
...@@ -47,7 +47,7 @@ let env : Env.env = Env.create_env (Whyconf.loadpath main) ...@@ -47,7 +47,7 @@ let env : Env.env = Env.create_env (Whyconf.loadpath main)
let alt_ergo_driver : Driver.driver = let alt_ergo_driver : Driver.driver =
try try
Printexc.record_backtrace true; Printexc.record_backtrace true;
Driver.load_driver env alt_ergo.Whyconf.driver [] Whyconf.load_driver main env alt_ergo.Whyconf.driver []
with e -> with e ->
let s = Printexc.get_backtrace () in let s = Printexc.get_backtrace () in
eprintf "Failed to load driver for alt-ergo: %a@.%s@." eprintf "Failed to load driver for alt-ergo: %a@.%s@."
...@@ -161,10 +161,6 @@ module Task = ...@@ -161,10 +161,6 @@ module Task =
let register_task parent_id task = let register_task parent_id task =
let id = gen_id () in let id = gen_id () in
let vid, expl, _ = Termcode.goal_expl_task ~root:false task in let vid, expl, _ = Termcode.goal_expl_task ~root:false task in
let expl = match expl with
| Some s -> s
| None -> vid.Ident.id_string
in
let id_loc = match vid.Ident.id_loc with let id_loc = match vid.Ident.id_loc with
None -> [] None -> []
| Some l -> begin match mk_loc (Loc.get l) with | Some l -> begin match mk_loc (Loc.get l) with
......
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