|
|
@ -256,9 +256,8 @@ let add_errors exe_env summary =
|
|
|
|
if (not (is_inconsistent env phi)) && is_inconsistent env psi then (
|
|
|
|
if (not (is_inconsistent env phi)) && is_inconsistent env psi then (
|
|
|
|
let property, _vname = ToplAutomaton.vname (Lazy.force automaton) error in
|
|
|
|
let property, _vname = ToplAutomaton.vname (Lazy.force automaton) error in
|
|
|
|
let message = Printf.sprintf "property %s reaches error" property in
|
|
|
|
let message = Printf.sprintf "property %s reaches error" property in
|
|
|
|
tt "INCONSISTENT (WARN)@\n" ;
|
|
|
|
tt "WARN@\n" ;
|
|
|
|
Reporting.log_error summary IssueType.topl_error ~loc message )
|
|
|
|
Reporting.log_error summary IssueType.topl_error ~loc message )
|
|
|
|
else tt "CONSISTENT (do NOT warn)@\n"
|
|
|
|
|
|
|
|
in
|
|
|
|
in
|
|
|
|
(* Don't warn if [lookup_static_var] fails. *)
|
|
|
|
(* Don't warn if [lookup_static_var] fails. *)
|
|
|
|
Option.iter ~f:handle_state_post_value (lookup_static_var env state_var post)
|
|
|
|
Option.iter ~f:handle_state_post_value (lookup_static_var env state_var post)
|
|
|
|