WIP

Gillian-C/examples/amazon/Makefile

@@ -42,4 +42,11 @@ byte-cursor-ub:
 bugs: string-bug header-bug byte-cursor-ub
 
 clean:
-	rm -rf *.i *.deps
+	rm -rf *.i *.deps
+
+t:
+	${VERIFY} \
+		header.c edk.c array_list.c ec.c byte_buf.c \
+		hash_table.c string.c allocator.c \
+		error.c base.c \
+		--fstruct-passing --no-lemma-proof --proc aws_cryptosdk_hdr_parse -l disabled --dump-smt

GillianCore/smt/smt.ml

@@ -16,7 +16,9 @@ let z3_config =
   ]
 
 let solver = new_solver z3
-let cmd s = ack_command solver s
+let cmd s =
+  let () = Fmt.pr "%a\n@?" Sexplib.Sexp.pp_hum s in
+  ack_command solver s
 let () = z3_config |> List.iter (fun (k, v) -> cmd (set_option (":" ^ k) v))
 
 exception SMT_unknown
@@ -984,7 +986,9 @@ let exec_sat (fs : Formula.Set.t) (gamma : typenv) : sexp option =
   in
   let encoded_assertions = encode_assertions fs gamma in
   let () = if !Config.dump_smt then Dump.dump fs gamma encoded_assertions in
-  let () = encoded_assertions |> List.iter (fun a -> cmd a) in
+  let () = Fmt.pr "== ABOUT TO SMT ==\n" in
+  let () = encoded_assertions |> List.iter (fun a -> cmd a)
+  in
   L.verbose (fun fmt -> fmt "Reached SMT.");
   let result = check solver in
   L.verbose (fun m ->
@@ -995,6 +999,7 @@ let exec_sat (fs : Formula.Set.t) (gamma : typenv) : sexp option =
         | Unknown -> "unknown"
       in
       m "The solver returned: %s" r);
+  (* TODO: fun protect with reset solver*)
   let ret =
     match result with
     | Unknown ->