From 414a4e439a5c3b4d9a0a2b1de10fa201ab42ff28 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 5 Feb 2021 09:39:15 +0100
Subject: [PATCH] Revert "[kernel] merged axioms and lemmas"
This reverts commit c7efb7f759ce2aeb07cd0850b03752390c68296b
---
convert_acsl.ml | 17 ++++++++---------
1 file changed, 8 insertions(+), 9 deletions(-)
diff --git a/convert_acsl.ml b/convert_acsl.ml
index b7e0cf32..d1761664 100644
--- a/convert_acsl.ml
+++ b/convert_acsl.ml
@@ -313,7 +313,7 @@ and convert_logic_expr_node env = function
let l = convert_logic_label_opt l in
let t = convert_logic_expr env t in
PLoffset(l,t)
- | TBlock_length(l,t) ->
+ | TBlock_length(l,t) ->
let l = convert_logic_label_opt l in
let t = convert_logic_expr env t in
PLblock_length(l,t)
@@ -403,7 +403,7 @@ and convert_logic_offset env base = function
and path_of_offset env = function
| TNoOffset -> []
- | TField(s,o) | TModel(s,o) ->
+ | TField(s,o) | TModel(s,o) ->
let path = path_of_offset env o in
PLpathField s :: path
| TBase(b,t,o) ->
@@ -529,7 +529,7 @@ and convert_pred env = function
let t1 = convert_logic_expr env t1 in
let t2 = convert_logic_expr env t2 in
PLfresh (None,t1,t2)
- | Pfresh(_,_,_,_) -> Frama_Clang_option.fatal
+ | Pfresh(_,_,_,_) -> Frama_Clang_option.fatal
"zero or two labels needed in fresh construct"
| Psubtype _ -> Frama_Clang_option.not_yet_implemented "subtyping relation"
@@ -593,10 +593,10 @@ let convert_assigns env = function
| Intermediate_format.Writes l ->
Logic_ptree.Writes (List.map (convert_from env) l)
-let convert_pred_tp env ?(kind=Cil_types.Assert) p =
+let convert_pred_tp env p =
(* TODO: support check and admit in ACSL++. *)
let tp_statement = convert_pred_named env p in
- { tp_kind = kind; tp_statement }
+ { tp_kind = Assert; tp_statement }
let convert_termination_kind = function
| Intermediate_format.Normal -> Cil_types.Normal
@@ -766,9 +766,8 @@ 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 kind = if is_axiom then Cil_types.Admit else Assert in
- let body = convert_pred_tp env ~kind body in
- LDlemma(name,labs,params,body), env
+ 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
let name =
@@ -779,7 +778,7 @@ let rec convert_annot env annot =
env body.li_name TStandard in
Mangling.mangle body_name t None
in
- let body =
+ let body =
match body.fun_body with
| LBpred p ->
convert_pred_named env p
--
GitLab