From 1b29ccd52bf77464ca99da1ae463f2d0c9680fa3 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 10 Sep 2020 15:55:07 +0200
Subject: [PATCH] update to new kernel API
---
convert_acsl.ml | 15 ++++++++++-----
generate_spec.ml | 27 +++++++++++++++++----------
2 files changed, 27 insertions(+), 15 deletions(-)
diff --git a/convert_acsl.ml b/convert_acsl.ml
index ffe108d6..04267725 100644
--- a/convert_acsl.ml
+++ b/convert_acsl.ml
@@ -593,6 +593,11 @@ let convert_assigns env = function
| Intermediate_format.Writes l ->
Logic_ptree.Writes (List.map (convert_from env) l)
+let convert_pred_tp env p =
+ (* TODO: support check in ACSL++. *)
+ let tp_statement = convert_pred_named env p in
+ { tp_only_check = false; tp_statement }
+
let convert_termination_kind = function
| Intermediate_format.Normal -> Cil_types.Normal
| Intermediate_format.Exits -> Cil_types.Exits
@@ -601,11 +606,11 @@ let convert_termination_kind = function
| Intermediate_format.Returns -> Cil_types.Returns
let convert_post_cond env p =
- convert_termination_kind p.tkind, convert_pred_named env p.pred
+ convert_termination_kind p.tkind, convert_pred_tp env p.pred
let convert_behavior env bhv =
let b_name = bhv.beh_name in
- let b_requires = List.map (convert_pred_named env) bhv.requires in
+ let b_requires = List.map (convert_pred_tp env) bhv.requires in
let b_assumes = List.map (convert_pred_named env) bhv.assumes in
let b_post_cond = List.map (convert_post_cond env) bhv.post_cond in
let b_assigns = convert_assigns env bhv.assignements in
@@ -664,11 +669,11 @@ let convert_pragma env = function
let convert_code_annot env = function
| Intermediate_format.Assert(bhvs,pred) ->
- AAssert(bhvs, Assert, convert_pred_named env pred)
+ AAssert(bhvs, convert_pred_tp env pred)
| StmtSpec(bhvs,spec) -> AStmtSpec(bhvs,convert_function_contract env spec)
| Invariant(bhvs,kind,inv) ->
let kind = convert_inv_kind kind in
- let inv = convert_pred_named env inv in
+ let inv = convert_pred_tp env inv in
AInvariant(bhvs,kind,inv)
| Variant v -> AVariant (convert_variant env v)
| Assigns (bhvs,a) -> AAssigns(bhvs,convert_assigns env a)
@@ -761,7 +766,7 @@ let rec convert_annot env annot =
| Dlemma(loc,name,is_axiom,labs,params,body) ->
let env = Convert_env.set_loc env loc in
let labs = List.map convert_logic_label labs in
- let body = convert_pred_named env body in
+ let body = convert_pred_tp env body in
LDlemma(name,is_axiom,labs,params,body), env
| Dinvariant(loc,body) ->
let env = Convert_env.set_loc env loc in
diff --git a/generate_spec.ml b/generate_spec.ml
index fec8522d..af83e29f 100644
--- a/generate_spec.ml
+++ b/generate_spec.ml
@@ -23,15 +23,17 @@
open Logic_ptree
open Intermediate_format
+let toplevel_pred tp_statement = { tp_only_check = false; tp_statement }
+
let const_valid lexpr_loc pkind t =
let lexpr_node =
match pkind with
| PDataPointer { qualifier = q } ->
if List.mem Const q then PLvalid_read(None, t) else PLvalid(None,t)
| PFunctionPointer _ | PStandardMethodPointer _ | PVirtualMethodPointer _
- -> PLvalid_function(t)
+ -> PLvalid_function(t)
in
- { lexpr_node; lexpr_loc }
+ toplevel_pred { lexpr_node; lexpr_loc }
let add_valid_result env typ =
let loc = Convert_env.get_loc env in
@@ -62,8 +64,10 @@ let add_valid_references env l = List.fold_left (add_valid_reference env) [] l
let add_valid_this env kind =
let lexpr_loc = Convert_env.get_loc env in
let this = { lexpr_node = PLvar "this"; lexpr_loc } in
- let valid_read = { lexpr_node = PLvalid_read (None, this); lexpr_loc } in
- let valid = { lexpr_node = PLvalid(None, this); lexpr_loc } in
+ let valid_read =
+ toplevel_pred { lexpr_node = PLvalid_read (None, this); lexpr_loc }
+ in
+ let valid = toplevel_pred { lexpr_node = PLvalid(None, this); lexpr_loc } in
match kind with
| FKCastMethodOperator (cv,_) when List.mem Const cv -> [ valid_read ]
| FKMethod cv when List.mem Const cv -> [ valid_read ]
@@ -79,12 +83,15 @@ let add_separated_arg env acc arg =
(name,ts) (Extlib.the (Convert_env.get_current_class env))
->
let lexpr_loc = Cil_datatype.Location.of_lexing_loc arg.arg_loc in
- { lexpr_node =
- PLseparated(
- [ { lexpr_node = PLvar "this"; lexpr_loc };
- { lexpr_node = PLvar arg.arg_name; lexpr_loc } ]);
- lexpr_loc }
- :: acc
+ let p =
+ { lexpr_node =
+ PLseparated(
+ [ { lexpr_node = PLvar "this"; lexpr_loc };
+ { lexpr_node = PLvar arg.arg_name; lexpr_loc } ]);
+ lexpr_loc }
+ in
+ let pred = toplevel_pred p in
+ pred :: acc
| Named (name,_), _ when Cxx_utils.is_builtin_qual_type name -> acc
| Named (name,_), _
-> check_class (Convert_env.get_typedef env name).plain_type
--
GitLab