diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index e2471a994e8bc829f5e98c7e27540d6892e099d0..ad2a6c5f1ce6aa919f840f588a4a0ba949778492 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -111,6 +111,7 @@
if flag then Hashtbl.add c_kw i t
)
[
+ "admit", (fun _ -> ADMIT), false;
"allocates", (fun _ -> ALLOCATES), false;
"assert", (fun _ -> ASSERT), false;
"assigns", (fun _ -> ASSIGNS), false;
@@ -312,6 +313,15 @@
| CHECK, LOOP -> true, CHECK_LOOP
| CHECK, INVARIANT -> true, CHECK_INVARIANT
| CHECK, LEMMA -> true, CHECK_LEMMA
+ | ADMIT, REQUIRES -> true, ADMIT_REQUIRES
+ | ADMIT, ENSURES -> true, ADMIT_ENSURES
+ | ADMIT, EXITS -> true, ADMIT_EXITS
+ | ADMIT, RETURNS -> true, ADMIT_RETURNS
+ | ADMIT, BREAKS -> true, ADMIT_BREAKS
+ | ADMIT, CONTINUES -> true, ADMIT_CONTINUES
+ | ADMIT, LOOP -> true, ADMIT_LOOP
+ | ADMIT, INVARIANT -> true, ADMIT_INVARIANT
+ | ADMIT, LEMMA -> true, ADMIT_LEMMA
| _ -> false, current
}
@@ -356,7 +366,7 @@ rule token = parse
let cabsloc = Cil_datatype.Location.of_lexing_loc loc in
let s = lexeme lexbuf in
let curr_tok = identifier s cabsloc in
- if curr_tok = CHECK then begin
+ if curr_tok = CHECK || curr_tok = ADMIT then begin
let next_tok =
token { lexbuf with refill_buff = lexbuf.refill_buff }
in
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index aff0ff384ad84bba322d6ac71bc4ac8be26bc350..5cdd093c8794c2fd9bcb4996020694cf08d8de67 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -251,7 +251,7 @@
let cv_const = Attr ("const", [])
let cv_volatile = Attr ("volatile", [])
- let toplevel_pred tp_only_check tp_statement = { tp_only_check; tp_statement }
+ let toplevel_pred tp_kind tp_statement = { tp_kind; tp_statement }
%}
/*****************************************************************************/
@@ -277,10 +277,12 @@
%token ALLOCATION STATIC REGISTER AUTOMATIC DYNAMIC UNALLOCATED
%token ALLOCABLE FREEABLE FRESH
%token DOLLAR QUESTION MINUS PLUS STAR AMP SLASH PERCENT LSQUARE RSQUARE EOF
-%token GLOBAL INVARIANT VARIANT DECREASES FOR LABEL ASSERT CHECK SEMICOLON NULL EMPTY
+%token GLOBAL INVARIANT VARIANT DECREASES FOR LABEL ASSERT CHECK ADMIT SEMICOLON NULL EMPTY
%token REQUIRES ENSURES ALLOCATES FREES ASSIGNS LOOP NOTHING SLICE IMPACT PRAGMA FROM
%token CHECK_REQUIRES CHECK_LOOP CHECK_INVARIANT CHECK_LEMMA
%token CHECK_ENSURES CHECK_EXITS CHECK_CONTINUES CHECK_BREAKS CHECK_RETURNS
+%token ADMIT_REQUIRES ADMIT_LOOP ADMIT_INVARIANT ADMIT_LEMMA
+%token ADMIT_ENSURES ADMIT_EXITS ADMIT_CONTINUES ADMIT_BREAKS ADMIT_RETURNS
%token <string> EXT_CODE_ANNOT EXT_GLOBAL EXT_GLOBAL_BLOCK EXT_CONTRACT
%token EXITS BREAKS CONTINUES RETURNS
%token VOLATILE READS WRITES
@@ -1143,6 +1145,7 @@ contract:
// use that to detect potentially missing ';' at end of clause
clause_kw:
+| ADMIT_REQUIRES { "admit requires" }
| CHECK_REQUIRES { "check requires" }
| REQUIRES { "requires" }
| ASSUMES {"assumes"}
@@ -1167,10 +1170,12 @@ requires:
;
ne_requires:
-| REQUIRES full_lexpr SEMICOLON requires { toplevel_pred false $2::$4 }
-| CHECK_REQUIRES full_lexpr SEMICOLON requires { toplevel_pred true $2 :: $4 }
+| REQUIRES full_lexpr SEMICOLON requires { toplevel_pred Assert $2::$4 }
+| CHECK_REQUIRES full_lexpr SEMICOLON requires { toplevel_pred Check $2 :: $4 }
+| ADMIT_REQUIRES full_lexpr SEMICOLON requires { toplevel_pred Admit $2 :: $4 }
| REQUIRES full_lexpr clause_kw { missing 2 ";" $3 }
| CHECK_REQUIRES full_lexpr clause_kw { missing 2 ";" $3 }
+| ADMIT_REQUIRES full_lexpr clause_kw { missing 2 ";" $3 }
;
terminates:
@@ -1209,10 +1214,10 @@ allocation:
ne_simple_clauses:
| post_cond_kind full_lexpr SEMICOLON simple_clauses
- { let only_check, kind = $1 in
+ { let tp_kind, kind = $1 in
let allocation,assigns,post_cond,extended = $4 in
allocation,assigns,
- ((kind,toplevel_pred only_check $2)::post_cond),extended }
+ ((kind,toplevel_pred tp_kind $2)::post_cond),extended }
| allocation SEMICOLON simple_clauses
{ let allocation,assigns,post_cond,extended = $3 in
let a = concat_allocation allocation $1 in
@@ -1448,8 +1453,9 @@ loop_allocation:
;
loop_invariant:
-| LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred false $3 }
-| CHECK_LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred true $3 }
+| LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred Assert $3 }
+| CHECK_LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred Check $3 }
+| ADMIT_LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred Admit $3 }
;
loop_variant:
@@ -1499,8 +1505,10 @@ beg_pragma_or_code_annotation:
| FOR {}
| ASSERT {}
| CHECK {}
+| ADMIT {}
| INVARIANT {}
| CHECK_INVARIANT {}
+| ADMIT_INVARIANT {}
| EXT_CODE_ANNOT {}
;
@@ -1512,13 +1520,17 @@ pragma_or_code_annotation:
code_annotation:
| ASSERT full_lexpr SEMICOLON
- { fun bhvs -> AAssert (bhvs,toplevel_pred false $2) }
+ { fun bhvs -> AAssert (bhvs,toplevel_pred Assert $2) }
| CHECK full_lexpr SEMICOLON
- { fun bhvs -> AAssert (bhvs,toplevel_pred true $2) }
+ { fun bhvs -> AAssert (bhvs,toplevel_pred Check $2) }
+| ADMIT full_lexpr SEMICOLON
+ { fun bhvs -> AAssert (bhvs,toplevel_pred Admit $2) }
| INVARIANT full_lexpr SEMICOLON
- { fun bhvs -> AInvariant (bhvs,false,toplevel_pred false $2) }
+ { fun bhvs -> AInvariant (bhvs,false,toplevel_pred Assert $2) }
| CHECK_INVARIANT full_lexpr SEMICOLON
- { fun bhvs -> AInvariant (bhvs,false,toplevel_pred true $2) }
+ { fun bhvs -> AInvariant (bhvs,false,toplevel_pred Check $2) }
+| ADMIT_INVARIANT full_lexpr SEMICOLON
+ { fun bhvs -> AInvariant (bhvs,false,toplevel_pred Admit $2) }
| EXT_CODE_ANNOT grammar_extension SEMICOLON
{ fun bhvs ->
let open Cil_types in
@@ -1687,11 +1699,15 @@ logic_def:
| LEMMA poly_id COLON full_lexpr SEMICOLON
{ let (id,labels,tvars) = $2 in
exit_type_variables_scope ();
- LDlemma (id, false, labels, tvars, toplevel_pred false $4) }
+ LDlemma (id, false, labels, tvars, toplevel_pred Assert $4) }
| CHECK_LEMMA poly_id COLON full_lexpr SEMICOLON
{ let (id,labels,tvars) = $2 in
exit_type_variables_scope ();
- LDlemma (id, false, labels, tvars, toplevel_pred true $4) }
+ LDlemma (id, false, labels, tvars, toplevel_pred Check $4) }
+| ADMIT_LEMMA poly_id COLON full_lexpr SEMICOLON
+ { let (id,labels,tvars) = $2 in
+ exit_type_variables_scope ();
+ LDlemma (id, false, labels, tvars, toplevel_pred Admit $4) }
| AXIOMATIC any_identifier LBRACE logic_decls RBRACE
{ LDaxiomatic($2,$4) }
| TYPE poly_id_type_add_typename EQUAL typedef SEMICOLON
@@ -1764,7 +1780,7 @@ logic_decl:
| AXIOM poly_id COLON full_lexpr SEMICOLON
{ let (id,labels,tvars) = $2 in
exit_type_variables_scope ();
- LDlemma (id, true, labels, tvars, toplevel_pred false $4) }
+ LDlemma (id, true, labels, tvars, toplevel_pred Assert $4) }
;
logic_decl_loc:
@@ -1926,16 +1942,21 @@ acsl_c_keyword:
;
post_cond:
-| ENSURES { (false,Normal), "ensures" }
-| EXITS { (false,Exits), "exits" }
-| BREAKS { (false,Breaks), "breaks" }
-| CONTINUES { (false,Continues), "continues" }
-| RETURNS { (false,Returns), "returns" }
-| CHECK_ENSURES { (true,Normal), "check ensures" }
-| CHECK_EXITS { (true,Exits), "check exits" }
-| CHECK_BREAKS { (true,Breaks), "check breaks" }
-| CHECK_CONTINUES { (true,Continues), "check continues" }
-| CHECK_RETURNS { (true,Returns), "check returns" }
+| ENSURES { (Assert,Normal), "ensures" }
+| EXITS { (Assert,Exits), "exits" }
+| BREAKS { (Assert,Breaks), "breaks" }
+| CONTINUES { (Assert,Continues), "continues" }
+| RETURNS { (Assert,Returns), "returns" }
+| CHECK_ENSURES { (Check,Normal), "check ensures" }
+| CHECK_EXITS { (Check,Exits), "check exits" }
+| CHECK_BREAKS { (Check,Breaks), "check breaks" }
+| CHECK_CONTINUES { (Check,Continues), "check continues" }
+| CHECK_RETURNS { (Check,Returns), "check returns" }
+| ADMIT_ENSURES { (Admit,Normal), "admit ensures" }
+| ADMIT_EXITS { (Admit,Exits), "admit exits" }
+| ADMIT_BREAKS { (Admit,Breaks), "admit breaks" }
+| ADMIT_CONTINUES { (Admit,Continues), "admit continues" }
+| ADMIT_RETURNS { (Admit,Returns), "admit returns" }
;
is_acsl_spec:
@@ -1947,6 +1968,7 @@ is_acsl_spec:
| BEHAVIOR { "behavior" }
| REQUIRES { "requires" }
| CHECK_REQUIRES { "check requires" }
+| ADMIT_REQUIRES { "admit requires" }
| TERMINATES { "terminates" }
| COMPLETE { "complete" }
| DECREASES { "decreases" }
@@ -1960,6 +1982,7 @@ is_acsl_decl_or_code_annot:
| ASSUMES { "assumes" }
| ASSERT { "assert" }
| CHECK { "check" }
+| ADMIT { "admit" }
| GLOBAL { "global" }
| IMPACT { "impact" }
| INDUCTIVE { "inductive" }
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index 3b312f516dba0e9d87ad9af7dd906870ced37fda..8d7d1cad9f432b1ea2d05a3d8eefb54e6110dc26 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -212,8 +212,13 @@ let code_annot = Annotations.code_annot ~filter:supported_annotation
let make_annotation kf stmt annot labels =
let kind, pred =
match annot.annot_content with
- | AAssert ([], {tp_only_check = false; tp_statement = pred}) -> Assert, pred
- | AAssert ([], {tp_only_check = true; tp_statement = pred}) -> Check, pred
+ | AAssert ([], {tp_kind; tp_statement = pred}) ->
+ begin
+ match tp_kind with
+ | Cil_types.Assert -> Assert, pred
+ | Cil_types.Check -> Check, pred
+ | Cil_types.Admit -> Assume, pred
+ end
| AInvariant ([], _, pred) -> Invariant, pred.tp_statement
| AVariant (v, None) -> Assert, variant_predicate stmt v
| _ -> assert false
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 38729e6fbee348c12af24dddce1b547ad16e66e3..d5425c2e242959d5f23a56f658a1dd2f66444771 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -1317,12 +1317,17 @@ let add_code_annot ?(keep_empty=true) emitter ?kf stmt ca =
fill_tables ca (Property.ip_of_code_annot kf stmt ca)
let add_assert e ?kf stmt a =
- let a = Logic_const.toplevel_predicate ~only_check:false a in
+ let a = Logic_const.toplevel_predicate ~kind:Assert a in
let a = Logic_const.new_code_annotation (AAssert ([],a)) in
add_code_annot e ?kf stmt a
let add_check e ?kf stmt a =
- let a = Logic_const.toplevel_predicate ~only_check:true a in
+ let a = Logic_const.toplevel_predicate ~kind:Check a in
+ let a = Logic_const.new_code_annotation (AAssert ([],a)) in
+ add_code_annot e ?kf stmt a
+
+let add_admit e ?kf stmt a =
+ let a = Logic_const.toplevel_predicate ~kind:Admit a in
let a = Logic_const.new_code_annotation (AAssert ([],a)) in
add_code_annot e ?kf stmt a
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index 1e49ae756b5729db03bcf120966a9e69e151ac27..9bea58d4ab70e336a338f68c06b7503a4ee589d1 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -299,6 +299,12 @@ val add_check:
provided, the function runs faster.
@plugin development guide *)
+val add_admit:
+ Emitter.t -> ?kf:kernel_function -> stmt -> predicate -> unit
+(** Add an hypothesis assertion attached to the given statement. If [kf] is
+ provided, the function runs faster.
+ @plugin development guide *)
+
val add_global: Emitter.t -> global_annotation -> unit
(** Add a new global annotation into the program. *)
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index f05d4b75c334e5fcdab357a2b4f7f66497d10a95..3e7cf2768e11f22a3b0ef9b1a9ec1e7f0c5f551b 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1597,9 +1597,14 @@ and identified_predicate = {
ip_content: toplevel_predicate; (** the predicate itself*)
}
+and predicate_kind =
+ | Assert
+ | Check
+ | Admit
+
(** main statement of an annotation. *)
and toplevel_predicate = {
- tp_only_check: bool;
+ tp_kind: predicate_kind;
(** whether the annotation is only used to check that [ip_content] holds, but
stays invisible for other verification tasks (see description of ACSL's
check keyword).
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index 20cfa49ccc1af5984386ab78c5f6230577d7e716..2be8813645a9ca63fd7b2c7403205f869ed79f77 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -1019,8 +1019,9 @@ struct
Format.asprintf "%sextended%a" (extended_loc_prefix le) pp_names [ext_name]
| IPCodeAnnot {ica_kf=kf; ica_ca=ca} ->
let name = match ca.annot_content with
- | AAssert (_, {tp_only_check = false }) -> "assert"
- | AAssert (_, {tp_only_check = true }) -> "check"
+ | AAssert (_, {tp_kind = Assert }) -> "assert"
+ | AAssert (_, {tp_kind = Check }) -> "check"
+ | AAssert (_, {tp_kind = Admit }) -> "admit"
| AInvariant (_,true,_) -> "loop_inv"
| AInvariant _ -> "inv"
| APragma _ -> "pragma"
@@ -1155,6 +1156,12 @@ struct
let open Sanitizer in
add_part buffer p ; add_sep buffer ; add_parts buffer ps
+ let prefix_with_kind tp name =
+ match tp.tp_kind with
+ | Assert -> name
+ | Check -> "check_" ^ name
+ | Admit -> "admit_" ^ name
+
let rec parts_of_property ip : part list =
match ip with
| IPBehavior {ib_kf; ib_kinstr=Kglobal; ib_bhv} ->
@@ -1165,34 +1172,22 @@ struct
| IPPredicate {ip_kind=PKAssumes bhv; ip_kf=kf; ip_pred=ip} ->
[ K kf ; B bhv ; A "assumes" ; I ip ]
| IPPredicate {ip_kind=PKRequires bhv; ip_kf=kf; ip_pred=ip} ->
- let a =
- if ip.ip_content.tp_only_check then "check_requires" else "requires"
- in
+ let a = prefix_with_kind ip.ip_content "requires" in
[ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Normal); ip_kf=kf; ip_pred=ip} ->
- let a =
- if ip.ip_content.tp_only_check then "check_ensures" else "ensures"
- in
+ let a = prefix_with_kind ip.ip_content "ensures" in
[ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Exits); ip_kf=kf; ip_pred=ip} ->
- let a =
- if ip.ip_content.tp_only_check then "check_exits" else "exits"
- in
+ let a = prefix_with_kind ip.ip_content "exits" in
[ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Breaks); ip_kf=kf; ip_pred=ip} ->
- let a =
- if ip.ip_content.tp_only_check then "check_breaks" else "breaks"
- in
+ let a = prefix_with_kind ip.ip_content "breaks" in
[ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Continues); ip_kf=kf; ip_pred=ip} ->
- let a =
- if ip.ip_content.tp_only_check then "check_continues" else "continues"
- in
+ let a = prefix_with_kind ip.ip_content "continues" in
[ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Returns); ip_kf=kf; ip_pred=ip} ->
- let a =
- if ip.ip_content.tp_only_check then "check_returns" else "returns"
- in
+ let a = prefix_with_kind ip.ip_content "returns" in
[ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKTerminates; ip_kf=kf; ip_pred=ip} ->
[ K kf ; A "terminates" ; I ip ]
@@ -1225,17 +1220,17 @@ struct
ica_ca={annot_content=AExtended (_, _, {ext_name})}} ->
[ K kf ; A ext_name ; S stmt ]
| IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AAssert (_,p)}} ->
- let a = if p.tp_only_check then "check" else "assert" in
+ let a = match p.tp_kind with
+ | Assert -> "assert"
+ | Check -> "check"
+ | Admit -> "admit"
+ in
[K kf ; A a ; P p.tp_statement ]
| IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AInvariant (_, true, p)}} ->
- let a =
- if p.tp_only_check then "check_loop_invariant" else "loop_invariant"
- in
+ let a = prefix_with_kind p "loop_invariant" in
[K kf ; A a ; P p.tp_statement ]
| IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AInvariant (_,false, p)}} ->
- let a =
- if p.tp_only_check then "check_invariant" else "invariant"
- in
+ let a = prefix_with_kind p "invariant" in
[K kf ; A a ; P p.tp_statement ]
| IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AVariant (e, _)}} ->
[K kf ; A "loop_variant" ; T e ]
@@ -1264,7 +1259,7 @@ struct
| IPAxiomatic _
| IPAxiom _ -> []
| IPLemma {il_name=name; il_pred=p} ->
- let a = if p.tp_only_check then "check_lemma" else "lemma" in
+ let a = prefix_with_kind p "lemma" in
[ A a ; A name ; P p.tp_statement ]
| IPTypeInvariant {iti_name=name}
diff --git a/src/kernel_services/ast_data/statuses_by_call.ml b/src/kernel_services/ast_data/statuses_by_call.ml
index f076603133d49546da0a86355c179bba4570f226..a623869699afdccd2e13c035aa06ee822a951357 100644
--- a/src/kernel_services/ast_data/statuses_by_call.ml
+++ b/src/kernel_services/ast_data/statuses_by_call.ml
@@ -174,8 +174,8 @@ let transpose_pred_at_callsite ~formals ~concretes id_pred =
let new_pred = Cil.visitCilPredicateNode visitor pred.pred_content in
let p_unnamed = Logic_const.unamed ~loc:pred.pred_loc new_pred in
let p_named = { p_unnamed with pred_name = pred.pred_name } in
- let only_check = id_pred.ip_content.tp_only_check in
- Some (Logic_const.new_predicate ~only_check p_named)
+ let kind = id_pred.ip_content.tp_kind in
+ Some (Logic_const.new_predicate ~kind p_named)
with Non_Transposable -> None
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 93f7a11edfe9e87b21528fedf243d23d61b58396..f3ee3536abee0d8f6038fff3709931c4bf0e427e 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2847,8 +2847,11 @@ class cil_printer () = object (self)
method decreases fmt v = self#decrement "decreases" fmt v
method variant fmt v = self#decrement "loop variant" fmt v
- method private pp_only_check fmt p =
- if p.tp_only_check then fprintf fmt "%a " self#pp_acsl_keyword "check"
+ method private pp_predicate_kind fmt p =
+ match p.tp_kind with
+ | Assert -> ()
+ | Check -> fprintf fmt "%a " self#pp_acsl_keyword "check"
+ | Admit -> fprintf fmt "%a " self#pp_acsl_keyword "admit"
method assumes fmt p =
fprintf fmt "@[<hov 2>%a@ %a;@]"
@@ -2857,7 +2860,7 @@ class cil_printer () = object (self)
method requires fmt p =
fprintf fmt "@[<hov 2>%a%a@ %a;@]"
- self#pp_only_check p.ip_content
+ self#pp_predicate_kind p.ip_content
self#pp_acsl_keyword "requires"
self#identified_predicate p
@@ -2870,7 +2873,7 @@ class cil_printer () = object (self)
method post_cond fmt (k,p) =
let kw = get_termination_kind_name k in
fprintf fmt "@[<hov 2>%a%a@ %a;@]"
- self#pp_only_check p.ip_content
+ self#pp_predicate_kind p.ip_content
self#pp_acsl_keyword kw
self#identified_predicate p
@@ -3083,7 +3086,11 @@ class cil_printer () = object (self)
in
match ca.annot_content with
| AAssert (behav,p) ->
- let kw = if p.tp_only_check then "check" else "assert" in
+ let kw = match p.tp_kind with
+ | Assert -> "assert"
+ | Check -> "check"
+ | Admit -> "admit"
+ in
fprintf fmt "@[%a%a@ %a;@]"
pp_for_behavs behav
self#pp_acsl_keyword kw
@@ -3115,13 +3122,13 @@ class cil_printer () = object (self)
| AInvariant(behav,true, i) ->
fprintf fmt "@[<2>%a%a%a@ %a;@]"
pp_for_behavs behav
- self#pp_only_check i
+ self#pp_predicate_kind i
self#pp_acsl_keyword "loop invariant"
self#predicate i.tp_statement
| AInvariant(behav,false,i) ->
fprintf fmt "@[<2>%a%a%a@ %a;@]"
pp_for_behavs behav
- self#pp_only_check i
+ self#pp_predicate_kind i
self#pp_acsl_keyword "invariant"
self#predicate i.tp_statement
| AVariant v ->
@@ -3214,7 +3221,7 @@ class cil_printer () = object (self)
(* attributes are meant to be purely internal for now. *)
let old_lab = current_label in
fprintf fmt "@[<hv 2>@[<hov 1>%a%a %a%a%a:@]@ %t%a;@]@\n"
- self#pp_only_check pred
+ self#pp_predicate_kind pred
self#pp_acsl_keyword (if is_axiom then "axiom" else "lemma")
self#varname name
self#labels labels
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 7ab3d3f9d0fc753b9d0097478f3702190d15cd57..326c95e4eab0f88c9d8bd2ed15a16bfc1ee063bf 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -882,9 +882,14 @@ and pp_identified_predicate fmt identified_predicate =
identified_predicate.ip_id
pp_toplevel_predicate identified_predicate.ip_content
+and pp_predicate_kind fmt = function
+ | Assert -> Format.fprintf fmt "Assert"
+ | Check -> Format.fprintf fmt "Check"
+ | Admit -> Format.fprintf fmt "Admit"
+
and pp_toplevel_predicate fmt toplevel_predicate =
- Format.fprintf fmt "{tp_only_check=%B;tp_statement=%a}"
- toplevel_predicate.tp_only_check
+ Format.fprintf fmt "{tp_kind=%a;tp_statement=%a}"
+ pp_predicate_kind toplevel_predicate.tp_kind
pp_predicate toplevel_predicate.tp_statement
and pp_predicate fmt predicate = Format.fprintf fmt "{%a%apred_content=%a}"
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index 8ccda1048a0f5e2fdada76f9db31d63eee68125a..fc6ff06a00e3f341ba21a247bd690dde81543fc9 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -119,10 +119,14 @@ let pp_top fmt tp = pp_named fmt tp.tp_statement
let pp_code_annot fmt ca =
match ca.annot_content with
- | AAssert(bs,tp) when not tp.tp_only_check ->
- Format.fprintf fmt "assertion%a%a" pp_for bs pp_top tp
| AAssert(bs,tp) ->
- Format.fprintf fmt "check%a%a" pp_for bs pp_top tp
+ let kind =
+ match tp.tp_kind with
+ | Assert -> "assertion"
+ | Check -> "check"
+ | Admit -> "admit"
+ in
+ Format.fprintf fmt "%s%a%a" kind pp_for bs pp_top tp
| AInvariant(bs,_,tp) ->
Format.fprintf fmt "invariant%a%a" pp_for bs pp_top tp
| AAssigns(bs,_) -> Format.fprintf fmt "assigns%a" pp_for bs
@@ -260,14 +264,15 @@ let rec pp_prop kfopt kiopt kloc fmt = function
pp_bhvs ic_bhvs
(pp_opt kiopt (pp_kinstr kloc)) ic_kinstr
(pp_opt kiopt pp_active) ic_active
- | IPCodeAnnot {ica_ca={annot_content=AAssert(bs,tp)}}
- when not tp.tp_only_check ->
- Format.fprintf fmt "Assertion%a%a%a"
- pp_for bs
- pp_top tp
- (pp_kloc kloc) tp.tp_statement.pred_loc
| IPCodeAnnot {ica_ca={annot_content=AAssert(bs,tp)}} ->
- Format.fprintf fmt "Check%a%a%a"
+ let kind =
+ match tp.tp_kind with
+ | Assert -> "Assertion"
+ | Check -> "Check"
+ | Admit -> "Admit"
+ in
+ Format.fprintf fmt "%s%a%a%a"
+ kind
pp_for bs
pp_top tp
(pp_kloc kloc) tp.tp_statement.pred_loc
@@ -368,13 +373,16 @@ let to_string pp elt =
Buffer.contents b
let code_annot_kind_and_node code_annot = match code_annot.annot_content with
- | AAssert (_, {tp_only_check; tp_statement = {pred_content; pred_name}}) ->
+ | AAssert (_, {tp_kind; tp_statement = {pred_content; pred_name}}) ->
let kind = match Alarms.find code_annot with
| Some alarm -> Alarms.get_name alarm
| None ->
if List.exists ((=) "missing_return") pred_name then "missing_return"
- else if tp_only_check then "user check"
- else "user assertion"
+ else
+ match tp_kind with
+ | Assert -> "user assertion"
+ | Check -> "user check"
+ | Admit -> "user hypothesis"
in
Some (kind, to_string Printer.pp_predicate_node pred_content)
| AInvariant (_, _, {tp_statement = {pred_content}}) ->
@@ -477,13 +485,15 @@ let for_order k = function
| [] -> [I k]
| bs -> I (succ k) :: named_order bs
let annot_order = function
- | {annot_content=AAssert(bs,tp)} when tp.tp_only_check ->
+ | {annot_content=AAssert(bs,tp)} when tp.tp_kind = Assert ->
for_order 0 bs @ named_order tp.tp_statement.pred_name
- | {annot_content=AAssert(bs,tp)} ->
+ | {annot_content=AAssert(bs,tp)} when tp.tp_kind = Check ->
for_order 2 bs @ named_order tp.tp_statement.pred_name
- | {annot_content=AInvariant(bs,_,tp)} ->
+ | {annot_content=AAssert(bs,tp)} when tp.tp_kind = Admit ->
for_order 4 bs @ named_order tp.tp_statement.pred_name
- | _ -> [I 6]
+ | {annot_content=AInvariant(bs,_,tp)} ->
+ for_order 6 bs @ named_order tp.tp_statement.pred_name
+ | _ -> [I 8]
let loop_order = function
| Id_contract (active,b) -> [B b; A active]
| Id_loop _ -> []
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 59f6809727dcdd724cb9b841d531c7f072164fa8..ffd4b850dda5c351dcc0ef170709c7077f0c48f5 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -366,7 +366,10 @@ let rec print_decl fmt d =
(pp_list ~sep:"@\n" print_case) cases
| LDlemma(name,is_axiom,labels,tvar,body) ->
fprintf fmt "@[<2>%s%a@ %s%a%a:@ %a;@]"
- (if body.tp_only_check then "check " else "")
+ (match body.tp_kind with
+ | Assert -> ""
+ | Check -> "check "
+ | Admit -> "admit")
(pp_cond ~pr_false:"lemma" is_axiom) "axiom" name
(pp_list ~pre:"{@[" ~sep:",@ " ~suf:"@]}" pp_print_string) labels
(pp_list ~pre:"<@[" ~sep:",@ " ~suf:"@>}" pp_print_string) tvar
@@ -419,7 +422,12 @@ let print_allocation ~isloop fmt fa =
let print_clause name fmt e = fprintf fmt "@\n%s@ %a;" name print_lexpr e
let print_tp_clause name fmt e =
- let name = if e.tp_only_check then "check " ^ name else name in
+ let name =
+ match e.tp_kind with
+ | Assert -> name
+ | Check -> "check " ^ name
+ | Admit -> "admit " ^ name
+ in
print_clause name fmt e.tp_statement
let print_post fmt (k,e) =
@@ -487,16 +495,20 @@ let print_code_annot fmt ca =
AAssert(bhvs,e) ->
fprintf fmt "%a%s@ %a;"
print_behaviors bhvs
- (if e.tp_only_check then "check" else "assert")
+ (match e.tp_kind with
+ | Assert -> ""
+ | Check -> "check "
+ | Admit -> "admit")
print_lexpr e.tp_statement
| AStmtSpec (bhvs,s) ->
fprintf fmt "%a%a"
print_behaviors bhvs
print_spec s
| AInvariant (bhvs,loop,e) ->
- fprintf fmt "%a%a%ainvariant@ %a;"
+ fprintf fmt "%a%a%a%ainvariant@ %a;"
print_behaviors bhvs
- (pp_cond e.tp_only_check) "check @"
+ (pp_cond (e.tp_kind = Check)) "check @"
+ (pp_cond (e.tp_kind = Admit)) "admit @"
(pp_cond loop) "loop@ "
print_lexpr e.tp_statement
| AVariant e -> fprintf fmt "loop@ variant@ %a;" print_variant e
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 82f5d57783837ad5cbfdb91000694700c0dd9ce7..882c494bce29891729f876f88bc199d62ae6f864 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2279,7 +2279,7 @@ module Toplevel_predicate = struct
type t = toplevel_predicate
let name = "Toplevel_predicate"
let reprs =
- [ { tp_statement = List.hd Predicate.reprs; tp_only_check = false }]
+ [ { tp_statement = List.hd Predicate.reprs; tp_kind = Assert }]
let internal_pretty_code = Datatype.undefined
let pretty fmt x = !pretty_ref fmt x
let varname _ = "p"
diff --git a/src/kernel_services/ast_queries/logic_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index e53a0d86219e1603a6eba5af8d01d0e6d3b51ae9..63f9e6486708d5aaddc2e997842e15127e610a8c 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -43,11 +43,11 @@ let new_code_annotation annot =
let fresh_code_annotation = AnnotId.next
-let toplevel_predicate ?(only_check=false) p =
- { tp_only_check = only_check; tp_statement = p }
+let toplevel_predicate ?(kind=Assert) p =
+ { tp_kind = kind; tp_statement = p }
-let new_predicate ?only_check p =
- { ip_id = PredicateId.next (); ip_content = toplevel_predicate ?only_check p }
+let new_predicate ?kind p =
+ { ip_id = PredicateId.next (); ip_content = toplevel_predicate ?kind p }
let fresh_predicate_id = PredicateId.next
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index 2c2ebd716d21ef10694c88d9c0e412285ceafe91..8db8710c818c7f5d9b7d774a72e1356a91a5e12c 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -47,18 +47,21 @@ val refresh_code_annotation: code_annotation -> code_annotation
val refresh_spec: funspec -> funspec
(** creates a new toplevel predicate.
- [only_check] is true if the corresponding predicate should only be used
- to check a property, without adding it as hypothesis for the rest of the
- verification. See {!Cil_types.toplevel_predicate} for more information.
- Default is [false], i.e. use standard ACSL semantics.
+ [predicate_kind] is [Assert] by default. It can be set to:
+ - [Check] for a predicate that should only be used to check a property,
+ without adding it as hypothesis for the rest of the verification.
+ - [Admit] for a predicate that is an hypothesis for the rest of the
+ verification and should not be checked by Frama-C.
+
+ See {!Cil_types.toplevel_predicate} for more information.
@since 22.0-Titanium
*)
-val toplevel_predicate: ?only_check:bool -> predicate -> toplevel_predicate
+val toplevel_predicate: ?kind:predicate_kind -> predicate -> toplevel_predicate
(** creates a new identified predicate with a fresh id.
@modify 22.0-Titanium add [only_check] optional parameter
*)
-val new_predicate: ?only_check:bool -> predicate -> identified_predicate
+val new_predicate: ?kind:predicate_kind -> predicate -> identified_predicate
(** creates a new acsl_extension with a fresh id.
@plugin development guide
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 4785bb01b5423f62615d1d30673151866b67ac28..250e409acf6a0d98e05f474c6cea24cec0d44f40 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3577,8 +3577,8 @@ struct
let id_predicate env pred = Logic_const.new_predicate (predicate env pred)
let id_predicate_top env pred =
- let { tp_only_check = only_check; tp_statement = pred } = pred in
- Logic_const.new_predicate ~only_check (predicate env pred)
+ let { tp_kind = kind; tp_statement = pred } = pred in
+ Logic_const.new_predicate ~kind (predicate env pred)
let id_term_ptr env t =
let loc = t.lexpr_loc in
@@ -3832,10 +3832,10 @@ struct
let code_annot loc current_behaviors current_return_type ca =
let source = fst loc in
let annot = match ca with
- | AAssert (behav,{tp_only_check=only_check; tp_statement = p}) ->
+ | AAssert (behav,{tp_kind = kind; tp_statement = p}) ->
check_behavior_names loc current_behaviors behav;
let p = predicate (code_annot_env()) p in
- let p = Logic_const.toplevel_predicate ~only_check p in
+ let p = Logic_const.toplevel_predicate ~kind p in
Cil_types.AAssert(behav,p)
| APragma (Impact_pragma sp) ->
Cil_types.APragma
@@ -3862,10 +3862,10 @@ struct
Cil_types.AStmtSpec (behav,my_spec)
| AVariant v ->
Cil_types.AVariant (type_variant (loop_annot_env ()) v)
- | AInvariant (behav,f,{ tp_only_check = only_check; tp_statement = i}) ->
+ | AInvariant (behav,f,{ tp_kind = kind; tp_statement = i}) ->
let env = if f then loop_annot_env () else code_annot_env () in
check_behavior_names loc current_behaviors behav;
- let p = Logic_const.toplevel_predicate ~only_check (predicate env i) in
+ let p = Logic_const.toplevel_predicate ~kind (predicate env i) in
Cil_types.AInvariant (behav,f,p)
| AAllocation (behav,fa) ->
check_behavior_names loc current_behaviors behav;
@@ -4188,8 +4188,7 @@ struct
C.error loc "Definition of %s is cyclic" s;
my_info.lt_def <- tdef;
Dtype (my_info,loc)
- | LDlemma (x,is_axiom, labels, poly,
- { tp_only_check = only_check; tp_statement = e}) ->
+ | LDlemma (x,is_axiom, labels, poly, {tp_kind = kind; tp_statement = e}) ->
if Logic_env.Lemmas.mem x then begin
let old_def = Logic_env.Lemmas.find x in
let old_loc = Cil_datatype.Global_annotation.loc old_def in
@@ -4205,7 +4204,7 @@ struct
Cil_datatype.Location.pretty old_loc
end;
let labels,env = annot_env loc labels poly in
- let p = Logic_const.toplevel_predicate ~only_check (predicate env e) in
+ let p = Logic_const.toplevel_predicate ~kind (predicate env e) in
let labels = match !Lenv.default_label with
| None -> labels
| Some lab -> [lab]
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index cf3a8f2a53fd2aa8ad7e50fc782804643f2c374d..13faf94caec036357b16559f031cd9b11fddf9e2 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1092,7 +1092,7 @@ and is_same_predicate pred1 pred2 =
and is_same_toplevel_predicate p1 p2 =
- p1.tp_only_check = p2.tp_only_check &&
+ p1.tp_kind = p2.tp_kind &&
is_same_predicate p1.tp_statement p2.tp_statement
and is_same_identified_predicate p1 p2 =
@@ -2230,10 +2230,13 @@ let lhost_c_type thost =
| TResult ty -> ty
let is_assert ca =
- match ca.annot_content with AAssert (_, p) -> not p.tp_only_check | _ -> false
+ match ca.annot_content with AAssert (_, p) -> p.tp_kind = Assert | _ -> false
let is_check ca =
- match ca.annot_content with AAssert (_, p) -> p.tp_only_check | _ -> false
+ match ca.annot_content with AAssert (_, p) -> p.tp_kind = Check | _ -> false
+
+let is_admit ca =
+ match ca.annot_content with AAssert (_, p) -> p.tp_kind = Admit | _ -> false
let is_contract ca =
match ca.annot_content with AStmtSpec _ -> true | _ -> false
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index ae2b76fdbd2762248cd4dbcb801571c71b641951..71579a36bf00d97439eefb4a3115a01d8916b62d 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -450,6 +450,7 @@ val clear_funspec: funspec -> unit
val is_assert : code_annotation -> bool
val is_check : code_annotation -> bool
+val is_admit : code_annotation -> bool
val is_contract : code_annotation -> bool
val is_stmt_invariant : code_annotation -> bool
val is_loop_invariant : code_annotation -> bool
diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.mli
index ccc7a1d24afbf114b911e6d3a33ab74748ec6e48..9dabbc955a66d5f78d7c6d26303f2c353da37193 100644
--- a/src/kernel_services/parsetree/logic_ptree.mli
+++ b/src/kernel_services/parsetree/logic_ptree.mli
@@ -161,7 +161,8 @@ and lexpr_node =
| PLrepeat of lexpr * lexpr
(** repeat a list of elements a number of times. *)
-type toplevel_predicate = { tp_only_check: bool; tp_statement: lexpr }
+type toplevel_predicate =
+ { tp_kind: Cil_types.predicate_kind; tp_statement: lexpr }
type extension = string * lexpr list
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 7bae8b34ad4fab3c19e3179626a316d3b725b09a..341fb420f6d0e2636d66fbbcc1c8204cd21bee7b 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -1082,7 +1082,7 @@ let mk_deterministic_lemma () =
in
let trans = Path_analysis.get_transitions_of_state state automaton in
let prop = Extlib.product_fold disjoint_guards ptrue trans trans in
- let prop = Logic_const.toplevel_predicate ~only_check:true prop in
+ let prop = Logic_const.toplevel_predicate ~kind:Check prop in
let name = state.Promelaast.name ^ "_deterministic_trans" in
let lemma =
Dlemma (name, false, [label],[],prop,[],Cil_datatype.Location.unknown)
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index 4ccc7150ee34e5fd96239908e934d25f9e3e9ab8..cbd09639a4b6fdfeeb50d9098a37c056b3f96935 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -113,6 +113,7 @@ module Refreshers: sig
val from: check
val user_assertions: check
val user_checks: check
+ val user_admits: check
val rte: check
val invariant: check
val variant: check
@@ -242,6 +243,8 @@ struct
add ~name:"User assertions" ~hint:"Show user assertions" ()
let user_checks =
add ~name:"User checks" ~hint:"Show user checks" ()
+ let user_admits =
+ add ~name:"User admits" ~hint:"Show user hypotheses" ()
(* Function called when RTEs are enabled or disabled. *)
let set_rte = ref (fun _b -> ())
let rte = add ~set:(fun b -> !set_rte b) ~name:"RTEs"
@@ -364,6 +367,7 @@ struct
from.add hb;
user_assertions.add hb;
user_checks.add hb;
+ user_admits.add hb;
rte.add hb;
invariant.add hb;
variant.add hb;
@@ -636,12 +640,15 @@ let make_panel (main_ui:main_window_extension_points) =
| IPLemma _ -> lemmas.get ()
| IPComplete _ -> complete_disjoint.get ()
| IPDisjoint _ -> complete_disjoint.get ()
- | IPCodeAnnot {ica_ca={annot_content=AAssert(_, {tp_only_check})} as ca} ->
+ | IPCodeAnnot {ica_ca={annot_content=AAssert(_, {tp_kind})} as ca} ->
begin
match Alarms.find ca with
| Some a -> rte.get () && active_alarm a
| None ->
- if tp_only_check then user_checks.get() else user_assertions.get ()
+ match tp_kind with
+ | Assert -> user_assertions.get ()
+ | Check -> user_checks.get ()
+ | Admit -> user_admits.get ()
end
| IPCodeAnnot {ica_ca={annot_content = AInvariant _}} ->
invariant.get ()
diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml
index 0bb6f66958fd1999236111f37dfa58f142626b50..06708db6d2f1ea32046517cf036ab18462c9f004 100644
--- a/src/plugins/obfuscator/obfuscate.ml
+++ b/src/plugins/obfuscator/obfuscate.ml
@@ -150,13 +150,13 @@ class visitor = object
Cil.SkipChildren
else begin
Identified_predicate.Hashtbl.add id_pred_visited p ();
- let { tp_only_check = only_check; tp_statement = pred } = p.ip_content in
+ let { tp_kind; tp_statement = pred } = p.ip_content in
let names = pred.pred_name in
let names' =
List.map (Dictionary.fresh Obfuscator_kind.Predicate) names
in
let pred' = { pred with pred_name = names' } in
- let ip_content = Logic_const.toplevel_predicate ~only_check pred' in
+ let ip_content = Logic_const.toplevel_predicate ~kind:tp_kind pred' in
let p' = { p with ip_content } in
Cil.ChangeDoChildrenPost (p', Extlib.id)
end
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index 481a00d4773639fdf3837ed580365eb5c6441e06..d1ae61bceb9d7ad0c1225d9d3d9029404079986c 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -488,7 +488,8 @@ let add_proven_annot (ca, stmt_ca) (ca_because, stmt_because) acc =
let check_stmt_annots (ca, stmt_ca) stmt acc =
let check _ annot acc =
match ca.annot_content, annot.annot_content with
- | AAssert (_, p'), AAssert (_, p) when not p'.tp_only_check ->
+ | AAssert (_, p'), AAssert (_, p)
+ when p'.tp_kind <> Check && p.tp_kind <> Admit ->
let p = p.tp_statement.pred_content in
let p' = p'.tp_statement.pred_content in
if Logic_utils.is_same_predicate_node p p' then
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index aca667ed895230689e9f31d7f81ee4d72edfe440..cc2f4484a24428ea79f7153d9fd78eee4fe2ee2b 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -66,6 +66,7 @@ struct
let t_assert = t_kind "assert" "Assertion"
let t_check = t_kind "check" "Check"
+ let t_admit = t_kind "admit" "Hypothesis"
let t_loop_invariant = t_loop "invariant"
let t_loop_assigns = t_loop "assigns"
let t_loop_variant = t_loop "variant"
@@ -114,8 +115,9 @@ struct
| IPDisjoint _ -> t_disjoint
| IPCodeAnnot { ica_ca={ annot_content } } ->
begin match annot_content with
- | AAssert (_, {tp_only_check = false}) -> t_assert
- | AAssert (_, {tp_only_check = true }) -> t_check
+ | AAssert (_, {tp_kind = Assert}) -> t_assert
+ | AAssert (_, {tp_kind = Check }) -> t_check
+ | AAssert (_, {tp_kind = Admit }) -> t_admit
| AStmtSpec _ -> t_code_contract
| AInvariant(_,false,_) -> t_code_invariant
| AInvariant(_,true,_) -> t_loop_invariant
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index a6efdf17d21b8abfa3ff22fabffb1155fd11ecfe..9308063e3e20779e837397e56a21ecfb175554f9 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -453,7 +453,7 @@ module Make
let emit = emit_message_and_status kind kf behavior ~active in
let aux_pred states pred =
let pr = Logic_const.pred_of_id_pred pred in
- let reduce = active && not pred.ip_content.tp_only_check in
+ let reduce = active && pred.ip_content.tp_kind <> Check in
let ip = build_prop pred in
if ignore_predicate pr then
states
@@ -581,8 +581,9 @@ module Make
let code_annotation_text ca =
match ca.annot_content with
- | AAssert (_,{tp_only_check = false}) -> "assertion"
- | AAssert (_,{tp_only_check = true}) -> "check"
+ | AAssert (_,{tp_kind = Assert}) -> "assertion"
+ | AAssert (_,{tp_kind = Check}) -> "check"
+ | AAssert (_,{tp_kind = Admit}) -> "admit"
| AInvariant _ -> "loop invariant"
| APragma _ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
| AExtended _ ->
@@ -690,7 +691,7 @@ module Make
match code_annot.annot_content with
| AAssert (behav, p)
| AInvariant (behav, true, p) ->
- aux ~reduce:(not p.tp_only_check) code_annot behav p.tp_statement
+ aux ~reduce:(p.tp_kind <> Check) code_annot behav p.tp_statement
| APragma _
| AInvariant (_, false, _)
| AVariant _ | AAssigns _ | AAllocation _ | AExtended _
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index 2c1c9b875bcf119b441ac20937f7a57c8d245e82..cffbd71e7888b40fd1a7d0f92d0dd589a45cddc6 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -29,8 +29,9 @@ let has_requires spec =
let code_annotation_text ca =
match ca.annot_content with
- | AAssert (_, {tp_only_check=false}) -> "assertion"
- | AAssert (_, {tp_only_check=true}) -> "check"
+ | AAssert (_, {tp_kind=Assert}) -> "assertion"
+ | AAssert (_, {tp_kind=Check}) -> "check"
+ | AAssert (_, {tp_kind=Admit}) -> "admit"
| AInvariant _ -> "loop invariant"
| APragma _ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
| AExtended _ ->
diff --git a/src/plugins/wp/LogicUsage.ml b/src/plugins/wp/LogicUsage.ml
index 58600b88db555f358165fc22d47223d459f36c4b..b3533aefe3d26836aebd9905f78071ee46374e4f 100644
--- a/src/plugins/wp/LogicUsage.ml
+++ b/src/plugins/wp/LogicUsage.ml
@@ -195,22 +195,22 @@ let pp_profile fmt l =
let ip_lemma l =
let open Property in
- let mk_prop, only_check =
+ let mk_prop, kind =
match l.lem_kind with
- | `Axiom -> Property.ip_axiom, false
- | `Lemma -> Property.ip_lemma, false
- | `Check -> Property.ip_lemma, true
+ | `Axiom -> Property.ip_axiom, Admit
+ | `Lemma -> Property.ip_lemma, Assert
+ | `Check -> Property.ip_lemma, Check
in
mk_prop
{il_name = l.lem_name; il_labels = l.lem_labels;
il_args = l.lem_types; il_loc = (l.lem_position, l.lem_position);
il_attrs = l.lem_attrs;
- il_pred = Logic_const.toplevel_predicate ~only_check l.lem_property}
+ il_pred = Logic_const.toplevel_predicate ~kind l.lem_property}
let lemma_of_global ~context = function
| Dlemma(name,axiom,labels,types,pred,attrs,loc) ->
let kind = if axiom then `Axiom else
- if pred.tp_only_check then `Check else `Lemma in
+ if pred.tp_kind = Check then `Check else `Lemma in
{
lem_name = name ;
lem_position = fst loc ;
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 4a8f6ea3aeadb06a0fde85baa9c1bc075daec05b..a64dbebde9028fe379f26e47077dd42b1f47863e 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -761,7 +761,7 @@ let add_called_post called_kf termination_kind acc =
let kind = WpStrategy.AcallHyp called_kf in
let assumes = (Ast_info.behavior_assumes b) in
let add_post acc (tk, p) =
- if tk = termination_kind && not p.ip_content.tp_only_check
+ if tk = termination_kind && p.ip_content.tp_kind <> Check
then WpStrategy.add_prop_call_post acc kind called_kf b tk ~assumes p
else acc
in List.fold_left add_post acc b.b_post_cond
@@ -838,7 +838,7 @@ let add_variant_annot config s ca var_exp loop_entry loop_back =
in loop_entry, loop_back
let add_loop_invariant_annot config vloop s ca b_list inv acc =
- let only_check = inv.tp_only_check in
+ let only_check = inv.tp_kind = Check in
let inv = inv.tp_statement in
let assigns, loop_entry, loop_back , loop_core = acc in
(* we have to prove that inv is true for each edge that goes
@@ -952,7 +952,7 @@ let get_stmt_annots config v s =
let acc = match is_annot_for_config config v s b_list with
| TBRno -> acc
| TBRhyp ->
- if p.tp_only_check then acc
+ if p.tp_kind = Check then acc
else
let b_acc =
WpStrategy.add_prop_assert
@@ -961,10 +961,10 @@ let get_stmt_annots config v s =
| TBRok | TBRpart ->
let id = WpPropId.mk_assert_id config.kf s a in
let goal = goal_to_select config id in
- if p.tp_only_check && not goal then acc
+ if p.tp_kind = Check && not goal then acc
else
let kind =
- WpStrategy.(if p.tp_only_check then Agoal else Aboth goal)
+ WpStrategy.(if p.tp_kind = Check then Agoal else Aboth goal)
in
let b_acc =
WpStrategy.add_prop_assert b_acc kind kf s a p.tp_statement
@@ -1136,7 +1136,7 @@ let add_global_annotations annots =
linfo.l_var_info.lv_name;
()
| Dlemma (name,_,_,_,p,_,_) ->
- if not (p.tp_only_check) then
+ if p.tp_kind <> Check then
WpStrategy.add_axiom annots (LogicUsage.logic_lemma name)
and do_globals gs = List.iter do_global gs in
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index a95b4a864909dffb1047d8539b10948a51d73d00..90595b127583dd55bb7e21a6654d18da290ebeae 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -470,7 +470,7 @@ let ident_names names =
let pred_names p =
let p_names = ident_names p.tp_statement.pred_name in
- if p.tp_only_check then "@check"::p_names else p_names
+ if p.tp_kind = Check then "@check"::p_names else p_names
let code_annot_names ca = match ca.annot_content with
| AAssert (_, pred) -> "@assert" :: pred_names pred
diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index 60fe40d175ef9651652217627cc829397fddd8c9..af9937189835ee08c28116f7fae6a97139c53011 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -92,7 +92,7 @@ let is_dead_annot ca =
is_unrolled_completely spec
| AAssert([],p)
| AInvariant([],_,p) ->
- not p.tp_only_check && is_predicate false p.tp_statement
+ p.tp_kind <> Check && is_predicate false p.tp_statement
| _ -> false
let is_dead_code stmt =
diff --git a/src/plugins/wp/wpStrategy.ml b/src/plugins/wp/wpStrategy.ml
index 7026d2402035f301bee12cf740d9b92663f712f0..2488ade0d3fb2356a45d5750778a27ef22e4436a 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -171,7 +171,7 @@ let add_prop_fct_pre_bhv acc kind kf bhv =
Logic_const.(pat (p,pre_label))
in
let requires =
- List.filter (fun x -> not x.ip_content.tp_only_check) bhv.b_requires
+ List.filter (fun x -> x.ip_content.tp_kind <> Check) bhv.b_requires
in
let requires = Logic_const.pands (List.map norm_pred requires) in
let assumes = Logic_const.pands (List.map norm_pred bhv.b_assumes) in
@@ -183,7 +183,7 @@ let add_prop_fct_pre_bhv acc kind kf bhv =
add_prop acc kind id p
let add_prop_fct_pre acc kind kf bhv ~assumes pre =
- if pre.ip_content.tp_only_check then acc else begin
+ if pre.ip_content.tp_kind = Check then acc else begin
let id = WpPropId.mk_pre_id kf Kglobal bhv pre in
let labels = NormAtLabels.labels_fct_pre in
let p = Logic_const.pred_of_id_pred pre in
@@ -234,7 +234,7 @@ let add_prop_stmt_post acc kind kf s bhv tkind l_post ~assumes post =
add_prop acc kind id p
let update_kind kind pre =
- if pre.ip_content.tp_only_check then begin
+ if pre.ip_content.tp_kind = Check then begin
match kind with
| AcallPre(false,_) -> None
| AcallPre(true, kf) -> Some (AcallCheck kf)
diff --git a/tests/syntax/syntactic_hook.ml b/tests/syntax/syntactic_hook.ml
index 5a479278793dbeb6d7f90325d44d63a624fc95d7..f8d04f6fcb3137bd306071d5d213a1fe2da20641 100644
--- a/tests/syntax/syntactic_hook.ml
+++ b/tests/syntax/syntactic_hook.ml
@@ -15,7 +15,7 @@ class visit = object
CODE_ANNOT(
AAssert(
[],
- { tp_only_check = false;
+ { tp_kind = Assert;
tp_statement =
{ lexpr_node =
PLat ({ lexpr_node = PLtrue; lexpr_loc = loc},"Pre");