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 5e85be61e3be3278d974217d2e03ca96cc46e447..6f45565db717af3e6a4c5e1021b47067240d340b 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -224,8 +224,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 235d396271078e77a6e0cd9d5231e09738511bcf..2ecf1e2e78967e04ee23d8522fd9301e23ac38aa 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -1054,8 +1054,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"
@@ -1190,6 +1191,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} ->
@@ -1200,34 +1207,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 ]
@@ -1260,17 +1255,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 ]
@@ -1299,7 +1294,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/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index e70cdf7f9f84b12b778be4a0a1d7bbf12263a12f..807c37dc47425e70d4a927d59fd701b95ae19148 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -338,6 +338,57 @@ let merge_distinct_emitted x y = match x, y with
| False_if_reachable, True | True, False_if_reachable ->
raise Unmergeable
+type property_kind =
+ | Admitted (* Admitted property with a [Considered_valid] status. *)
+ | Unverifiable (* Postconditions and assigns of functions without code. *)
+ | Consequence of Property.identified_property list (* Logical consequence. *)
+ | Tautology (* Always valid. *)
+ | Ignored (* Property with no logical status. *)
+ | Verifiable
+
+let is_admitted_code_annot = function
+ | Cil_types.AAssert (_, tp)
+ | Cil_types.AInvariant (_, _, tp) -> tp.tp_kind = Admit
+ | _ -> false
+
+let rec is_admitted = function
+ | Property.IPAxiom _ -> true
+ | Property.IPPredicate ip -> ip.ip_pred.ip_content.tp_kind = Admit
+ | IPLemma lemma -> lemma.il_pred.tp_kind = Admit
+ | IPCodeAnnot ca -> is_admitted_code_annot ca.ica_ca.annot_content
+ | IPPropertyInstance instance -> is_admitted instance.ii_ip
+ | _ -> false
+
+let is_verifiable = function
+ | Property.IPPredicate {ip_kind = PKEnsures _ | PKTerminates; ip_kf = kf }
+ | IPAssigns {ias_kf = kf}
+ | IPFrom {if_kf = kf}
+ | IPAllocation {ial_kf = kf} -> Kernel_function.has_definition kf
+ | _ -> true
+
+let property_kind = function
+ | Property.IPAxiomatic {iax_props} -> Consequence iax_props
+ | IPBehavior {ib_kf; ib_kinstr; ib_active; ib_bhv} ->
+ (* logical consequence of its postconditions *)
+ let active = Datatype.String.Set.elements ib_active in
+ let post = Property.ip_post_cond_of_behavior ib_kf ib_kinstr active ib_bhv in
+ Consequence post
+ | IPReachable {ir_kf; ir_kinstr; ir_program_point} ->
+ begin
+ match ir_kf, ir_kinstr, ir_program_point with
+ | None, Kglobal, Before -> Tautology
+ | None, Kglobal, After -> assert false
+ | None, Kstmt _, _ ->
+ Kernel.fatal "reachability of a stmt without function"
+ | Some kf, Kglobal, Before when Kernel_function.is_main kf -> Tautology
+ | _ -> Verifiable
+ end
+ | p ->
+ if Property.has_status p then
+ if is_admitted p then Admitted else
+ if is_verifiable p then Verifiable else Unverifiable
+ else Ignored
+
module Register_hook = Hook.Build (struct type t = Property.t end)
let register_property_add_hook = Register_hook.extend
@@ -356,71 +407,11 @@ let rec register ppt =
Register_hook.apply ppt;
register_as_kernel_logical_consequence ppt
-(* the functions below and this one MUST be synchronized *)
and register_as_kernel_logical_consequence ppt =
- let open Property in match ppt with
- | IPAxiom _
- | IPPredicate {ip_kind = PKAssumes _} ->
- (* always valid, but must be verifiable by the end-user,
- see [is_not_verifiable_but_valid] *)
- ()
- | IPAxiomatic {iax_props} -> logical_consequence Emitter.kernel ppt iax_props
- | IPBehavior {ib_kf; ib_kinstr; ib_active; ib_bhv} ->
- let active = Datatype.String.Set.elements ib_active in
- (* logical consequence of its postconditions *)
- logical_consequence
- Emitter.kernel ppt (ip_post_cond_of_behavior ib_kf ib_kinstr active ib_bhv)
- | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kglobal;
- ir_program_point = Before} ->
- (* valid: global properties are always reachable *)
- emit_valid ppt
- | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kglobal;
- ir_program_point = After} ->
- assert false
- | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kstmt _} ->
- Kernel.fatal "reachability of a stmt without function"
- | IPReachable {ir_kf = Some kf; ir_kinstr = Cil_types.Kglobal;
- ir_program_point = Before} ->
- let f = kf.Cil_types.fundec in
- if Ast_info.Function.get_name f = Kernel.MainFunction.get_plain_string ()
- (* main is always reachable *)
- then emit_valid ppt
- | IPOther _ | IPReachable _
- | IPExtended _
- | IPPredicate _ | IPCodeAnnot _ | IPComplete _
- | IPDisjoint _ | IPAssigns _ | IPFrom _
- | IPAllocation _ | IPDecrease _ | IPLemma _
- | IPPropertyInstance _
- | IPTypeInvariant _ | IPGlobalInvariant _ ->
- ()
-
-(* the functions above and below MUST be synchronized *)
-and is_kernel_logical_consequence ppt =
- let open Property in match ppt with
- | IPPredicate {ip_kind = PKAssumes _}
- | IPBehavior _
- | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kglobal;
- ir_program_point = Before} ->
- true
- | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kglobal;
- ir_program_point = After} ->
- assert false
- | IPReachable {ir_kf = None; ir_kinstr = Cil_types.Kstmt _} ->
- Kernel.fatal "reachability of a stmt without function"
- | IPReachable {ir_kf = Some kf; ir_kinstr = Cil_types.Kglobal;
- ir_program_point = Before} ->
- let f = kf.Cil_types.fundec in (* main is always reachable *)
- Ast_info.Function.get_name f = Kernel.MainFunction.get_plain_string ()
- | IPAxiom _
- | IPExtended _
- | IPAxiomatic _
- | IPOther _ | IPReachable _
- | IPPredicate _ | IPCodeAnnot _ | IPComplete _
- | IPDisjoint _ | IPAssigns _ | IPFrom _
- | IPAllocation _ | IPDecrease _ | IPLemma _
- | IPPropertyInstance _
- | IPTypeInvariant _ | IPGlobalInvariant _ ->
- false
+ match property_kind ppt with
+ | Consequence ips -> logical_consequence Emitter.kernel ppt ips
+ | Tautology -> emit_valid ppt
+ | Admitted | Unverifiable | Ignored | Verifiable -> ()
and unsafe_emit_and_get e ~hyps ~auto ppt ?(distinct=false) s =
Kernel.feedback ~dkey:Kernel.dkey_prop_status_emit
@@ -492,7 +483,7 @@ and unsafe_emit_and_get e ~hyps ~auto ppt ?(distinct=false) s =
(match hyps with
| [] ->
let reach_ppt = Property.ip_reachable_ppt ppt in
- if is_kernel_logical_consequence reach_ppt then emit_valid reach_ppt;
+ if property_kind reach_ppt = Tautology then emit_valid reach_ppt;
add { emitter with properties = [ reach_ppt ] } s
| _ :: _ -> Kernel.fatal "Emitter %a proves invalidity of %a under \
hypotheses: unsound!" Emitter.pretty e Property.pretty ppt));
@@ -542,22 +533,13 @@ let () =
register_as_kernel_logical_consequence
let emit_and_get e ~hyps ppt ?distinct s =
- let open Property in begin match ppt with
- | IPBehavior _ | IPAxiom _ | IPAxiomatic _
- | IPPredicate {ip_kind = PKAssumes _} ->
- Kernel.fatal
- "only the kernel should set the status of property %a"
- pretty
- ppt
- | IPPredicate _ | IPCodeAnnot _ | IPComplete _
- | IPDisjoint _ | IPAssigns _ | IPFrom _
- | IPDecrease _ | IPLemma _ | IPReachable _
- | IPAllocation _ | IPOther _
- | IPPropertyInstance _
- | IPExtended _
- | IPTypeInvariant _ | IPGlobalInvariant _ -> ()
- end;
- unsafe_emit_and_get e ~hyps ~auto:false ppt ?distinct s
+ match property_kind ppt with
+ | Admitted | Consequence _ | Ignored ->
+ Kernel.fatal
+ "Only the kernel should set the status of property %a (%a, %a)"
+ Property.pretty ppt Emitter.pretty e Emitted_status.pretty s
+ | Verifiable | Tautology | Unverifiable ->
+ unsafe_emit_and_get e ~hyps ~auto:false ppt ?distinct s
let emit e ~hyps ppt ?distinct s = ignore (emit_and_get e ~hyps ppt ?distinct s)
@@ -644,32 +626,11 @@ let conjunction s1 s2 = match s1, s2 with
| Dont_know, _ | _, Dont_know -> Dont_know
| True, True -> True
-let is_not_verifiable_but_valid ppt status = match status with
- | Never_tried ->
- (match ppt with
- | Property.IPOther _ ->
- (* Non-ACSL properties are not verifiable *)
- false
- | Property.IPReachable _ -> false
- | Property.IPAxiom _ | Property.IPAxiomatic _ -> true
- | _ ->
- match Property.get_kf ppt with
- | None -> false
- | Some kf ->
- (* cannot use module [Kernel_function] nor [Globals] here *)
- let f = kf.Cil_types.fundec in
- if Ast_info.Function.is_definition f then
- false
- else
- (* postconditions of functions without code are not verifiable *)
- let open Property in match ppt with
- | IPPredicate {ip_kind = PKEnsures _ | PKTerminates}
- | IPAssigns _ | IPAllocation _
- | IPFrom _ -> true
- | _ -> false)
- | Best((True | False_if_reachable | False_and_reachable | Dont_know), _)
- | Inconsistent _ ->
- false
+let is_not_verifiable_but_valid ppt status =
+ match property_kind ppt with
+ | Admitted -> true
+ | Unverifiable -> status = Never_tried
+ | Verifiable | Consequence _ | Tautology | Ignored -> false
let rec compute_automatic_status _e properties =
let local_get p =
@@ -717,12 +678,8 @@ and get_status ?(must_register=true) ppt =
match ppt with
| Property.IPOther _ | Property.IPReachable _
| Property.IPPropertyInstance _ ->
- if must_register then begin
- register ppt;
- if is_kernel_logical_consequence ppt then get_status ppt
- else Never_tried
- end else
- Never_tried
+ if must_register then register ppt;
+ Never_tried
| Property.IPBehavior _
| Property.IPExtended _
| Property.IPPredicate _ | Property.IPCodeAnnot _ | Property.IPComplete _
@@ -737,26 +694,10 @@ and get_status ?(must_register=true) ppt =
(* local alias: too much local definitions of get implies name clashes *)
let get ppt = get_status ppt
-let automatically_proven ppt =
- is_kernel_logical_consequence ppt
- &&
- (* nobody else tried to prove it *)
- try
- let by_emitter = Status.find ppt in
- try
- Emitter_with_properties.Hashtbl.iter
- (fun e _ ->
- if not (Emitter.equal
- (Emitter.Usable_emitter.get e.emitter)
- Emitter.kernel)
- then raise Exit)
- by_emitter;
- true
- with Exit ->
- false
- with Not_found ->
- true
-
+let automatically_computed ppt =
+ match property_kind ppt with
+ | Admitted | Unverifiable | Ignored | Consequence _ | Tautology -> true
+ | Verifiable -> false
(**************************************************************************)
(** {3 Consolidated property status} *)
diff --git a/src/kernel_services/ast_data/property_status.mli b/src/kernel_services/ast_data/property_status.mli
index 3cf7daca5c6deb96e7e0df987ad8962e1e0e212f..5656c38152bc9d7009c892748ecdf561bed82fcf 100644
--- a/src/kernel_services/ast_data/property_status.mli
+++ b/src/kernel_services/ast_data/property_status.mli
@@ -261,8 +261,8 @@ val merge: old:Property.t list -> Property.t list -> unit
(** [merge old new] registers properties in [new] which are not in [old] and
removes properties in [old] which are not in [new]. *)
-val automatically_proven: Property.t -> bool
-(** Is the status of the given property only automatically handled by the
+val automatically_computed: Property.t -> bool
+(** Is the status of the given property only automatically handled by the
kernel? *)
(*
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/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index 90397e1a57896a91e8579098704d7e752adb3e8f..3a0b67f0857f54158c41ba96b0974678e1683240 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -108,24 +108,33 @@ let term_lvals_of_term t =
let behavior_assumes b =
Logic_const.pands (List.map Logic_const.pred_of_id_pred b.b_assumes)
-let behavior_postcondition b k =
+let take_ip ~goal (ip : identified_predicate) =
+ let { tp_kind ; tp_statement } = ip.ip_content in
+ let take_it =
+ if goal
+ then Logic_utils.verify_predicate tp_kind
+ else Logic_utils.use_predicate tp_kind in
+ if take_it then tp_statement else Logic_const.ptrue
+
+let behavior_postcondition ~goal b k =
let assumes = Logic_const.pold (behavior_assumes b) in
let postcondition =
Logic_const.pands
- (Extlib.filter_map (fun (x,_) -> x = k)
- (Extlib.($) Logic_const.pred_of_id_pred snd) b.b_post_cond)
- in
- Logic_const.pimplies (assumes,postcondition)
+ (List.map
+ (fun (tk,ip) ->
+ if tk = k then take_ip ~goal ip else Logic_const.ptrue)
+ b.b_post_cond)
+ in Logic_const.pimplies (assumes,postcondition)
-let behavior_precondition ?check b =
+let behavior_precondition ~goal b =
let assumes = behavior_assumes b in
- let requires = Logic_const.pands
- (List.rev_map (Logic_const.pred_of_id_pred ?check) b.b_requires)
- in
- Logic_const.pimplies (assumes,requires)
+ let requires =
+ Logic_const.pands
+ (List.map (take_ip ~goal) b.b_requires)
+ in Logic_const.pimplies (assumes,requires)
-let precondition ?check spec =
- Logic_const.pands (List.map (behavior_precondition ?check) spec.spec_behavior)
+let precondition ~goal spec =
+ Logic_const.pands (List.map (behavior_precondition ~goal) spec.spec_behavior)
(** find the behavior named [name] in the list *)
let get_named_bhv bhv_list name =
diff --git a/src/kernel_services/ast_queries/ast_info.mli b/src/kernel_services/ast_queries/ast_info.mli
index cce23bff9a1c2a30d5eff5494593f4fc154bc85c..1adcb7480a59fa6b5c0efd6bab272097749773fa 100644
--- a/src/kernel_services/ast_queries/ast_info.mli
+++ b/src/kernel_services/ast_queries/ast_info.mli
@@ -65,22 +65,25 @@ val term_lvals_of_term: term -> term_lval list
(** @return the list of all the term lvals of a given term.
Purely syntactic function. *)
-val precondition : ?check:bool -> funspec -> predicate
+val precondition : goal:bool -> funspec -> predicate
(** Builds the precondition from [b_assumes] and [b_requires] clauses.
- If [~check:false] is specified, check-only requires are skipped.
+ With [~goal:true], only returns assert and check predicates.
+ With [~goal:false], only returns assert and admit predicates.
@since Carbon-20101201 *)
val behavior_assumes : funbehavior -> predicate
(** Builds the conjunction of the [b_assumes].
@since Nitrogen-20111001 *)
-val behavior_precondition : ?check:bool -> funbehavior -> predicate
+val behavior_precondition : goal:bool -> funbehavior -> predicate
(** Builds the precondition from [b_assumes] and [b_requires] clauses.
- If [~check:false] is specified, check-only requires are skipped.
+ For flag [~goal] see [precondition] above.
@since Carbon-20101201 *)
-val behavior_postcondition : funbehavior -> termination_kind -> predicate
+val behavior_postcondition :
+ goal:bool -> funbehavior -> termination_kind -> predicate
(** Builds the postcondition from [b_assumes] and [b_post_cond] clauses.
+ For flag [~goal] see [precondition] above.
@modify Boron-20100401 added termination kind as filtering argument. *)
val disjoint_behaviors : funspec -> string list -> predicate
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 36830964006757eb5019e2af468559fa88fcabd4..63f9e6486708d5aaddc2e997842e15127e610a8c 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -43,14 +43,16 @@ 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
+let pred_of_id_pred p = p.ip_content.tp_statement
+
let refresh_predicate p = { p with ip_id = PredicateId.next () }
let new_identified_term t =
@@ -340,10 +342,6 @@ let unamed ?(loc=Cil_datatype.Location.unknown) p =
let ptrue = unamed Ptrue
let pfalse = unamed Pfalse
-let pred_of_id_pred ?(check=true) p =
- let tp = p.ip_content in
- if tp.tp_only_check && not check then ptrue else tp.tp_statement
-
let pold ?(loc=Cil_datatype.Location.unknown) p = match p.pred_content with
| Ptrue | Pfalse -> p
| _ -> {p with pred_content = Pat(p, old_label); pred_loc = loc}
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index fadbb859a3705fabe6d8959d2ea3726d8ee6d69e..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
@@ -75,10 +78,8 @@ val refresh_predicate: identified_predicate -> identified_predicate
(** @return a fresh id for predicates *)
val fresh_predicate_id: unit -> int
-(** extract a named predicate for an identified predicate.
- When [~check:false] is specified, check-only predicate
- returns a [ptrue] condition. *)
-val pred_of_id_pred: ?check:bool -> identified_predicate -> predicate
+(** extract a named predicate for an identified predicate. *)
+val pred_of_id_pred: identified_predicate -> predicate
(** creates a new identified term with a fresh id*)
val new_identified_term: term -> identified_term
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..e6b2f808798a2dcc4640e9495d8c2f4afce22e7b 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 =
@@ -2229,11 +2229,17 @@ let lhost_c_type thost =
| _ -> assert false)
| TResult ty -> ty
+let use_predicate = function Assert | Admit -> true | Check -> false
+let verify_predicate = function Assert | Check -> true | Admit -> false
+
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..1e0ddf5ad4106ae99271c9e65edbeb9270fa57fb 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -444,12 +444,22 @@ val merge_funspec :
val clear_funspec: funspec -> unit
(** {2 Discriminating code_annotations} *)
+
+(** Checks if a predicate kind can be used as an hypothesis or requirement.
+ It is true for `Admit` and `Assert`, and false for `Check`. *)
+val use_predicate : predicate_kind -> bool
+
+(** Checks if a predicate kind shall be put under verification.
+ It is true for `Assert` and `Check`, and false for `Admit`. *)
+val verify_predicate : predicate_kind -> bool
+
(** Functions below allows to test a special kind of code_annotation.
Use them in conjunction with {!Annotations.get_filter} to retrieve
a particular kind of annotations associated to a statement. *)
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..2293ed64aefdfa541a1b00c069a631ebb15bac70 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -220,8 +220,8 @@ let ip_from_precondition kf call_ki b pre =
let process_inactive_behavior kf call_ki behavior =
let emitted = ref false in
(* We emit a valid status for every requires and ensures of the behavior. *)
- List.iter (fun (tk, _ as post) ->
- if tk = Normal then begin
+ List.iter (fun (tk, pred as post) ->
+ if tk = Normal && pred.ip_content.tp_kind <> Admit then begin
emitted := true;
if emit_postcond_status (post_kind kf) then
let ip = Property.ip_of_ensures kf Kglobal behavior post in
@@ -229,9 +229,11 @@ let process_inactive_behavior kf call_ki behavior =
end
) behavior.b_post_cond;
List.iter (fun pre ->
- emitted := true;
- let ip = ip_from_precondition kf call_ki behavior pre in
- emit_status ip Property_status.True;
+ if pre.ip_content.tp_kind <> Admit then begin
+ emitted := true;
+ let ip = ip_from_precondition kf call_ki behavior pre in
+ emit_status ip Property_status.True;
+ end
) behavior.b_requires;
if !emitted then
Value_parameters.result ~once:true ~current:true ~level:2
@@ -247,8 +249,8 @@ let process_inactive_postconds kf inactive_bhvs =
List.iter
(fun b ->
let emitted = ref false in
- List.iter (fun (tk, _ as post) ->
- if tk = Normal then begin
+ List.iter (fun (tk, pred as post) ->
+ if tk = Normal && pred.ip_content.tp_kind <> Admit then begin
emitted := true;
if emit_postcond_status (post_kind kf) then
let ip = Property.ip_of_ensures kf Kglobal b post in
@@ -387,7 +389,7 @@ module Make
let eval_split_and_reduce limit ~reduce pred build_env state =
let env = build_env state in
let status = Domain.evaluate_predicate env state pred in
- let reduced_states =
+ let reduced_states =
if reduce then
match status with
| Alarmset.False -> States.empty
@@ -453,12 +455,13 @@ 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 record = pred.ip_content.tp_kind <> Admit in
+ let reduce = active && pred.ip_content.tp_kind <> Check in
let ip = build_prop pred in
if ignore_predicate pr then
states
else if States.is_empty states then begin
- emit ~empty:true ip pr Alarmset.True;
+ if record then emit ~empty:true ip pr Alarmset.True;
states
end
else
@@ -472,8 +475,12 @@ module Make
fst (States.merge ~into:acc_states reduced_states)))
states ([], States.empty)
in
- List.iter (fun status -> emit ~empty:false ip pr status) statuses;
- check_ensures_false kf behavior active pr kind statuses;
+ if record
+ then
+ begin
+ List.iter (fun status -> emit ~empty:false ip pr status) statuses;
+ check_ensures_false kf behavior active pr kind statuses;
+ end;
States.reorder reduced_states
in
List.fold_left aux_pred states ips
@@ -581,8 +588,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 _ ->
@@ -595,13 +603,14 @@ module Make
| Some loc when not (Cil_datatype.Location.(equal loc unknown)) -> loc
| _ -> Cil_datatype.Stmt.loc stmt
+
(* Reduce the given states according to the given code annotations.
If [record] is true, update the proof state of the code annotation.
DO NOT PASS record=false unless you know what your are doing *)
let interp_annot ~limit ~record kf ab stmt code_annot ~initial_state states =
let ips = Property.ip_of_code_annot kf stmt code_annot in
let source, _ = code_annotation_loc code_annot stmt in
- let aux_interp ~reduce code_annot behav p =
+ let aux_interp ~record ~reduce code_annot behav p =
let text = code_annotation_text code_annot in
let in_behavior =
match behav with
@@ -672,7 +681,7 @@ module Make
'nice' ordering *)
if reduce then States.reorder reduced_states else states
in
- let aux code_annot ~reduce behav p =
+ let aux code_annot ~record ~reduce behav p =
if ignore_predicate p then
states
else if States.is_empty states then (
@@ -685,12 +694,14 @@ module Make
end;
states
) else
- aux_interp ~reduce code_annot behav p
+ aux_interp ~record ~reduce code_annot behav p
in
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
+ let record = record && p.tp_kind <> Admit in
+ let reduce = p.tp_kind <> Check in
+ aux ~record ~reduce 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..f9c730b433d7558be89d8ba2b6c066f545400d2e 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 _ ->
@@ -46,7 +47,7 @@ let code_annotation_loc ca stmt =
let mark_unreachable () =
let mark ppt =
- if not (Property_status.automatically_proven ppt) then begin
+ if not (Property_status.automatically_computed ppt) then begin
Value_parameters.debug "Marking property %a as dead"
Description.pp_property ppt;
let emit =
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/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index da498f0142c91d6812508bad8657dfc1ff5e1975..3b0b61f20b7641035b4c7081295ff314f0548922 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -135,15 +135,10 @@ let get_behavior kf ki has_exit ~active bhv =
let get_assumes kf bhv =
normalize_assumes kf Kglobal (Ast_info.behavior_assumes bhv)
-let get_preconditions kf =
- (*TODO use this code instead! *)
- (*
- let assumes = get_assumes kf bhv in
- List.map (normalize_pre kf Kglobal ~assumes bhv) bhv.b_requires
- *)
+let get_preconditions ~goal kf =
List.map
(fun bhv ->
- let p = Ast_info.behavior_precondition ~check:false bhv in
+ let p = Ast_info.behavior_precondition ~goal bhv in
normalize_pre kf Kglobal bhv (Logic_const.new_predicate p)
) (Annotations.behaviors kf)
@@ -278,12 +273,13 @@ module CodeAssertions = WpContext.StaticGenerator(CodeKey)
| AAssert(_,a) ->
let p =
WpPropId.mk_assert_id kf stmt ca ,
- normalize_pred a.tp_statement
- in if a.tp_only_check then {
- l with code_verified = p :: l.code_verified ;
- } else {
- code_admitted = p :: l.code_admitted ;
- code_verified = p :: l.code_verified ;
+ normalize_pred a.tp_statement in
+ let admit = Logic_utils.use_predicate a.tp_kind in
+ let verif = Logic_utils.verify_predicate a.tp_kind in
+ let use flag p ps = if flag then p::ps else ps in
+ {
+ code_admitted = use admit p l.code_admitted ;
+ code_verified = use verif p l.code_verified ;
}
| _ -> l
end stmt {
@@ -339,17 +335,16 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
match ca.annot_content with
| AInvariant(_,true,inv) ->
let p = normalize_pred inv.tp_statement in
+ let g_hyp = WpPropId.mk_inv_hyp_id kf stmt ca in
let g_est, g_ind = WpPropId.mk_loop_inv kf stmt ca in
- if inv.tp_only_check then
- { l with
- loop_established = (g_est,p) :: l.loop_established ;
- loop_preserved = (g_ind,p) :: l.loop_preserved }
- else
- let g_hyp = WpPropId.mk_inv_hyp_id kf stmt ca in
- { l with
- loop_established = (g_est,p) :: l.loop_established ;
- loop_invariants = (g_hyp,p) :: l.loop_invariants ;
- loop_preserved = (g_ind,p) :: l.loop_preserved }
+ let admit = Logic_utils.use_predicate inv.tp_kind in
+ let verif = Logic_utils.verify_predicate inv.tp_kind in
+ let use flag id p ps = if flag then (id,p) :: ps else ps in
+ { l with
+ loop_established = use verif g_est p l.loop_established ;
+ loop_invariants = use admit g_hyp p l.loop_invariants ;
+ loop_preserved = use verif g_ind p l.loop_preserved ;
+ }
| AVariant(term, None) ->
let vpos , vdec =
WpStrategy.mk_variant_properties kf stmt ca term in
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 9f27aab9ad44e9f9d29a587d92f9fed833d9d500..a3330628d2f4e53e14191d88e67d7c236fe874c6 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -46,7 +46,7 @@ val get_behavior :
kernel_function -> kinstr -> bool -> active:string list -> funbehavior ->
behavior
-val get_preconditions : kernel_function -> pred_info list
+val get_preconditions : goal:bool ->kernel_function -> pred_info list
val get_complete_behaviors : kernel_function -> pred_info list
val get_disjoint_behaviors : kernel_function -> pred_info list
diff --git a/src/plugins/wp/cfgCalculus.ml b/src/plugins/wp/cfgCalculus.ml
index 46a448a6586fccc2ce3adcf1054e7635af37d7b6..1c36f418463526bfc9a009da0a7ef04d88a6fc6d 100644
--- a/src/plugins/wp/cfgCalculus.ml
+++ b/src/plugins/wp/cfgCalculus.ml
@@ -337,7 +337,7 @@ struct
let behaviors kf =
if WpStrategy.is_main_init kf || WpLog.PrecondWeakening.get () then []
- else CfgAnnot.get_preconditions kf
+ else CfgAnnot.get_preconditions ~goal:false kf
let complete mode kf =
if not (is_default_bhv mode) then []
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 752f4b46d09ca40ec3123b7c3cb30c3dc7f3fc7a..db7a24fa9c2e464c38476a6b5021ee560798263b 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -28,6 +28,7 @@ let debug fmt = Wp_parameters.debug ~dkey fmt
open Cil_types
open Cil_datatype
+open Logic_utils
(* -------------------------------------------------------------------------- *)
(* --- Status of Unreachable Annotations --- *)
@@ -646,7 +647,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 && use_predicate p.ip_content.tp_kind
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
@@ -723,7 +724,8 @@ 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 hyp = use_predicate inv.tp_kind in
+ let goal = verify_predicate inv.tp_kind 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
@@ -734,22 +736,29 @@ let add_loop_invariant_annot config vloop s ca b_list inv acc =
| TBRpart (* TODO: PKPartial *)
->
begin
- let loop_entry = add_prop_loop_inv ~established:true config loop_entry
- WpStrategy.Agoal s ca inv in
- let loop_back = add_prop_loop_inv ~established:false config loop_back
- WpStrategy.Agoal s ca inv in
+ let loop_entry =
+ if goal then
+ add_prop_loop_inv ~established:true config loop_entry
+ WpStrategy.Agoal s ca inv
+ else loop_entry in
+ let loop_back =
+ if goal then
+ add_prop_loop_inv ~established:false config loop_back
+ WpStrategy.Agoal s ca inv
+ else loop_back in
let loop_core =
- if only_check then loop_core
- else
+ if hyp then
add_prop_inv_fixpoint config loop_core WpStrategy.Ahyp s ca inv
- in
+ else loop_core in
assigns, loop_entry , loop_back , loop_core
end
- | TBRhyp when not only_check ->
- let kind = WpStrategy.Ahyp in
- let loop_core = add_prop_inv_fixpoint config loop_core kind s ca inv
- in assigns, loop_entry , loop_back , loop_core
- | TBRhyp | TBRno -> acc
+ | TBRhyp ->
+ if hyp then
+ let kind = WpStrategy.Ahyp in
+ let loop_core = add_prop_inv_fixpoint config loop_core kind s ca inv
+ in assigns, loop_entry , loop_back , loop_core
+ else acc
+ | TBRno -> acc
(** Returns the annotations for the three edges of the loop node:
* - loop_entry : goals for the edge entering in the loop
@@ -837,24 +846,25 @@ 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
- else
+ if use_predicate p.tp_kind then
let b_acc =
WpStrategy.add_prop_assert
b_acc WpStrategy.Ahyp kf s a p.tp_statement
in (b_acc, (a_acc, e_acc))
+ else acc
| 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
- else
- let kind =
- WpStrategy.(if p.tp_only_check then Agoal else Aboth goal)
- in
+ let add, kind =
+ match p.tp_kind with
+ | Admit -> true, WpStrategy.Ahyp
+ | Assert -> true, Aboth goal
+ | Check -> goal, Agoal
+ in if add then
let b_acc =
WpStrategy.add_prop_assert b_acc kind kf s a p.tp_statement
- in
- (b_acc, (a_acc, e_acc))
+ in (b_acc, (a_acc, e_acc))
+ else acc
in acc
| AAllocation (_b_list, _frees_allocates) ->
(* [PB] TODO *) acc
@@ -1021,7 +1031,7 @@ let add_global_annotations annots =
linfo.l_var_info.lv_name;
()
| Dlemma (name,_,_,_,p,_,_) ->
- if not (p.tp_only_check) then
+ if use_predicate p.tp_kind 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 ded4109cf1db5ad57c8b3ff36de0e35913feefe9..7e4772e1af310fe3b6a76ce337f732d438fd0278 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -478,7 +478,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..549725d8cf107ae9bb045665c282e5116864ba6d 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
+ Logic_utils.use_predicate p.tp_kind && 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 38aca8858461ece782e5e32f03949f5c1bc24131..420016431a7b9c76333f8c1e6c75186e81181ca6 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -24,6 +24,7 @@ let dkey = Wp_parameters.register_category "strategy" (* debugging key *)
let debug fmt = Wp_parameters.debug ~dkey fmt
open Cil_types
+open Logic_utils
open LogicUsage
(* -------------------------------------------------------------------------- *)
@@ -171,7 +172,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 -> use_predicate x.ip_content.tp_kind) 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,21 +184,23 @@ 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 use_predicate pre.ip_content.tp_kind then 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
let p = Logic_const.(pat (p,pre_label)) in
let p = normalize id ?assumes labels p in
add_prop acc kind id p
- end
+ end else acc
let add_prop_fct_post acc kind kf bhv tkind post =
- let id = WpPropId.mk_fct_post_id kf bhv (tkind, post) in
- let labels = NormAtLabels.labels_fct_post in
- let p = Logic_const.pred_of_id_pred post in
- let p = normalize id labels p in
- add_prop acc kind id p
+ if verify_predicate post.ip_content.tp_kind then begin
+ let id = WpPropId.mk_fct_post_id kf bhv (tkind, post) in
+ let labels = NormAtLabels.labels_fct_post in
+ let p = Logic_const.pred_of_id_pred post in
+ let p = normalize id labels p in
+ add_prop acc kind id p
+ end else acc
let add_prop_fct_bhv_pre acc kind kf bhv =
let assumes = None in
@@ -206,11 +209,13 @@ let add_prop_fct_bhv_pre acc kind kf bhv =
List.fold_left add acc bhv.b_assumes
let add_prop_stmt_pre acc kind kf s bhv ~assumes pre =
- let id = WpPropId.mk_pre_id kf (Kstmt s) bhv pre in
- let labels = NormAtLabels.labels_stmt_pre ~kf s in
- let p = Logic_const.pred_of_id_pred pre in
- let p = normalize id labels ?assumes p in
- add_prop acc kind id p
+ if use_predicate pre.ip_content.tp_kind then begin
+ let id = WpPropId.mk_pre_id kf (Kstmt s) bhv pre in
+ let labels = NormAtLabels.labels_stmt_pre ~kf s in
+ let p = Logic_const.pred_of_id_pred pre in
+ let p = normalize id labels ?assumes p in
+ add_prop acc kind id p
+ end else acc
let add_prop_stmt_bhv_requires acc kind kf s bhv ~with_assumes =
let assumes =
@@ -227,14 +232,16 @@ let add_prop_stmt_spec_pre acc kind kf s spec =
in List.fold_left add_bhv_pre acc spec.spec_behavior
let add_prop_stmt_post acc kind kf s bhv tkind l_post ~assumes post =
- let id = WpPropId.mk_stmt_post_id kf s bhv (tkind, post) in
- let labels = NormAtLabels.labels_stmt_post_l ~kf s l_post in
- let p = Logic_const.pred_of_id_pred post in
- let p = normalize id labels ?assumes p in
- add_prop acc kind id p
+ if verify_predicate post.ip_content.tp_kind then begin
+ let id = WpPropId.mk_stmt_post_id kf s bhv (tkind, post) in
+ let labels = NormAtLabels.labels_stmt_post_l ~kf s l_post in
+ let p = Logic_const.pred_of_id_pred post in
+ let p = normalize id labels ?assumes p in
+ add_prop acc kind id p
+ end else acc
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");