Commit 2e437378 authored by Sylvain Dailler's avatar Sylvain Dailler

Change name of print_attrs debug flag. Address part of #187

parent a82670de
......@@ -33,7 +33,7 @@ run () {
f="$2_$1"
printf "WP $2 ($1)... "
echo "Weakest Precondition" > "$f.out"
$dir/../bin/why3prove.opt --debug print_attrs -P "$1,counterexamples" --timelimit 1 -a split_vc "$2.mlw" | \
$dir/../bin/why3prove.opt --debug print_model_attrs -P "$1,counterexamples" --timelimit 1 -a split_vc "$2.mlw" | \
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
sed 's/ ([0-9]\+\.[0-9]\+s)//' | \
......@@ -42,7 +42,7 @@ run () {
sed -r 's/(Timeout|Unknown \(unknown\))/Timeout or Unknown/' >> "$f.out"
printf "SP $2 ($1)... "
echo "Strongest Postcondition" >> "$f.out"
$dir/../bin/why3prove.opt --debug print_attrs --debug vc_sp -P "$1,counterexamples" --timelimit 1 -a split_vc "$2.mlw" | \
$dir/../bin/why3prove.opt --debug print_model_attrs --debug vc_sp -P "$1,counterexamples" --timelimit 1 -a split_vc "$2.mlw" | \
# This ad hoc sed removes any timing information from counterexamples output.
# Counterexamples in JSON format cannot match this regexp.
sed 's/ ([0-9]\+\.[0-9]\+s)//' | \
......
......@@ -16,8 +16,8 @@ let debug = Debug.register_info_flag "call_prover"
~desc:"Print@ debugging@ messages@ about@ prover@ calls@ \
and@ keep@ temporary@ files."
let debug_attrs = Debug.register_info_flag "print_attrs"
~desc:"Print@ attrs@ of@ identifiers@ and@ expressions."
let debug_attrs = Debug.register_info_flag "print_model_attrs"
~desc:"Print@ attrs@ of@ identifiers@ and@ expressions@ in prover@ results."
(* BEGIN{proveranswer} anchor for automatic documentation, do not remove *)
type prover_answer =
......
......@@ -279,8 +279,8 @@ module C = Controller_itp.Make(S)
let debug = Debug.register_flag "itp_server" ~desc:"ITP server"
let debug_attrs = Debug.register_info_flag "print_attrs"
~desc:"Print@ attrs@ of@ identifiers@ and@ expressions."
let debug_attrs = Debug.register_info_flag "print_model_attrs"
~desc:"Print@ attrs@ of@ identifiers@ and@ expressions@ in prover@ results."
(****************)
(* Command list *)
......
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