diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 6f2547db91ff1ebf4e193024ad1158e06428e887..4ad71347daf28a3cdee1d158fdb8911b02d5ca3a 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -109,7 +109,7 @@ let check_funspec_abrupt_clauses fname spec =
(function
| (Cil_types.Normal | Cil_types.Exits),_ -> ()
| (Cil_types.Breaks | Cil_types.Continues | Cil_types.Returns),
- {Logic_ptree.lexpr_loc = (loc,_)} ->
+ { Logic_ptree.tp_statement = { lexpr_loc = (loc,_)}} ->
Errorloc.parse_error ~source:loc
"Specification of function %s can only contain ensures or \
exits post-conditions" fname)
diff --git a/src/kernel_internals/parsing/logic_lexer.mll b/src/kernel_internals/parsing/logic_lexer.mll
index ca329de4aef0f70a65206da351f27f04d235e13c..b86e9200489ea822f2dfb2315a2d5134b2bfd3b3 100644
--- a/src/kernel_internals/parsing/logic_lexer.mll
+++ b/src/kernel_internals/parsing/logic_lexer.mll
@@ -297,6 +297,18 @@
let accept_c_comments_into_acsl_spec = ref false
+ let hack_merge_tokens current next =
+ match (current,next) with
+ | CHECK, REQUIRES -> true, CHECK_REQUIRES
+ | CHECK, ENSURES -> true, CHECK_ENSURES
+ | CHECK, EXITS -> true, CHECK_EXITS
+ | CHECK, RETURNS -> true, CHECK_RETURNS
+ | CHECK, BREAKS -> true, CHECK_BREAKS
+ | CHECK, CONTINUES -> true, CHECK_CONTINUES
+ | CHECK, LOOP -> true, CHECK_LOOP
+ | CHECK, INVARIANT -> true, CHECK_INVARIANT
+ | CHECK, LEMMA -> true, CHECK_LEMMA
+ | _ -> false, current
}
let space = [' ' '\t' '\012' '\r' '@' ]
@@ -339,7 +351,15 @@ rule token = parse
let loc = Lexing.(lexeme_start_p lexbuf, lexeme_end_p lexbuf) in
let cabsloc = Cil_datatype.Location.of_lexing_loc loc in
let s = lexeme lexbuf in
- identifier s cabsloc
+ let curr_tok = identifier s cabsloc in
+ if curr_tok = CHECK then begin
+ let next_tok =
+ token { lexbuf with refill_buff = lexbuf.refill_buff }
+ in
+ let (eat_next, tok) = hack_merge_tokens curr_tok next_tok in
+ if eat_next then ignore (token lexbuf);
+ tok
+ end else curr_tok
}
| '0'['x''X'] rH+ rIS? { CONSTANT (IntConstant (lexeme lexbuf)) }
diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index cc86b0d9c1da06ba1beb012a70be1036e51dfff4..38d5b09db50efc5c67c3e204aa83669652d7c1a1 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -225,6 +225,7 @@
let cv_const = Attr ("const", [])
let cv_volatile = Attr ("volatile", [])
+ let toplevel_pred tp_only_check tp_statement = { tp_only_check; tp_statement }
%}
/*****************************************************************************/
@@ -250,6 +251,8 @@
%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 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 <string> EXT_CODE_ANNOT EXT_GLOBAL EXT_CONTRACT
%token EXITS BREAKS CONTINUES RETURNS
%token VOLATILE READS WRITES
@@ -1098,6 +1101,7 @@ contract:
// use that to detect potentially missing ';' at end of clause
clause_kw:
+| CHECK_REQUIRES { "check requires" }
| REQUIRES { "requires" }
| ASSUMES {"assumes"}
| ASSIGNS { "assigns" }
@@ -1121,8 +1125,10 @@ requires:
;
ne_requires:
-| REQUIRES full_lexpr SEMICOLON requires { $2::$4 }
-| REQUIRES full_lexpr clause_kw { missing 2 ";" $3}
+| REQUIRES full_lexpr SEMICOLON requires { toplevel_pred false $2::$4 }
+| CHECK_REQUIRES full_lexpr SEMICOLON requires { toplevel_pred true $2 :: $4 }
+| REQUIRES full_lexpr clause_kw { missing 2 ";" $3 }
+| CHECK_REQUIRES full_lexpr clause_kw { missing 2 ";" $3 }
;
terminates:
@@ -1161,7 +1167,10 @@ allocation:
ne_simple_clauses:
| post_cond_kind full_lexpr SEMICOLON simple_clauses
- { let allocation,assigns,post_cond,extended = $4 in allocation,assigns,(($1,$2)::post_cond),extended }
+ { let only_check, kind = $1 in
+ let allocation,assigns,post_cond,extended = $4 in
+ allocation,assigns,
+ ((kind,toplevel_pred only_check $2)::post_cond),extended }
| allocation SEMICOLON simple_clauses
{ let allocation,assigns,post_cond,extended = $3 in
let a = concat_allocation allocation $1 in
@@ -1388,7 +1397,8 @@ loop_allocation:
;
loop_invariant:
-| LOOP INVARIANT full_lexpr SEMICOLON { $3 }
+| LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred false $3 }
+| CHECK_LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred true $3 }
;
loop_variant:
@@ -1439,6 +1449,7 @@ beg_pragma_or_code_annotation:
| ASSERT {}
| CHECK {}
| INVARIANT {}
+| CHECK_INVARIANT {}
| EXT_CODE_ANNOT {}
;
@@ -1450,10 +1461,13 @@ pragma_or_code_annotation:
code_annotation:
| ASSERT full_lexpr SEMICOLON
- { fun bhvs -> AAssert (bhvs,Assert,$2) }
+ { fun bhvs -> AAssert (bhvs,toplevel_pred false $2) }
| CHECK full_lexpr SEMICOLON
- { fun bhvs -> AAssert (bhvs,Check,$2) }
-| INVARIANT full_lexpr SEMICOLON { fun bhvs -> AInvariant (bhvs,false,$2) }
+ { fun bhvs -> AAssert (bhvs,toplevel_pred true $2) }
+| INVARIANT full_lexpr SEMICOLON
+ { fun bhvs -> AInvariant (bhvs,false,toplevel_pred false $2) }
+| CHECK_INVARIANT full_lexpr SEMICOLON
+ { fun bhvs -> AInvariant (bhvs,false,toplevel_pred true $2) }
| EXT_CODE_ANNOT grammar_extension SEMICOLON
{ fun bhvs ->
let open Cil_types in
@@ -1601,7 +1615,11 @@ logic_def:
| LEMMA poly_id COLON full_lexpr SEMICOLON
{ let (id,labels,tvars) = $2 in
exit_type_variables_scope ();
- LDlemma (id, false, labels, tvars, $4) }
+ LDlemma (id, false, labels, tvars, toplevel_pred false $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) }
| AXIOMATIC any_identifier LBRACE logic_decls RBRACE
{ LDaxiomatic($2,$4) }
| TYPE poly_id_type_add_typename EQUAL typedef SEMICOLON
@@ -1674,7 +1692,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, $4) }
+ LDlemma (id, true, labels, tvars, toplevel_pred false $4) }
;
logic_decl_loc:
@@ -1836,11 +1854,16 @@ acsl_c_keyword:
;
post_cond:
-| ENSURES { Normal, "ensures" }
-| EXITS { Exits, "exits" }
-| BREAKS { Breaks, "breaks" }
-| CONTINUES { Continues, "continues" }
-| RETURNS { Returns, "returns" }
+| 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" }
;
is_acsl_spec:
@@ -1851,6 +1874,7 @@ is_acsl_spec:
| FREES { "frees" }
| BEHAVIOR { "behavior" }
| REQUIRES { "requires" }
+| CHECK_REQUIRES { "check requires" }
| TERMINATES { "terminates" }
| COMPLETE { "complete" }
| DECREASES { "decreases" }
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index de0e67072492daa5af65815d4cff643da90a7455..6c2f452b6c5abfa7196cba938b0215a74a1dd61f 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -8876,9 +8876,14 @@ and createLocal ghost ((_, sto, _, _) as specs)
Logic_const.prel ~loc:castloc (Rle, talloca_size, max_bound)
in
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 alloca_bounds =
+ { alloca_bounds with pred_name = ["alloca_bounds"] }
+ in
+ let alloca_bounds =
+ Logic_const.toplevel_predicate alloca_bounds
+ in
let annot =
- Logic_const.new_code_annotation (AAssert ([], Assert, alloca_bounds))
+ Logic_const.new_code_annotation (AAssert ([], alloca_bounds))
in
(mkStmtOneInstr ~ghost ~valid_sid
(Code_annot (annot, castloc)),
@@ -9395,9 +9400,10 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
[\assert \false]*)
let pfalse = Logic_const.unamed ~loc Pfalse in
let pfalse = { pfalse with pred_name = ["missing_return"] } in
+ let pfalse = Logic_const.toplevel_predicate pfalse in
let assert_false () =
let annot =
- Logic_const.new_code_annotation (AAssert ([], Assert, pfalse))
+ Logic_const.new_code_annotation (AAssert ([], 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 1ffc5c6b32b0e4bfa3fff39766b17671e172ba3d..3438e59ff51819ce28c437e4f00287ca463da39e 100644
--- a/src/kernel_internals/typing/cfg.ml
+++ b/src/kernel_internals/typing/cfg.ml
@@ -360,7 +360,8 @@ let xform_switch_block ?(keepSwitch=false) b =
let () = Stack.push (Stack.create()) continues_stack in
let assert_of_clause f ca =
match ca.annot_content with
- | AAssert _ | AInvariant _ | AVariant _ | AAssigns _ | AAllocation _ | APragma _ | AExtended _ -> Logic_const.ptrue
+ | AAssert _ | AInvariant _ | AVariant _
+ | AAssigns _ | AAllocation _ | APragma _ | AExtended _ -> Logic_const.ptrue
| AStmtSpec (_bhv,s) ->
let open Logic_const in
List.fold_left
@@ -371,8 +372,8 @@ let xform_switch_block ?(keepSwitch=false) b =
(pands
(List.map
(fun p ->
- pold ~loc:p.ip_content.pred_loc
- (Logic_const.pred_of_id_pred p))
+ let p = Logic_const.pred_of_id_pred p in
+ pold ~loc:p.pred_loc p)
bhv.b_assumes),
pands
(List.fold_left
@@ -478,8 +479,9 @@ let xform_switch_block ?(keepSwitch=false) b =
xform_switch_stmt
rest break_dest cont_dest label_index 0
| p ->
+ let p = Logic_const.toplevel_predicate p in
let a =
- Logic_const.new_code_annotation (AAssert ([], Assert, p))
+ Logic_const.new_code_annotation (AAssert ([], p))
in
let assertion = mkStmt (Instr(Code_annot(a,l))) in
popn popstack;
@@ -501,9 +503,8 @@ 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 ([], Assert, p))
- in
+ let p = Logic_const.toplevel_predicate p in
+ let a = Logic_const.new_code_annotation (AAssert ([], 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 f41401c9a7e8d91360f8f91a7498ff38f48feee4..164f5b48e7887784a264e4c55beaaaa74421f352 100644
--- a/src/kernel_internals/typing/oneret.ml
+++ b/src/kernel_internals/typing/oneret.ml
@@ -235,8 +235,8 @@ let oneret ?(callback: callback option) (f: fundec) : unit =
(pands
(List.map
(fun p ->
- pold ~loc:p.ip_content.pred_loc
- (Logic_const.pred_of_id_pred p))
+ let p = Logic_const.pred_of_id_pred p in
+ pold ~loc:p.pred_loc p)
bhv.b_assumes),
pands
(List.fold_left
@@ -381,7 +381,8 @@ 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 ([],Assert,p)) in
+ let p = Logic_const.toplevel_predicate p in
+ let a = Logic_const.new_code_annotation (AAssert ([],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_internals/typing/unroll_loops.ml b/src/kernel_internals/typing/unroll_loops.ml
index fc2af50b9c1c20573594c2f62d30c6b4575d36e6..e73b70a19d740f53d7b2e2c390297b7473f4d1fd 100644
--- a/src/kernel_internals/typing/unroll_loops.ml
+++ b/src/kernel_internals/typing/unroll_loops.ml
@@ -684,7 +684,7 @@ class do_it global_find_init ((force:bool),(times:int)) = object(self)
| Some emitter ->
let annot =
Logic_const.new_code_annotation
- (AInvariant ([],true,Logic_const.pfalse))
+ (AInvariant ([],true,Logic_const.(toplevel_predicate pfalse)))
in
Annotations.add_code_annot
emitter ~kf:(Extlib.the self#current_kf) sloop annot;
diff --git a/src/kernel_services/analysis/exn_flow.ml b/src/kernel_services/analysis/exn_flow.ml
index a75151352f640348731a343532d6cfa4da1a5646..45859e0a17ce45666c024f5e9085369c1656130f 100644
--- a/src/kernel_services/analysis/exn_flow.ml
+++ b/src/kernel_services/analysis/exn_flow.ml
@@ -660,7 +660,7 @@ object(self)
we haven't seen an uncaught exception anyway. *)
| Exits | Breaks | Continues -> orig
| Returns | Normal ->
- let loc = pred.ip_content.pred_loc in
+ let loc = (Logic_const.pred_of_id_pred pred).pred_loc in
let p = self#pred_uncaught_flag loc false in
let pred' = Logic_const.pred_of_id_pred pred in
(kind,
diff --git a/src/kernel_services/analysis/interpreted_automata.ml b/src/kernel_services/analysis/interpreted_automata.ml
index ae1d5a4f3cff63f0f6562dde13fa0a9eec6c3b25..32a98309ead70a015f9269dbe4c382f2abc97e72 100644
--- a/src/kernel_services/analysis/interpreted_automata.ml
+++ b/src/kernel_services/analysis/interpreted_automata.ml
@@ -204,7 +204,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 *)
@@ -214,9 +214,9 @@ 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 ([], Cil_types.Assert, pred) -> Assert, pred
- | AAssert ([], Cil_types.Check, pred) -> Check, pred
- | AInvariant ([], _, pred) -> Invariant, pred
+ | AAssert ([], {tp_only_check = false; tp_statement = pred}) -> Assert, pred
+ | AAssert ([], {tp_only_check = true; tp_statement = pred}) -> Check, pred
+ | AInvariant ([], _, pred) -> Invariant, pred.tp_statement
| AVariant (v, None) -> Assert, variant_predicate stmt v
| _ -> assert false
in
@@ -552,7 +552,10 @@ let build_automaton ~annotations kf =
let bind_labels (v1, edge, v2) =
match edge.edge_transition with
| Prop (annot, stmt) ->
- let l = Cil.extract_labels_from_pred annot.predicate.ip_content in
+ let l =
+ Cil.extract_labels_from_pred
+ (Logic_const.pred_of_id_pred annot.predicate)
+ in
let bind label map =
try
let vertex = match label with
diff --git a/src/kernel_services/analysis/logic_interp.ml b/src/kernel_services/analysis/logic_interp.ml
index ca8044ead8db1d5b6bb9cfb3459f5aca44692aa4..5235e6aec142f3c85c6363fc58002714829453ec 100644
--- a/src/kernel_services/analysis/logic_interp.ml
+++ b/src/kernel_services/analysis/logic_interp.ml
@@ -947,17 +947,17 @@ 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;
+ get_zone_from_pred ki pred.tp_statement;
| AInvariant (_behav,true,pred) -> (* loop invariant *)
(* WARNING this is obsolete *)
(* [JS 2010/09/02] TODO: so what is the right way to do? *)
(* to preserve the interpretation of the loop invariant *)
- get_zone_from_pred (Extlib.the loop_body_opt) pred;
+ get_zone_from_pred (Extlib.the loop_body_opt) pred.tp_statement;
| AInvariant (_behav,false,pred) -> (* code invariant *)
(* to preserve the interpretation of the code invariant *)
- get_zone_from_pred ki pred;
+ get_zone_from_pred ki pred.tp_statement;
| AVariant (term,_) ->
(* to preserve the interpretation of the variant *)
get_zone_from_term (Extlib.the loop_body_opt) term;
diff --git a/src/kernel_services/ast_data/alarms.ml b/src/kernel_services/ast_data/alarms.ml
index a0845e815040b754587d15eca7cf150ba0911b25..0138ec1f79086c159276d18b5c0ef6fac9cbdb78 100644
--- a/src/kernel_services/ast_data/alarms.ml
+++ b/src/kernel_services/ast_data/alarms.ml
@@ -705,7 +705,8 @@ 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([], Assert, pred))
+ let pred = Logic_const.toplevel_predicate pred in
+ Logic_const.new_code_annotation (AAssert([], 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 056d57d7a3eff673eadf2da8c7bd9adb4f3f9809..4febe26e5fb3c67fdd1eae0311b100785a480a34 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -717,13 +717,16 @@ let extend_name e pred =
if Emitter.equal e Emitter.end_user || Emitter.equal e Emitter.kernel
then pred
else
- let names = pred.pred_name in
+ let names = pred.tp_statement.pred_name in
let s = Emitter.get_name e in
if (List.mem s names) ||
let acsl_identifier_regexp =
Str.regexp "^\\([\\][_a-zA-Z]\\|[_a-zA-Z]\\)[0-9_a-zA-Z]*$"
in not (Str.string_match acsl_identifier_regexp s 0)
- then pred else { pred with pred_name = s :: names }
+ then pred
+ else
+ { pred with
+ tp_statement = { pred.tp_statement with pred_name = s :: names }}
(** {3 Adding subparts of a function contract} *)
@@ -1072,8 +1075,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, kind, p) ->
- let a = { a with annot_content=AAssert(l,kind,extend_name emitter p) } in
+ | AAssert(l, p) ->
+ let a = { a with annot_content=AAssert(l,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,11 +1273,13 @@ 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 ([],Assert,a)) in
+ let a = Logic_const.toplevel_predicate ~only_check:false 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.new_code_annotation (AAssert ([],Check,a)) in
+ let a = Logic_const.toplevel_predicate ~only_check:true a in
+ let a = Logic_const.new_code_annotation (AAssert ([],a)) in
add_code_annot e ?kf stmt a
(** {3 Adding globals} *)
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 9ad9fdb7a7684514813a0b79fee5116fcd7ab814..53a410ee52c920a514dc2cfe38a15e149b96959d 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1590,7 +1590,17 @@ and predicate_node =
create fresh predicates *)
and identified_predicate = {
ip_id: int; (** identifier *)
- ip_content: predicate; (** the predicate itself*)
+ ip_content: toplevel_predicate; (** the predicate itself*)
+}
+
+(** main statement of an annotation. *)
+and toplevel_predicate = {
+ tp_only_check: bool;
+ (** 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).
+ *)
+ tp_statement: predicate;
}
(** predicates with a location and an optional list of names *)
@@ -1745,17 +1755,11 @@ 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 * assertion_kind * predicate
+ | AAssert of string list * toplevel_predicate
(** assertion to be checked. The list of strings is the list of
behaviors to which this assertion applies. *)
@@ -1763,7 +1767,7 @@ and code_annotation_node =
(** statement contract
(potentially restricted to some enclosing behaviors). *)
- | AInvariant of string list * bool * predicate
+ | AInvariant of string list * bool * toplevel_predicate
(** loop/code invariant. The list of strings is the list of behaviors to which
this invariant applies. The boolean flag is true for normal loop
invariants and false for invariant-as-assertions. *)
@@ -1814,7 +1818,7 @@ and global_annotation =
| Dtype of logic_type_info * location (** declaration of a logic type. *)
| Dlemma of
string * bool * logic_label list * string list *
- predicate * attributes * location
+ toplevel_predicate * attributes * location
(** definition of a lemma. The boolean flag is [true] if the property should
be taken as an axiom and [false] if it must be proved. *)
| Dinvariant of logic_info * location
diff --git a/src/kernel_services/ast_data/property.ml b/src/kernel_services/ast_data/property.ml
index a4720657054383c60c52711a697cf07ba7c7d144..04e98b3d88abb2cfcc90ae5f5686a8af6c494185 100644
--- a/src/kernel_services/ast_data/property.ml
+++ b/src/kernel_services/ast_data/property.ml
@@ -126,7 +126,7 @@ and identified_lemma = {
il_name : string;
il_labels : logic_label list;
il_args : string list;
- il_pred : predicate;
+ il_pred : toplevel_predicate;
il_loc : location
}
@@ -281,7 +281,7 @@ let loc_of_loc_o = function
| OLGlob loc -> loc
let rec location = function
- | IPPredicate {ip_pred} -> ip_pred.ip_content.pred_loc
+ | IPPredicate {ip_pred} -> (Logic_const.pred_of_id_pred ip_pred).pred_loc
| IPBehavior {ib_kf=kf; ib_kinstr=ki}
| IPComplete {ic_kf=kf; ic_kinstr=ki}
| IPDisjoint {ic_kf=kf; ic_kinstr=ki}
@@ -397,8 +397,13 @@ include Datatype.Make_with_collections
type t = identified_property
let name = "Property.t"
- let reprs = [IPAxiom {il_name="";il_labels=[];il_args=[];
- il_pred=Logic_const.ptrue;il_loc=Location.unknown}]
+ let reprs = [
+ IPAxiom {
+ il_name="";il_labels=[];il_args=[];
+ il_pred=Logic_const.(toplevel_predicate ptrue);
+ il_loc=Location.unknown
+ }]
+
let mem_project = Datatype.never_any_project
let pp_active fmt active =
@@ -688,9 +693,10 @@ include Datatype.Make_with_collections
end)
let rec short_pretty fmt p = match p with
- | IPPredicate {ip_pred={ip_content={pred_name=name::_}}} ->
- Format.pp_print_string fmt name
- | IPPredicate _ -> pretty fmt p
+ | IPPredicate {ip_pred} ->
+ (match (Logic_const.pred_of_id_pred ip_pred).pred_name with
+ | name :: _ -> Format.pp_print_string fmt name
+ | [] -> pretty fmt p)
| IPExtended {ie_ext={ext_name}} -> Format.pp_print_string fmt ext_name
| IPAxiom {il_name=n} | IPLemma {il_name=n}
| IPTypeInvariant {iti_name=n} | IPGlobalInvariant {igi_name=n}
@@ -704,9 +710,11 @@ let rec short_pretty fmt p = match p with
| IPDisjoint {ic_kf} ->
Format.fprintf fmt "disjoint clause in function %a"
Kernel_function.pretty ic_kf
- | IPCodeAnnot {ica_ca={annot_content=AAssert (_, _, {pred_name=name::_})}}
- | IPCodeAnnot {ica_ca={annot_content=AInvariant (_, _, {pred_name=name::_})}} ->
- Format.pp_print_string fmt name
+ | IPCodeAnnot {ica_ca={annot_content=AAssert (_, {tp_statement})}}
+ | IPCodeAnnot {ica_ca={annot_content=AInvariant (_, _, {tp_statement})}} ->
+ (match tp_statement.pred_name with
+ | name :: _ -> Format.pp_print_string fmt name
+ | [] -> pretty fmt p)
| IPCodeAnnot _ -> pretty fmt p
| IPAllocation {ial_kf} ->
Format.fprintf fmt "allocates/frees clause in function %a"
@@ -813,7 +821,7 @@ let rec pretty_debug fmt = function
Cil_types_debug.pp_string il_name
(Cil_types_debug.pp_list Cil_types_debug.pp_logic_label) il_labels
(Cil_types_debug.pp_list Cil_types_debug.pp_string) il_args
- Cil_types_debug.pp_predicate il_pred
+ Cil_types_debug.pp_toplevel_predicate il_pred
Cil_types_debug.pp_location il_loc
| IPAxiomatic {iax_name; iax_props} ->
Format.fprintf fmt "IPAxiomatic(%a,%a)"
@@ -824,7 +832,7 @@ let rec pretty_debug fmt = function
Cil_types_debug.pp_string il_name
(Cil_types_debug.pp_list Cil_types_debug.pp_logic_label) il_labels
(Cil_types_debug.pp_list Cil_types_debug.pp_string) il_args
- Cil_types_debug.pp_predicate il_pred
+ Cil_types_debug.pp_toplevel_predicate il_pred
Cil_types_debug.pp_location il_loc
| IPTypeInvariant {iti_name; iti_type; iti_pred; iti_loc} ->
Format.fprintf fmt "IPTypeInvariant(%a,%a,%a,%a)"
@@ -919,7 +927,8 @@ 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,pred) | AInvariant(for_bhv,_,pred) ->
+ let named_pred = pred.tp_statement in
let pp_for_bhv fmt l =
match l with
| [] -> ()
@@ -976,13 +985,13 @@ struct
| IPPredicate {ip_kind=pk;ip_kf=kf;ip_kinstr=ki;ip_pred=idp} ->
Format.asprintf "%s%s%a"
(kf_prefix kf) (predicate_kind_txt pk ki)
- pp_names idp.ip_content.pred_name
+ pp_names (Logic_const.pred_of_id_pred idp).pred_name
| IPExtended {ie_ext={ext_name};ie_loc=le} ->
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 (_, Assert, _) -> "assert"
- | AAssert (_, Check, _) -> "check"
+ | AAssert (_, {tp_only_check = false }) -> "assert"
+ | AAssert (_, {tp_only_check = true }) -> "check"
| AInvariant (_,true,_) -> "loop_inv"
| AInvariant _ -> "inv"
| APragma _ -> "pragma"
@@ -1003,10 +1012,10 @@ struct
| IPDecrease {id_kf=kf; id_variant=variant} ->
(kf_prefix kf) ^ "loop_term" ^ (variant_suffix variant)
| IPAxiom {il_name=name; il_pred} ->
- Format.asprintf "axiom_%s%a" name pp_names il_pred.pred_name
+ Format.asprintf "axiom_%s%a" name pp_names il_pred.tp_statement.pred_name
| IPAxiomatic {iax_name} -> "axiomatic_" ^ iax_name
| IPLemma {il_name=name; il_pred} ->
- Format.asprintf "lemma_%s%a" name pp_names il_pred.pred_name
+ Format.asprintf "lemma_%s%a" name pp_names il_pred.tp_statement.pred_name
| IPTypeInvariant {iti_name; iti_pred} ->
Format.asprintf "type_invariant_%s%a"
iti_name pp_names iti_pred.pred_name
@@ -1106,7 +1115,7 @@ struct
| K kf -> Sanitizer.add_string buffer (Kernel_function.get_name kf)
| A msg -> Sanitizer.add_string buffer msg
| S stmt -> Sanitizer.add_string buffer (Printf.sprintf "s%d" stmt.sid)
- | I { ip_content = { pred_name = a } }
+ | I { ip_content = { tp_statement = { pred_name = a } } }
| P { pred_name = a } | T { term_name = a } -> Sanitizer.add_list buffer a
let rec add_parts buffer = function
@@ -1125,17 +1134,35 @@ 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} ->
- [ K kf ; B bhv ; A "requires" ; I ip ]
+ let a =
+ if ip.ip_content.tp_only_check then "check_requires" else "requires"
+ in
+ [ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Normal); ip_kf=kf; ip_pred=ip} ->
- [ K kf ; B bhv ; A "ensures" ; I ip ]
+ let a =
+ if ip.ip_content.tp_only_check then "check_ensures" else "ensures"
+ in
+ [ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Exits); ip_kf=kf; ip_pred=ip} ->
- [ K kf ; B bhv ; A "exits" ; I ip ]
+ let a =
+ if ip.ip_content.tp_only_check then "check_exits" else "exits"
+ in
+ [ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Breaks); ip_kf=kf; ip_pred=ip} ->
- [ K kf ; B bhv ; A "breaks" ; I ip ]
+ let a =
+ if ip.ip_content.tp_only_check then "check_breaks" else "breaks"
+ in
+ [ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Continues); ip_kf=kf; ip_pred=ip} ->
- [ K kf ; B bhv ; A "continues" ; I ip ]
+ let a =
+ if ip.ip_content.tp_only_check then "check_continues" else "continues"
+ in
+ [ K kf ; B bhv ; A a ; I ip ]
| IPPredicate {ip_kind=PKEnsures (bhv, Returns); ip_kf=kf; ip_pred=ip} ->
- [ K kf ; B bhv ; A "returns" ; I ip ]
+ let a =
+ if ip.ip_content.tp_only_check then "check_returns" else "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 ]
@@ -1166,14 +1193,19 @@ struct
| IPCodeAnnot {ica_kf=kf; ica_stmt=stmt;
ica_ca={annot_content=AExtended (_, _, {ext_name})}} ->
[ K kf ; A ext_name ; S stmt ]
- | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AAssert (_, Assert,p)}} ->
- [K kf ; A "assert" ; P p ]
- | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AAssert (_, Check,p)}} ->
- [K kf ; A "check" ; P p ]
+ | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AAssert (_,p)}} ->
+ let a = if p.tp_only_check then "check" else "assert" in
+ [K kf ; A a ; P p.tp_statement ]
| IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AInvariant (_, true, p)}} ->
- [K kf ; A "loop_invariant" ; P p ]
- | IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AInvariant (_, false, p)}} ->
- [K kf ; A "invariant" ; P p ]
+ let a =
+ if p.tp_only_check then "check_loop_invariant" else "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
+ [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 ]
| IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AAssigns _}} ->
@@ -1199,7 +1231,8 @@ struct
| IPAxiomatic _
| IPAxiom _ -> []
| IPLemma {il_name=name; il_pred=p} ->
- [ A "lemma" ; A name ; P p ]
+ let a = if p.tp_only_check then "check_lemma" else "lemma" in
+ [ A a ; A name ; P p.tp_statement ]
| IPTypeInvariant {iti_name=name}
| IPGlobalInvariant {igi_name=name} ->
diff --git a/src/kernel_services/ast_data/property.mli b/src/kernel_services/ast_data/property.mli
index 02db66a05b03a21a453f145017b482ed89717c85..068d8a76fc1eecd8fcb0b31051f62a78e2024008 100644
--- a/src/kernel_services/ast_data/property.mli
+++ b/src/kernel_services/ast_data/property.mli
@@ -156,7 +156,7 @@ and identified_lemma = {
il_name : string;
il_labels : logic_label list;
il_args : string list;
- il_pred : predicate;
+ il_pred : toplevel_predicate;
il_loc : location
}
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index fbfc904dc2a8963412e321eaa01982d36048325e..a95db1207b8feca44ff8871dbcaab4fc81cc8378 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -2828,13 +2828,17 @@ 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 assumes fmt p =
fprintf fmt "@[<hov 2>%a@ %a;@]"
self#pp_acsl_keyword "assumes"
self#identified_predicate p
method requires fmt p =
- fprintf fmt "@[<hov 2>%a@ %a;@]"
+ fprintf fmt "@[<hov 2>%a%a@ %a;@]"
+ self#pp_only_check p.ip_content
self#pp_acsl_keyword "requires"
self#identified_predicate p
@@ -2846,7 +2850,8 @@ 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;@]"
+ fprintf fmt "@[<hov 2>%a%a@ %a;@]"
+ self#pp_only_check p.ip_content
self#pp_acsl_keyword kw
self#identified_predicate p
@@ -3053,16 +3058,12 @@ class cil_printer () = object (self)
(Pretty_utils.pp_list ~sep:",@ " pp_print_string) l
in
match ca.annot_content with
- | AAssert (behav,Assert,p) ->
+ | AAssert (behav,p) ->
+ let kw = if p.tp_only_check then "check" else "assert" in
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
+ self#pp_acsl_keyword kw
+ self#predicate p.tp_statement
| APragma (Slice_pragma sp) ->
fprintf fmt "@[%a@ %a;@]"
self#pp_acsl_keyword "slice pragma"
@@ -3088,15 +3089,17 @@ class cil_printer () = object (self)
pp_for_behavs behav
(self#allocation ~isloop:true) af
| AInvariant(behav,true, i) ->
- fprintf fmt "@[<2>%a%a@ %a;@]"
+ fprintf fmt "@[<2>%a%a%a@ %a;@]"
pp_for_behavs behav
+ self#pp_only_check i
self#pp_acsl_keyword "loop invariant"
- self#predicate i
+ self#predicate i.tp_statement
| AInvariant(behav,false,i) ->
- fprintf fmt "@[<2>%a%a@ %a;@]"
+ fprintf fmt "@[<2>%a%a%a@ %a;@]"
pp_for_behavs behav
+ self#pp_only_check i
self#pp_acsl_keyword "invariant"
- self#predicate i
+ self#predicate i.tp_statement
| AVariant v ->
self#variant fmt v
| AExtended (behav, is_loop, e) ->
@@ -3186,7 +3189,8 @@ class cil_printer () = object (self)
| Dlemma(name, is_axiom, labels, tvars, pred, _attr, _) ->
(* 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:@]@ %t%a;@]@\n"
+ fprintf fmt "@[<hv 2>@[<hov 1>%a%a %a%a%a:@]@ %t%a;@]@\n"
+ self#pp_only_check pred
self#pp_acsl_keyword (if is_axiom then "axiom" else "lemma")
self#varname name
self#labels labels
@@ -3197,7 +3201,7 @@ class cil_printer () = object (self)
the pretty-printing of labels, and before pretty-printing predicate
*)
(fun _ -> (match labels with [l] -> current_label <- l | _ -> ()))
- self#predicate pred;
+ self#predicate pred.tp_statement;
current_label <- old_lab
| Dtype (ti,_) ->
fprintf fmt "@[<hv 2>@[%a %a%a%a;@]@\n"
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 0b4be0a9ac93ec2a8d93fb8a07047eaf2ff7a62e..cca0b496be8e8135493306671bf2202391f9ba2c 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -881,7 +881,13 @@ and pp_predicate_node fmt = function
and pp_identified_predicate fmt identified_predicate =
Format.fprintf fmt "{ip_id=%d;ip_content=%a}"
- identified_predicate.ip_id pp_predicate identified_predicate.ip_content
+ identified_predicate.ip_id
+ pp_toplevel_predicate identified_predicate.ip_content
+
+and pp_toplevel_predicate fmt toplevel_predicate =
+ Format.fprintf fmt "{tp_only_check=%B;tp_statement=%a}"
+ toplevel_predicate.tp_only_check
+ pp_predicate toplevel_predicate.tp_statement
and pp_predicate fmt predicate = Format.fprintf fmt "{%a%apred_content=%a}"
(pp_if_list_not_empty "pred_name=" ";" (pp_list pp_string)) predicate.pred_name
@@ -960,17 +966,16 @@ and pp_pragma fmt = function
| Impact_pragma(term) ->
Format.fprintf fmt "Impact_pragma(%a)" pp_impact_pragma 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,kind,predicate) ->
- Format.fprintf fmt "AAssert(%a,%a,%a)" (pp_list pp_string) string_list pp_assertion_kind kind pp_predicate predicate
+ | AAssert(string_list,p) ->
+ Format.fprintf fmt "AAssert(%a,%a)"
+ (pp_list pp_string) string_list
+ pp_toplevel_predicate p
| AStmtSpec(string_list,spec) ->
Format.fprintf fmt "AStmtSpec(%a,%a)" (pp_list pp_string) string_list pp_spec spec
- | AInvariant(string_list,bool,predicate) ->
- Format.fprintf fmt "AInvariant(%a,%a,%a)" (pp_list pp_string) string_list pp_bool bool pp_predicate predicate
+ | AInvariant(string_list,bool,p) ->
+ Format.fprintf fmt "AInvariant(%a,%a,%a)"
+ (pp_list pp_string) string_list pp_bool bool pp_toplevel_predicate p
| AVariant(term_variant) ->
Format.fprintf fmt "AVariant(%a)" pp_variant term_variant
| AAssigns(string_list,assigns) ->
@@ -1010,7 +1015,8 @@ and pp_global_annotation fmt = function
| Dlemma(string,bool,logic_label_list,string_list,predicate,attributes,location) ->
Format.fprintf fmt "Dlemma(%a,%a,%a,%a,%a,%a,%a)" pp_string string pp_bool bool
(pp_list pp_logic_label) logic_label_list (pp_list pp_string) string_list
- pp_predicate predicate pp_attributes attributes pp_location location
+ pp_toplevel_predicate predicate
+ pp_attributes attributes pp_location location
| Dinvariant(logic_info,location) ->
Format.fprintf fmt "Dinvariant(%a,%a)" pp_logic_info logic_info pp_location location
| Dtype_annot(logic_info,location) ->
diff --git a/src/kernel_services/ast_printing/cil_types_debug.mli b/src/kernel_services/ast_printing/cil_types_debug.mli
index c9f1318b512cc8430d085f7c53b4fb8392bcb099..b64e8fbfebde6a2bb71a95224180bbcdb9f135ac 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.mli
+++ b/src/kernel_services/ast_printing/cil_types_debug.mli
@@ -135,6 +135,7 @@ val pp_quantifiers : Format.formatter -> Cil_types.quantifiers -> unit
val pp_relation : Format.formatter -> Cil_types.relation -> unit
val pp_predicate_node : Format.formatter -> Cil_types.predicate_node -> unit
val pp_identified_predicate : Format.formatter -> Cil_types.identified_predicate -> unit
+val pp_toplevel_predicate: Format.formatter -> Cil_types.toplevel_predicate -> unit
val pp_predicate : Cil_types.predicate Pretty_utils.formatter
val pp_spec : Format.formatter -> Cil_types.spec -> unit
val pp_acsl_extension : Format.formatter -> Cil_types.acsl_extension -> unit
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index 47add398d3dbb5684c85af5f42351c50b8090032..4f152488f0b06c8f5ec161379b09408d0bb47bda 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -54,7 +54,7 @@ let pp_labels fmt stmt =
| ls -> Format.fprintf fmt " '%s'" (String.concat "," ls)
let pp_idpred kloc fmt idpred =
- let np = idpred.ip_content in
+ let np = Logic_const.pred_of_id_pred idpred in
if np.pred_name <> []
then Format.fprintf fmt " '%s'" (String.concat "," np.pred_name)
else pp_kloc kloc fmt np.pred_loc
@@ -110,14 +110,16 @@ let pp_named fmt nx =
if nx.pred_name <> [] then
Format.fprintf fmt " '%s'" (String.concat "," nx.pred_name)
+let pp_top fmt tp = pp_named fmt tp.tp_statement
+
let pp_code_annot fmt ca =
match ca.annot_content with
- | 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
+ | 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
+ | 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
| AAllocation(bs,_) -> Format.fprintf fmt "allocates_frees%a" pp_for bs
| APragma _ -> Format.pp_print_string fmt "pragma"
@@ -253,21 +255,22 @@ 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,Assert,np)}} ->
+ | 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_named np
- (pp_kloc kloc) np.pred_loc
- | IPCodeAnnot {ica_ca={annot_content=AAssert(bs,Check,np)}} ->
+ 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"
pp_for bs
- pp_named np
- (pp_kloc kloc) np.pred_loc
- | IPCodeAnnot {ica_ca={annot_content=AInvariant(bs,_,np)}} ->
+ pp_top tp
+ (pp_kloc kloc) tp.tp_statement.pred_loc
+ | IPCodeAnnot {ica_ca={annot_content=AInvariant(bs,_,tp)}} ->
Format.fprintf fmt "Invariant%a%a%a"
pp_for bs
- pp_named np
- (pp_kloc kloc) np.pred_loc
+ pp_top tp
+ (pp_kloc kloc) tp.tp_statement.pred_loc
| IPCodeAnnot {ica_ca={annot_content=AExtended(bs,_,{ext_name})};ica_stmt} ->
Format.fprintf fmt "%a%a %a"
pp_capitalize ext_name pp_for bs (pp_stmt kloc) ica_stmt
@@ -360,18 +363,16 @@ let to_string pp elt =
Buffer.contents b
let code_annot_kind_and_node code_annot = match code_annot.annot_content with
- | AAssert (_, kind, {pred_content; pred_name}) ->
+ | AAssert (_, {tp_only_check; 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 match kind with
- | Assert -> "user assertion"
- | Check -> "user check"
+ if List.exists ((=) "missing_return") pred_name then "missing_return"
+ else if tp_only_check then "user check"
+ else "user assertion"
in
Some (kind, to_string Printer.pp_predicate_node pred_content)
- | AInvariant (_, _, {pred_content}) ->
+ | AInvariant (_, _, {tp_statement = {pred_content}}) ->
Some ("loop invariant", to_string Printer.pp_predicate_node pred_content)
| _ -> None
@@ -471,12 +472,12 @@ let for_order k = function
| [] -> [I k]
| bs -> I (succ k) :: named_order bs
let annot_order = function
- | {annot_content=AAssert(bs,Check,np)} ->
- for_order 0 bs @ named_order np.pred_name
- | {annot_content=AAssert(bs,Assert,np)} ->
- for_order 2 bs @ named_order np.pred_name
- | {annot_content=AInvariant(bs,_,np)} ->
- for_order 4 bs @ named_order np.pred_name
+ | {annot_content=AAssert(bs,tp)} when tp.tp_only_check ->
+ for_order 0 bs @ named_order tp.tp_statement.pred_name
+ | {annot_content=AAssert(bs,tp)} ->
+ for_order 2 bs @ named_order tp.tp_statement.pred_name
+ | {annot_content=AInvariant(bs,_,tp)} ->
+ for_order 4 bs @ named_order tp.tp_statement.pred_name
| _ -> [I 6]
let loop_order = function
| Id_contract (active,b) -> [B b; A active]
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index fca0da4953174ea419fd0fe96a21a520e7a80f18..1b3c0544fc39e38fce56da4f47fe2a8dae606f60 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -356,11 +356,12 @@ let rec print_decl fmt d =
(pp_list ~sep:",@ " print_typed_ident) prms
(pp_list ~sep:"@\n" print_case) cases
| LDlemma(name,is_axiom,labels,tvar,body) ->
- fprintf fmt "@[<2>%a@ %s%a%a:@ %a;@]"
+ fprintf fmt "@[<2>%s%a@ %s%a%a:@ %a;@]"
+ (if body.tp_only_check then "check " else "")
(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
- print_lexpr body
+ print_lexpr body.tp_statement
| LDaxiomatic (s,d) ->
fprintf fmt "@[<2>axiomatic@ %s@ {@\n%a@]@\n}" s
(pp_list ~sep:"@\n" print_decl) d
@@ -409,14 +410,18 @@ 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
+ print_clause name fmt e.tp_statement
+
let print_post fmt (k,e) =
- print_clause (Cil_printer.get_termination_kind_name k) fmt e
+ print_tp_clause (Cil_printer.get_termination_kind_name k) fmt e
let print_behavior fmt bhv =
fprintf fmt "@[<2>behavior@ %s:%a%a%a%a%a@]"
bhv.b_name
(pp_list ~pre:"" ~suf:"" (print_clause "assumes")) bhv.b_assumes
- (pp_list ~pre:"" ~suf:"" (print_clause "requires")) bhv.b_requires
+ (pp_list ~pre:"" ~suf:"" (print_tp_clause "requires")) bhv.b_requires
(pp_list ~pre:"" ~suf:"" print_post) bhv.b_post_cond
(print_allocation ~isloop:false) bhv.b_allocation
print_assigns bhv.b_assigns
@@ -463,10 +468,6 @@ 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
@@ -475,16 +476,21 @@ let print_code_annot fmt ca =
(pp_list ~pre:"for@ " ~sep:",@ " ~suf:":@ " pp_print_string) fmt bhvs
in
match ca with
- AAssert(bhvs,kind,e) ->
- fprintf fmt "%a%a@ %a;"
- print_behaviors bhvs print_assertion_kind kind print_lexpr e
+ AAssert(bhvs,e) ->
+ fprintf fmt "%a%s@ %a;"
+ print_behaviors bhvs
+ (if e.tp_only_check then "check" else "assert")
+ 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%ainvariant@ %a;"
- print_behaviors bhvs (pp_cond loop) "loop@ " print_lexpr e
+ fprintf fmt "%a%a%ainvariant@ %a;"
+ print_behaviors bhvs
+ (pp_cond e.tp_only_check) "check @"
+ (pp_cond loop) "loop@ "
+ print_lexpr e.tp_statement
| AVariant e -> fprintf fmt "loop@ variant@ %a;" print_variant e
| AAssigns (bhvs,a) ->
fprintf fmt "%aloop@ %a" print_behaviors bhvs print_assigns a
diff --git a/src/kernel_services/ast_printing/printer.ml b/src/kernel_services/ast_printing/printer.ml
index 336d08c7b428d42fdadd796b4ff037804b02f3d0..aaaf74c2fd22f90d4cffa88e0bb00867fa28f71d 100644
--- a/src/kernel_services/ast_printing/printer.ml
+++ b/src/kernel_services/ast_printing/printer.ml
@@ -288,6 +288,7 @@ let () = Cil_datatype.Logic_label.pretty_ref := pp_logic_label
let () = Cil_datatype.Global_annotation.pretty_ref := pp_global_annotation
let () = Cil_datatype.Global.pretty_ref := pp_global
let () = Cil_datatype.Predicate.pretty_ref := pp_predicate
+let () = Cil_datatype.Toplevel_predicate.pretty_ref := pp_toplevel_predicate
let () = Cil_datatype.Identified_predicate.pretty_ref := pp_identified_predicate
let () = Cil_datatype.Fundec.pretty_ref := pp_fundec
diff --git a/src/kernel_services/ast_printing/printer_api.mli b/src/kernel_services/ast_printing/printer_api.mli
index 428ff0df997022496c722540f5228eb284e5f2dd..566723c11c7ea5cc3fe179211b78ce2716e687ae 100644
--- a/src/kernel_services/ast_printing/printer_api.mli
+++ b/src/kernel_services/ast_printing/printer_api.mli
@@ -451,6 +451,8 @@ module type S_pp = sig
(** @since 21.0-Scandium *)
val pp_predicate_node: Format.formatter -> predicate_node -> unit
val pp_predicate: Format.formatter -> predicate -> unit
+ val pp_toplevel_predicate: Format.formatter -> toplevel_predicate -> unit
+ (** @since Frama-C+dev *)
val pp_identified_predicate: Format.formatter -> identified_predicate -> unit
val pp_code_annotation: Format.formatter -> code_annotation -> unit
val pp_funspec: Format.formatter -> funspec -> unit
diff --git a/src/kernel_services/ast_printing/printer_builder.ml b/src/kernel_services/ast_printing/printer_builder.ml
index beb17790e42b8bf9968b5368d8831d6edda3297b..94ef3b64e1f6d32232daf0ac0ef9174300f5b942 100644
--- a/src/kernel_services/ast_printing/printer_builder.ml
+++ b/src/kernel_services/ast_printing/printer_builder.ml
@@ -65,6 +65,8 @@ struct
let pp_term_offset fmt x = (printer ())#term_offset fmt x
let pp_predicate_node fmt x = (printer ())#predicate_node fmt x
let pp_predicate fmt x = (printer ())#predicate fmt x
+ let pp_toplevel_predicate fmt x =
+ (printer())#predicate fmt x.Cil_types.tp_statement
let pp_identified_predicate fmt x = (printer ())#identified_predicate fmt x
let pp_code_annotation fmt x = (printer ())#code_annotation fmt x
let pp_funspec fmt x = (printer ())#funspec fmt x
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 544e912ca692472f847d2aa060ffd96c604f2c19..2ca9b6460174ddb4e2a31eaa05cb845814feaaec 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -1769,9 +1769,14 @@ and visitCilPredicate vis p =
doVisitCil vis
id vis#vpredicate childrenPredicate p
+and visitCilToplevel_predicate vis p =
+ let s = p.tp_statement in
+ let s' = visitCilPredicate vis s in
+ if s != s' then { p with tp_statement = s' } else p
+
and childrenIdentified_predicate vis ip =
let p = ip.ip_content in
- let p' = visitCilPredicate vis p in
+ let p' = visitCilToplevel_predicate vis p in
if p != p' then { ip with ip_content = p' }
else ip
@@ -2089,7 +2094,7 @@ and childrenAnnotation vis a =
vis#get_filling_actions;
if ti' != ti then Dtype (ti',loc) else a
| Dlemma(s,is_axiom,labels,tvars,p,attr,loc) ->
- let p' = visitCilPredicate vis p in
+ let p' = visitCilToplevel_predicate vis p in
let attr' = visitCilAttributes vis attr in
if p' != p || attr != attr' then
Dlemma(s,is_axiom,labels,tvars,p',attr',loc)
@@ -2142,14 +2147,14 @@ and visitCilCodeAnnotation vis ca =
vis (Visitor_behavior.ccode_annotation vis#behavior) vis#vcode_annot childrenCodeAnnot ca
and childrenCodeAnnot vis ca =
- let vPred p = visitCilPredicate vis p in
+ let vPred p = visitCilToplevel_predicate vis p in
let vTerm t = visitCilTerm vis t in
let vSpec s = visitCilFunspec vis s in
let change_content annot = { ca with annot_content = annot } in
match ca.annot_content with
- AAssert (behav,kind,p) ->
+ AAssert (behav,p) ->
let p' = vPred p in if p' != p then
- change_content (AAssert (behav,kind,p'))
+ change_content (AAssert (behav,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 c9f743a32f6e55252fbed085583b467a45c07492..cd957175947d1393dee11370e9ebb96f9d4cea10 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -2235,8 +2235,8 @@ module Code_annotation = struct
end)
let loc ca = match ca.annot_content with
- | AAssert(_,_,{pred_loc=loc})
- | AInvariant(_,_,{pred_loc=loc})
+ | AAssert(_,{ tp_statement = {pred_loc=loc}})
+ | AInvariant(_,_,{tp_statement = {pred_loc=loc}})
| AVariant({term_loc=loc},_) -> Some loc
| AAssigns _ | AAllocation _ | APragma _ | AExtended _
| AStmtSpec _ -> None
@@ -2259,6 +2259,20 @@ module Predicate = struct
end)
end
+module Toplevel_predicate = struct
+ let pretty_ref = ref (fun _ _ -> assert false)
+ include Make
+ (struct
+ type t = toplevel_predicate
+ let name = "Toplevel_predicate"
+ let reprs =
+ [ { tp_statement = List.hd Predicate.reprs; tp_only_check = false }]
+ let internal_pretty_code = Datatype.undefined
+ let pretty fmt x = !pretty_ref fmt x
+ let varname _ = "p"
+ end)
+end
+
module Identified_predicate = struct
let pretty_ref = ref (fun _ _ -> assert false)
include Make_with_collections
@@ -2266,7 +2280,7 @@ module Identified_predicate = struct
type t = identified_predicate
let name = "Identified_predicate"
let reprs =
- [ { ip_content = List.hd Predicate.reprs; ip_id = -1} ]
+ [ { ip_content = List.hd Toplevel_predicate.reprs; ip_id = -1} ]
let compare x y = Extlib.compare_basic x.ip_id y.ip_id
let equal x y = x.ip_id = y.ip_id
let copy = Datatype.undefined
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index 52f914d8ebe394785d5d998afbe9cf7e640a7e0b..34041802d4ba1afa79f34415c0e9c707818f0331 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -293,6 +293,7 @@ module Term_lval: S_with_collections_pretty with type t = term_lval
module Logic_real: S_with_collections_pretty with type t = logic_real
module Predicate: S_with_pretty with type t = predicate
+module Toplevel_predicate: S_with_pretty with type t = toplevel_predicate
module Identified_predicate:
S_with_collections_pretty with type t = identified_predicate
(** @since Neon-20140301 *)
diff --git a/src/kernel_services/ast_queries/filecheck.ml b/src/kernel_services/ast_queries/filecheck.ml
index c6214a4461ba9731be1ba117c42aa38093129d4c..2eb9c7560b2bd1dd8164cb4cffc039614fca390a 100644
--- a/src/kernel_services/ast_queries/filecheck.ml
+++ b/src/kernel_services/ast_queries/filecheck.ml
@@ -650,7 +650,7 @@ module Base_checker = struct
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_const.ml b/src/kernel_services/ast_queries/logic_const.ml
index 8ee64b0b36651d60f18a87251d73e9db53d5a161..861d64099492abe32e3cc6026ce0eee7beba3c1f 100644
--- a/src/kernel_services/ast_queries/logic_const.ml
+++ b/src/kernel_services/ast_queries/logic_const.ml
@@ -43,12 +43,15 @@ let new_code_annotation annot =
let fresh_code_annotation = AnnotId.next
-let new_predicate p =
- { ip_id = PredicateId.next (); ip_content = p }
+let toplevel_predicate ?(only_check=false) p =
+ { tp_only_check = only_check; tp_statement = p }
+
+let new_predicate ?only_check p =
+ { ip_id = PredicateId.next (); ip_content = toplevel_predicate ?only_check p }
let fresh_predicate_id = PredicateId.next
-let pred_of_id_pred p = p.ip_content
+let pred_of_id_pred p = p.ip_content.tp_statement
let refresh_predicate p = { p with ip_id = PredicateId.next () }
diff --git a/src/kernel_services/ast_queries/logic_const.mli b/src/kernel_services/ast_queries/logic_const.mli
index 51759d05c132490f56e7b7a7644677cc944c9fac..9079513585804f3b4d54d1c4052eb7b30f392675 100644
--- a/src/kernel_services/ast_queries/logic_const.mli
+++ b/src/kernel_services/ast_queries/logic_const.mli
@@ -46,8 +46,19 @@ val refresh_code_annotation: code_annotation -> code_annotation
*)
val refresh_spec: funspec -> funspec
-(** creates a new identified predicate with a fresh id. *)
-val new_predicate: predicate -> identified_predicate
+(** 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.
+ @since Frama-C+dev
+*)
+val toplevel_predicate: ?only_check:bool -> predicate -> toplevel_predicate
+
+(** creates a new identified predicate with a fresh id.
+ @modify Frama-C+dev add [only_check] optional parameter
+ *)
+val new_predicate: ?only_check:bool -> predicate -> identified_predicate
(** creates a new acsl_extension with a fresh id.
@plugin development guide
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index d0298228e25e382a6a140398d4a14ec0fd524f7b..70e213f6bdc137f92f134cfdfb75dee1e8cedf71 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -3513,6 +3513,10 @@ 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 id_term_ptr env t =
let loc = t.lexpr_loc in
let t = term env t in
@@ -3675,11 +3679,12 @@ struct
~type_assigns:type_assign
in
let b_assumes = List.map (id_predicate env) bas in
- let b_requires= List.map (id_predicate env) br in
+ let b_requires= List.map (id_predicate_top env) br in
let b_post_cond =
List.map
(fun (k,p)->
- let p' = id_predicate (post_state_env k) p in (k,p')) be
+ let p' = id_predicate_top (post_state_env k) p in (k,p'))
+ be
in
let b_assigns =
type_assign typing_context ~accept_formal:is_stmt_contract assigns_env ba
@@ -3773,15 +3778,14 @@ 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,k,p) ->
+ | AAssert (behav,{tp_only_check=only_check; tp_statement = p}) ->
check_behavior_names loc current_behaviors behav;
- Cil_types.AAssert(behav,assertion_kind k,predicate (code_annot_env()) p)
+ let p = predicate (code_annot_env()) p in
+ let p = Logic_const.toplevel_predicate ~only_check p in
+ Cil_types.AAssert(behav,p)
| APragma (Impact_pragma sp) ->
Cil_types.APragma
(Cil_types.Impact_pragma (impact_pragma (code_annot_env()) sp))
@@ -3807,10 +3811,11 @@ struct
Cil_types.AStmtSpec (behav,my_spec)
| AVariant v ->
Cil_types.AVariant (type_variant (loop_annot_env ()) v)
- | AInvariant (behav,f,i) ->
+ | AInvariant (behav,f,{ tp_only_check = only_check; tp_statement = i}) ->
let env = if f then loop_annot_env () else code_annot_env () in
check_behavior_names loc current_behaviors behav;
- Cil_types.AInvariant (behav,f,predicate env i)
+ let p = Logic_const.toplevel_predicate ~only_check (predicate env i) in
+ Cil_types.AInvariant (behav,f,p)
| AAllocation (behav,fa) ->
check_behavior_names loc current_behaviors behav;
Cil_types.AAllocation(behav,
@@ -4116,7 +4121,8 @@ 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, e) ->
+ | LDlemma (x,is_axiom, labels, poly,
+ { tp_only_check = only_check; 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
@@ -4132,7 +4138,7 @@ struct
Cil_datatype.Location.pretty old_loc
end;
let labels,env = annot_env loc labels poly in
- let p = predicate env e in
+ let p = Logic_const.toplevel_predicate ~only_check (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 242feb6c6a054e09f4016d0168be57a3e4a9c38f..019913fdd973d36c15460410bd7cbe9669db5220 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -129,7 +129,7 @@ let coerce_type typ =
else if Cil.isFloatingType ty then Lreal
else Ctype typ
-let predicate_of_identified_predicate ip = ip.ip_content
+let predicate_of_identified_predicate ip = ip.ip_content.tp_statement
let translate_old_label s p =
let get_label () =
@@ -1025,8 +1025,13 @@ and is_same_predicate pred1 pred2 =
is_same_list Datatype.String.equal pred1.pred_name pred2.pred_name &&
is_same_predicate_node pred1.pred_content pred2.pred_content
+
+and is_same_toplevel_predicate p1 p2 =
+ p1.tp_only_check = p2.tp_only_check &&
+ is_same_predicate p1.tp_statement p2.tp_statement
+
and is_same_identified_predicate p1 p2 =
- is_same_predicate p1.ip_content p2.ip_content
+ is_same_toplevel_predicate p1.ip_content p2.ip_content
and is_same_identified_term l1 l2 =
is_same_term l1.it_content l2.it_content
@@ -1130,12 +1135,12 @@ let is_same_extension x1 x2 =
let is_same_code_annotation (ca1:code_annotation) (ca2:code_annotation) =
match ca1.annot_content, ca2.annot_content with
- | AAssert(l1,k1,p1), AAssert(l2,k2,p2) ->
- is_same_list (=) l1 l2 && k1 = k2 && is_same_predicate p1 p2
+ | AAssert(l1,p1), AAssert(l2,p2) ->
+ is_same_list (=) l1 l2 && is_same_toplevel_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) ->
- is_same_list (=) l1 l2 && b1 = b2 && is_same_predicate p1 p2
+ is_same_list (=) l1 l2 && b1 = b2 && is_same_toplevel_predicate p1 p2
| AVariant v1, AVariant v2 -> is_same_variant v1 v2
| AAssigns(l1,a1), AAssigns(l2,a2) ->
is_same_list (=) l1 l2 && is_same_assigns a1 a2
@@ -1165,7 +1170,7 @@ let rec is_same_global_annotation ga1 ga2 =
Dlemma(n2,ax2,labs2,typs2,st2,attr2,_) ->
is_same_string n1 n2 && ax1 = ax2 &&
is_same_list is_same_logic_label labs1 labs2 &&
- is_same_list (=) typs1 typs2 && is_same_predicate st1 st2 &&
+ is_same_list (=) typs1 typs2 && is_same_toplevel_predicate st1 st2 &&
is_same_attributes attr1 attr2
| Dinvariant (li1,_), Dinvariant (li2,_) -> is_same_logic_info li1 li2
| Dtype_annot (li1,_), Dtype_annot (li2,_) -> is_same_logic_info li1 li2
@@ -2158,10 +2163,10 @@ let lhost_c_type thost =
| TResult ty -> ty
let is_assert ca =
- match ca.annot_content with AAssert (_, Assert, _) -> true | _ -> false
+ match ca.annot_content with AAssert (_, p) -> not p.tp_only_check | _ -> false
let is_check ca =
- match ca.annot_content with AAssert (_, Check, _) -> true | _ -> false
+ match ca.annot_content with AAssert (_, p) -> p.tp_only_check | _ -> false
let is_contract ca =
match ca.annot_content with AStmtSpec _ -> true | _ -> false
@@ -2205,7 +2210,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.tp_statement
| APragma _ | AStmtSpec _ | AInvariant _ | AVariant _
| AAssigns _| AAllocation _ | AExtended _
-> false
diff --git a/src/kernel_services/ast_transformations/filter.ml b/src/kernel_services/ast_transformations/filter.ml
index caff6cef46efa2b4fe32181dfc5868163ff6509d..d36b2cf000fee0b47bff693060a297d72a290f9f 100644
--- a/src/kernel_services/ast_transformations/filter.ml
+++ b/src/kernel_services/ast_transformations/filter.ml
@@ -448,9 +448,12 @@ end = struct
Printer.pp_code_annotation v;
ChangeTo
(Logic_const.new_code_annotation
- (AAssert ([], Assert,
- { pred_name = []; pred_loc = Cil_datatype.Location.unknown;
- pred_content = Ptrue})))
+ (AAssert
+ ([],
+ Logic_const.toplevel_predicate
+ { pred_name = [];
+ pred_loc = Cil_datatype.Location.unknown;
+ pred_content = Ptrue})))
end
method private process_call is_init_call call_stmt lval _f args loc =
@@ -714,7 +717,8 @@ end = struct
method private visit_pred p =
Logic_const.new_predicate
- (visitCilPredicate (self:>Cil.cilVisitor) p.ip_content)
+ (visitCilPredicate (self:>Cil.cilVisitor)
+ (Logic_const.pred_of_id_pred p))
method private visit_identified_term t =
let t' = visitCilTerm (self:>Cil.cilVisitor) t.it_content in
@@ -733,11 +737,15 @@ end = struct
method! vbehavior b =
let finfo = self#get_finfo () in
- let pre_visible p = Info.fun_precond_visible finfo p.ip_content in
+ let pre_visible p =
+ Info.fun_precond_visible finfo (Logic_const.pred_of_id_pred p)
+ in
b.b_assumes <- filter_list pre_visible self#visit_pred b.b_assumes;
b.b_requires <- filter_list pre_visible self#visit_pred b.b_requires;
- let ensure_visible (_,p) = Info.fun_postcond_visible finfo p.ip_content in
+ let ensure_visible (_,p) =
+ Info.fun_postcond_visible finfo (Logic_const.pred_of_id_pred p)
+ in
b.b_post_cond <-
filter_list ensure_visible (fun (k,p) -> k,self#visit_pred p)
b.b_post_cond;
@@ -785,7 +793,7 @@ end = struct
let new_term = match spec.spec_terminates with
| None -> None
| Some p ->
- if Info.fun_precond_visible finfo p.ip_content
+ if Info.fun_precond_visible finfo (Logic_const.pred_of_id_pred p)
then Some (self#visit_pred p)
else None
in
diff --git a/src/kernel_services/parsetree/cabshelper.mli b/src/kernel_services/parsetree/cabshelper.mli
index a4b0498146e4bce7b14fa47a60c7adf8d615981e..458c01febc4a9f2eb6b482b78cd1d48e7dda3ab8 100644
--- a/src/kernel_services/parsetree/cabshelper.mli
+++ b/src/kernel_services/parsetree/cabshelper.mli
@@ -80,8 +80,9 @@ val is_attr_test: unit -> bool
val mk_behavior :
?name:string ->
?assumes:Logic_ptree.lexpr list ->
- ?requires:Logic_ptree.lexpr list ->
- ?post_cond:(Cil_types.termination_kind * Logic_ptree.lexpr) list ->
+ ?requires:Logic_ptree.toplevel_predicate list ->
+ ?post_cond:
+ (Cil_types.termination_kind * Logic_ptree.toplevel_predicate) list ->
?assigns:Logic_ptree.assigns ->
?allocation:Logic_ptree.allocation ->
?extended:Logic_ptree.extension list ->
diff --git a/src/kernel_services/parsetree/logic_ptree.mli b/src/kernel_services/parsetree/logic_ptree.mli
index adde2634144cb07084ca310b5ea944ea7ed119c8..bff3332bb8dff7075b6aedd448b7caecbfb70469 100644
--- a/src/kernel_services/parsetree/logic_ptree.mli
+++ b/src/kernel_services/parsetree/logic_ptree.mli
@@ -161,6 +161,7 @@ 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 extension = string * lexpr list
@@ -231,7 +232,7 @@ and decl_node =
(** [LDinductive_def(name,labels,type_params, parameters, indcases)]
represents an inductive definition of a new predicate.
*)
- | LDlemma of string * bool * string list * string list * lexpr
+ | LDlemma of string * bool * string list * string list * toplevel_predicate
(** LDlemma(name,is_axiom,labels,type_params,property) represents
a lemma or an axiom [name].
[is_axiom] is true for an axiom and false for a lemma. [labels]
@@ -276,9 +277,11 @@ and variant = lexpr * string option
with {!Cil_types.behavior}. *)
type behavior = {
mutable b_name : string; (** name of the behavior. *)
- mutable b_requires : lexpr list; (** require clauses. *)
+ mutable b_requires : toplevel_predicate list; (** require clauses. *)
mutable b_assumes : lexpr list; (** assume clauses. *)
- mutable b_post_cond : (Cil_types.termination_kind * lexpr) list; (** post-condition. *)
+ mutable b_post_cond :
+ (Cil_types.termination_kind * toplevel_predicate) list;
+ (** post-condition. *)
mutable b_assigns : assigns; (** assignments. *)
mutable b_allocation : allocation; (** frees, allocates. *)
mutable b_extended : extension list (** extensions *)
@@ -329,13 +332,10 @@ 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 * assertion_kind * lexpr
+ | AAssert of string list * toplevel_predicate
(** assertion to be checked. The list of strings is the list of
behaviors to which this assertion applies. *)
@@ -343,7 +343,7 @@ type code_annot =
(** statement contract
(potentially restricted to some enclosing behaviors). *)
- | AInvariant of string list * bool * lexpr
+ | AInvariant of string list * bool * toplevel_predicate
(** loop/code invariant. The list of strings is the list of behaviors to which
this invariant applies. The boolean flag is true for normal loop
invariants and false for invariant-as-assertions. *)
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index c4fb25191c1f4b7f166ad3666763e6eff90a1aa1..8ace0513ae632217120f86caaa07cee32e0dd722 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -957,6 +957,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 name = state.Promelaast.name ^ "_deterministic_trans" in
let lemma =
Dlemma (name, false, [label],[],prop,[],Cil_datatype.Location.unknown)
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 004941db6742cd482c8910fc0e7a1d3f3d0f197a..0bffbd505a4068b3530c5d266d90200595322839 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -460,6 +460,7 @@ let get_unchanged_aux_var loc current_state =
class visit_adding_pre_post_from_buch treatloops =
let predicate_to_invariant kf stmt pred =
+ let pred = Logic_const.toplevel_predicate pred in
Annotations.add_code_annot
Aorai_option.emitter
~kf
diff --git a/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle b/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle
index 2434556b05d580bac96d12dfa195f2e84cc9ee09..1ae6c45cb17fbe316a8edc9df3ce59f761d38989 100644
--- a/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle
@@ -18,15 +18,15 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ lemma in_main_deterministic_trans{L}: \true;
+/*@ check lemma in_main_deterministic_trans{L}: \true;
*/
-/*@ lemma Sf_deterministic_trans{L}: \true;
+/*@ check lemma Sf_deterministic_trans{L}: \true;
*/
-/*@ lemma S_in_f_deterministic_trans{L}: \true;
+/*@ check lemma S_in_f_deterministic_trans{L}: \true;
*/
-/*@ lemma S2_deterministic_trans{L}: \true;
+/*@ check lemma S2_deterministic_trans{L}: \true;
*/
-/*@ lemma S1_deterministic_trans{L}: \true;
+/*@ check lemma S1_deterministic_trans{L}: \true;
*/
int X;
/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
diff --git a/src/plugins/aorai/tests/aorai/oracle/declared_function.res.oracle b/src/plugins/aorai/tests/aorai/oracle/declared_function.res.oracle
index f30827619507d6a1d3244f24cb2af9416e749eb3..9d37fe0b6442bed85a03f3b4a22d895bf153f3ca 100644
--- a/src/plugins/aorai/tests/aorai/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/declared_function.res.oracle
@@ -19,7 +19,7 @@ int f(void);
/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
/*@
-lemma I_deterministic_trans{L}:
+check lemma I_deterministic_trans{L}:
(∀ int __retres_f;
¬(\at(aorai_CurOperation,L) ≡ op_f ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
diff --git a/src/plugins/aorai/tests/aorai/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/aorai/oracle/deterministic.res.oracle
index 37d537ca5af54b6e147169cb5a78c9903dc749fb..75acb9204ee5a6aee059455def9e02c64419a037 100644
--- a/src/plugins/aorai/tests/aorai/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/deterministic.res.oracle
@@ -23,22 +23,22 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ lemma Si_deterministic_trans{L}: \true;
+/*@ check lemma Si_deterministic_trans{L}: \true;
*/
-/*@ lemma Sf_deterministic_trans{L}: \true;
+/*@ check lemma Sf_deterministic_trans{L}: \true;
*/
-/*@ lemma S5_deterministic_trans{L}: \true;
+/*@ check lemma S5_deterministic_trans{L}: \true;
*/
-/*@ lemma S4_deterministic_trans{L}: \true;
+/*@ check lemma S4_deterministic_trans{L}: \true;
*/
-/*@ lemma S2_deterministic_trans{L}: \true;
+/*@ check lemma S2_deterministic_trans{L}: \true;
*/
int X;
int Y;
/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
/*@
-lemma S3_deterministic_trans{L}:
+check lemma S3_deterministic_trans{L}:
∀ int x;
¬(\at(aorai_CurOperation,L) ≡ op_g ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ x ≡ 5 ∧
@@ -46,7 +46,7 @@ lemma S3_deterministic_trans{L}:
\at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ x ≡ 4);
*/
/*@
-lemma S1_deterministic_trans{L}:
+check lemma S1_deterministic_trans{L}:
∀ int __retres_f, int x;
¬(\at(aorai_CurOperation,L) ≡ op_f ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧ __retres_f ≡ 0 ∧
@@ -54,7 +54,7 @@ lemma S1_deterministic_trans{L}:
\at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ x ≡ 4);
*/
/*@
-lemma S0_deterministic_trans{L}:
+check lemma S0_deterministic_trans{L}:
∀ int c;
¬(\at(aorai_CurOperation,L) ≡ op_real_main ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ c ≢ 0 ∧
diff --git a/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle b/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
index b850086cbe94dbafa142e58f40a017022d73a22c..f7b7f60952fc0de58218d819587217b5ac8e2cb3 100644
--- a/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
@@ -22,16 +22,16 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ lemma init_deterministic_trans{L}: \true;
+/*@ check lemma init_deterministic_trans{L}: \true;
*/
-/*@ lemma aorai_reject_deterministic_trans{L}: \true;
+/*@ check lemma aorai_reject_deterministic_trans{L}: \true;
*/
-/*@ lemma OK_deterministic_trans{L}: \true;
+/*@ check lemma OK_deterministic_trans{L}: \true;
*/
/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
/*@
-lemma main_0_deterministic_trans{L}:
+check lemma main_0_deterministic_trans{L}:
∀ int x;
¬(\at(aorai_CurOperation,L) ≡ op_f ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ x ≡ 3 ∧
@@ -39,7 +39,7 @@ lemma main_0_deterministic_trans{L}:
\at(aorai_CurOpStatus,L) ≡ aorai_Called ∧ x ≡ 1);
*/
/*@
-lemma aorai_intermediate_state_0_deterministic_trans{L}:
+check lemma aorai_intermediate_state_0_deterministic_trans{L}:
¬(\at(aorai_CurOperation,L) ≡ op_g ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Called ∧
¬(\at(aorai_CurOperation,L) ≡ op_g ∧
@@ -48,7 +48,7 @@ lemma aorai_intermediate_state_0_deterministic_trans{L}:
/*@ ghost int aorai_CurStates = init; */
/*@ ghost int aorai_x_0 = 0; */
/*@
-lemma aorai_intermediate_state_2_deterministic_trans{L}:
+check lemma aorai_intermediate_state_2_deterministic_trans{L}:
¬(\at(aorai_CurOperation,L) ≡ op_f ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
\at(aorai_x_0,L) ≡ 3 ∧
@@ -58,7 +58,7 @@ lemma aorai_intermediate_state_2_deterministic_trans{L}:
*/
/*@ ghost int aorai_y = 0; */
/*@
-lemma aorai_intermediate_state_1_deterministic_trans{L}:
+check lemma aorai_intermediate_state_1_deterministic_trans{L}:
¬(\at(aorai_CurOperation,L) ≡ op_g ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
\at(aorai_y,L) ≡ 2 ∧
@@ -68,7 +68,7 @@ lemma aorai_intermediate_state_1_deterministic_trans{L}:
*/
/*@ ghost int aorai_x = 0; */
/*@
-lemma aorai_intermediate_state_deterministic_trans{L}:
+check lemma aorai_intermediate_state_deterministic_trans{L}:
¬(\at(aorai_CurOperation,L) ≡ op_f ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
\at(aorai_x,L) ≡ 1 ∧
diff --git a/src/plugins/aorai/tests/aorai/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/aorai/oracle/incorrect.res.oracle
index ebe6f07db4c9567f195bde9895293748e61bd6a4..f0441fa89f01c774e4a8ac2e8e94708bf91e14b0 100644
--- a/src/plugins/aorai/tests/aorai/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/incorrect.res.oracle
@@ -15,7 +15,7 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ lemma s0_deterministic_trans{L}: \true;
+/*@ check lemma s0_deterministic_trans{L}: \true;
*/
int f(void);
diff --git a/src/plugins/aorai/tests/aorai/oracle/monostate.res.oracle b/src/plugins/aorai/tests/aorai/oracle/monostate.res.oracle
index e4e6c64f81a3e62fcd37119fae12ca6dd86062c6..00d9af27024d4c9f1ab797e12c8459678891dfb0 100644
--- a/src/plugins/aorai/tests/aorai/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/aorai/oracle/monostate.res.oracle
@@ -19,19 +19,19 @@ enum aorai_OpStatusList {
aorai_Terminated = 1,
aorai_Called = 0
};
-/*@ lemma aorai_reject_deterministic_trans{L}: \true;
+/*@ check lemma aorai_reject_deterministic_trans{L}: \true;
*/
/*@ ghost enum aorai_ListOper aorai_CurOperation = op_main; */
/*@ ghost enum aorai_OpStatusList aorai_CurOpStatus = aorai_Called; */
/*@
-lemma aorai_intermediate_state_deterministic_trans{L}:
+check lemma aorai_intermediate_state_deterministic_trans{L}:
¬(\at(aorai_CurOperation,L) ≡ op_main ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Terminated ∧
¬(\at(aorai_CurOperation,L) ≡ op_main ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Terminated));
*/
/*@
-lemma Init_deterministic_trans{L}:
+check lemma Init_deterministic_trans{L}:
¬(\at(aorai_CurOperation,L) ≡ op_main ∧
\at(aorai_CurOpStatus,L) ≡ aorai_Called ∧
¬(\at(aorai_CurOperation,L) ≡ op_main ∧
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 6a77b6530dfb5e6fd13a9a96e9878c3b5d48c6c9..018963ff23b879f9279c5d65080f4f9a42346a93 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -856,13 +856,14 @@ and translate_rte_annots:
let env =
List.fold_left
(fun env a -> match a.annot_content with
- | AAssert(_, _, p) ->
+ | AAssert(_, p) ->
handle_error
(fun env ->
Options.feedback ~dkey ~level:4 "prevent RTE from %a" pp elt;
(* The logic scope MUST NOT be reset here since we still might
be in the middle of the translation of the original
predicate. *)
+ let p = p.tp_statement in
let lscope_reset_old = Env.Logic_scope.get_reset env in
let env = Env.Logic_scope.set_reset env false in
let env = translate_named_predicate kf (Env.rte env false) p in
@@ -958,10 +959,11 @@ let term_to_exp typ t =
let assumes_predicate bhv =
List.fold_left
(fun acc p ->
- let loc = p.ip_content.pred_loc in
+ let pred = p.ip_content.tp_statement in
+ let loc = pred.pred_loc in
Logic_const.pand ~loc
(acc,
- Logic_const.unamed ~loc p.ip_content.pred_content))
+ Logic_const.unamed ~loc pred.pred_content))
Logic_const.ptrue
bhv.b_assumes
@@ -971,14 +973,15 @@ let translate_preconditions kf env behaviors =
let assumes_pred = assumes_predicate b in
List.fold_left
(fun env p ->
+ let pred = p.ip_content.tp_statement in
let do_it env =
if Keep_status.must_translate kf Keep_status.K_Requires then
- let loc = p.ip_content.pred_loc in
+ let loc = pred.pred_loc in
let p =
Logic_const.pimplies
~loc
(assumes_pred,
- Logic_const.unamed ~loc p.ip_content.pred_content)
+ Logic_const.unamed ~loc pred.pred_content)
in
translate_named_predicate kf env p
else
@@ -1012,8 +1015,8 @@ let translate_postconditions kf env behaviors =
let do_it env =
match t with
| Normal ->
- let loc = p.ip_content.pred_loc in
- let p = p.ip_content in
+ let p = p.ip_content.tp_statement in
+ let loc = p.pred_loc in
let p =
Logic_const.pimplies
~loc
@@ -1083,12 +1086,12 @@ let translate_post_spec kf env spec =
let translate_pre_code_annotation kf env annot =
let convert env = match annot.annot_content with
- | AAssert(l, _, p) ->
+ | AAssert(l, p) ->
if Keep_status.must_translate kf Keep_status.K_Assert then
let env = Env.set_annotation_kind env Constructor.Assertion in
if l <> [] then
not_yet env "@[assertion applied only on some behaviors@]";
- translate_named_predicate kf env p
+ translate_named_predicate kf env p.tp_statement
else
env
| AStmtSpec(l, spec) ->
@@ -1100,8 +1103,10 @@ let translate_pre_code_annotation kf env annot =
let env = Env.set_annotation_kind env Constructor.Invariant in
if l <> [] then
not_yet env "@[invariant applied only on some behaviors@]";
- let env = translate_named_predicate kf env p in
- if loop_invariant then Env.add_loop_invariant env p else env
+ let env = translate_named_predicate kf env p.tp_statement in
+ if loop_invariant then
+ Env.add_loop_invariant env p.tp_statement
+ else env
else
env
| AVariant _ ->
diff --git a/src/plugins/gui/property_navigator.ml b/src/plugins/gui/property_navigator.ml
index cc6b91fad051562f7170a891918d900a29429f23..e2f62844d00d39aac3e2c09cc96e44f7b8138d3e 100644
--- a/src/plugins/gui/property_navigator.ml
+++ b/src/plugins/gui/property_navigator.ml
@@ -636,14 +636,12 @@ 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 (_, kind, _)} as ca} ->
+ | IPCodeAnnot {ica_ca={annot_content=AAssert(_, {tp_only_check})} 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 ()
+ if tp_only_check then user_checks.get() else user_assertions.get ()
end
| IPCodeAnnot {ica_ca={annot_content = AInvariant _}} ->
invariant.get ()
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 777c7ce0892b7a680201d7920f83d8fca3b58014..0215a63e3161bf2e3b3c60fc6ed78d6d9b9a9706 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -373,7 +373,7 @@ end) = struct
Annotations.iter_code_annot
(fun _ ca ->
match ca.annot_content with
- | AAssert (_, _, p)
+ | AAssert (_, p)
| AInvariant (_, true, p) ->
begin
let env =
@@ -382,7 +382,7 @@ end) = struct
~here:(X.stmt_state stmt)
()
in
- match Eva.Eval_terms.predicate_deps env p with
+ match Eva.Eval_terms.predicate_deps env p.tp_statement with
| None ->
(* To be sound, we should perform a join with the top zone here.
We do nothing instead because the latter behavior would
diff --git a/src/plugins/instantiate/stdlib/basic_alloc.ml b/src/plugins/instantiate/stdlib/basic_alloc.ml
index a35a97b53e37d96e97149e0bb851c4db758cac6c..42142cc28c44a5064df718b6d0499850aff7bca7 100644
--- a/src/plugins/instantiate/stdlib/basic_alloc.ml
+++ b/src/plugins/instantiate/stdlib/basic_alloc.ml
@@ -82,6 +82,7 @@ let make_axiomatic_is_allocable loc () =
let cond = pand (prel (Rlt, t_i, zero), prel (Rgt, t_i, max)) in
let app = pnot (papp (is_allocable,[label],[t_i])) in
let prop = pforall ([lv_i], pimplies (cond, app)) in
+ let prop = Logic_const.toplevel_predicate prop in
let gfun = Dfun_or_pred(is_allocable, loc) in
let axiom = Dlemma("never_allocable", true, [label],[],prop,[], loc) in
("dynamic_allocation", [gfun ; axiom]), [is_allocable]
diff --git a/src/plugins/obfuscator/obfuscate.ml b/src/plugins/obfuscator/obfuscate.ml
index 5cf8be87e632f5db30d2b4cce7477fb4e65dfde6..adbe1215a838a78ebd76bbfc1f087e3aa716e9be 100644
--- a/src/plugins/obfuscator/obfuscate.ml
+++ b/src/plugins/obfuscator/obfuscate.ml
@@ -150,11 +150,14 @@ class visitor = object
Cil.SkipChildren
else begin
Identified_predicate.Hashtbl.add id_pred_visited p ();
- let names = p.ip_content.pred_name in
+ let { tp_only_check = only_check; 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 p' = { p with ip_content = { p.ip_content with pred_name = names'}} in
+ let pred' = { pred with pred_name = names' } in
+ let ip_content = Logic_const.toplevel_predicate ~only_check 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 6c190670c612e36b26f3bf757832171056c6de0d..1fb31afa260c5dd460f811a9024fede3e1ee27cb 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -488,15 +488,17 @@ 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 (_, 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
- R.debug "annot at stmt %d could be removed: %a"
- stmt.sid Printer.pp_code_annotation annot;
- acc
- else
- acc
+ | AAssert (_, p'), AAssert (_, p) when not p'.tp_only_check ->
+ 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
+ let acc, added = add_proven_annot (annot, stmt) (ca, stmt_ca) acc in
+ if added then
+ R.debug "annot at stmt %d could be removed: %a"
+ stmt.sid Printer.pp_code_annotation annot;
+ acc
+ else
+ acc
| _ -> acc
in
Annotations.fold_code_annot check stmt acc
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index 21475b79a7a7d523304ec22c16b5d8ed8b76e2d5..c0577e7c88ff21791d2b2be88d0f40430129ee30 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -216,9 +216,10 @@ 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;
+ let p = p.tp_statement.pred_content in
+ Format.fprintf fmt "@[<v>@[assert@ %a;@]" self#predicate_node p;
(* print temporary variables information *)
if not (Cil_datatype.Varinfo.Set.is_empty temporaries) then begin
Format.fprintf fmt "@ @[(%t)@]" self#pp_temporaries
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index c7cb5f5219d7ce702517e27cfac0d85b2b665b05..f10b631cfe65a596c50cbf3f6706cae73b02709e 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -1082,7 +1082,8 @@ let rec stmts_of_cfg cfg current var_map locals return_exp acc =
let exp = subst_in_exp var_map exp in
let predicate = Logic_utils.expr_to_predicate exp in
let predicate = if b then predicate else Logic_const.pnot predicate in
- let code_node = Cil_types.AAssert([],Assert,predicate) in
+ let predicate = Logic_const.toplevel_predicate predicate in
+ let code_node = Cil_types.AAssert([],predicate) in
let code_annot = Logic_const.new_code_annotation code_node in
let stmt_kind = Cil_types.Code_annot(code_annot,exp.eloc) in
let stmt = Cil.mkStmtOneInstr ~valid_sid stmt_kind in
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index 294b81b7245753a7e05e23047eb3aa8c25ecbd54..a6efdf17d21b8abfa3ff22fabffb1155fd11ecfe 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -137,7 +137,7 @@ let emit_message_and_status kind kf behavior ~active ~empty property named_pred
let create_conjunction l=
let loc = match l with
| [] -> None
- | p :: _ -> Some p.ip_content.pred_loc
+ | p :: _ -> Some (Logic_const.pred_of_id_pred p).pred_loc
in
Logic_const.(List.fold_right (fun p1 p2 -> pand ?loc (p1, p2)) (List.map pred_of_id_pred l) ptrue)
@@ -384,11 +384,11 @@ module Make
else (* Not enough slevel to split, and reduction not required *)
States.singleton state
- let eval_split_and_reduce limit active pred build_env state =
+ 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 =
- if active then
+ if reduce then
match status with
| Alarmset.False -> States.empty
| Alarmset.True ->
@@ -453,6 +453,7 @@ module Make
let emit = emit_message_and_status kind kf behavior ~active in
let aux_pred states pred =
let pr = Logic_const.pred_of_id_pred pred in
+ let reduce = active && not pred.ip_content.tp_only_check in
let ip = build_prop pred in
if ignore_predicate pr then
states
@@ -465,7 +466,7 @@ module Make
States.fold
(fun state (acc_status, acc_states) ->
let status, reduced_states =
- eval_split_and_reduce limit active pr build_env state
+ eval_split_and_reduce limit ~reduce pr build_env state
in
(status :: acc_status,
fst (States.merge ~into:acc_states reduced_states)))
@@ -580,8 +581,8 @@ module Make
let code_annotation_text ca =
match ca.annot_content with
- | AAssert (_, Assert, _) -> "assertion"
- | AAssert (_, Check, _) -> "check"
+ | AAssert (_,{tp_only_check = false}) -> "assertion"
+ | AAssert (_,{tp_only_check = true}) -> "check"
| AInvariant _ -> "loop invariant"
| APragma _ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
| AExtended _ ->
@@ -687,9 +688,9 @@ module Make
aux_interp ~reduce code_annot behav p
in
match code_annot.annot_content with
- | 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
+ | AAssert (behav, p)
+ | AInvariant (behav, true, p) ->
+ aux ~reduce:(not p.tp_only_check) code_annot behav p.tp_statement
| 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 8671ed982494460661e53c88939c4ae85d6b9e5e..fdd4ce7ec5dfe2549bdd6f4ec86c5133e4ea584b 100644
--- a/src/plugins/value/gui_files/gui_red.ml
+++ b/src/plugins/value/gui_files/gui_red.ml
@@ -69,7 +69,8 @@ type red_alarm = {
let get_predicate ca =
match ca.annot_content with
- | AAssert (_, _, p) -> { p with pred_name = [] }
+ | AAssert (_, p) ->
+ { p with tp_statement = { p.tp_statement with pred_name = [] }}
| _ -> assert false
let make_red_alarm function_name ki alarm callstacks =
@@ -84,7 +85,9 @@ let make_red_alarm function_name ki alarm callstacks =
let ip = Property.ip_of_code_annot_single kf stmt ca in
let kind = String.capitalize_ascii (Alarms.get_name alarm) in
let p = get_predicate ca in
- let acsl = Format.asprintf "@[<hov>%a@]" Cil_datatype.Predicate.pretty p in
+ let acsl =
+ Format.asprintf "@[<hov>%a@]" Cil_datatype.Toplevel_predicate.pretty p
+ in
let alarm_or_prop = Red_statuses.Alarm alarm in
{ function_name; ip; kind; alarm_or_prop; acsl; callstacks }
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index dc46ee11e7e5528f14f49c0d9ca4d2cc4861ff30..19d46c75109c13781b61f0069a2258aa9b916ec6 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -461,13 +461,17 @@ module Select (Eval: Eval) = struct
| PVDecl (Some kf, Kstmt stmt, vi) ->
let lv = (Var vi, NoOffset) in
select_lv main_ui (GL_Stmt (kf, stmt)) lv
- | PIP (IPCodeAnnot {ica_kf = kf; ica_stmt = stmt;
- ica_ca = {annot_content =
- AAssert (_, _, p)
- | AInvariant (_, true, p)} as ca
- } as ip) ->
+ | PIP (
+ IPCodeAnnot {
+ ica_kf = kf; ica_stmt = stmt;
+ ica_ca = {
+ annot_content =
+ AAssert (_, p) | AInvariant (_, true, p)
+ } as ca
+ } as ip) ->
begin
let loc = GL_Stmt (kf, stmt) in
+ let p = p.tp_statement in
let alarm_or_property =
match Alarms.find ca with
| None -> Red_statuses.Prop ip
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index e043c43a0b809b5727ee35e0d7868ac84dc8a94d..978309b89bba0f5296392d41e793d4783e1be46f 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -29,8 +29,8 @@ let has_requires spec =
let code_annotation_text ca =
match ca.annot_content with
- | AAssert (_, Assert, _) -> "assertion"
- | AAssert (_, Check, _) -> "check"
+ | AAssert (_, {tp_only_check=false}) -> "assertion"
+ | AAssert (_, {tp_only_check=true}) -> "check"
| AInvariant _ -> "loop invariant"
| APragma _ | AVariant _ | AAssigns _ | AAllocation _ | AStmtSpec _
| AExtended _ ->
@@ -203,7 +203,8 @@ 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 p = p.tp_statement in
let loc = code_annotation_loc ca stmt in
Cil.CurrentLoc.set loc;
let kf = Kernel_function.find_englobing_kf stmt in
@@ -246,7 +247,8 @@ let mark_invalid_initializers () =
| None -> ()
| Some _ ->
match ca.annot_content with
- | AAssert (_, _, p) ->
+ | AAssert (_, p) ->
+ let p = p.tp_statement in
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/Changelog b/src/plugins/wp/Changelog
index bdfeb67ae5865b23b198d32b88d71b4a01a126df..5d908195357178785cda176070da7a0a96635a29 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,6 +20,8 @@
# <Prover>: prover
###############################################################################
+- Wp [2020-09-09] Support for generalized @check ACSL annotations
+
#########################
Plugin WP 21.1 (Scandium)
#########################
diff --git a/src/plugins/wp/Cstring.ml b/src/plugins/wp/Cstring.ml
index 7705498957b67213b63c2dc7142c5bd396f6b3f7..826350e8a6739e7b6e3de05a70bf97dded252a81 100644
--- a/src/plugins/wp/Cstring.ml
+++ b/src/plugins/wp/Cstring.ml
@@ -76,7 +76,7 @@ module LIT = WpContext.Generator(STR)
define_lemma {
l_name = prefix ^ "_literal" ;
l_cluster = cluster () ;
- l_assumed = true ;
+ l_kind = `Axiom ;
l_types = 0 ;
l_forall = [] ;
l_triggers = [] ;
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index 6a55329e78dc75a7ab03e577f4e79e17529a68b3..7fa51bc9552b65ef190faf123100abd1970c0519 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -53,7 +53,7 @@ type cluster = {
and dlemma = {
l_name : string ;
l_cluster : cluster ;
- l_assumed : bool ;
+ l_kind : lkind ;
l_types : int ;
l_forall : var list ;
l_triggers : trigger list list (* OR of AND triggers *) ;
diff --git a/src/plugins/wp/Definitions.mli b/src/plugins/wp/Definitions.mli
index 7bc141a15b431d8af5c1f741c15317cbe8241486..8adf448cde8cdbf8bc28b94d564081dc68c3017b 100644
--- a/src/plugins/wp/Definitions.mli
+++ b/src/plugins/wp/Definitions.mli
@@ -49,7 +49,7 @@ type typedef = (tau,field,lfun) Qed.Engine.ftypedef
type dlemma = {
l_name : string ;
l_cluster : cluster ;
- l_assumed : bool ;
+ l_kind : lkind ;
l_types : int ;
l_forall : var list ;
l_triggers : trigger list list ; (** OR of AND-triggers *)
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 8c88a3af10b1598c786be81e67386363fd551c2a..69019743d70d1b3ae649826081996e4f618fa102 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -498,7 +498,7 @@ struct
| Pforall(qs,q) -> strip_forall (xs @ qs) q
| _ -> xs , p
- let compile_lemma cluster name ~assumed types labels lemma =
+ let compile_lemma cluster name ~kind types labels lemma =
let qs,prop = strip_forall [] lemma in
let xs,tgs,domain,prop,_ =
let cc_pred = pred `Positive in
@@ -508,7 +508,7 @@ struct
{
l_name = name ;
l_types = List.length types ;
- l_assumed = assumed ;
+ l_kind = kind ;
l_triggers = [tgs] ;
l_forall = xs ;
l_cluster = cluster ;
@@ -539,7 +539,7 @@ struct
let trigger = Trigger.of_term result in
Definitions.define_lemma {
l_name = name ;
- l_assumed = true ;
+ l_kind = `Axiom ;
l_types = ldef.d_types ;
l_forall = ldef.d_params ;
l_triggers = [[trigger]] ;
@@ -721,7 +721,7 @@ struct
(* Re-compile final cases *)
let cases = List.map
(fun (case,labels,types,lemma) ->
- compile_lemma cluster ~assumed:true case types labels lemma)
+ compile_lemma cluster ~kind:`Axiom case types labels lemma)
cases in
Definitions.update_symbol { ldef with d_definition = Inductive cases } ;
type_for_signature l ldef sigp (* sufficient *) ; SIG sigm
@@ -770,7 +770,7 @@ struct
{
l_name ;
l_types = 0 ;
- l_assumed = true ;
+ l_kind = `Axiom ;
l_triggers = [frame.triggers] ;
l_forall = vs ;
l_cluster = cluster ;
@@ -802,7 +802,7 @@ struct
"Lemma '%s' has labels, consider using global invariant instead."
l.lem_name ;
Definitions.define_lemma
- (compile_lemma c ~assumed:l.lem_axiom
+ (compile_lemma c ~kind:l.lem_kind
l.lem_name l.lem_types l.lem_labels l.lem_property)
let define_axiomatic cluster ax =
diff --git a/src/plugins/wp/LogicUsage.ml b/src/plugins/wp/LogicUsage.ml
index 953d1c9b92b14b94f18577e6653c22df5c06e345..1058d7ffa962fa3063fd853fc8039e5a8aa9450c 100644
--- a/src/plugins/wp/LogicUsage.ml
+++ b/src/plugins/wp/LogicUsage.ml
@@ -57,10 +57,12 @@ let trim name =
(* --- Definition Blocks --- *)
(* -------------------------------------------------------------------------- *)
+type lkind = [ `Axiom | `Check | `Lemma ]
+
type logic_lemma = {
lem_name : string ;
+ lem_kind : lkind ;
lem_position : Filepath.position ;
- lem_axiom : bool ;
lem_types : string list ;
lem_labels : logic_label list ;
lem_property : predicate ;
@@ -192,27 +194,36 @@ let pp_profile fmt l =
let ip_lemma l =
let open Property in
- (if l.lem_axiom then Property.ip_axiom else Property.ip_lemma)
+ let mk_prop, only_check =
+ match l.lem_kind with
+ | `Axiom -> Property.ip_axiom, false
+ | `Lemma -> Property.ip_lemma, false
+ | `Check -> Property.ip_lemma, true
+ 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_pred = l.lem_property}
-
-let lemma_of_global proof = function
- | Dlemma(name,axiom,labels,types,pred,_,loc) -> {
- lem_name = name ;
- lem_position = fst loc ;
- lem_types = types ;
- lem_labels = labels ;
- lem_axiom = axiom ;
- lem_property = pred ;
- lem_depends = proof ;
- }
+ il_pred = Logic_const.toplevel_predicate ~only_check l.lem_property}
+
+let lemma_of_global ~context = function
+ | Dlemma(name,axiom,labels,types,pred,_,loc) ->
+ let kind = if axiom then `Axiom else
+ if pred.tp_only_check then `Check else `Lemma in
+ {
+ lem_name = name ;
+ lem_position = fst loc ;
+ lem_types = types ;
+ lem_labels = labels ;
+ lem_kind = kind ;
+ lem_property = pred.tp_statement ;
+ lem_depends = context ;
+ }
| _ -> assert false
-let populate a proof = function
+let populate a ~context = function
| Dfun_or_pred(l,_) -> a.ax_logics <- l :: a.ax_logics
| Dtype(t,_) -> a.ax_types <- t :: a.ax_types
- | Dlemma _ as g -> a.ax_lemmas <- lemma_of_global proof g :: a.ax_lemmas
+ | Dlemma _ as g -> a.ax_lemmas <- lemma_of_global ~context g :: a.ax_lemmas
| _ -> ()
let ip_of_axiomatic g =
@@ -220,7 +231,7 @@ let ip_of_axiomatic g =
| None -> assert false
| Some ip -> ip
-let axiomatic_of_global proof = function
+let axiomatic_of_global ~context = function
| Daxiomatic(name,globals,_,loc) as g ->
let a = {
ax_name = name ;
@@ -229,7 +240,7 @@ let axiomatic_of_global proof = function
ax_reads = Varinfo.Set.empty ;
ax_types = [] ; ax_lemmas = [] ; ax_logics = [] ;
} in
- List.iter (populate a proof) globals ;
+ List.iter (populate a ~context) globals ;
a.ax_types <- List.rev a.ax_types ;
a.ax_logics <- List.rev a.ax_logics ;
a.ax_lemmas <- List.rev a.ax_lemmas ;
@@ -402,7 +413,8 @@ class visitor =
| Dlemma _ ->
let lem = lemma_of_global database.proofcontext global in
register_lemma database self#section lem ;
- database.proofcontext <- lem :: database.proofcontext ;
+ if lem.lem_kind <> `Check then
+ database.proofcontext <- lem :: database.proofcontext ;
SkipChildren
| Dtype(t,_) ->
@@ -502,9 +514,9 @@ let proof_context () =
(* --- Dump API --- *)
(* -------------------------------------------------------------------------- *)
-let dump_type fmt t = Format.fprintf fmt " * type '%s'@\n" t.lt_name
+let pp_type fmt t = Format.fprintf fmt " * type '%s'@\n" t.lt_name
-let dump_profile fmt kind l =
+let pp_sig fmt kind l =
begin
Format.fprintf fmt " * %s '%s'@\n" kind (compute_logicname l) ;
if is_overloaded l then
@@ -513,11 +525,11 @@ let dump_profile fmt kind l =
Format.fprintf fmt " recursive@\n" ;
end
-let dump_logic fmt d l =
+let pp_decl fmt d l =
begin
try
let cases = LMap.find l d.cases in
- dump_profile fmt "inductive" l ;
+ pp_sig fmt "inductive" l ;
List.iter
(fun ind ->
Format.fprintf fmt " @[case %s:" ind.ind_case ;
@@ -532,14 +544,16 @@ let dump_logic fmt d l =
) cases ;
with Not_found ->
let kind = if l.l_type = None then "predicate" else "function" in
- dump_profile fmt kind l ;
+ pp_sig fmt kind l ;
end
-let dump_lemma fmt l =
- if l.lem_axiom then
- Format.fprintf fmt " * axiom '%s'@\n" l.lem_name
- else
- Format.fprintf fmt " * lemma '%s'@\n" l.lem_name
+let pp_kind fmt = function
+ | `Axiom -> Format.pp_print_string fmt "axiom"
+ | `Lemma -> Format.pp_print_string fmt "lemma"
+ | `Check -> Format.pp_print_string fmt "check lemma"
+
+let pp_lemma fmt l =
+ Format.fprintf fmt " * %a '%s'@\n" pp_kind l.lem_kind l.lem_name
let get_name l = compute () ; compute_logicname l
@@ -556,9 +570,9 @@ let dump () =
SMap.iter
(fun _ a ->
Format.fprintf fmt "Axiomatic %s {@\n" a.ax_name ;
- List.iter (dump_type fmt) a.ax_types ;
- List.iter (dump_logic fmt d) a.ax_logics ;
- List.iter (dump_lemma fmt) a.ax_lemmas ;
+ List.iter (pp_type fmt) a.ax_types ;
+ List.iter (pp_decl fmt d) a.ax_logics ;
+ List.iter (pp_lemma fmt) a.ax_lemmas ;
Format.fprintf fmt "}@\n"
) d.axiomatics ;
TMap.iter
@@ -573,8 +587,8 @@ let dump () =
d.logics ;
SMap.iter
(fun l (lem,s) ->
- Format.fprintf fmt " * %s '%s' in %a@\n"
- (if lem.lem_axiom then "axiom" else "lemma")
+ Format.fprintf fmt " * %a '%s' in %a@\n"
+ pp_kind lem.lem_kind
l pp_section s)
d.lemmas ;
Format.fprintf fmt "-------------------------------------------------@." ;
diff --git a/src/plugins/wp/LogicUsage.mli b/src/plugins/wp/LogicUsage.mli
index 4ae195a680c70fe9ffa329b0c725dd105417f90d..b36713d5209e66a077ef0a5beb8e8778c7150bf3 100644
--- a/src/plugins/wp/LogicUsage.mli
+++ b/src/plugins/wp/LogicUsage.mli
@@ -30,10 +30,12 @@ open Clabels
val basename : varinfo -> string (** Trims the original name *)
+type lkind = [ `Axiom | `Check | `Lemma ]
+
type logic_lemma = {
lem_name : string ;
+ lem_kind : lkind ;
lem_position : Filepath.position ;
- lem_axiom : bool ;
lem_types : string list ;
lem_labels : logic_label list ;
lem_property : predicate ;
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 5d940330603ac683267919647abc0ceb32f3e4dc..8edca8a418d8b027ccddc13a879c864b6301d6d5 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -141,7 +141,7 @@ struct
prefix name Chunk.pretty chunk i in
let l_lemma = F.p_hyps conditions (p_equal value1 value2) in
Definitions.define_lemma {
- l_assumed = true ;
+ l_kind = `Axiom ;
l_name ; l_types = 0 ;
l_triggers ;
l_forall = F.p_vars l_lemma ;
@@ -226,7 +226,7 @@ struct
let lfun = Lang.generated_f ~result "Array%a%s_%s" pp_rid r
(Matrix.id ds) (Matrix.natural_id obj_e) in
let prefix = Lang.Fun.debug lfun in
- let axiom = prefix ^ "_access" in
+ let name = prefix ^ "_access" in
let xmem,chunks,sigma = signature domain in
let denv = Matrix.denv ds in
let phi = e_fun lfun (v :: denv.size_val @ List.map e_var xmem) in
@@ -242,8 +242,8 @@ struct
d_cluster = cluster ;
} ;
Definitions.define_lemma {
- l_assumed = true ;
- l_name = axiom ; l_types = 0 ;
+ l_kind = `Axiom ;
+ l_name = name ; l_types = 0 ;
l_forall = F.p_vars lemma ;
l_triggers = [[Trigger.of_term va]] ;
l_lemma = lemma ;
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index b717626bea998d91c4a13bdde52727de723ff4f2..4c308904f053b65ad0068ca6316849e9108f53b0 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -193,14 +193,14 @@ let constructor ~basename ~params ~index ~addrof ~consistent =
} ;
Definitions.define_lemma {
l_cluster = cluster ;
- l_assumed = true ;
+ l_kind = `Axiom ;
l_name = Printf.sprintf "addrof_%s_%d" basename id ;
l_forall = params ; l_types = 0 ; l_triggers = [] ;
l_lemma = p_addrof ;
} ;
Definitions.define_lemma {
l_cluster = cluster ;
- l_assumed = true ;
+ l_kind = `Axiom ;
l_name = Printf.sprintf "consistent_%s_%d" basename id ;
l_forall = params ; l_types = 0 ; l_triggers = [] ;
l_lemma = p_consistent ;
@@ -208,7 +208,7 @@ let constructor ~basename ~params ~index ~addrof ~consistent =
if p_index != F.p_true then
Definitions.define_lemma {
l_cluster = cluster ;
- l_assumed = true ;
+ l_kind = `Axiom ;
l_name = Printf.sprintf "index_%s_%d" basename id ;
l_forall = params @ [k] ; l_types = 0 ; l_triggers = [] ;
l_lemma = p_index ;
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 12f4230be78dc3c929fc275951e98918d101e0ab..fd2770c3c3eafe10a024308fcac514e4d4d1ce04 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -409,7 +409,7 @@ module STRING = WpContext.Generator(LITERAL)
let alloc = F.e_get m base in (* The size is alloc-1 *)
let sized = Cstring.str_len cst (F.e_add alloc F.e_minus_one) in
Definitions.define_lemma {
- l_assumed = true ;
+ l_kind = `Axiom ;
l_name = name ; l_types = 0 ;
l_triggers = [] ; l_forall = [] ;
l_lemma = p_forall [a] (p_imply m_linked sized) ;
@@ -420,7 +420,7 @@ module STRING = WpContext.Generator(LITERAL)
let name = prefix ^ "_region" in
let re = - Cstring.str_id cst in
Definitions.define_lemma {
- l_assumed = true ;
+ l_kind = `Axiom ;
l_name = name ; l_types = 0 ; l_triggers = [] ; l_forall = [] ;
l_lemma = p_equal (e_fun f_region [base]) (e_int re) ;
l_cluster = Cstring.cluster () ;
@@ -437,7 +437,7 @@ module STRING = WpContext.Generator(LITERAL)
let v = F.e_get (e_var m) addr in
let read = F.p_equal c v in
Definitions.define_lemma {
- l_assumed = true ;
+ l_kind = `Axiom ;
l_name = name ; l_types = 0 ; l_triggers = [] ;
l_forall = [m;i] ;
l_cluster = Cstring.cluster () ;
@@ -461,7 +461,7 @@ module STRING = WpContext.Generator(LITERAL)
} ;
Definitions.define_lemma {
l_name = prefix ^ "_base" ;
- l_assumed = true ;
+ l_kind = `Axiom ;
l_types = 0 ; l_triggers = [] ; l_forall = [] ;
l_lemma = F.p_lt base F.e_zero ;
l_cluster = Cstring.cluster () ;
@@ -495,7 +495,7 @@ module BASE = WpContext.Generator(Varinfo)
let name = prefix ^ "_region" in
let re = if x.vglob then 0 else if x.vformal then 1 else 2 in
Definitions.define_lemma {
- l_assumed = true ;
+ l_kind = `Axiom ;
l_name = name ; l_types = 0 ; l_triggers = [] ; l_forall = [] ;
l_lemma = p_equal (e_fun f_region [base]) (e_int re) ;
l_cluster = cluster_globals () ;
@@ -519,7 +519,7 @@ module BASE = WpContext.Generator(Varinfo)
let m_linked = p_call p_linked [m] in
let base_size = p_equal (F.e_get m base) (e_int size) in
Definitions.define_lemma {
- l_assumed = true ;
+ l_kind = `Axiom ;
l_name = name ; l_types = 0 ;
l_triggers = [] ; l_forall = [] ;
l_lemma = p_forall [a] (p_imply m_linked base_size) ;
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 343f4a4affd0f6039e445ee74960ec5c7f284c78..813eda4cf32ee1350d7b6a68c1dd47fb70f1069e 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -911,7 +911,7 @@ class visitor (ctx:context) c =
id, t
method on_dlemma l =
- let kind = Why3.Decl.(if l.l_assumed then Paxiom else Plemma) in
+ let kind = Why3.Decl.(if l.l_kind = `Axiom then Paxiom else Plemma) in
let cnv = empty_cnv ctx in
let id, t = self#make_lemma cnv l in
let decl = Why3.Decl.create_prop_decl kind id t in
diff --git a/src/plugins/wp/Splitter.ml b/src/plugins/wp/Splitter.ml
index b5930b40748cf9752bc470ee58ebb5c1eb70baf0..a0707f3bd7ee887c775265ec395ecfefdbf9d4e4 100644
--- a/src/plugins/wp/Splitter.ml
+++ b/src/plugins/wp/Splitter.ml
@@ -50,7 +50,7 @@ let pretty fmt = function
let loc = function
| THEN s | ELSE s | CASE(s,_) | CALL(s,_) | DEFAULT s -> Stmt.loc s
- | ASSERT(p,_,_) -> p.ip_content.pred_loc
+ | ASSERT(p,_,_) -> p.ip_content.tp_statement.pred_loc
let compare p q =
if p == q then 0 else
@@ -103,8 +103,7 @@ and unwrap p =
(unwrap p)
| _ -> raise Exit
-let predicate ip =
- ip.ip_content
+let predicate ip = ip.ip_content.tp_statement
let rec enumerate ip k n = function
| [] -> []
diff --git a/src/plugins/wp/StmtSemantics.ml b/src/plugins/wp/StmtSemantics.ml
index 22b7335e91ecd96befa323fb73703dcab40a81ba..6ba37de4959f4d9e35742cd11d71c5073a11f621 100644
--- a/src/plugins/wp/StmtSemantics.ml
+++ b/src/plugins/wp/StmtSemantics.ml
@@ -297,9 +297,9 @@ struct
with Not_found -> Wp_parameters.fatal "Error during compilation"
let assert_ env p prop_id =
- let pos = pred env `Positive p.ip_content in
+ let pos = pred env `Positive p.ip_content.tp_statement in
let env' = env @* [Clabels.here, env @: Clabels.next ] in
- let neg = pred env' `Negative p.ip_content in
+ let neg = pred env' `Negative p.ip_content.tp_statement in
let goal = {
goal_pred = pos;
goal_prop = prop_id;
@@ -430,7 +430,7 @@ struct
in
let post_cond termination_kind env (tk, ip) =
if tk = termination_kind then
- assume_ env `Positive ip.ip_content
+ assume_ env `Positive ip.ip_content.tp_statement
else nop
in
let behavior env b =
@@ -540,7 +540,7 @@ struct
let node = get_node nodes vertex in
bind c_label node acc
) a.labels env in
- assume (pred env `Negative a.predicate.ip_content) @^
+ assume (pred env `Negative a.predicate.ip_content.tp_statement) @^
goto (env @: Clabels.here) (env @: Clabels.next)
| Prop _ ->
not_yet "[StmtSemantics] Annots other than 'assert'"
@@ -717,7 +717,7 @@ struct
in
assume,
List.fold_left
- (fun acc ip -> acc @^ pre_cond `Negative env ip.ip_content)
+ (fun acc ip -> acc @^ pre_cond `Negative env ip.ip_content.tp_statement)
nop b.b_requires
@^ goto (env @: Clabels.here) (env @: Clabels.next)
in
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index b8389519cc2b552a62d28100f2ae7c1b8b7ecab1..8a35afd310f5d85c5e14bcfc8effb75ece93956b 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1394,7 +1394,7 @@ struct
let compile_lemma l = ignore (VCG.lemma l)
let prove_lemma collection l =
- if not l.lem_axiom then
+ if l.lem_kind <> `Axiom then
begin
let id = WpPropId.mk_lemma_id l in
let def = VCG.lemma l in
diff --git a/src/plugins/wp/tests/README.md b/src/plugins/wp/tests/README.md
index c88b74cb66da4ec06b1b519cc8808a595c96eec8..a4ca41d8419b1182981f16b2c79cac381ac594c8 100644
--- a/src/plugins/wp/tests/README.md
+++ b/src/plugins/wp/tests/README.md
@@ -1,3 +1,9 @@
+# Running qualif tests
+
+- Be sure that you have installed the appropriate versions of
+ alt-ergo and coq _before_ having compiled Frama-C.
+- use `make wp-qualif` in the toplevel Frama-C directory
+
# How to add a new test
```
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index a474167455ddc2e1c51857f25dcc425304d63b93..2603c8fa245d66ce14db353223f0b2bdcff4979c 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -54,7 +54,8 @@ let run () =
pred_content = Cil_types.Ptrue;
}
in
- let annot = Logic_const.new_code_annotation (AAssert ([],Assert,pred)) in
+ let pred = Logic_const.toplevel_predicate pred in
+ let annot = Logic_const.new_code_annotation (AAssert ([],pred)) in
let po = Wpo.{
po_gid = "";
po_leg = "";
diff --git a/src/plugins/wp/tests/wp_acsl/checks.i b/src/plugins/wp/tests/wp_acsl/checks.i
index 1a1174504f7e46923c594d5f5d11049ad5fdd1f0..f3fdcbfcab8f623e1c5393ae7e7b4b977300a6c2 100644
--- a/src/plugins/wp/tests/wp_acsl/checks.i
+++ b/src/plugins/wp/tests/wp_acsl/checks.i
@@ -1,7 +1,7 @@
/* run.config
OPT: -eva -load-module scope,eva,report -then -report
OPT: -wp-prop=@check
- OPT: -wp-prop=@assert
+ OPT: -wp-prop=-@check
*/
/* run.config_qualif
OPT: -load-module report -wp-steps 5 -then -report
diff --git a/src/plugins/wp/tests/wp_acsl/generalized_checks.i b/src/plugins/wp/tests/wp_acsl/generalized_checks.i
new file mode 100644
index 0000000000000000000000000000000000000000..3b34ced34e21bad22ab97aaefd60da416ce909d5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/generalized_checks.i
@@ -0,0 +1,66 @@
+/* run.config_qualif
+ OPT: -wp-timeout 1
+ */
+
+/*@
+ axiomatic Th {
+
+ predicate P(integer p);
+ predicate Q(integer q);
+ predicate R(integer r);
+
+ axiom A: \forall integer x; P(x) ==> Q(x);
+ check lemma C: ko: \forall integer x; Q(x) ==> R(x);
+ lemma L: ko: \forall integer x; P(x) ==> R(x); // C is not used
+
+ }
+ */
+
+/*@
+ axiomatic Cfg {
+ logic integer F(integer x);
+ predicate A(integer x);
+ predicate B(integer x);
+ predicate CA1(integer x);
+ predicate CA2(integer x);
+ predicate CB1(integer x);
+ predicate CB2(integer x);
+
+ axiom AFB: \forall integer x; A(x) ==> B(F(x));
+ axiom ACB1: \forall integer x; A(x) ==> CB1(F(x));
+ axiom CA1B2: \forall integer x; CA1(x) ==> CB2(F(x));
+
+ }
+ */
+
+/*@
+ ensures \result == F(x);
+ assigns \nothing;
+ */
+int f(int x);
+
+/*@
+ requires A: A(x);
+ check requires CA1: CA1(x);
+ check requires CA2: ko: CA2(x);
+ ensures B: B(\result);
+ check ensures CB1: CB1(\result);
+ check ensures CB2: ko: CB2(\result); // CA1 is not used
+ assigns \nothing;
+*/
+int job(int x) {
+ return f(x);
+}
+
+/*@
+ requires A(x);
+ requires CA1(x);
+ ensures R: B(\result);
+ ensures R1: ko: CB1(\result); // CB1 is not used from job
+ ensures R2: ko: CA2(x); // CA2 is not used from job
+ assigns \nothing;
+*/
+int caller(int x)
+{
+ return job(x); // CA2 is not proved
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6b7463a9cd6fe372fa0d12a2c30aa428cbe48498
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle
@@ -0,0 +1,139 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Axiomatic 'Th'
+------------------------------------------------------------
+
+Lemma C:
+Assume: 'A'
+Prove: (P_Q x_0) -> (P_R x_0)
+
+------------------------------------------------------------
+
+Lemma L:
+Assume: 'A'
+Prove: (P_P x_0) -> (P_R x_0)
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function caller
+------------------------------------------------------------
+
+Goal Post-condition 'R' in 'caller':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition 'R1,ko' in 'caller':
+Assume {
+ Type: is_sint32(caller_0) /\ is_sint32(x).
+ (* Pre-condition *)
+ Have: P_A(x) /\ P_CA1(x).
+ (* Call 'job' *)
+ Have: P_B(caller_0).
+}
+Prove: P_CB1(caller_0).
+
+------------------------------------------------------------
+
+Goal Post-condition 'R2,ko' in 'caller':
+Assume {
+ Type: is_sint32(caller_0) /\ is_sint32(x).
+ (* Pre-condition *)
+ Have: P_A(x) /\ P_CA1(x).
+ (* Call 'job' *)
+ Have: P_B(caller_0).
+}
+Prove: P_CA2(x).
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'caller':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'caller' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'caller' (2/2):
+Call Result at line 65
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'A' in 'job'' in 'caller' at call 'job' (file tests/wp_acsl/generalized_checks.i, line 65)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'CA1' in 'job'' in 'caller' at call 'job' (file tests/wp_acsl/generalized_checks.i, line 65)
+:
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition 'CA2,ko' in 'job'' in 'caller' at call 'job' (file tests/wp_acsl/generalized_checks.i, line 65)
+:
+Assume { Type: is_sint32(x). (* Pre-condition *) Have: P_A(x) /\ P_CA1(x). }
+Prove: P_CA2(x).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function job
+------------------------------------------------------------
+
+Goal Post-condition 'B' in 'job':
+Let x_1 = L_F(x).
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Pre-condition *)
+ Have: P_A(x).
+}
+Prove: P_B(x_1).
+
+------------------------------------------------------------
+
+Goal Post-condition 'CB1' in 'job':
+Let x_1 = L_F(x).
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Pre-condition *)
+ Have: P_A(x).
+}
+Prove: P_CB1(x_1).
+
+------------------------------------------------------------
+
+Goal Post-condition 'CB2,ko' in 'job':
+Let x_1 = L_F(x).
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1).
+ (* Pre-condition *)
+ Have: P_A(x).
+}
+Prove: P_CB2(x_1).
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'job':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'job' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'job' (2/2):
+Call Result at line 52
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..4b3a0044393faa02a60d3f95120b5a17991d3a11
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/generalized_checks.res.oracle
@@ -0,0 +1,34 @@
+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 17 goals scheduled
+[wp] [Alt-Ergo] Goal typed_check_lemma_C_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_lemma_L_ko : Unsuccess
+[wp] [Qed] Goal typed_caller_ensures_R : Valid
+[wp] [Alt-Ergo] Goal typed_caller_ensures_R1_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_caller_ensures_R2_ko : Unsuccess
+[wp] [Qed] Goal typed_caller_assigns_exit : Valid
+[wp] [Qed] Goal typed_caller_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_caller_assigns_normal_part2 : Valid
+[wp] [Qed] Goal typed_caller_call_job_requires_A : Valid
+[wp] [Qed] Goal typed_caller_call_job_check_requires_CA1 : Valid
+[wp] [Alt-Ergo] Goal typed_caller_call_job_check_requires_CA2_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_ensures_B : Valid
+[wp] [Alt-Ergo] Goal typed_job_check_ensures_CB1 : Valid
+[wp] [Alt-Ergo] Goal typed_job_check_ensures_CB2_ko : Unsuccess
+[wp] [Qed] Goal typed_job_assigns_exit : Valid
+[wp] [Qed] Goal typed_job_assigns_normal_part1 : Valid
+[wp] [Qed] Goal typed_job_assigns_normal_part2 : Valid
+[wp] Proved goals: 11 / 17
+ Qed: 9
+ Alt-Ergo: 2 (unsuccess: 6)
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Axiomatic Th - - 2 0.0%
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job 3 2 6 83.3%
+ caller 6 - 9 66.7%
+------------------------------------------------------------
diff --git a/src/plugins/wp/wpAnnot.ml b/src/plugins/wp/wpAnnot.ml
index b7b5698f643fdcafecc7251c539a7beec9b5ca2d..eaee55511cfafb12924c110f9ab35ad17d8f4b6c 100644
--- a/src/plugins/wp/wpAnnot.ml
+++ b/src/plugins/wp/wpAnnot.ml
@@ -373,6 +373,9 @@ let kind_to_select config kind id = match kind with
| WpStrategy.AcallPre(goal,fct) ->
let goal = goal && goal_to_select config id in
Some (WpStrategy.AcallPre(goal,fct))
+ | WpStrategy.AcallCheck(fct) ->
+ if goal_to_select config id then Some (WpStrategy.AcallCheck fct)
+ else None
| WpStrategy.AcallPost _ ->
if goal_to_select config id then Some kind else None
| WpStrategy.Ahyp | WpStrategy.AcallHyp _ -> Some kind
@@ -753,7 +756,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
+ if tk = termination_kind && not p.ip_content.tp_only_check
then WpStrategy.add_prop_call_post acc kind called_kf b tk ~assumes p
else acc
in List.fold_left add_post acc b.b_post_cond
@@ -830,6 +833,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 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
* in the loop, so we can assume that inv is true for each edge
@@ -843,15 +848,18 @@ let add_loop_invariant_annot config vloop s ca b_list inv acc =
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_core = add_prop_inv_fixpoint config loop_core
- WpStrategy.Ahyp s ca inv in
+ let loop_core =
+ if only_check then loop_core
+ else
+ add_prop_inv_fixpoint config loop_core WpStrategy.Ahyp s ca inv
+ in
assigns, loop_entry , loop_back , loop_core
end
- | TBRhyp ->
+ | 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
- | TBRno -> acc
+ | TBRhyp | TBRno -> acc
(** Returns the annotations for the three edges of the loop node:
* - loop_entry : goals for the edge entering in the loop
@@ -934,24 +942,28 @@ let get_stmt_annots config v s =
Printer.pp_code_annotation a;
acc
end
- | AAssert (b_list, kind, p) ->
+ | AAssert (b_list, p) ->
let kf = config.kf in
let acc = match is_annot_for_config config v s b_list with
| TBRno -> acc
| TBRhyp ->
- if kind = Check then acc
+ if p.tp_only_check then acc
else
let b_acc =
- WpStrategy.add_prop_assert b_acc WpStrategy.Ahyp kf s a p
+ WpStrategy.add_prop_assert
+ b_acc WpStrategy.Ahyp kf s a p.tp_statement
in (b_acc, (a_acc, e_acc))
| TBRok | TBRpart ->
let id = WpPropId.mk_assert_id config.kf s a in
- let check = kind = Check
- and goal = goal_to_select config id in
- if check && not goal then acc
+ let goal = goal_to_select config id in
+ if p.tp_only_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
+ let kind =
+ WpStrategy.(if p.tp_only_check then Agoal else Aboth goal)
+ in
+ let b_acc =
+ WpStrategy.add_prop_assert b_acc kind kf s a p.tp_statement
+ in
(b_acc, (a_acc, e_acc))
in acc
| AAllocation (_b_list, _frees_allocates) ->
@@ -1118,8 +1130,9 @@ let add_global_annotations annots =
"Global invariant not handled yet ('%s' ignored)"
linfo.l_var_info.lv_name;
()
- | Dlemma (name,_,_,_,_,_,_) ->
- WpStrategy.add_axiom annots (LogicUsage.logic_lemma name)
+ | Dlemma (name,_,_,_,p,_,_) ->
+ if not (p.tp_only_check) then
+ WpStrategy.add_axiom annots (LogicUsage.logic_lemma name)
and do_globals gs = List.iter do_global gs in
(*[LC]: forcing order of iteration: hash is not the same on 32 and 64 bits *)
@@ -1425,7 +1438,7 @@ let get_id_prop_strategies ~model ?(assigns=WithAssigns) p =
let open Property in match p with
| IPCodeAnnot {ica_kf; ica_ca} ->
let bhvs = match ica_ca.annot_content with
- | AAssert (l, _, _) | AInvariant (l, _, _) | AAssigns (l, _) -> l
+ | AAssert (l, _) | AInvariant (l, _, _) | AAssigns (l, _) -> l
| _ -> []
in get_strategies assigns ica_kf model bhvs None (IdProp p)
| IPAssigns {ias_kf = kf; ias_bhv = Id_loop _}
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 9821c657890900dac6b7ba825e5dc6c5f025f2d1..458a2fcf48f0597f432a0cd3f2f236a18127852b 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -465,10 +465,13 @@ let ident_names names =
List.filter (function "" -> true
| _ as n -> '\"' <> (String.get n 0) ) 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
+
let code_annot_names ca = match ca.annot_content with
- | 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)
+ | AAssert (_, pred) -> "@assert" :: pred_names pred
+ | AInvariant (_,_,pred) -> "@invariant":: pred_names pred
| AVariant (term, _) -> "@variant"::(ident_names term.term_name)
| AExtended(_,_,{ext_name}) -> [Printf.sprintf "@%s" ext_name]
| _ -> [] (* TODO : add some more names ? *)
@@ -479,7 +482,7 @@ let user_prop_names p =
let open Property in match p with
| IPPredicate {ip_kind; ip_pred} ->
Format.asprintf "@@%a" Property.pretty_predicate_kind ip_kind ::
- ip_pred.ip_content.pred_name
+ pred_names ip_pred.ip_content
| IPExtended {ie_ext={ext_name}} -> [ Printf.sprintf "@%s" ext_name ]
| IPCodeAnnot {ica_ca} -> code_annot_names ica_ca
| IPComplete {ic_bhvs} ->
@@ -497,8 +500,8 @@ let user_prop_names p =
| IPDecrease {id_ca=Some ca} -> "@decreases"::code_annot_names ca
| IPDecrease _ -> [ "@decreases" ]
| IPLemma {il_name = a; il_pred = l} ->
- let names = "@lemma"::a::(ident_names l.pred_name)
- in begin
+ let names = "@lemma"::a::pred_names l in
+ begin
match LogicUsage.section_of_lemma a with
| LogicUsage.Toplevel _ -> names
| LogicUsage.Axiomatic ax -> ax.LogicUsage.ax_name::names
@@ -641,8 +644,8 @@ 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) ->
- List.iter (add_hint hs) (ident_names ipred.pred_name) ;
+ | AAssert(bs,ipred) | AInvariant(bs,_,ipred) ->
+ List.iter (add_hint hs) (ident_names ipred.tp_statement.pred_name) ;
List.iter (add_hint hs) bs
| AAssigns(bs,Writes froms) ->
List.iter (add_hint hs) bs ;
@@ -654,12 +657,12 @@ let property_hints hs =
let open Property in function
| IPAxiom {il_name; il_pred}
| IPLemma {il_name; il_pred} ->
- List.iter (add_required hs) (il_name::il_pred.pred_name)
+ List.iter (add_required hs) (il_name::il_pred.tp_statement.pred_name)
| IPBehavior _ -> ()
| IPComplete {ic_bhvs} | IPDisjoint {ic_bhvs} ->
List.iter (add_required hs) ic_bhvs
| IPPredicate {ip_pred} ->
- List.iter (add_hint hs) ip_pred.ip_content.pred_name
+ List.iter (add_hint hs) ip_pred.ip_content.tp_statement.pred_name
| IPExtended {ie_ext={ext_name}} -> List.iter (add_hint hs) [ext_name]
| IPCodeAnnot {ica_ca} -> annot_hints hs ica_ca.annot_content
| IPAssigns {ias_froms} -> assigns_hints hs ias_froms
diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index 98acfad8ecbdd9dcf19e600ffe29b1efa795a5b6..f2b7abc13875fb0113053421aace7c796df5eaf7 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -84,8 +84,9 @@ let is_dead_annot ca =
match ca.annot_content with
| APragma (Loop_pragma (Unroll_specs [ spec ; _ ])) ->
false && is_unrolled_completely spec
- | AAssert([],Assert,p) -> is_predicate false p
- | AInvariant([],_,p) -> is_predicate false p
+ | AAssert([],p) ->
+ not p.tp_only_check && is_predicate false p.tp_statement
+ | AInvariant([],_,p) -> 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 ee31dab55e746eef3b68c77901182615c54cffce..96f589da256b9329369a41a49b171e172f687230 100644
--- a/src/plugins/wp/wpStrategy.ml
+++ b/src/plugins/wp/wpStrategy.ml
@@ -48,10 +48,15 @@ type annot_kind =
| AcallPre of bool * kernel_function
(* annotation is a called function precondition :
to be considered as hyp, and goal if bool=true *)
+ | AcallCheck of kernel_function
+ (* annotation is a called function check-only precondition.
+ to be considered as goal only. *)
| AcallPost of kernel_function
(* annotation is a called function post check :
to be considered as goal only *)
+type call_pre_kind = CPhyp | CPgoal | CPboth
+
(* -------------------------------------------------------------------------- *)
(* --- Annotations for one program point. --- *)
(* -------------------------------------------------------------------------- *)
@@ -68,7 +73,7 @@ type annots = {
p_both : (bool * WpPropId.pred_info) list;
p_cut : (bool * WpPropId.pred_info) list;
call_hyp : WpPropId.pred_info list ForCall.t; (* post and pre *)
- call_pre : (bool * WpPropId.pred_info) list ForCall.t; (* goal only *)
+ call_pre : (call_pre_kind * WpPropId.pred_info) list ForCall.t;
call_post : WpPropId.pred_info list ForCall.t; (* post goals only (not hyp) *)
call_asgn : WpPropId.assigns_full_info ForCall.t;
a_goal : WpPropId.assigns_full_info;
@@ -112,10 +117,20 @@ let add_prop acc kind id p =
| Some p -> Some(WpPropId.mk_pred_info id p) in
let add_hyp l = match get_p with None -> l | Some p -> p::l in
let add_goal l = match get_p with None -> l | Some p -> p::l in
+ let add_both_std goal l =
+ match get_p with None -> l | Some p -> (goal,p) :: l
+ in
let add_both goal l =
match get_p with
| None -> l
- | Some p -> (goal, p)::l
+ | Some p ->
+ let kind = if goal then CPboth else CPhyp in
+ (kind, p)::l
+ in
+ let add_pre l =
+ match get_p with
+ | None -> l
+ | Some p -> (CPgoal, p) :: l
in
let add_for_call fct calls =
let l = try ForCall.find fct calls with Not_found -> [] in
@@ -123,6 +138,10 @@ let add_prop acc kind id p =
let add_both_call fct goal calls =
let l = try ForCall.find fct calls with Not_found -> [] in
ForCall.add fct (add_both goal l) calls in
+ let add_pre_call fct calls =
+ let l = try ForCall.find fct calls with Not_found -> [] in
+ ForCall.add fct (add_pre l) calls
+ in
let info = acc.info in
let goal, info = match kind with
| Ahyp ->
@@ -130,13 +149,15 @@ let add_prop acc kind id p =
| Agoal ->
true, { info with p_goal = add_goal info.p_goal }
| Aboth goal ->
- goal, { info with p_both = add_both goal info.p_both }
+ goal, { info with p_both = add_both_std goal info.p_both }
| AcutB goal ->
- goal, { info with p_cut = add_both goal info.p_cut }
+ goal, { info with p_cut = add_both_std goal info.p_cut }
| AcallHyp fct ->
false, { info with call_hyp = add_for_call fct info.call_hyp }
| AcallPre (goal,fct) ->
goal, { info with call_pre = add_both_call fct goal info.call_pre }
+ | AcallCheck fct ->
+ true, { info with call_pre = add_pre_call fct info.call_pre }
| AcallPost fct ->
true, { info with call_post = add_for_call fct info.call_post }
in let acc = { acc with info = info } in
@@ -149,7 +170,10 @@ let add_prop_fct_pre_bhv acc kind kf bhv =
let p = Logic_const.pred_of_id_pred pred in
Logic_const.(pat (p,pre_label))
in
- let requires = Logic_const.pands (List.map norm_pred bhv.b_requires) in
+ let requires =
+ List.filter (fun x -> not x.ip_content.tp_only_check) bhv.b_requires
+ in
+ let requires = Logic_const.pands (List.map norm_pred requires) in
let assumes = Logic_const.pands (List.map norm_pred bhv.b_assumes) in
let precond = Logic_const.pimplies (assumes, requires) in
let precond_id = Logic_const.new_predicate precond in
@@ -159,12 +183,14 @@ 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 =
- 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
+ if pre.ip_content.tp_only_check then acc else begin
+ let id = WpPropId.mk_pre_id kf Kglobal bhv pre in
+ let labels = NormAtLabels.labels_fct_pre in
+ let p = Logic_const.pred_of_id_pred pre in
+ let p = Logic_const.(pat (p,pre_label)) in
+ let p = normalize id ?assumes labels p in
+ add_prop acc kind id p
+ end
let add_prop_fct_post acc kind kf bhv tkind post =
let id = WpPropId.mk_fct_post_id kf bhv (tkind, post) in
@@ -207,13 +233,24 @@ let add_prop_stmt_post acc kind kf s bhv tkind l_post ~assumes post =
let p = normalize id labels ?assumes p in
add_prop acc kind id p
+let update_kind kind pre =
+ if pre.ip_content.tp_only_check then begin
+ match kind with
+ | AcallPre(false,_) -> None
+ | AcallPre(true, kf) -> Some (AcallCheck kf)
+ | _ -> Some kind
+ end else Some kind
+
let add_prop_call_pre acc kind id ~assumes pre =
- let labels = NormAtLabels.labels_fct_pre in
- let p = Logic_const.pred_of_id_pred pre in
- (* assumes can be normalized in the same time *)
- let p = Logic_const.pimplies (assumes, p) in
- let p = normalize id labels p in
- add_prop acc kind id p
+ match update_kind kind pre with
+ | None -> acc
+ | Some kind ->
+ let labels = NormAtLabels.labels_fct_pre in
+ let p = Logic_const.pred_of_id_pred pre in
+ (* assumes can be normalized in the same time *)
+ let p = Logic_const.pimplies (assumes, p) in
+ let p = normalize id labels p in
+ add_prop acc kind id p
let add_prop_call_post acc kind called_kf bhv tkind ~assumes post =
let id = WpPropId.mk_fct_post_id called_kf bhv (tkind, post) in
@@ -439,6 +476,14 @@ let filter_both l =
p::h_acc, if goal then p::g_acc else g_acc
in List.fold_left add ([], []) l
+let filter_both_call l =
+ let add (h_acc, g_acc) (goal, p) =
+ match goal with
+ | CPboth -> p :: h_acc, p :: g_acc
+ | CPhyp -> p :: h_acc, g_acc
+ | CPgoal -> h_acc, p :: g_acc
+ in List.fold_left add ([], []) l
+
let get_both_hyp_goals annots = filter_both annots.info.p_both
let get_call_hyp annots fct =
@@ -446,7 +491,7 @@ let get_call_hyp annots fct =
with Not_found -> []
let get_call_pre annots fct =
- try filter_both (ForCall.find fct annots.info.call_pre)
+ try filter_both_call (ForCall.find fct annots.info.call_pre)
with Not_found -> [],[]
let get_call_post annots fct =
@@ -473,8 +518,14 @@ let pp_annots fmt acc =
Format.fprintf fmt "%s%s: %a@."
k (if b then "" else " (h)") WpPropId.pp_pred_of_pred_info p
in
+ let pp_pred_c k c p =
+ let kind = match c with CPboth -> "(h+g)" | CPgoal -> "g" | CPhyp -> "h" in
+ Format.fprintf fmt "%s%s: %a@."
+ k kind WpPropId.pp_pred_of_pred_info p
+ in
let pp_pred_list k l = List.iter (fun p -> pp_pred k true p) l in
let pp_pred_b_list k l = List.iter (fun (b, p) -> pp_pred k b p) l in
+ let pp_pred_c_list k l = List.iter (fun (c, p) -> pp_pred_c k c p) l in
begin
pp_pred_list "H" acc.p_hyp;
pp_pred_list "G" acc.p_goal;
@@ -488,7 +539,7 @@ let pp_annots fmt acc =
ForCall.iter
(fun kf bhs ->
let name = "CallPre:" ^ (Kernel_function.get_name kf) in
- pp_pred_b_list name bhs)
+ pp_pred_c_list name bhs)
acc.call_pre;
ForCall.iter
(fun kf asgn ->
diff --git a/src/plugins/wp/wpStrategy.mli b/src/plugins/wp/wpStrategy.mli
index 9177f1fe53676af44dc9d2ed1345dd6cbc64234d..8f30ea928ce13ce88e7d6f240dc2f4905fe0df8e 100644
--- a/src/plugins/wp/wpStrategy.mli
+++ b/src/plugins/wp/wpStrategy.mli
@@ -58,6 +58,9 @@ type annot_kind =
| AcallPre of bool * kernel_function
(** annotation is a called function precondition :
to be considered as hyp, and goal if bool=true *)
+ | AcallCheck of kernel_function
+ (** annotation is check-only called function precondition.
+ handled internally by {!add_prop_call_pre} below. *)
| AcallPost of kernel_function
(** annotation is a called function post check :
to be considered as goal only (no hyp) *)
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 51394d3c145b1a8a66650b4ddb7f957a6bac49e4..94bc7d0af63478b4c7a3dff2146d14c708425ca9 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -84,7 +84,7 @@ module Behaviors =
(struct
let option_name = "-wp-bhv"
let arg_name = "b,..."
- let help = "Select properties of the given behaviors (defaults to all behaviors) of the selected functions."
+ let help = "Select only properties belonging to listed behaviors."
end)
let () = on_reset Behaviors.clear
@@ -96,10 +96,14 @@ module Properties =
(struct
let option_name = "-wp-prop"
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, check, invariant, variant, breaks, continues, returns.\n\
- Starts by a minus character to remove properties from the selection."
+ let help =
+ "Select properties based names and category.\n\
+ Use +name or +category to select properties and -name or -category\n\
+ to remove them from the selection. The '+' sign can be omitted.\n\
+ Categories are: @lemma, @requires, @assigns, @ensures, @exits,\n\
+ @assert, @invariant, @variant, @breaks, @continues, @returns,\n\
+ @complete_behaviors, @disjoint_behaviors and\n\
+ @check (which includes all check clauses)."
end)
let () = on_reset Properties.clear
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 21f7f3a9fa1b25a40763c3172b6f9f529ac61746..032fa83fa1ee75034d6cfc2df03b5dd75cce06cd 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -722,7 +722,8 @@ let set_doomed emitter pid =
let pred_loc = Stmt.loc stmt in
let pred_name = [ "Wp" ; "SmokeTest" ] in
let pf = { Logic_const.pfalse with pred_loc ; pred_name } in
- let ca = Logic_const.new_code_annotation (AAssert ([],Assert,pf)) in
+ let pf = Logic_const.toplevel_predicate pf in
+ let ca = Logic_const.new_code_annotation (AAssert ([],pf)) in
Annotations.add_code_annot emitter ~kf stmt ca ; ca
in
List.iter (set_invalid emitter) (Property.ip_of_code_annot kf stmt ca)
diff --git a/tests/libc/check_const.ml b/tests/libc/check_const.ml
index 60f734a6e459c69be94b71a90bd1faad019d9f25..965f710a3caa345008a615bf2a99d4e4532a2f1c 100644
--- a/tests/libc/check_const.ml
+++ b/tests/libc/check_const.ml
@@ -21,7 +21,7 @@ let warn_if_not_const kf string typ vi loc =
string Printer.pp_varinfo vi string
let check_annot kf _ (a: identified_predicate) =
- let p = a.ip_content.pred_content in
+ let p = (Logic_const.pred_of_id_pred a).pred_content in
match p with
| Pvalid (_, t) | Pvalid_read (_, t)
| Papp ({l_var_info={lv_name=("valid_string"|"valid_read_string")}},
diff --git a/tests/libc/check_libc_naming_conventions.ml b/tests/libc/check_libc_naming_conventions.ml
index c7a991504950d391779f9761b7a51b4bb0a0d294..c928b21109bbdf51e6ef14a7d61d59db44b7fd73 100644
--- a/tests/libc/check_libc_naming_conventions.ml
+++ b/tests/libc/check_libc_naming_conventions.ml
@@ -58,21 +58,21 @@ let () =
if Cil.hasAttribute "fc_stdlib" fun_attrs then begin
Annotations.iter_behaviors (fun _emitter bhv ->
List.iter (fun ip ->
- let pred = ip.ip_content in
+ let pred = Logic_const.pred_of_id_pred ip in
warn_if_unnamed "requires" pred;
check_initialized pred;
check_dangling pred;
check_separated pred;
) bhv.b_requires;
List.iter (fun ip ->
- let pred = ip.ip_content in
+ let pred = Logic_const.pred_of_id_pred ip in
warn_if_unnamed "assumes" pred;
check_initialized pred;
check_dangling pred;
check_separated pred;
) bhv.b_assumes;
List.iter (fun (_termination, ip) ->
- let pred = ip.ip_content in
+ let pred = Logic_const.pred_of_id_pred ip in
warn_if_unnamed "ensures" pred;
check_initialized pred;
check_dangling pred;
diff --git a/tests/spec/add_global.ml b/tests/spec/add_global.ml
index 39b169539e4b0cf0ab265c7217223c93ba5b8bcd..0a8f954137c1f7f9ff583f8be0ef3e617fc3e0fc 100644
--- a/tests/spec/add_global.ml
+++ b/tests/spec/add_global.ml
@@ -15,7 +15,8 @@ object(self)
("MyAxiomatic",
[ Dlemma(
"myaxiom", true, [], [],
- Logic_const.ptrue, [], Cil_datatype.Location.unknown)],
+ Logic_const.(toplevel_predicate ptrue),
+ [], Cil_datatype.Location.unknown)],
[], Cil_datatype.Location.unknown)
in
Queue.add (fun () -> Annotations.add_global emitter ax)
diff --git a/tests/spec/bts0578.ml b/tests/spec/bts0578.ml
index df12b588dd1d7888ce952084172349671679de70..594d3b71e4b03b506173990f569c70b3ae21ddcf 100644
--- a/tests/spec/bts0578.ml
+++ b/tests/spec/bts0578.ml
@@ -16,12 +16,12 @@ let main () =
in
add s (AStmtSpec ([],contract))
in
- add s (AInvariant(["foo"], true, ptrue));
+ add s (AInvariant(["foo"], true, toplevel_predicate ptrue));
add s (AVariant(tinteger 0, None));
- add s (AInvariant([], true, ptrue));
- add s (AInvariant(["foo"], true, ptrue));
+ add s (AInvariant([], true, toplevel_predicate ptrue));
+ add s (AInvariant(["foo"], true, toplevel_predicate ptrue));
Filecheck.check_ast "after adding invariants";
- let requires = [Logic_const.new_predicate Logic_const.ptrue] in
+ let requires = [new_predicate ptrue] in
let bhv = [Cil.mk_behavior ~requires ()] in
add_behavior !s1 bhv;
Filecheck.check_ast "after adding contract";
diff --git a/tests/spec/expr_to_term.ml b/tests/spec/expr_to_term.ml
index b6ce6b3ab15e0fab3b0e5eb4f46909816c7b4d8d..450dd0d0235313762e4a527d5b891776c1db0566 100644
--- a/tests/spec/expr_to_term.ml
+++ b/tests/spec/expr_to_term.ml
@@ -11,7 +11,7 @@ let check_expr_term check fct s post =
in
let term =
match post with
- | (_, { ip_content = { pred_content = Papp(_,_,[l;_]) } }) -> l
+ | (_,{ip_content={tp_statement={pred_content = Papp(_,_,[l;_])}}}) -> l
| _ -> Kernel.fatal "Unexpected ensures %a" Printer.pp_post_cond post
in
let term' = Logic_utils.expr_to_term ~coerce:false exp in
diff --git a/tests/spec/generalized_check.i b/tests/spec/generalized_check.i
new file mode 100644
index 0000000000000000000000000000000000000000..7f7c9748c531a7cb0812633335a4ccbd1a73d558
--- /dev/null
+++ b/tests/spec/generalized_check.i
@@ -0,0 +1,42 @@
+/* run.config
+OPT: -wp -wp-prover qed -wp-msg-key no-cache-info,no-time-info
+OPT: -eva -eva-use-spec f
+OPT: -print
+*/
+/*@ check lemma easy_proof: \false; */ // should not be put in any environment
+
+/*@ check requires f_valid_x: \valid(x);
+ assigns *x;
+ check ensures f_init_x: *x == 0;
+*/
+void f(int* x) {
+ /*@ check f_valid_ko: \valid(x); */
+ *x = 0;
+}
+
+void loop(void);
+
+int main() {
+ int a = 4;
+ volatile int c;
+ int* p = (void*)0;
+ if (c) p = &a;
+ f(p);
+ /*@ check main_valid_ko: \valid(p); */
+ /*@ check main_p_content_ko: *p == 0; */
+ loop();
+}
+
+void loop () {
+ int j = 0;
+ /*@ check loop invariant false_but_preserved: j == 10;
+ loop assigns i;
+ */
+ for (int i = 0; i< 10; i++);
+ /*@ check implied_by_false_invariant: j == 10; */
+ l: /*@ check invariant \true; */ ;
+ if (j >= 10) goto l1;
+ j++;
+ goto l;
+ l1 : ;
+}
diff --git a/tests/spec/oracle/generalized_check.0.res.oracle b/tests/spec/oracle/generalized_check.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7f7128dfa8d7a982a69817b1f63a4e4ef677a02b
--- /dev/null
+++ b/tests/spec/oracle/generalized_check.0.res.oracle
@@ -0,0 +1,23 @@
+[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] tests/spec/generalized_check.i:30: Warning:
+ Unsupported generalized invariant, use loop invariant instead.
+ Ignored invariant
+ check invariant \true;
+[wp] Warning: Missing RTE guards
+[wp] tests/spec/generalized_check.i:37: Warning:
+ Missing assigns clause (assigns 'everything' instead)
+[wp] 11 goals scheduled
+[wp] [Qed] Goal typed_f_assigns : Valid
+[wp] [Failed] Goal typed_f_check_f_valid_ko
+[wp] [Qed] Goal typed_f_check_ensures_f_init_x : Valid
+[wp] [Failed] Goal typed_check_lemma_easy_proof
+[wp] [Qed] Goal typed_loop_loop_assigns : Valid
+[wp] [Failed] Goal typed_loop_check_implied_by_false_invariant
+[wp] [Failed] Goal typed_loop_check_loop_invariant_false_but_preserved_established
+[wp] [Failed] Goal typed_loop_check_loop_invariant_false_but_preserved_preserved
+[wp] [Failed] Goal typed_main_call_f_check_requires_f_valid_x
+[wp] [Failed] Goal typed_main_check_main_p_content_ko
+[wp] [Failed] Goal typed_main_check_main_valid_ko
+[wp] Proved goals: 3 / 11
+ Qed: 3
diff --git a/tests/spec/oracle/generalized_check.1.res.oracle b/tests/spec/oracle/generalized_check.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f93e7228b403b708b01b4386186ab29d200d1a5a
--- /dev/null
+++ b/tests/spec/oracle/generalized_check.1.res.oracle
@@ -0,0 +1,47 @@
+[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
+[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/spec/generalized_check.i:23: Warning:
+ accessing uninitialized left-value. assert \initialized(&c);
+[eva] using specification for function f
+[eva:alarm] tests/spec/generalized_check.i:24: Warning:
+ function f: precondition 'f_valid_x' got status unknown.
+[eva] tests/spec/generalized_check.i:9: Warning:
+ no \from part for clause 'assigns *x;'
+[eva:alarm] tests/spec/generalized_check.i:25: Warning:
+ check 'main_valid_ko' got status unknown.
+[eva:alarm] tests/spec/generalized_check.i:26: Warning:
+ check 'main_p_content_ko' got status unknown.
+[eva:alarm] tests/spec/generalized_check.i:32: Warning:
+ loop invariant 'false_but_preserved' got status invalid.
+[eva] tests/spec/generalized_check.i:35: starting to merge loop iterations
+[eva:alarm] tests/spec/generalized_check.i:36: Warning:
+ check 'implied_by_false_invariant' got status invalid.
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function loop:
+ j ∈ {10}
+[eva:final-states] Values at end of function main:
+ a ∈ [--..--]
+ p ∈ {{ NULL ; &a }}
+ __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+ ----------------------------------------------------------------------------
+ 3 functions analyzed (out of 3): 100% coverage.
+ In these functions, 25 statements reached (out of 28): 89% coverage.
+ ----------------------------------------------------------------------------
+ Some errors and warnings have been raised during the analysis:
+ by the Eva analyzer: 0 errors 1 warning
+ by the Frama-C kernel: 0 errors 0 warnings
+ ----------------------------------------------------------------------------
+ 1 alarm generated by the analysis:
+ 1 access to uninitialized left-values
+ ----------------------------------------------------------------------------
+ Evaluation of the logical properties reached by the analysis:
+ Assertions 0 valid 2 unknown 2 invalid 4 total
+ Preconditions 0 valid 1 unknown 0 invalid 1 total
+ 0% of the logical properties reached have been proven.
+ ----------------------------------------------------------------------------
diff --git a/tests/spec/oracle/generalized_check.2.res.oracle b/tests/spec/oracle/generalized_check.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..dd870d5dc009e1cf2c1e19963f7f6d1bbae27bfb
--- /dev/null
+++ b/tests/spec/oracle/generalized_check.2.res.oracle
@@ -0,0 +1,51 @@
+[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ check lemma easy_proof: \false;
+ */
+/*@ check requires f_valid_x: \valid(x);
+ check ensures f_init_x: *\old(x) ≡ 0;
+ assigns *x;
+ */
+void f(int *x)
+{
+ /*@ check f_valid_ko: \valid(x); */ ;
+ *x = 0;
+ return;
+}
+
+void loop(void);
+
+int main(void)
+{
+ int __retres;
+ int volatile c;
+ int a = 4;
+ int *p = (int *)0;
+ if (c) p = & a;
+ f(p);
+ /*@ check main_valid_ko: \valid(p); */ ;
+ /*@ check main_p_content_ko: *p ≡ 0; */ ;
+ loop();
+ __retres = 0;
+ return __retres;
+}
+
+void loop(void)
+{
+ int j = 0;
+ {
+ int i = 0;
+ /*@ check loop invariant false_but_preserved: j ≡ 10;
+ loop assigns i; */
+ while (i < 10) i ++;
+ }
+ /*@ check implied_by_false_invariant: j ≡ 10; */ ;
+ l: /*@ check invariant \true; */ ;
+ if (j >= 10) goto l1;
+ j ++;
+ goto l;
+ l1: ;
+ return;
+}
+
+
diff --git a/tests/syntax/syntactic_hook.ml b/tests/syntax/syntactic_hook.ml
index c6a5d1f3517e261599913c4c0f8f577ece146a2c..5a479278793dbeb6d7f90325d44d63a624fc95d7 100644
--- a/tests/syntax/syntactic_hook.ml
+++ b/tests/syntax/syntactic_hook.ml
@@ -13,10 +13,15 @@ class visit = object
[{ stmt_ghost = false;
stmt_node =
CODE_ANNOT(
- AAssert([], Assert,
- { lexpr_node =
- PLat ({ lexpr_node = PLtrue; lexpr_loc = loc},"Pre");
- lexpr_loc = loc}), loc)};
+ AAssert(
+ [],
+ { tp_only_check = false;
+ tp_statement =
+ { lexpr_node =
+ PLat ({ lexpr_node = PLtrue; lexpr_loc = loc},"Pre");
+ lexpr_loc = loc}
+ }),
+ loc)};
s]
end