Remove Asrt.Star (fix #159)

Gillian-C/lib/Constr.ml

@@ -3,7 +3,7 @@ open Gil_syntax
 module Core = struct
   let pred ga ins outs =
     let ga_name = LActions.str_ga ga in
-    Asrt.GA (ga_name, ins, outs)
+    Asrt.CorePred (ga_name, ins, outs)
 
   let single ~loc ~ofs ~chunk ~sval ~perm =
     let chunk = Expr.Lit (String (ValueTranslation.string_of_chunk chunk)) in

Gillian-C/lib/MonadicSMemory.ml

@@ -256,7 +256,7 @@ module Mem = struct
 
   let prod_bounds map loc bounds =
     let open DR.Syntax in
-    let** loc_name = resolve_loc_result loc in
+    let* loc_name = resolve_or_create_loc_name loc in
     let* tree = get_or_create_tree map loc_name in
     let++ tree_set =
       SHeapTree.prod_bounds tree bounds |> DR.of_result |> map_lift_err loc_name
@@ -525,7 +525,7 @@ let execute_prod_single heap params =
   ] ->
       let perm = ValueTranslation.permission_of_string perm_string in
       let chunk = ValueTranslation.chunk_of_string chunk_string in
-      let* sval = SVal.of_gil_expr_exn sval_e in
+      let* sval = SVal.of_gil_expr_vanish sval_e in
       let++ mem = Mem.prod_single heap.mem loc ofs chunk sval perm in
       { heap with mem }
   | _ -> fail_ungracefully "set_single" params

Gillian-C/lib/MonadicSVal.ml

@@ -89,9 +89,9 @@ let of_gil_expr sval_e =
   let open Patterns in
   Logging.verbose (fun fmt -> fmt "OF_GIL_EXPR : %a" Expr.pp sval_e);
   let* sval_e = Delayed.reduce sval_e in
-  match%ent sval_e with
-  | undefined -> DO.some SUndefined
-  | obj ->
+  if%sat undefined sval_e then DO.some SUndefined
+  else
+    if%sat obj sval_e then
       let loc_expr = Expr.list_nth sval_e 0 in
       let ofs = Expr.list_nth sval_e 1 in
       let* ofs = Delayed.reduce ofs in
@@ -105,11 +105,16 @@ let of_gil_expr sval_e =
             (aloc, learned)
       in
       DO.some ~learned (Sptr (loc, ofs))
-  | int_typ -> DO.some (SVint (Expr.list_nth sval_e 1))
-  | float_typ -> DO.some (SVfloat (Expr.list_nth sval_e 1))
-  | long_typ -> DO.some (SVlong (Expr.list_nth sval_e 1))
-  | single_typ -> DO.some (SVsingle (Expr.list_nth sval_e 1))
-  | _ -> DO.none ()
+    else
+      if%sat int_typ sval_e then DO.some (SVint (Expr.list_nth sval_e 1))
+      else
+        if%sat float_typ sval_e then DO.some (SVfloat (Expr.list_nth sval_e 1))
+        else
+          if%sat long_typ sval_e then DO.some (SVlong (Expr.list_nth sval_e 1))
+          else
+            if%sat single_typ sval_e then
+              DO.some (SVsingle (Expr.list_nth sval_e 1))
+            else DO.none ()
 
 let of_gil_expr_exn sval_e =
   let* value_opt = of_gil_expr sval_e in
@@ -119,6 +124,12 @@ let of_gil_expr_exn sval_e =
       if !Gillian.Utils.Config.under_approximation then Delayed.vanish ()
       else raise (NotACompCertValue sval_e)
 
+let of_gil_expr_vanish sval_e =
+  let* value_opt = of_gil_expr sval_e in
+  match value_opt with
+  | Some value -> Delayed.return value
+  | None -> Delayed.vanish ()
+
 let to_gil_expr_undelayed = to_gil_expr
 
 let to_gil_expr sval =

Gillian-C/lib/SHeapTree.mli

@@ -85,7 +85,7 @@ val allocated_function : t
     [dst_tree] after modification *)
 val move : t -> Expr.t -> t -> Expr.t -> Expr.t -> t d_or_error
 
-val assertions : loc:string -> t -> Asrt.t list
+val assertions : loc:string -> t -> Asrt.t
 
 val substitution :
   le_subst:(Expr.t -> Expr.t) ->