Commit 2bfff3b8 authored by MARCHE Claude's avatar MARCHE Claude

Bitvector, replay and smoke detector

parent 0efd8519
......@@ -18,6 +18,8 @@ TMPERR=$PWD/why3regtests.err
cd `dirname $0`
# too early to do that
# REPLAYOPT="$REPLAYOPT -smoke-detector top"
res=0
export success=0
......
......@@ -326,30 +326,32 @@ let add_to_check_no_smoke config found_obs env_session sched =
| _ -> true)
report
in
if report = [] then begin
if found_obs then
if n=m then
printf " %d/%d (replay OK, all proved: obsolete session \
if report = [] then
begin
if found_obs then
if n=m then
printf " %d/%d (replay OK, all proved: obsolete session \
updated)@." n m
else
if !opt_force then
printf " %d/%d (replay OK, but not all proved: session going to be saved since -force was given)@." n m
else
printf " %d/%d (replay OK, but not all proved: obsolete \
if !opt_force then
printf " %d/%d (replay OK, but not all proved: session going to be saved since -force was given)@." n m
else
printf " %d/%d (replay OK, but not all proved: obsolete \
session NOT updated)@." n m
else
printf " %d/%d@." n m ;
if !opt_stats && n<m then print_statistics files;
eprintf "Everything replayed OK.@.";
if found_obs && (n=m || !opt_force) then
begin
eprintf "Saving session...@?";
S.save_session config session;
eprintf " done@."
end;
exit 0
end
else
printf " %d/%d@." n m ;
if !opt_stats && n<m then print_statistics files;
eprintf "Everything replayed OK.@.";
if found_obs && (n=m || !opt_force) then
begin
eprintf "Saving session...@?";
S.save_session config session;
eprintf " done@."
end;
exit 0
end
else
let report = List.rev report in
begin
printf " %d/%d (replay failed)@." n m ;
List.iter print_report report;
......
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