Commit d5b08c0d authored by Tristan Le Gall's avatar Tristan Le Gall Committed by Julien Signoles
Browse files

supression of Psubtype and PLsubtype (jessie)

parent cdedac5f
......@@ -525,8 +525,6 @@ lexpr_inner:
| LPAR range RPAR { info $2.lexpr_node }
| LPAR cast_logic_type RPAR lexpr_inner %prec prec_cast
{ info (PLcast ($2, $4)) }
| lexpr_inner LTCOLON lexpr_inner %prec prec_cast
{ info (PLsubtype ($1, $3)) }
| lexpr_inner COLONGT logic_type
{ info (PLcoercion ($1, $3)) }
| lexpr_inner COLONGT lexpr_inner %prec prec_cast
......
......@@ -803,7 +803,7 @@ to function contracts."
| Pvalid_function _ ->
DoChildren
| Papp _ | Pallocable _ | Pfreeable _ | Pfresh _ | Psubtype _
| Papp _ | Pallocable _ | Pfreeable _ | Pfresh _
-> fail ()
method private do_term_lval t =
......
......@@ -1583,8 +1583,6 @@ and predicate_node =
| Pfresh of logic_label * logic_label * term * term
(** \fresh(pointer, n)
A memory block of n bytes is newly allocated to the pointer.*)
| Psubtype of term * term
(** First term is a type tag that is a subtype of the second. *)
(** predicate with an unique identifier. Use {!Logic_const.new_predicate} to
create fresh predicates *)
......
......@@ -199,7 +199,6 @@ module Precedence = struct
| Pfresh _ -> 0
| Papp _ as p -> if subset_is_backslash_in p = None then 0 else 36
| Pnot _ -> 30
| Psubtype _ -> 75
| Pand _ -> and_level
| Pxor _ -> xor_level
| Por _ -> or_level
......@@ -2654,8 +2653,6 @@ class cil_printer () = object (self)
self#pred_prec_named (Precedence.upperLevel,p)
self#logic_label lab;
current_label <- old_label
| Psubtype (e,ce) ->
fprintf fmt "@[%a@ <:@ %a@]" term e term ce
method private decrement kw fmt (t, rel) = match rel with
| None -> fprintf fmt "@[<2>%a@ %a;@]" self#pp_acsl_keyword kw self#term t
......
......@@ -879,8 +879,6 @@ and pp_predicate_node fmt = function
| Pfresh(logic_label1,logic_label2,term1,term2) ->
Format.fprintf fmt "Pfresh(%a,%a,%a,%a)" pp_logic_label logic_label1 pp_logic_label logic_label2
pp_term term1 pp_term term2
| Psubtype(term1,term2) ->
Format.fprintf fmt "Psubtype(%a,%a)" pp_term term1 pp_term term2
and pp_identified_predicate fmt identified_predicate =
Format.fprintf fmt "{ip_id=%d;ip_content=%a}"
......
......@@ -133,7 +133,7 @@ let getParenthLevel e =
| PLvalid _ | PLvalid_read _ | PLvalid_function _
| PLinitialized _ | PLdangling _
| PLallocable _ | PLfreeable _ | PLfresh _
| PLseparated _ | PLsubtype _ | PLunion _ | PLinter _ -> 10
| PLseparated _ | PLunion _ | PLinter _ -> 10
| PLvar _ | PLconstant _ | PLresult | PLnull | PLtypeof _ | PLtype _
| PLfalse | PLtrue | PLcomprehension _ | PLempty | PLset _ | PLlist _ -> 0
......@@ -273,8 +273,6 @@ and print_lexpr_level n fmt e =
| PLfresh (l2,e1,e2) ->
fprintf fmt "\\fresh%a(@;@[%a@],@[%a@]@;)" print_label_2 l2 print_lexpr_plain e1 print_lexpr_plain e2
| PLnamed(s,e) -> fprintf fmt "%s:@ %a" s print_lexpr e
| PLsubtype (e1,e2) ->
fprintf fmt "%a@ <:@ %a" print_lexpr e1 print_lexpr e2
| PLcomprehension(e,q,p) ->
fprintf fmt "{@ @[%a;@ %a%a@]@ }"
print_lexpr e print_quantifiers q
......
......@@ -2894,10 +2894,6 @@ and childrenLogicLabel vis l =
let t' = vTerm t in
let n' = vTerm n in
if t' != t || n' != n || s1 != s1' || s2 != s2' then Pfresh (s1',s2',t',n') else p
| Psubtype(te,tc) ->
let tc' = vTerm tc in
let te' = vTerm te in
if tc' != tc || te' != te then Psubtype(te',tc') else p
and visitCilIdTerm vis loc =
doVisitCil vis vis#behavior.cidentified_term vis#videntified_term
......@@ -7882,7 +7878,6 @@ and free_vars_predicate bound_vars p = match p.pred_content with
seps
| Pfresh (_,_,t1,t2)
| Prel (_,t1,t2)
| Psubtype (t1,t2)
->
Logic_var.Set.union
(free_vars_term bound_vars t1)
......
......@@ -444,8 +444,6 @@ let pinitialized ?(loc=Cil_datatype.Location.unknown) (l,p) =
unamed ~loc (Pinitialized (l,p))
let pdangling ?(loc=Cil_datatype.Location.unknown) (l,p) =
unamed ~loc (Pdangling (l,p))
let psubtype ?(loc=Cil_datatype.Location.unknown) (p,q) =
unamed ~loc (Psubtype (p,q))
let pseparated ?(loc=Cil_datatype.Location.unknown) seps =
unamed ~loc (Pseparated seps)
......
......@@ -188,9 +188,6 @@ val pvalid_index: ?loc:location -> logic_label * term * term -> predicate
(** \valid_range: requires bounds having integer type *)
val pvalid_range: ?loc:location -> logic_label * term * term * term -> predicate
(** subtype relation *)
val psubtype: ?loc:location -> term * term -> predicate
(** \separated *)
val pseparated: ?loc:location -> term list -> predicate
......
......@@ -1044,7 +1044,6 @@ struct
| Pinitialized (_,t) | Pdangling (_, t)
| Pallocable(_,t) | Pfreeable(_,t)-> needs_at t
| Pfresh (_,_,t,n) -> (needs_at t) && (needs_at n)
| Psubtype _ -> false
in
if needs_at idx then tat ~loc:idx.term_loc (idx,here_label) else idx
......@@ -3000,7 +2999,7 @@ struct
| PLfresh _ | PLallocable _ | PLfreeable _
| PLinitialized _ | PLdangling _ | PLexists _ | PLforall _
| PLimplies _ | PLiff _
| PLxor _ | PLsubtype _ | PLseparated _ ->
| PLxor _ | PLseparated _ ->
if ctxt.silent then raise Backtrack;
ctxt.error loc "syntax error (expression expected but predicate found)"
and type_relation:
......@@ -3431,7 +3430,6 @@ struct
| PLrange _ -> ctxt.error loc "cannot use operator .. within a predicate"
| PLnamed (n, p) ->
let p = predicate env p in { p with pred_name = n::p.pred_name }
| PLsubtype (t,tc) -> psubtype ~loc (term env t, term env tc)
| PLseparated seps ->
let seps = List.map (term_ptr ~check_non_void:true) seps in
pseparated ~loc seps
......
......@@ -900,8 +900,6 @@ and is_same_predicate_node p1 p2 =
| Pfresh (l1,m1,t1,n1), Pfresh (l2,m2,t2,n2) ->
is_same_logic_label l1 l2 && is_same_logic_label m1 m2 &&
is_same_term t1 t2 && is_same_term n1 n2
| Psubtype(lt1,rt1), Psubtype(lt2,rt2) ->
is_same_term lt1 lt2 && is_same_term rt1 rt2
| Pseparated(seps1), Pseparated(seps2) ->
(try List.for_all2 is_same_term seps1 seps2
with Invalid_argument _ -> false)
......@@ -909,7 +907,7 @@ and is_same_predicate_node p1 p2 =
| Piff _ | Pnot _ | Pif _ | Plet _ | Pforall _ | Pexists _
| Pat _ | Pvalid _ | Pvalid_read _ | Pvalid_function _
| Pinitialized _ | Pdangling _
| Pfresh _ | Pallocable _ | Pfreeable _ | Psubtype _ | Pxor _ | Pseparated _
| Pfresh _ | Pallocable _ | Pfreeable _ | Pxor _ | Pseparated _
), _ -> false
and is_same_predicate pred1 pred2 =
......@@ -1220,8 +1218,7 @@ and is_same_lexpr l1 l2 =
is_same_opt is_same_lexpr l1 l2 && is_same_opt is_same_lexpr h1 h2
| PLsizeof t1, PLsizeof t2 -> is_same_pl_type t1 t2
| PLsizeofE e1,PLsizeofE e2 | PLtypeof e1,PLtypeof e2-> is_same_lexpr e1 e2
| PLcoercionE (b1,t1), PLcoercionE(b2,t2)
| PLsubtype(b1,t1), PLsubtype(b2,t2) ->
| PLcoercionE (b1,t1), PLcoercionE(b2,t2) ->
is_same_lexpr b1 b2 && is_same_lexpr t1 t2
| PLupdate(b1,p1,r1), PLupdate(b2,p2,r2) ->
is_same_lexpr b1 b2
......@@ -1280,7 +1277,7 @@ and is_same_lexpr l1 l2 =
| PLexists _ | PLvalid _ | PLvalid_read _ | PLvalid_function _
| PLfreeable _ | PLallocable _
| PLinitialized _ | PLdangling _ | PLseparated _ | PLfresh _ | PLnamed _
| PLsubtype _ | PLcomprehension _ | PLunion _ | PLinter _
| PLcomprehension _ | PLunion _ | PLinter _
| PLset _ | PLempty
),_ -> false
......@@ -1507,9 +1504,6 @@ and hash_predicate (acc,depth,tot) p =
(acc + 259 + hash_label l1 + hash_label l2, depth - 1, tot - 2) t1
in
hash_term (acc, depth-1, tot) t2
| Psubtype(t1, t2) ->
let (acc, tot) = hash_term (acc + 263, depth - 1, tot - 1) t1 in
hash_term (acc, depth - 1, tot) t2
end
let hash_term t =
......@@ -1834,11 +1828,6 @@ and compare_predicate_node p1 p2 =
else res
| Pfresh _, _ -> 1
| _, Pfresh _ -> -1
| Psubtype(lt1,rt1), Psubtype(lt2,rt2) ->
let res = compare_term lt1 lt2 in
if res = 0 then compare_term rt1 rt2 else res
| Psubtype _, _ -> 1
| _, Psubtype _ -> -1
| Pseparated(seps1), Pseparated(seps2) ->
Extlib.list_compare compare_term seps1 seps2
......
......@@ -147,8 +147,6 @@ and lexpr_node =
| PLseparated of lexpr list
(** separation predicate. *)
| PLnamed of string * lexpr (** named expression. *)
| PLsubtype of lexpr * lexpr
(** first type tag is a subtype of second one. *)
(* tsets *)
| PLcomprehension of lexpr * quantifiers * lexpr option
(** set of expression defined in comprehension
......
......@@ -1968,7 +1968,6 @@ let rec reduce_by_predicate ~alarm_mode env positive p =
| true, Pexists (_, _) | false, Pforall (_, _)
| _,Plet (_, _)
| _,Pallocable (_,_) | _,Pfreeable (_,_) | _,Pfresh (_,_,_,_)
| _,Psubtype _
| _, Pseparated _
-> env
in
......@@ -2223,7 +2222,6 @@ and eval_predicate env pred =
| Pfresh (_,_,_,_)
| Pallocable _ | Pfreeable _
| Plet (_,_)
| Psubtype _
-> Unknown
(* Logic predicates. Update the list known_predicates above if you
......@@ -2372,7 +2370,7 @@ let predicate_deps env pred =
| Some p' -> do_eval env p'
end
| Pfresh _ | Pallocable _ | Pfreeable _ | Psubtype _
| Pfresh _ | Pallocable _ | Pfreeable _
-> assert false
in
do_eval env pred
......
......@@ -896,8 +896,6 @@ struct
"Allocation, initialization and danglingness not yet implemented@\n\
@[<hov 0>(%a)@]" Printer.pp_predicate p
| Psubtype _ ->
Warning.error "Type tags not implemented yet"
(* -------------------------------------------------------------------------- *)
(* --- Set of locations for a term representing a set of l-values --- *)
......
......@@ -482,7 +482,7 @@ and addr_lval env (h,ofs) = match h with
(* --- Predicates --- *)
and pred (env:ctx) p : value = match p.pred_content with
| Psubtype (_, _) | Pfalse | Ptrue -> E.bot
| Pfalse | Ptrue -> E.bot
(* Unary *)
| Pat(p,_)
......
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