Commit 7a817565 authored by SOLIMAN Sylvain's avatar SOLIMAN Sylvain

Proper cleanup, even with instantiated Result for check_ctl_impl

parent c99fd1ac
......@@ -519,6 +519,8 @@ check_ctl_impl(Query, some, NusmvCX, BoolSem, Result) :-
:- dynamic(trace/1).
% care that if Result is instantiated, the predicate might fail before parsing
% the full output/trace
check_ctl_impl(Query, all, NusmvCX, BoolSem, Result) :-
retractall(trace(_)),
translate_ctl_for_nusmv(Query, NusmvQuery),
......@@ -540,7 +542,7 @@ check_ctl_impl(Query, all, NusmvCX, BoolSem, Result) :-
['-df', '-source', 'nusmv.cmd'],
[stdin(null), stdout(pipe(NusmvOut))]
),
parse_nusmv_out(NusmvOut, NusmvCX, Result),
call_cleanup(parse_nusmv_out(NusmvOut, NusmvCX, Result), close(NusmvOut)),
(
NusmvCX == 'yes',
trace(_)
......@@ -607,7 +609,6 @@ parse_nusmv_out(Out, NusmvCX, Result) :-
(
Codes = end_of_file
->
close(Out),
Result = 'error'
;
% "-- "
......@@ -630,8 +631,7 @@ parse_nusmv_out(Out, NusmvCX, Result) :-
true
;
parse_nusmv_out_trace(Out)
),
close(Out)
)
;
parse_nusmv_out(Out, NusmvCX, Result)
).
......
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