From 0874d2992b32ac6ab732d2026f6c22e99ddc9559 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 7 Mar 2019 18:24:55 +0100
Subject: [PATCH] [typing] slight refactoring
---
.../ast_queries/logic_typing.ml | 19 +++++++++++--------
1 file changed, 11 insertions(+), 8 deletions(-)
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index e281a3b8920..49ffb79f66f 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3774,21 +3774,24 @@ struct
append_loop_labels (append_here_label (append_pre_label (append_init_label
(Lenv.empty()))))
+ let assertion_kind =
+ function Assert -> Cil_types.Assert | Check -> Cil_types.Check
+
let code_annot loc current_behaviors current_return_type ca =
let source = fst loc in
let annot = match ca with
- | AAssert (behav,Assert,p) ->
- check_behavior_names loc current_behaviors behav;
- Cil_types.AAssert (behav, Cil_types.Assert, predicate (code_annot_env()) p)
- | AAssert (behav,Check,p) ->
+ | AAssert (behav,k,p) ->
check_behavior_names loc current_behaviors behav;
- Cil_types.AAssert (behav, Cil_types.Check, predicate (code_annot_env()) p)
+ Cil_types.AAssert(behav,assertion_kind k,predicate (code_annot_env()) p)
| APragma (Impact_pragma sp) ->
- Cil_types.APragma (Cil_types.Impact_pragma (impact_pragma (code_annot_env()) sp))
+ Cil_types.APragma
+ (Cil_types.Impact_pragma (impact_pragma (code_annot_env()) sp))
| APragma (Slice_pragma sp) ->
- Cil_types.APragma (Cil_types.Slice_pragma (slice_pragma (code_annot_env()) sp))
+ Cil_types.APragma
+ (Cil_types.Slice_pragma (slice_pragma (code_annot_env()) sp))
| APragma (Loop_pragma lp) ->
- Cil_types.APragma (Cil_types.Loop_pragma (loop_pragma (code_annot_env()) lp))
+ Cil_types.APragma
+ (Cil_types.Loop_pragma (loop_pragma (code_annot_env()) lp))
| AStmtSpec (behav,s) ->
(* function behaviors and statement behaviors are not at the
same level. Do not mix them in a complete or disjoint clause
--
GitLab