Commit 3486b24d authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[kernel] add support in the AST to identify check-and-forget annotations

this is a generalization of `check` vs. `assert` to other annotations. Not all
annotations are relevant though. Currently, there are more annotation nodes in
the AST that can have a flag `{ tp_only_check }` than was deemed useful in
pub/frama-c#25, but said flag can in fact safely be ignored. Moreover, this
commit only add this flag in the AST, but provides no further mean to set it to
true except for the original `check` keyword (i.e. on `AAssert`). The parser
and the behavior of the plugins that can handle the flag will be updated in
subsequent commits
parent 6bf55767
......@@ -8890,9 +8890,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)),
......@@ -9414,9 +9419,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
......
......@@ -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 ::
......
......@@ -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
......
......@@ -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;
......
......@@ -660,7 +660,7 @@ class erase_exn =
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,
......
......@@ -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
......
......@@ -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;
......
......@@ -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
......
......@@ -739,13 +739,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} *)
......@@ -1147,8 +1150,8 @@ let add_code_annot ?(keep_empty=true) emitter ?kf stmt ca =
Code_annots.add stmt tbl
in
match ca.annot_content with
| AAssert(l, kind, p) ->
let a = { ca with annot_content=AAssert(l,kind,extend_name emitter p) } in
| AAssert(l, p) ->
let a = { ca with annot_content=AAssert(l,extend_name emitter p) } in
fill_tables a (Property.ip_of_code_annot kf stmt a)
| AInvariant(l, b, p) ->
let a={ca with annot_content=AInvariant(l,b,extend_name emitter p)} in
......@@ -1283,11 +1286,13 @@ let add_code_annot ?(keep_empty=true) emitter ?kf stmt ca =
fill_tables ca (Property.ip_of_code_annot kf stmt ca)
let add_assert e ?kf stmt a =
let a = Logic_const.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} *)
......
......@@ -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
......
......@@ -272,7 +272,7 @@ let get_kf = function
| IPTypeInvariant _ | IPGlobalInvariant _ -> None
let rec get_names = function
| IPPredicate ip -> ip.ip_pred.ip_content.pred_name
| IPPredicate ip -> (Logic_const.pred_of_id_pred ip.ip_pred).pred_name
| IPExtended { ie_ext = {ext_name = name} }
| IPAxiom { il_name = name }
| IPAxiomatic { iax_name = name }
......@@ -285,8 +285,8 @@ let rec get_names = function
| IPCodeAnnot annot ->
begin
match annot.ica_ca.annot_content with
| AAssert (_, _, pred)
| AInvariant (_, _, pred) -> pred.pred_name
| AAssert (_, pred)
| AInvariant (_, _, pred) -> pred.tp_statement.pred_name
| _ -> []
end
| IPComplete _ | IPDisjoint _ | IPAllocation _
......@@ -302,7 +302,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}
......@@ -709,9 +709,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}
......@@ -725,9 +726,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"
......@@ -940,7 +943,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
| [] -> ()
......@@ -997,13 +1001,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"
......@@ -1127,7 +1131,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
......@@ -1187,14 +1191,13 @@ 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 ]
[K kf ; A "loop_invariant" ; P p.tp_statement ]
| IPCodeAnnot {ica_kf=kf; ica_ca={annot_content=AInvariant (_, false, p)}} ->
[K kf ; A "invariant" ; P p ]
[K kf ; A "invariant" ; 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 _}} ->
......@@ -1508,8 +1511,10 @@ let ip_of_global_annotation a =
let iax_props = List.fold_left aux [] l in
IPAxiomatic {iax_name; iax_props} :: (iax_props @ acc)
| Dlemma(il_name, true, il_labels, il_args, il_pred, _, il_loc) ->
let il_pred = il_pred.tp_statement in
ip_axiom {il_name; il_labels; il_args; il_pred; il_loc} :: acc
| Dlemma(il_name, false, il_labels, il_args, il_pred, _, il_loc) ->
let il_pred = il_pred.tp_statement in
ip_lemma {il_name; il_labels; il_args; il_pred; il_loc} :: acc
| Dinvariant(l, igi_loc) ->
let igi_pred = match l.l_body with
......
......@@ -3060,16 +3060,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"
......@@ -3098,12 +3094,12 @@ class cil_printer () = object (self)
fprintf fmt "@[<2>%a%a@ %a;@]"
pp_for_behavs behav
self#pp_acsl_keyword "loop invariant"
self#predicate i
self#predicate i.tp_statement
| AInvariant(behav,false,i) ->
fprintf fmt "@[<2>%a%a@ %a;@]"
pp_for_behavs behav
self#pp_acsl_keyword "invariant"
self#predicate i
self#predicate i.tp_statement
| AVariant v ->
self#variant fmt v
| AExtended (behav, is_loop, e) ->
......@@ -3204,7 +3200,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"
......
......@@ -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) ->
......
......@@ -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