diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index c02a126964259ed12cdceb977060569ca62eaed4..f06f0573b63623fbf2a2dae4f4e6b77ccbcc6170 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -94,6 +94,7 @@
"breaks", BREAKS, false;
"case", CASE, true;
"char", CHAR, true;
+ "check", CHECK, false;
"complete", COMPLETE, false;
"const", CONST, true;
"continues", CONTINUES, false;
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index 489cf83599cba3d1c347d9b5f45f835d5c7d29a2..4f81bcc7f2476868e7de78547d402440840a907e 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -247,7 +247,7 @@
%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 SEMICOLON NULL EMPTY
+%token GLOBAL INVARIANT VARIANT DECREASES FOR LABEL ASSERT CHECK SEMICOLON NULL EMPTY
%token REQUIRES ENSURES ALLOCATES FREES ASSIGNS LOOP NOTHING SLICE IMPACT PRAGMA FROM
%token <string> EXT_CODE_ANNOT EXT_GLOBAL EXT_CONTRACT
%token EXITS BREAKS CONTINUES RETURNS
@@ -1430,6 +1430,7 @@ beg_pragma_or_code_annotation:
| SLICE {}
| FOR {}
| ASSERT {}
+| CHECK {}
| INVARIANT {}
| EXT_CODE_ANNOT {}
;
@@ -1442,7 +1443,9 @@ pragma_or_code_annotation:
code_annotation:
| ASSERT full_lexpr SEMICOLON
- { fun bhvs -> AAssert (bhvs,$2) }
+ { fun bhvs -> AAssert (bhvs,Assert,$2) }
+| CHECK full_lexpr SEMICOLON
+ { fun bhvs -> AAssert (bhvs,Check,$2) }
| INVARIANT full_lexpr SEMICOLON { fun bhvs -> AInvariant (bhvs,false,$2) }
| EXT_CODE_ANNOT grammar_extension SEMICOLON
{ fun bhvs ->
@@ -1837,6 +1840,7 @@ is_acsl_decl_or_code_annot:
| EXT_GLOBAL { $1 }
| ASSUMES { "assumes" }
| ASSERT { "assert" }
+| CHECK { "check" }
| GLOBAL { "global" }
| IMPACT { "impact" }
| INDUCTIVE { "inductive" }
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index eb3177307c5d71e8f9037b17f89cb6f1e121fded..320b570ab51b9afb1bfb86ab3e5f2376b03830db 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -8605,7 +8605,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
let alloca_bounds = Logic_const.pand ~loc:castloc (pos_size, max_size) in
let alloca_bounds = { alloca_bounds with pred_name = ["alloca_bounds"] } in
let annot =
- Logic_const.new_code_annotation (AAssert ([], alloca_bounds))
+ Logic_const.new_code_annotation (AAssert ([], Assert, alloca_bounds))
in
(mkStmtOneInstr ~ghost ~valid_sid
(Code_annot (annot, castloc)),
@@ -9125,7 +9125,7 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
let pfalse = { pfalse with pred_name = ["missing_return"] } in
let assert_false () =
let annot =
- Logic_const.new_code_annotation (AAssert ([], pfalse))
+ Logic_const.new_code_annotation (AAssert ([], Assert, pfalse))
in
Cil.mkStmt ~ghost ~valid_sid (Instr(Code_annot(annot,loc)))
in
diff --git a/src/kernel_internals/typing/cfg.ml b/src/kernel_internals/typing/cfg.ml
index f306e0798342e5a0978fa287bf881b43c9483dc7..2d52020ae408c3d0f22febebc4d5ce80263f006e 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -474,7 +474,9 @@ let xform_switch_block ?(keepSwitch=false) b =
xform_switch_stmt
rest break_dest cont_dest label_index 0
| p ->
- let a = Logic_const.new_code_annotation (AAssert ([],p)) in
+ let a =
+ Logic_const.new_code_annotation (AAssert ([], Assert, p))
+ in
let assertion = mkStmt (Instr(Code_annot(a,l))) in
popn popstack;
assertion:: s ::
@@ -495,7 +497,9 @@ let xform_switch_block ?(keepSwitch=false) b =
xform_switch_stmt
rest break_dest cont_dest label_index 0
| p ->
- let a = Logic_const.new_code_annotation (AAssert([],p)) in
+ let a =
+ Logic_const.new_code_annotation (AAssert ([], Assert, p))
+ in
let assertion = mkStmt (Instr(Code_annot(a,l))) in
popn popstack;
assertion :: s ::
diff --git a/src/kernel_internals/typing/oneret.ml b/src/kernel_internals/typing/oneret.ml
index 7f2887414b80ed3d7d6138c0c35bf896499cfdfc..ec872584b89aa0763597f5401a811b42d81b92ef 100644
--- a/src/kernel_internals/typing/oneret.ml
+++ b/src/kernel_internals/typing/oneret.ml
@@ -315,7 +315,7 @@ let oneret ?(callback: callback option) (f: fundec) : unit =
match !returns_assert with
| { pred_content = Ptrue } -> [s; sg]
| p ->
- let a = Logic_const.new_code_annotation (AAssert ([],p)) in
+ let a = Logic_const.new_code_annotation (AAssert ([],Assert,p)) in
let sta = mkStmt (Instr (Code_annot (a,loc))) in
if callback<>None then
( let gclause = sta , a in
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index 7038bbce318da3fdf1a9a6541b73a257930490db..fd73d9c1eb22c83d8d33bb3711085d7f4f39b6c6 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -206,7 +206,7 @@ let variant_predicate stmt v =
Logic_const.pand ~loc (pred1, pred2)
let supported_annotation annot = match annot.annot_content with
- | AAssert ([], _)
+ | AAssert ([], _, _)
| AInvariant ([], _, _)
| AVariant (_, None) -> true
| _ -> false (* TODO *)
@@ -216,7 +216,8 @@ 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 ([], pred) -> Assert, pred
+ | AAssert ([], Cil_types.Assert, pred) -> Assert, pred
+ | AAssert ([], Cil_types.Check, pred) -> Check, pred
| AInvariant ([], _, pred) -> Invariant, pred
| AVariant (v, None) -> Assert, variant_predicate stmt v
| _ -> assert false
diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index e8af8bc2a58e2fde1a50c2f14031a506b46a3388..0baf4c9f58fed39b8debfc5323de3da60e620159 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -947,7 +947,7 @@ to function contracts."
(* to preserve the effect of the statement *)
pragmas :=
{ !pragmas with stmt = Stmt.Set.add ki !pragmas.stmt}
- | AAssert (_behav,pred) ->
+ | AAssert (_behav,_,pred) ->
(* to preserve the interpretation of the assertion *)
get_zone_from_pred ki pred;
| AInvariant (_behav,true,pred) -> (* loop invariant *)
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index a33a5047ef460dc233a85e1afa1a0b4ffc6131f5..248d57078c094a74bcb2b58d5e0e205361a7d307 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -669,7 +669,7 @@ let to_annot_aux kinstr ?(loc=Kinstr.loc kinstr) alarm =
(* Kernel.debug "registering alarm %a" D.pretty alarm;*)
let add alarm =
let pred = create_predicate ~loc alarm in
- Logic_const.new_code_annotation (AAssert([], pred))
+ Logic_const.new_code_annotation (AAssert([], Assert, pred))
in
try
let by_emitter = State.find kinstr in
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index 8051b863e0d6e10256fff2665917d6a25abaa14f..684fcea7ce24a3b1e2749e43036b2b917b6df2d7 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -1072,8 +1072,8 @@ let add_code_annot emitter ?kf stmt ca =
let kf = find_englobing_kf ?kf stmt in
let convert a =
match a.annot_content with
- | AAssert(l, p) ->
- let a = { a with annot_content=AAssert(l,extend_name emitter p) } in
+ | AAssert(l, kind, p) ->
+ let a = { a with annot_content=AAssert(l,kind,extend_name emitter p) } in
a, Property.ip_of_code_annot kf stmt a
| AInvariant(l, b, p) ->
let a={a with annot_content=AInvariant(l,b,extend_name emitter p)} in
@@ -1270,7 +1270,11 @@ let add_code_annot emitter ?kf stmt ca =
Code_annots.add stmt tbl
let add_assert e ?kf stmt a =
- let a = Logic_const.new_code_annotation (AAssert ([],a)) in
+ let a = Logic_const.new_code_annotation (AAssert ([],Assert,a)) in
+ add_code_annot e ?kf stmt a
+
+let add_check e ?kf stmt a =
+ let a = Logic_const.new_code_annotation (AAssert ([],Check,a)) in
add_code_annot e ?kf stmt a
(** {3 Adding globals} *)
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index 3252d40e661210bc7754c71483567110d4a31abc..8e23a13514b40c60071a2b361d6628b460a3f7dc 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -281,6 +281,12 @@ val add_assert:
provided, the function runs faster.
@plugin development guide *)
+val add_check:
+ Emitter.t -> ?kf:kernel_function -> stmt -> predicate -> unit
+(** Add a checking 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 f0eb6d86d0a0ea8d55cd9ac567a80295ffca5f28..9ca6bee84604575fe2f429beada46f30681d215f 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1739,11 +1739,17 @@ and pragma =
| Slice_pragma of slice_pragma
| Impact_pragma of impact_pragma
+(** Kind of an assertion:
+ - an assert is both evaluated and used as hypothesis afterwards;
+ - a check is only evaluated, but is not used as an hypothesis: it does not
+ affect the analyses. *)
+and assertion_kind = Assert | Check
+
(** all annotations that can be found in the code.
This type shares the name of its constructors with
{!Logic_ptree.code_annot}. *)
and code_annotation_node =
- | AAssert of string list * predicate
+ | AAssert of string list * assertion_kind * predicate
(** assertion to be checked. The list of strings is the list of
behaviors to which this assertion applies. *)
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index ccba7c4f34b98bd4947c104ab47e58a8c5c390d9..2b35d02c825e07820bec0be9d2192080fe912288 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -628,7 +628,7 @@ let rec short_pretty fmt p = match p with
| IPDisjoint (kf,_,_,_) ->
Format.fprintf fmt "disjoint clause in function %a"
Kernel_function.pretty kf
- | IPCodeAnnot (_,_,{ annot_content = AAssert (_, { pred_name = name :: _ })}) ->
+ | IPCodeAnnot (_,_,{ annot_content = AAssert (_, _, { pred_name = name :: _ })}) ->
Format.pp_print_string fmt name
| IPCodeAnnot(_,_,{annot_content =
AInvariant (_,_, { pred_name = name :: _ })})->
@@ -845,7 +845,7 @@ struct
let pp_code_annot_names fmt ca =
match ca.annot_content with
- | AAssert(for_bhv,named_pred) | AInvariant(for_bhv,_,named_pred) ->
+ | AAssert(for_bhv,_,named_pred) | AInvariant(for_bhv,_,named_pred) ->
let pp_for_bhv fmt l =
match l with
| [] -> ()
@@ -907,7 +907,8 @@ struct
Format.asprintf "%sextended%a" (extended_loc_prefix le) pp_names [name]
| IPCodeAnnot (kf,_, ca) ->
let name = match ca.annot_content with
- | AAssert _ -> "assert"
+ | AAssert (_, Assert, _) -> "assert"
+ | AAssert (_, Check, _) -> "check"
| AInvariant (_,true,_) -> "loop_inv"
| AInvariant _ -> "inv"
| APragma _ -> "pragma"
@@ -1094,8 +1095,10 @@ struct
| IPCodeAnnot (kf,stmt, { annot_content = AExtended(_,_,(_,clause,_,_,_)) } )
-> [ K kf ; A clause ; S stmt ]
- | IPCodeAnnot (kf,_, { annot_content = AAssert(_,p) } ) ->
+ | IPCodeAnnot (kf,_, { annot_content = AAssert(_,Assert,p) } ) ->
[K kf ; A "assert" ; P p ]
+ | IPCodeAnnot (kf,_, { annot_content = AAssert(_,Check,p) } ) ->
+ [K kf ; A "check" ; P p ]
| IPCodeAnnot (kf,_, { annot_content = AInvariant(_,true,p) } ) ->
[K kf ; A "loop_invariant" ; P p ]
| IPCodeAnnot (kf,_, { annot_content = AInvariant(_,false,p) } ) ->
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index a5248ccff9865ba8282c2cdf631cb647ea4cb2e1..c395c874ff08e5d890f14ed23d6ca741f1209eab 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2893,11 +2893,16 @@ class cil_printer () = object (self)
(Pretty_utils.pp_list ~sep:",@ " pp_print_string) l
in
match ca.annot_content with
- | AAssert (behav,p) ->
+ | AAssert (behav,Assert,p) ->
fprintf fmt "@[%a%a@ %a;@]"
pp_for_behavs behav
self#pp_acsl_keyword "assert"
self#predicate p
+ | AAssert (behav,Check,p) ->
+ fprintf fmt "@[%a%a@ %a;@]"
+ pp_for_behavs behav
+ self#pp_acsl_keyword "check"
+ self#predicate p
| APragma (Slice_pragma sp) ->
fprintf fmt "@[%a@ %a;@]"
self#pp_acsl_keyword "slice pragma"
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 029bb8bf79afab4827fed87758d55056bba87b69..c1c21886248bc6562a74e93dc5072bb4388b09a6 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -922,9 +922,13 @@ and pp_pragma pp_term fmt = function
| Slice_pragma(term) -> Format.fprintf fmt "Slice_pragma(%a)" (pp_slice_pragma pp_term) term
| Impact_pragma(term) -> Format.fprintf fmt "Impact_pragma(%a)" (pp_impact_pragma pp_term) term
+and pp_assertion_kind fmt = function
+ | Assert -> Format.pp_print_string fmt "Assert"
+ | Check -> Format.pp_print_string fmt "Check"
+
and pp_code_annotation_node fmt = function
- | AAssert(string_list,predicate) ->
- Format.fprintf fmt "AAssert(%a,%a)" (pp_list pp_string) string_list pp_predicate predicate
+ | AAssert(string_list,kind,predicate) ->
+ Format.fprintf fmt "AAssert(%a,%a,%a)" (pp_list pp_string) string_list pp_assertion_kind kind pp_predicate predicate
| AStmtSpec(string_list,spec) ->
Format.fprintf fmt "AStmtSpec(%a,%a)" (pp_list pp_string) string_list pp_spec spec
| AInvariant(string_list,bool,predicate) ->
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index ade7c65cc86b8c94b7cacbb38c36a9cc19367c00..e314dca611ad44aa5f4d27d8db5e9e31311bed5c 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -112,7 +112,10 @@ let pp_named fmt nx =
let pp_code_annot fmt ca =
match ca.annot_content with
- | AAssert(bs,np) -> Format.fprintf fmt "assertion%a%a" pp_for bs pp_named np
+ | AAssert(bs,Assert,np) ->
+ Format.fprintf fmt "assertion%a%a" pp_for bs pp_named np
+ | AAssert(bs,Check,np) ->
+ Format.fprintf fmt "check%a%a" pp_for bs pp_named np
| AInvariant(bs,_,np) ->
Format.fprintf fmt "invariant%a%a" pp_for bs pp_named np
| AAssigns(bs,_) -> Format.fprintf fmt "assigns%a" pp_for bs
@@ -250,11 +253,16 @@ let rec pp_prop kfopt kiopt kloc fmt = function
pp_bhvs bs
(pp_opt kiopt (pp_kinstr kloc)) ki
(pp_opt kiopt pp_active) active
- | IPCodeAnnot(_,_,{annot_content=AAssert(bs,np)}) ->
+ | IPCodeAnnot(_,_,{annot_content=AAssert(bs,Assert,np)}) ->
Format.fprintf fmt "Assertion%a%a%a"
pp_for bs
pp_named np
(pp_kloc kloc) np.pred_loc
+ | IPCodeAnnot(_,_,{annot_content=AAssert(bs,Check,np)}) ->
+ Format.fprintf fmt "Check%a%a%a"
+ pp_for bs
+ pp_named np
+ (pp_kloc kloc) np.pred_loc
| IPCodeAnnot(_,_,{annot_content=AInvariant(bs,_,np)}) ->
Format.fprintf fmt "Invariant%a%a%a"
pp_for bs
@@ -348,13 +356,15 @@ let to_string pp elt =
Buffer.contents b
let code_annot_kind_and_node code_annot = match code_annot.annot_content with
- | AAssert (_, {pred_content; pred_name}) ->
+ | AAssert (_, kind, {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 "user assertion"
+ else match kind with
+ | Assert -> "user assertion"
+ | Check -> "user check"
in
Some (kind, to_string Printer.pp_predicate_node pred_content)
| AInvariant (_, _, {pred_content}) ->
@@ -456,11 +466,13 @@ let for_order k = function
| [] -> [I k]
| bs -> I (succ k) :: named_order bs
let annot_order = function
- | {annot_content=AAssert(bs,np)} ->
+ | {annot_content=AAssert(bs,Check,np)} ->
for_order 0 bs @ named_order np.pred_name
- | {annot_content=AInvariant(bs,_,np)} ->
+ | {annot_content=AAssert(bs,Assert,np)} ->
for_order 2 bs @ named_order np.pred_name
- | _ -> [I 4]
+ | {annot_content=AInvariant(bs,_,np)} ->
+ for_order 4 bs @ named_order np.pred_name
+ | _ -> [I 6]
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 1de61b503727954aa7997505551792d4c91ea0c1..e74712d1ab373e5c949cd15d9063412fb58d239e 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -466,6 +466,10 @@ let print_pragma fmt p =
| Slice_pragma p -> fprintf fmt "slice@ pragma@ %a;" print_slice_pragma p
| Impact_pragma p -> fprintf fmt "impact@ pragma@ %a;" print_impact_pragma p
+let print_assertion_kind fmt = function
+ | Assert -> pp_print_string fmt "assert"
+ | Check -> pp_print_string fmt "check"
+
let print_extension fmt (name, ext) =
fprintf fmt "%s %a" name (pp_list ~sep:",@ " print_lexpr) ext
@@ -474,8 +478,9 @@ let print_code_annot fmt ca =
(pp_list ~pre:"for@ " ~sep:",@ " ~suf:":@ " pp_print_string) fmt bhvs
in
match ca with
- AAssert(bhvs,e) ->
- fprintf fmt "%aassert@ %a;" print_behaviors bhvs print_lexpr e
+ AAssert(bhvs,kind,e) ->
+ fprintf fmt "%a%a@ %a;"
+ print_behaviors bhvs print_assertion_kind kind print_lexpr e
| AStmtSpec (bhvs,s) ->
fprintf fmt "%a%a"
print_behaviors bhvs
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 027a3758727e31a37b87840c49e4f65172cc7793..23e9a64223935754b638f38147a59a69cf90bf1c 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3113,9 +3113,9 @@ and childrenSpec vis s =
let vSpec s = visitCilFunspec vis s in
let change_content annot = { ca with annot_content = annot } in
match ca.annot_content with
- AAssert (behav,p) ->
+ AAssert (behav,kind,p) ->
let p' = vPred p in if p' != p then
- change_content (AAssert (behav,p'))
+ change_content (AAssert (behav,kind,p'))
else ca
| APragma (Impact_pragma t) ->
let t' = visitCilImpactPragma vis t in
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 17b141196aacedcb19746db9f02ac4d65c8a38aa..49792655353f2789c2cad7e88873e1f2ac7ea31c 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2178,7 +2178,7 @@ module Code_annotation = struct
end)
let loc ca = match ca.annot_content with
- | AAssert(_,{pred_loc=loc})
+ | AAssert(_,_,{pred_loc=loc})
| AInvariant(_,_,{pred_loc=loc})
| AVariant({term_loc=loc},_) -> Some loc
| AAssigns _ | AAllocation _ | APragma _ | AExtended _
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index 3b292cce6677521f1dceb355c4642eef80ab9781..af3f16c4a2766f9df561b3c5bf2ab20a4724e81a 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -648,7 +648,7 @@ class check ?(is_normalized=true) what : Visitor.frama_c_visitor =
names of statement contracts. *)
if is_normalized then begin
match ca.annot_content with
- | AAssert(bhvs,_) | AStmtSpec(bhvs,_) | AInvariant (bhvs,_,_)
+ | AAssert(bhvs,_,_) | AStmtSpec(bhvs,_) | AInvariant (bhvs,_,_)
| AAssigns(bhvs,_) | AAllocation(bhvs,_) | AExtended (bhvs,_,_) ->
List.iter
(fun b ->
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index a5a205947e2da1f126523a65eacaee1c753ddcef..49ffb79f66f68216a4917a8bae7187ca1341984e 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3774,18 +3774,24 @@ struct
append_loop_labels (append_here_label (append_pre_label (append_init_label
(Lenv.empty()))))
+ let assertion_kind =
+ function Assert -> Cil_types.Assert | Check -> Cil_types.Check
+
let code_annot loc current_behaviors current_return_type ca =
let source = fst loc in
let annot = match ca with
- | AAssert (behav,p) ->
+ | AAssert (behav,k,p) ->
check_behavior_names loc current_behaviors behav;
- Cil_types.AAssert (behav,predicate (code_annot_env()) p)
+ Cil_types.AAssert(behav,assertion_kind k,predicate (code_annot_env()) p)
| APragma (Impact_pragma sp) ->
- Cil_types.APragma (Cil_types.Impact_pragma (impact_pragma (code_annot_env()) sp))
+ Cil_types.APragma
+ (Cil_types.Impact_pragma (impact_pragma (code_annot_env()) sp))
| APragma (Slice_pragma sp) ->
- Cil_types.APragma (Cil_types.Slice_pragma (slice_pragma (code_annot_env()) sp))
+ Cil_types.APragma
+ (Cil_types.Slice_pragma (slice_pragma (code_annot_env()) sp))
| APragma (Loop_pragma lp) ->
- Cil_types.APragma (Cil_types.Loop_pragma (loop_pragma (code_annot_env()) lp))
+ Cil_types.APragma
+ (Cil_types.Loop_pragma (loop_pragma (code_annot_env()) lp))
| AStmtSpec (behav,s) ->
(* function behaviors and statement behaviors are not at the
same level. Do not mix them in a complete or disjoint clause
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 352824e171c1585f0746e879da519a37f82c871a..c99bcaee9a110f7dfb6d1c89390e686da30bebca 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -1021,8 +1021,8 @@ let is_same_extension (_,e1,_,s1,c1) (_,e2,_,s2,c2) =
let is_same_code_annotation (ca1:code_annotation) (ca2:code_annotation) =
match ca1.annot_content, ca2.annot_content with
- | AAssert(l1,p1), AAssert(l2,p2) ->
- is_same_list (=) l1 l2 && is_same_predicate p1 p2
+ | AAssert(l1,k1,p1), AAssert(l2,k2,p2) ->
+ is_same_list (=) l1 l2 && k1 = k2 && is_same_predicate p1 p2
| AStmtSpec (l1,s1), AStmtSpec (l2,s2) ->
is_same_list (=) l1 l2 && is_same_spec s1 s2
| AInvariant(l1,b1,p1), AInvariant(l2,b2,p2) ->
@@ -2057,7 +2057,11 @@ let lhost_c_type thost =
| _ -> assert false)
| TResult ty -> ty
-let is_assert ca = match ca.annot_content with AAssert _ -> true | _ -> false
+let is_assert ca =
+ match ca.annot_content with AAssert (_, Assert, _) -> true | _ -> false
+
+let is_check ca =
+ match ca.annot_content with AAssert (_, Check, _) -> true | _ -> false
let is_contract ca =
match ca.annot_content with AStmtSpec _ -> true | _ -> false
@@ -2101,7 +2105,7 @@ let is_loop_annot s =
let is_trivial_annotation a =
match a.annot_content with
- | AAssert (_,a) -> is_trivially_true a
+ | AAssert (_,_,a) -> is_trivially_true a
| APragma _ | AStmtSpec _ | AInvariant _ | AVariant _
| AAssigns _| AAllocation _ | AExtended _
-> false
diff --git a/src/kernel_services/ast_queries/logic_utils.mli b/src/kernel_services/ast_queries/logic_utils.mli
index c5c7be4b017ea70d3b412c0fb03c8b6bea7939be..20f930b2b2f32927c1a016cafbea995c1e121da7 100644
--- a/src/kernel_services/ast_queries/logic_utils.mli
+++ b/src/kernel_services/ast_queries/logic_utils.mli
@@ -380,6 +380,7 @@ val clear_funspec: funspec -> unit
a particular kind of annotations associated to a statement. *)
val is_assert : code_annotation -> bool
+val is_check : 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/ast_transformations/filter.ml b/src/kernel_services/ast_transformations/filter.ml
index 50fcb567f702d5a7393eca2815b87e50bd6a5797..53907e6dc53d71f21bd0f3866f0a5e6b5a6f39b6 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -447,7 +447,7 @@ end = struct
Printer.pp_code_annotation v;
ChangeTo
(Logic_const.new_code_annotation
- (AAssert ([],
+ (AAssert ([], Assert,
{ pred_name = []; pred_loc = Cil_datatype.Location.unknown;
pred_content = Ptrue})))
end
diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.mli
index 3b97808c2aa5ec0230cd69ae7945420ea918677a..3461d6bd82a062519fb369c7f4e040b65a13ca7c 100644
--- a/src/kernel_services/parsetree/logic_ptree.mli
+++ b/src/kernel_services/parsetree/logic_ptree.mli
@@ -334,11 +334,13 @@ and pragma =
| Slice_pragma of slice_pragma
| Impact_pragma of impact_pragma
+and assertion_kind = Assert | Check
+
(** all annotations that can be found in the code. This type shares the name of
its constructors with {!Cil_types.code_annotation_node}. *)
type code_annot =
- | AAssert of string list * lexpr
+ | AAssert of string list * assertion_kind * lexpr
(** assertion to be checked. The list of strings is the list of
behaviors to which this assertion applies. *)
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index a859ed50bd7e119fa26cbd6f9f7983e7400d82ef..8ada692acfdd87176caef70de3dad2c766e3f90f 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -112,6 +112,7 @@ module Refreshers: sig
val assigns: check
val from: check
val user_assertions: check
+ val user_checks: check
val rte: check
val invariant: check
val variant: check
@@ -239,6 +240,8 @@ struct
~hint:"Show functional dependencies in function assigns"
let user_assertions =
add ~name:"User assertions" ~hint:"Show user assertions" ()
+ let user_checks =
+ add ~name:"User checks" ~hint:"Show user checks" ()
(* 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"
@@ -360,6 +363,7 @@ struct
assigns.add hb;
from.add hb;
user_assertions.add hb;
+ user_checks.add hb;
rte.add hb;
invariant.add hb;
variant.add hb;
@@ -630,10 +634,15 @@ let make_panel (main_ui:main_window_extension_points) =
| Property.IPLemma _ -> lemmas.get ()
| Property.IPComplete _ -> complete_disjoint.get ()
| Property.IPDisjoint _ -> complete_disjoint.get ()
- | Property.IPCodeAnnot(_,_,({annot_content = AAssert _} as ca)) ->
- (match Alarms.find ca with
- | None -> user_assertions.get ()
- | Some a -> rte.get () && active_alarm a)
+ | Property.IPCodeAnnot(_,_,({annot_content = AAssert (_, kind, _)} as ca)) ->
+ begin
+ match Alarms.find ca with
+ | Some a -> rte.get () && active_alarm a
+ | None ->
+ match kind with
+ | Assert -> user_assertions.get ()
+ | Check -> user_checks.get ()
+ end
| Property.IPCodeAnnot(_,_,{annot_content = AInvariant _}) ->
invariant.get ()
| Property.IPCodeAnnot(_,_,{annot_content = APragma p}) ->
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index b64f3530965336676e0abe2f7855017ae6475bb3..007449cd839883d7bc0e23c04090445f2b2be633 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -488,7 +488,7 @@ 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) ->
+ | AAssert (_, Assert, p'), AAssert (_, _, p) ->
if Logic_utils.is_same_predicate_node p.pred_content p'.pred_content then
let acc, added = add_proven_annot (annot, stmt) (ca, stmt_ca) acc in
if added then
@@ -574,7 +574,7 @@ class check_annot_visitor = object(self)
Cil.get_original_stmt self#behavior (Extlib.the self#current_stmt)
in
begin match annot.annot_content with
- | AAssert (_, _) ->
+ | AAssert _ ->
R.debug ~level:2 "[check] annot %d at stmt %d in %a : %a@."
annot.annot_id stmt.sid Kernel_function.pretty kf
Printer.pp_code_annotation annot;
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index 58e5b96280fd67851df297755143e0bfd2c0bd0e..0dc0cb5b874c64a708b1ed41c11ed7241fa7cd63 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -216,7 +216,7 @@ let local_printer: Printer.extensible_printer =
method! code_annotation fmt ca =
temporaries <- Cil_datatype.Varinfo.Set.empty;
match ca.annot_content with
- | AAssert(_, p) ->
+ | AAssert (_, _, p) ->
(* ignore the ACSL name *)
Format.fprintf fmt "@[<v>@[assert@ %a;@]" self#predicate_node p.pred_content;
(* print temporary variables information *)
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index c9e1050abf3cda4b83c8429a7bdcb8145d129bd5..79b128e2dfacbad5e6c453171c1a75a3eb36bd1b 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -580,7 +580,8 @@ module Make
let code_annotation_text ca =
match ca.annot_content with
- | AAssert _ -> "assertion"
+ | AAssert (_, Assert, _) -> "assertion"
+ | AAssert (_, Check, _) -> "check"
| AInvariant _ -> "loop invariant"
| APragma _ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
| AExtended _ ->
@@ -599,7 +600,7 @@ module Make
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 code_annot behav p =
+ let aux_interp ~reduce code_annot behav p =
let text = code_annotation_text code_annot in
let in_behavior =
match behav with
@@ -628,7 +629,7 @@ module Make
"valid"
| Alarmset.False, `True ->
change_status Property_status.False_if_reachable;
- "invalid (stopping propagation)"
+ "invalid" ^ (if reduce then " (stopping propagation)" else "")
| Alarmset.False, `Unknown ->
change_status Property_status.False_if_reachable;
"invalid"
@@ -636,38 +637,41 @@ module Make
msg_status status ~once:true ~source
"%s%a got status %s." text Description.pp_named p message
in
+ let reduce_state here res accstateset =
+ match res, in_behavior with
+ | _, `Unknown ->
+ (* Cannot conclude because behavior might be inactive *)
+ States.add here accstateset
+
+ | Alarmset.False, `True -> (* Dead/invalid branch *)
+ accstateset
+
+ | (Alarmset.Unknown | Alarmset.True), `True ->
+ let env = here_env ~pre:initial_state ~here in
+ (* Reduce by p if it is a disjunction, or if it did not
+ evaluate to True *)
+ let reduce = res = Alarmset.Unknown in
+ let reduced_states =
+ split_disjunction_and_reduce ~reduce ~limit env here p
+ in
+ fst (States.merge reduced_states ~into:accstateset)
+ in
let reduced_states =
States.fold
(fun (here: Domain.t) accstateset ->
let env = here_env ~pre:initial_state ~here in
let res = Domain.evaluate_predicate env here p in
- (* if record [holds], emit statuses in the Kernel,
- and print a message *)
+ (* if [record] holds, emit kernel status and print a message *)
if record then emit res;
- match res, in_behavior with
- | _, `Unknown ->
- (* Cannot conclude because behavior might be inactive *)
- States.add here accstateset
-
- | Alarmset.False, `True -> (* Dead/invalid branch *)
- accstateset
-
- | (Alarmset.Unknown | Alarmset.True), `True ->
- let env = here_env ~pre:initial_state ~here in
- (* Reduce by p if it is a disjunction, or if it did not
- evaluate to True *)
- let reduce = res = Alarmset.Unknown in
- let reduced_states =
- split_disjunction_and_reduce ~reduce ~limit env here p
- in
- fst (States.merge reduced_states ~into:accstateset)
- ) states States.empty
+ (* if [reduce] holds, reduce the state. *)
+ if reduce then reduce_state here res accstateset else accstateset)
+ states States.empty
in
(* States resulting from disjunctions are reversed compared to the
'nice' ordering *)
- States.reorder reduced_states
+ if reduce then States.reorder reduced_states else states
in
- let aux code_annot behav p =
+ let aux code_annot ~reduce behav p =
if ignore_predicate p then
states
else if States.is_empty states then (
@@ -680,11 +684,12 @@ module Make
end;
states
) else
- aux_interp code_annot behav p
+ aux_interp ~reduce code_annot behav p
in
match code_annot.annot_content with
- | AAssert (behav,p)
- | AInvariant (behav, true, p) -> aux code_annot behav p
+ | AAssert (behav, Check, p) -> aux ~reduce:false code_annot behav p
+ | AAssert (behav, Assert, p)
+ | AInvariant (behav, true, p) -> aux ~reduce:true code_annot behav p
| APragma _
| AInvariant (_, false, _)
| AVariant _ | AAssigns _ | AAllocation _ | AExtended _
diff --git a/src/plugins/value/gui_files/gui_red.ml b/src/plugins/value/gui_files/gui_red.ml
index 4b807209ea73577e1a3e4bdd3e65cfab925630f6..a5d78c61b30a2e722f05c9d077547d68858f8b32 100644
--- a/src/plugins/value/gui_files/gui_red.ml
+++ b/src/plugins/value/gui_files/gui_red.ml
@@ -69,7 +69,7 @@ type red_alarm = {
let get_predicate ca =
match ca.annot_content with
- | AAssert (_, p) -> { p with pred_name = [] }
+ | AAssert (_, _, p) -> { p with pred_name = [] }
| _ -> assert false
let make_red_alarm function_name ki alarm callstacks =
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index 08eabb21cd9325eac38793407301dfa4287d6779..80d4d7ebce2766f4310fe98fcd23170f348f4543 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -454,7 +454,7 @@ module Select (Eval: Eval) = struct
let lv = (Var vi, NoOffset) in
select_lv main_ui (GL_Stmt (kf, stmt)) lv
| PIP (IPCodeAnnot (kf, stmt,
- ({annot_content = AAssert (_, p) | AInvariant (_, true, p)} as ca)) as ip) ->
+ ({annot_content = AAssert (_, _, p) | AInvariant (_, true, p)} as ca)) as ip) ->
begin
let loc = GL_Stmt (kf, stmt) in
let alarm_or_property =
@@ -623,7 +623,7 @@ let add_keybord_shortcut_evaluate main_ui =
select (find_loc kf fdec bl)
end
| PIP (Property.IPCodeAnnot (kf, stmt,
- {annot_content = AAssert (_, _) | AInvariant (_, true, _)} )) ->
+ {annot_content = AAssert _ | AInvariant (_, true, _)} )) ->
select (Some (GL_Stmt (kf, stmt)))
| PIP (Property.IPPredicate (_, kf, Kglobal, _) as ip) ->
select (Gui_eval.classify_pre_post kf ip)
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index e81cf164105c817b09af211696cd504a5c6ca7b7..6b2e67872412b52392079aef644e5f3242c5f8b9 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -29,7 +29,8 @@ let has_requires spec =
let code_annotation_text ca =
match ca.annot_content with
- | AAssert _ -> "assertion"
+ | AAssert (_, Assert, _) -> "assertion"
+ | AAssert (_, Check, _) -> "check"
| AInvariant _ -> "loop invariant"
| APragma _ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
| AExtended _ ->
@@ -202,7 +203,7 @@ let mark_green_and_red () =
currently skipped during evaluation. *)
if contains_c_at ca || (Alarms.find ca <> None) then
match ca.annot_content with
- | AAssert (_, p) | AInvariant (_, true, p) ->
+ | AAssert (_, _, p) | AInvariant (_, true, p) ->
let loc = code_annotation_loc ca stmt in
Cil.CurrentLoc.set loc;
let kf = Kernel_function.find_englobing_kf stmt in
@@ -245,7 +246,7 @@ let mark_invalid_initializers () =
| None -> ()
| Some _ ->
match ca.annot_content with
- | AAssert (_, p) ->
+ | AAssert (_, _, p) ->
let ip = Property.ip_of_code_annot_single kf first_stmt ca in
(* Evaluate in a fully empty state. Only predicates that do not
depend on the memory will result in 'False' *)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 6d1d1a3a70cec1a9675a2c229b0f72e0ecacce18..40d9d63d4dbbbe2a2b8d52cdd48e586e158b999a 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -754,7 +754,7 @@ interface of the programmatic API.
\texttt{@<category>} of properties.
\\
Recognized categories are: \texttt{@lemma}, \texttt{@requires}, \texttt{@assigns},
- \texttt{@ensures}, \texttt{@exits}, \texttt{@assert},
+ \texttt{@ensures}, \texttt{@exits}, \texttt{@assert}, \texttt{@check},
\texttt{@invariant}, \texttt{@variant}, \texttt{@breaks},
\texttt{@continues}, \texttt{@returns}, \\
\texttt{\mbox{@complete\_behaviors}}, \texttt{\mbox{@disjoint\_behaviors}}.
diff --git a/src/plugins/wp/tests/wp_acsl/checks.i b/src/plugins/wp/tests/wp_acsl/checks.i
new file mode 100644
index 0000000000000000000000000000000000000000..1a1174504f7e46923c594d5f5d11049ad5fdd1f0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/checks.i
@@ -0,0 +1,19 @@
+/* run.config
+ OPT: -eva -load-module scope,eva,report -then -report
+ OPT: -wp-prop=@check
+ OPT: -wp-prop=@assert
+*/
+/* run.config_qualif
+ OPT: -load-module report -wp-steps 5 -then -report
+*/
+
+// note: eva and wp gives the same reporting
+
+//@ axiomatic A { predicate P reads \nothing ; }
+void main() {
+ //@check c1: P;
+ //@assert a1: P;
+ //@check c2: P;
+ //@assert a2: P;
+ ;
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a99ec33e26d36787a9fc88e173e145acb5ac2b4a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.0.res.oracle
@@ -0,0 +1,75 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function main
+------------------------------------------------------------
+
+Goal Check 'c1' (file tests/wp_acsl/checks.i, line 14):
+Prove: P_P.
+
+------------------------------------------------------------
+
+Goal Assertion 'a1' (file tests/wp_acsl/checks.i, line 15):
+Prove: P_P.
+
+------------------------------------------------------------
+
+Goal Check 'c2' (file tests/wp_acsl/checks.i, line 16):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'a2' (file tests/wp_acsl/checks.i, line 17):
+Prove: true.
+
+------------------------------------------------------------
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+
+[eva:alarm] tests/wp_acsl/checks.i:14: Warning: check 'c1' got status unknown.
+[eva:alarm] tests/wp_acsl/checks.i:15: Warning:
+ assertion 'a1' got status unknown.
+[eva:alarm] tests/wp_acsl/checks.i:16: Warning: check 'c2' got status unknown.
+[eva:alarm] tests/wp_acsl/checks.i:17: Warning:
+ assertion 'a2' got status unknown.
+[eva] done for function main
+[scope:rm_asserts] removing 2 assertion(s)
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+
+[report] Computing properties status...
+--------------------------------------------------------------------------------
+--- Global Properties
+--------------------------------------------------------------------------------
+
+[ Valid ] Axiomatic 'A'
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'main'
+--------------------------------------------------------------------------------
+
+[ - ] Check 'c1' (file tests/wp_acsl/checks.i, line 14)
+ tried with Eva.
+[ - ] Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+ tried with Eva.
+[ Partial ] Check 'c2' (file tests/wp_acsl/checks.i, line 16)
+ By RedundantAlarms, with pending:
+ - Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+[ Partial ] Assertion 'a2' (file tests/wp_acsl/checks.i, line 17)
+ By RedundantAlarms, with pending:
+ - Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+
+--------------------------------------------------------------------------------
+--- Status Report Summary
+--------------------------------------------------------------------------------
+ 1 Completely validated
+ 2 Locally validated
+ 2 To be validated
+ 5 Total
+--------------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6de4c09508772db4e0a498cd8342d9401c6e88eb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.1.res.oracle
@@ -0,0 +1,18 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function main
+------------------------------------------------------------
+
+Goal Check 'c1' (file tests/wp_acsl/checks.i, line 14):
+Prove: P_P.
+
+------------------------------------------------------------
+
+Goal Check 'c2' (file tests/wp_acsl/checks.i, line 16):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..db600bf51f7bba62adcd95988f5b589ddb7fa068
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/checks.2.res.oracle
@@ -0,0 +1,18 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function main
+------------------------------------------------------------
+
+Goal Assertion 'a1' (file tests/wp_acsl/checks.i, line 15):
+Prove: P_P.
+
+------------------------------------------------------------
+
+Goal Assertion 'a2' (file tests/wp_acsl/checks.i, line 17):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7f27fd0f13f0ebe09ac0befc560084d9b6d8beb5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/checks.res.oracle
@@ -0,0 +1,50 @@
+# frama-c -wp -wp-timeout 90 -wp-steps 5 [...]
+[kernel] Parsing tests/wp_acsl/checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 4 goals scheduled
+[wp] [Alt-Ergo] Goal typed_main_check_c1 : Unsuccess
+[wp] [Alt-Ergo] Goal typed_main_assert_a1 : Unsuccess
+[wp] [Qed] Goal typed_main_check_c2 : Valid
+[wp] [Qed] Goal typed_main_assert_a2 : Valid
+[wp] Proved goals: 2 / 4
+ Qed: 2
+ Alt-Ergo: 0 (unsuccess: 2)
+[wp] Report in: 'tests/wp_acsl/oracle_qualif/checks.0.report.json'
+[wp] Report out: 'tests/wp_acsl/result_qualif/checks.0.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+main 2 - 4 50.0%
+-------------------------------------------------------------
+[report] Computing properties status...
+--------------------------------------------------------------------------------
+--- Global Properties
+--------------------------------------------------------------------------------
+
+[ Valid ] Axiomatic 'A'
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'main'
+--------------------------------------------------------------------------------
+
+[ - ] Check 'c1' (file tests/wp_acsl/checks.i, line 14)
+ tried with Wp.typed.
+[ - ] Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+ tried with Wp.typed.
+[ Partial ] Check 'c2' (file tests/wp_acsl/checks.i, line 16)
+ By Wp.typed, with pending:
+ - Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+[ Partial ] Assertion 'a2' (file tests/wp_acsl/checks.i, line 17)
+ By Wp.typed, with pending:
+ - Assertion 'a1' (file tests/wp_acsl/checks.i, line 15)
+
+--------------------------------------------------------------------------------
+--- Status Report Summary
+--------------------------------------------------------------------------------
+ 1 Completely validated
+ 2 Locally validated
+ 2 To be validated
+ 5 Total
+--------------------------------------------------------------------------------
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index 81744b579a92317b77a4d957d7116ff5a5213165..5369d46e449d160f921822ea13e6ca1488681109 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -902,24 +902,25 @@ let get_stmt_annots config v s =
Printer.pp_code_annotation a;
acc
end
- | AAssert (b_list,p) ->
+ | AAssert (b_list, kind, p) ->
let kf = config.kf in
let acc = match is_annot_for_config config v s b_list with
| TBRno -> acc
| TBRhyp ->
- let b_acc =
- WpStrategy.add_prop_assert b_acc WpStrategy.Ahyp kf s a p
- in (b_acc, (a_acc, e_acc))
+ if kind = Check then acc
+ else
+ let b_acc =
+ WpStrategy.add_prop_assert b_acc WpStrategy.Ahyp kf s a p
+ in (b_acc, (a_acc, e_acc))
| TBRok | TBRpart ->
let id = WpPropId.mk_assert_id config.kf s a in
- let kind =
- if Wp_parameters.Assert_check_only.get () then
- WpStrategy.Agoal
- else
- WpStrategy.Aboth (goal_to_select config id)
- in
- let b_acc = WpStrategy.add_prop_assert b_acc kind kf s a p in
- (b_acc, (a_acc, e_acc))
+ let check = kind = Check || Wp_parameters.Assert_check_only.get ()
+ and goal = goal_to_select config id in
+ if check && not goal then acc
+ else
+ let kind = WpStrategy.(if check then Agoal else Aboth goal) in
+ let b_acc = WpStrategy.add_prop_assert b_acc kind kf s a p in
+ (b_acc, (a_acc, e_acc))
in acc
| AAllocation (_b_list, _frees_allocates) ->
(* [PB] TODO *) acc
@@ -1385,7 +1386,7 @@ let get_id_prop_strategies ~model ?(assigns=WithAssigns) p =
match p with
| Property.IPCodeAnnot (kf,_,ca) ->
let bhvs = match ca.annot_content with
- | AAssert (l, _) | AInvariant (l, _, _) | AAssigns (l, _) -> l
+ | AAssert (l, _, _) | AInvariant (l, _, _) | AAssigns (l, _) -> l
| _ -> []
in get_strategies assigns kf model bhvs None (IdProp p)
| Property.IPAssigns (kf, _, Property.Id_loop _, _)
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 7e3009c53bb7fe0117b0c4850da8094daff69536..c20fbae10bf92f26c788a3b839a34a9b3183dd0a 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -420,7 +420,8 @@ let ident_names names =
| _ as n -> '\"' <> (String.get n 0) ) names
let code_annot_names ca = match ca.annot_content with
- | AAssert (_, named_pred) -> "@assert"::(ident_names named_pred.pred_name)
+ | AAssert (_, Check, named_pred) -> "@check"::(ident_names named_pred.pred_name)
+ | AAssert (_, Assert, named_pred) -> "@assert"::(ident_names named_pred.pred_name)
| AInvariant (_,_,named_pred) -> "@invariant"::(ident_names named_pred.pred_name)
| AVariant (term, _) -> "@variant"::(ident_names term.term_name)
| AExtended(_,_,(_,name,_,_,_)) -> [Printf.sprintf "@%s" name]
@@ -588,7 +589,7 @@ let assigns_hints hs froms =
List.iter (fun ({it_content=t},_) -> term_hints hs t) froms
let annot_hints hs = function
- | AAssert(bs,ipred) | AInvariant(bs,_,ipred) ->
+ | AAssert(bs,_,ipred) | AInvariant(bs,_,ipred) ->
List.iter (add_hint hs) (ident_names ipred.pred_name) ;
List.iter (add_hint hs) bs
| AAssigns(bs,Writes froms) ->
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 9222639296b0f70ef47ae9602868db255f8271bb..bd5be9fa57d460d53a05cfbf15a933803537d46f 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -100,7 +100,7 @@ module Properties =
let arg_name = "p,..."
let help = "Select properties having the one of the given tagnames (defaults to all properties).\n\
You may also replace the tagname by '@category' for the selection of all properties of the given category.\n\
- Accepted categories are: lemmas, requires, assigns, ensures, exits, complete_behaviors, disjoint_behaviors assert, invariant, variant, breaks, continues, returns.\n\
+ Accepted categories are: lemmas, requires, assigns, ensures, exits, complete_behaviors, disjoint_behaviors, assert, check, invariant, variant, breaks, continues, returns.\n\
Starts by a minus character to remove properties from the selection."
end)
let () = on_reset Properties.clear
diff --git a/tests/syntax/syntactic_hook.ml b/tests/syntax/syntactic_hook.ml
index e731d80478a1ad85e8d97ee19fa17f11717eee9d..c6a5d1f3517e261599913c4c0f8f577ece146a2c 100644
--- a/tests/syntax/syntactic_hook.ml
+++ b/tests/syntax/syntactic_hook.ml
@@ -13,7 +13,7 @@ class visit = object
[{ stmt_ghost = false;
stmt_node =
CODE_ANNOT(
- AAssert([],
+ AAssert([], Assert,
{ lexpr_node =
PLat ({ lexpr_node = PLtrue; lexpr_loc = loc},"Pre");
lexpr_loc = loc}), loc)};
diff --git a/tests/value/logic.c b/tests/value/logic.c
index bf9938b58236f08412fa112d30f000c4992babb9..9ba0bf437d48621353f33ea92f8749c3f9ba9726 100644
--- a/tests/value/logic.c
+++ b/tests/value/logic.c
@@ -288,6 +288,26 @@ void min_max () {
//@ assert d == \min(a, b);
}
+/* Tests assert and check assertions. */
+void check_and_assert () {
+ int x;
+ x = v;
+ /*@ assert x == 42; */
+ Frama_C_show_each_42(x);
+ /*@ check x == 42; */
+ x = v;
+ /*@ check x == 42; */
+ Frama_C_show_each_imprecise(x);
+ /*@ assert x == 42; */
+ if (v) {
+ /*@ assert x == 0; */
+ Frama_C_show_each_unreachable(x); /* The assert led to bottom. */
+ } else {
+ /*@ check x == 0; */
+ Frama_C_show_each_reachable(x); /* A check should never lead to bottom. */
+ }
+}
+
void main () {
eq_tsets();
eq_char();
@@ -300,4 +320,5 @@ void main () {
float_sign();
min_max();
assign_tsets();
+ check_and_assert ();
}
diff --git a/tests/value/oracle/logic.res.oracle b/tests/value/oracle/logic.res.oracle
index 07c802ebd74d6cc8d69bc60c86d61b8ba18c3edf..1920a84df5ef397cf97a49829ce57f1d79f6f942 100644
--- a/tests/value/oracle/logic.res.oracle
+++ b/tests/value/oracle/logic.res.oracle
@@ -14,7 +14,7 @@
arr_ptr[0..2] ∈ {0}
arr_ptr_arr[0..5] ∈ {0}
[eva] computing for function eq_tsets <- main.
- Called from tests/value/logic.c:292.
+ Called from tests/value/logic.c:312.
[eva] tests/value/logic.c:103:
cannot evaluate ACSL term, unsupported ACSL construct: == operation on non-supported type set<_#8>
[eva:alarm] tests/value/logic.c:103: Warning: assertion got status unknown.
@@ -56,20 +56,20 @@
[eva] Recording results for eq_tsets
[eva] Done for function eq_tsets
[eva] computing for function eq_char <- main.
- Called from tests/value/logic.c:293.
+ Called from tests/value/logic.c:313.
[eva] tests/value/logic.c:149: Frama_C_show_each: {-126}
[eva] tests/value/logic.c:150: assertion got status valid.
[eva] tests/value/logic.c:151: assertion got status valid.
[eva] Recording results for eq_char
[eva] Done for function eq_char
[eva] computing for function casts <- main.
- Called from tests/value/logic.c:294.
+ Called from tests/value/logic.c:314.
[eva] tests/value/logic.c:155: assertion got status valid.
[eva] tests/value/logic.c:156: assertion got status valid.
[eva] Recording results for casts
[eva] Done for function casts
[eva] computing for function empty_tset <- main.
- Called from tests/value/logic.c:295.
+ Called from tests/value/logic.c:315.
[eva] computing for function f_empty_tset <- empty_tset <- main.
Called from tests/value/logic.c:166.
[eva] using specification for function f_empty_tset
@@ -82,7 +82,7 @@
[eva] Recording results for empty_tset
[eva] Done for function empty_tset
[eva] computing for function reduce_by_equal <- main.
- Called from tests/value/logic.c:296.
+ Called from tests/value/logic.c:316.
[eva:alarm] tests/value/logic.c:172: Warning:
accessing out of bounds index. assert 0 ≤ v;
[eva:alarm] tests/value/logic.c:172: Warning:
@@ -92,7 +92,7 @@
[eva] Recording results for reduce_by_equal
[eva] Done for function reduce_by_equal
[eva] computing for function alarms <- main.
- Called from tests/value/logic.c:297.
+ Called from tests/value/logic.c:317.
[eva:alarm] tests/value/logic.c:182: Warning:
assertion 'ASSUME' got status unknown.
[eva:alarm] tests/value/logic.c:184: Warning:
@@ -124,7 +124,7 @@
[eva] Recording results for alarms
[eva] Done for function alarms
[eva] computing for function cond_in_lval <- main.
- Called from tests/value/logic.c:298.
+ Called from tests/value/logic.c:318.
[eva] computing for function select_like <- cond_in_lval <- main.
Called from tests/value/logic.c:228.
[eva] using specification for function select_like
@@ -152,7 +152,7 @@
[eva] Recording results for cond_in_lval
[eva] Done for function cond_in_lval
[eva] computing for function pred <- main.
- Called from tests/value/logic.c:299.
+ Called from tests/value/logic.c:319.
[eva] tests/value/logic.c:90: assertion got status valid.
[eva] tests/value/logic.c:91: assertion got status valid.
[eva] tests/value/logic.c:31:
@@ -201,7 +201,7 @@
[eva] Recording results for pred
[eva] Done for function pred
[eva] computing for function float_sign <- main.
- Called from tests/value/logic.c:300.
+ Called from tests/value/logic.c:320.
[eva] tests/value/logic.c:251: assertion got status valid.
[eva] tests/value/logic.c:252: assertion got status valid.
[eva] tests/value/logic.c:253: assertion got status valid.
@@ -210,7 +210,7 @@
[eva] Recording results for float_sign
[eva] Done for function float_sign
[eva] computing for function min_max <- main.
- Called from tests/value/logic.c:301.
+ Called from tests/value/logic.c:321.
[eva] computing for function Frama_C_interval <- min_max <- main.
Called from tests/value/logic.c:274.
[eva] using specification for function Frama_C_interval
@@ -235,16 +235,31 @@
[eva] Recording results for min_max
[eva] Done for function min_max
[eva] computing for function assign_tsets <- main.
- Called from tests/value/logic.c:302.
+ Called from tests/value/logic.c:322.
[eva] computing for function assign_tsets_aux <- assign_tsets <- main.
Called from tests/value/logic.c:269.
[eva] using specification for function assign_tsets_aux
[eva] Done for function assign_tsets_aux
[eva] Recording results for assign_tsets
[eva] Done for function assign_tsets
+[eva] computing for function check_and_assert <- main.
+ Called from tests/value/logic.c:323.
+[eva:alarm] tests/value/logic.c:295: Warning: assertion got status unknown.
+[eva] tests/value/logic.c:296: Frama_C_show_each_42: {42}
+[eva] tests/value/logic.c:297: check got status valid.
+[eva:alarm] tests/value/logic.c:299: Warning: check got status unknown.
+[eva] tests/value/logic.c:300:
+ Frama_C_show_each_imprecise: [-2147483648..2147483647]
+[eva:alarm] tests/value/logic.c:301: Warning: assertion got status unknown.
+[eva:alarm] tests/value/logic.c:303: Warning:
+ assertion got status invalid (stopping propagation).
+[eva:alarm] tests/value/logic.c:306: Warning: check got status invalid.
+[eva] tests/value/logic.c:307: Frama_C_show_each_reachable: {42}
+[eva] Recording results for check_and_assert
+[eva] Done for function check_and_assert
[eva] Recording results for main
[eva] done for function main
-[scope:rm_asserts] removing 4 assertion(s)
+[scope:rm_asserts] removing 5 assertion(s)
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function alarms:
x_0 ∈ {1}
@@ -258,6 +273,8 @@
[4..5] ∈ [--..--]
[eva:final-states] Values at end of function casts:
+[eva:final-states] Values at end of function check_and_assert:
+ x_0 ∈ {42}
[eva:final-states] Values at end of function eq_char:
c ∈ {-126}
[eva:final-states] Values at end of function eq_tsets:
@@ -330,6 +347,8 @@
[from] Done for function assign_tsets
[from] Computing for function casts
[from] Done for function casts
+[from] Computing for function check_and_assert
+[from] Done for function check_and_assert
[from] Computing for function eq_char
[from] Done for function eq_char
[from] Computing for function eq_tsets
@@ -376,6 +395,8 @@
arr_ptr_arr{[1]; [4..5]} FROM \nothing
[from] Function casts:
NO EFFECTS
+[from] Function check_and_assert:
+ NO EFFECTS
[from] Function eq_char:
NO EFFECTS
[from] Function eq_tsets:
@@ -426,6 +447,10 @@
\nothing
[inout] Inputs for function casts:
\nothing
+[inout] Out (internal) for function check_and_assert:
+ x_0
+[inout] Inputs for function check_and_assert:
+ v
[inout] Out (internal) for function eq_char:
c
[inout] Inputs for function eq_char: