diff --git a/GillianCore/GIL_Syntax/Literal.ml b/GillianCore/GIL_Syntax/Literal.ml index 2b28368dd..0a869ffb6 100644 --- a/GillianCore/GIL_Syntax/Literal.ml +++ b/GillianCore/GIL_Syntax/Literal.ml @@ -15,7 +15,19 @@ type t = TypeDef__.literal = | Type of Type.t (** GIL types ({!type:Type.t}) *) | LList of t list (** Lists of GIL literals *) | Nono -[@@deriving eq, ord] +[@@deriving ord] + +let rec equal la lb = + match (la, lb) with + | Undefined, Undefined | Null, Null | Empty, Empty | Nono, Nono -> true + | Constant cl, Constant cr -> Constant.equal cr cl + | Bool bl, Bool br -> Bool.equal bl br + | Int zl, Int zr -> Z.equal zl zr + | Num za, Num zb -> Int.equal (Stdlib.compare za zb) 0 + | String sl, String sr | Loc sl, Loc sr -> String.equal sl sr + | Type tl, Type tr -> Type.equal tl tr + | LList ll, LList lr -> List.for_all2 equal ll lr + | _ -> false let to_yojson = TypeDef__.literal_to_yojson let of_yojson = TypeDef__.literal_of_yojson diff --git a/GillianCore/command_line/s_interpreter_console.ml b/GillianCore/command_line/s_interpreter_console.ml index 991504028..8935d6a5e 100644 --- a/GillianCore/command_line/s_interpreter_console.ml +++ b/GillianCore/command_line/s_interpreter_console.ml @@ -20,10 +20,20 @@ struct open ChangeTracker let run_main prog init_data = - ignore - (S_interpreter.evaluate_proc - (fun x -> x) - prog !Config.entry_point [] (SState.init init_data)) + let all_results = + S_interpreter.evaluate_proc + (fun x -> x) + prog !Config.entry_point [] (SState.init init_data) + in + let success = + List.for_all + (function + | Exec_res.RSucc _ -> true + | _ -> false) + all_results + in + if success then Fmt.pr "%a@\n@?" (Fmt.styled `Green Fmt.string) "Success!" + else Fmt.pr "%a@\n@?" (Fmt.styled `Red Fmt.string) "Errors happened!" let run_incr source_files prog init_data = (* Only re-run program if transitive callees of main proc have changed *)