Updates with respect to kernel changes.

convert_acsl.ml

@@ -594,9 +594,9 @@ let convert_assigns env = function
       Logic_ptree.Writes (List.map (convert_from env) l)
 
 let convert_pred_tp env p =
-  (* TODO: support check in ACSL++. *)
+  (* TODO: support check and admit in ACSL++. *)
   let tp_statement = convert_pred_named env p in
-  { tp_only_check = false; tp_statement }
+  { tp_kind = Assert; tp_statement }
 
 let convert_termination_kind = function
   | Intermediate_format.Normal -> Cil_types.Normal

generate_spec.ml

@@ -23,7 +23,7 @@
 open Logic_ptree
 open Intermediate_format
 
-let toplevel_pred tp_statement = { tp_only_check = false; tp_statement }
+let toplevel_pred tp_statement = { tp_kind = Assert; tp_statement }
 
 let const_valid lexpr_loc pkind t =
   let lexpr_node =