Reducing Nan would infinite loop because of Nan != Nan. This is fixed

Signed-off-by: Sacha Ayoun <[email protected]>

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

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 *)