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

@@ -119,6 +119,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) ->