Commit f91260fb authored by Lionel Blatter's avatar Lionel Blatter Committed by Virgile Prevosto
Browse files

Add support for recursive Extended annotation in AST

parent 292964f3
......@@ -442,28 +442,33 @@ let hash_list f l =
| _ -> acc
in aux 47 3 l
let hash_ext_kind = function
| Ext_id i -> Datatype.Int.hash i
| Ext_terms terms -> 29 * (hash_list Logic_utils.hash_term terms)
| Ext_preds preds -> 47 * (hash_list Logic_utils.hash_predicate preds)
let compare_ext_kind k1 k2 =
match k1, k2 with
| Ext_id i1, Ext_id i2 -> Datatype.Int.compare i1 i2
| Ext_id _, _ -> 1 | _, Ext_id _ -> -1
| Ext_terms terms1, Ext_terms terms2 ->
Extlib.list_compare Logic_utils.compare_term terms1 terms2
| Ext_terms _, _ -> 1 | _, Ext_terms _ -> -1
| Ext_preds p1, Ext_preds p2 ->
Extlib.list_compare Logic_utils.compare_predicate p1 p2
module ExtMerging =
Merging
(struct
type t = acsl_extension
let hash (e : acsl_extension) =
let rec hash (e : acsl_extension) =
let hash_ext_kind = function
| Ext_id i -> Datatype.Int.hash i
| Ext_terms terms -> 29 * (hash_list Logic_utils.hash_term terms)
| Ext_preds preds -> 47 * (hash_list Logic_utils.hash_predicate preds)
| Ext_annot annots -> 5 * (hash_list hash annots)
in
Datatype.String.hash e.ext_name + 5 * hash_ext_kind e.ext_kind
let compare (e1 : acsl_extension) (e2 : acsl_extension) =
let rec compare (e1 : acsl_extension) (e2 : acsl_extension) =
let compare_ext_kind k1 k2 =
match k1, k2 with
| Ext_id i1, Ext_id i2 -> Datatype.Int.compare i1 i2
| Ext_id _, _ -> 1 | _, Ext_id _ -> -1
| Ext_terms terms1, Ext_terms terms2 ->
Extlib.list_compare Logic_utils.compare_term terms1 terms2
| Ext_terms _, _ -> 1 | _, Ext_terms _ -> -1
| Ext_preds p1, Ext_preds p2 ->
Extlib.list_compare Logic_utils.compare_predicate p1 p2
| Ext_preds _, _ -> 1 | _, Ext_preds _ -> -1
| Ext_annot a1 , Ext_annot a2 ->
Extlib.list_compare compare a1 a2
in
let res = Datatype.String.compare e1.ext_name e2.ext_name in
if res <> 0 then res
else
......
......@@ -1692,6 +1692,7 @@ and acsl_extension_kind =
| Ext_id of int (** id used internally by the extension itself. *)
| Ext_terms of term list
| Ext_preds of predicate list
| Ext_annot of acsl_extension list
(** a list of predicates, the most common case of for extensions *)
(** Where are we expected to find corresponding extension keyword.
......
......@@ -921,6 +921,7 @@ and pp_acsl_extension_kind fmt = function
| Ext_id(int) -> Format.fprintf fmt "Ext_id(%a)" pp_int int
| Ext_terms(term_list) -> Format.fprintf fmt "Ext_terms(%a)" (pp_list pp_term) term_list
| Ext_preds(predicate_list) -> Format.fprintf fmt "Ext_preds(%a)" (pp_list pp_predicate) predicate_list
| Ext_annot(annotation_list ) -> Format.fprintf fmt "Ext_annots(%a)" (pp_list pp_acsl_extension) annotation_list
and pp_behavior fmt behavior =
Format.fprintf fmt
......
......@@ -47,6 +47,7 @@ let default_printer printer fmt = function
| Ext_id i -> Format.fprintf fmt "%d" i
| Ext_terms ts -> Pretty_utils.pp_list ~sep:",@ " printer#term fmt ts
| Ext_preds ps -> Pretty_utils.pp_list ~sep:",@ " printer#predicate fmt ps
| Ext_annot an -> Pretty_utils.pp_list ~sep:",@ " printer#extended fmt an
let default_short_printer name _printer fmt _ext_kind =
Format.fprintf fmt "%s" name
......
......@@ -1994,6 +1994,9 @@ and childrenCilExtended vis p =
| Ext_preds preds ->
let preds' = mapNoCopy (visitCilPredicate vis) preds in
if preds == preds' then p else Ext_preds preds'
| Ext_annot annots ->
let annots' = mapNoCopy (visitCilExtended vis) annots in
if annots == annots' then p else Ext_annot annots'
and visitCilPredicates vis ps = mapNoCopy (visitCilIdPredicate vis) ps
......
......@@ -1186,7 +1186,7 @@ let is_same_pragma p1 p2 =
| Impact_pragma p1, Impact_pragma p2 -> is_same_impact_pragma p1 p2
| (Loop_pragma _ | Slice_pragma _ | Impact_pragma _), _ -> false
let is_same_extension x1 x2 =
let rec is_same_extension x1 x2 =
Datatype.String.equal x1.ext_name x2.ext_name &&
(x1.ext_has_status = x2.ext_has_status) &&
match x1.ext_kind, x2.ext_kind with
......@@ -1195,7 +1195,9 @@ let is_same_extension x1 x2 =
is_same_list is_same_term t1 t2
| Ext_preds p1, Ext_preds p2 ->
is_same_list is_same_predicate p1 p2
| (Ext_id _ | Ext_preds _ | Ext_terms _), _ -> false
| Ext_annot a1, Ext_annot a2 ->
is_same_list is_same_extension a1 a2
| (Ext_id _ | Ext_preds _ | Ext_terms _ | Ext_annot _ ), _ -> false
let is_same_code_annotation (ca1:code_annotation) (ca2:code_annotation) =
match ca1.annot_content, ca2.annot_content with
......
......@@ -148,6 +148,7 @@ let printer _pp fmt ext =
match ext with
| Ext_id _ -> assert false
| Ext_preds _ -> assert false
| Ext_annot _ -> assert false
| Ext_terms terms ->
match widen_hint_terms_of_terms terms with
| Some (hint_lval, hint_terms) ->
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment