From 4b2f76d34110d79c6dd77cb9f74075cf43c48020 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 21 Oct 2020 17:39:37 +0200
Subject: [PATCH] Updates with respect to kernel changes.
---
convert_acsl.ml | 4 ++--
generate_spec.ml | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/convert_acsl.ml b/convert_acsl.ml
index 82c53f05..d1761664 100644
--- a/convert_acsl.ml
+++ b/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
diff --git a/generate_spec.ml b/generate_spec.ml
index 93f48b10..a18b5560 100644
--- a/generate_spec.ml
+++ b/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 =
--
GitLab