Commit f20e009f authored by Julien Signoles's avatar Julien Signoles
Browse files

Merge branch 'bugfix/issue549' into 'master'

Bugfix/issue549

See merge request frama-c/e-acsl!289
parents 18eac92b 760e4405
......@@ -239,8 +239,7 @@ let rec infer t =
let i1 = infer t1 in
let i2 = infer t2 in
Ival.bitwise_or i1 i2
| TCastE (ty, t)
| TCoerce (t, ty) ->
| TCastE (ty, t) ->
(try
let it = infer t in
let ity = interv_of_typ ty in
......@@ -281,10 +280,6 @@ let rec infer t =
| _ -> assert false)
| Tnull -> singleton_of_int 0
| TLogic_coerce (_, t) -> infer t
| TCoerceE (t1, t2) ->
let i1 = infer t1 in
let i2 = infer t2 in
Ival.meet i1 i2
| Tapp (li, _, _args) ->
(match li.l_body with
......
......@@ -338,8 +338,6 @@ module rec Transfer
| Toffset _ -> Error.not_yet "\\offset"
| Tblock_length _ -> Error.not_yet "\\block_length"
| TLogic_coerce(_, t) -> register_term kf varinfos t
| TCoerce _ -> Error.not_yet "coerce"
| TCoerceE _ -> Error.not_yet "coerce expression"
| TUpdate _ -> Error.not_yet "functional update"
| Ttypeof _ -> Error.not_yet "typeof"
| Tempty_set -> Error.not_yet "empty set"
......@@ -372,7 +370,7 @@ module rec Transfer
| Pdangling _ -> Error.not_yet "\\dangling"
| Ptrue | Pfalse | Papp _ | Prel _
| Pand _ | Por _ | Pxor _ | Pimplies _ | Piff _ | Pnot _ | Pif _
| Pforall _ | Pexists _ | Pat _ | Psubtype _ ->
| Pforall _ | Pexists _ | Pat _ ->
Cil.DoChildren
| Plet(li, _) ->
if may_alias li then Error.not_yet "let-binding on array or pointer"
......@@ -391,7 +389,7 @@ module rec Transfer
| TUnOp _ | TBinOp _ | Ttypeof _ | TSizeOfE _
| TLval _ | TAlignOfE _ | TCastE _ | TAddrOf _
| TStartOf _ | Tapp _ | Tlambda _ | TDataCons _ | Tif _ | Tat _
| TCoerce _ | TCoerceE _ | TUpdate _ | Tunion _ | Tinter _
| TUpdate _ | Tunion _ | Tinter _
| Tcomprehension _ | Trange _ | TLogic_coerce _ ->
(* potential sub-term inside *)
Cil.DoChildren
......
......@@ -541,8 +541,6 @@ and context_insensitive_term_to_exp kf env t =
e, env, false, name
| Tblock_length _ -> not_yet env "labeled \\block_length"
| Tnull -> Cil.mkCast (Cil.zero ~loc) (TPtr(TVoid [], [])), env, false, "null"
| TCoerce _ -> Error.untypable "coercion" (* Jessie specific *)
| TCoerceE _ -> Error.untypable "expression coercion" (* Jessie specific *)
| TUpdate _ -> not_yet env "functional update"
| Ttypeof _ -> not_yet env "typeof"
| Ttype _ -> not_yet env "C type"
......@@ -808,7 +806,6 @@ and named_predicate_content_to_exp ?name kf env p =
Mmodel_translate.call ~loc kf "freeable" Cil.intType env t
| Pfreeable _ -> not_yet env "labeled \\freeable"
| Pfresh _ -> not_yet env "\\fresh"
| Psubtype _ -> Error.untypable "subtyping relation" (* Jessie specific *)
and named_predicate_to_exp ?name kf ?rte env p =
let rte = match rte with None -> Env.generate_rte env | Some b -> b in
......
......@@ -389,8 +389,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| TBinOp (BXor, _, _) -> Error.not_yet "bitwise xor"
| TBinOp (BOr, _, _) -> Error.not_yet "bitwise or"
| TCastE(_, t')
| TCoerce(t', _) ->
| TCastE(_, t') ->
let ctx =
try
(* compute the smallest interval from the whole term [t] *)
......@@ -427,20 +426,6 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| TLogic_coerce (_, t) ->
dup (type_term ~use_gmp_opt ~arith_operand ?ctx t).ty
| TCoerceE (t1, t2) ->
let ctx =
try
let i = Interval.infer t in
let i1 = Interval.infer t1 in
let i2 = Interval.infer t2 in
ty_of_interv ?ctx (Ival.join i (Ival.join i1 i2))
with Interval.Not_an_integer ->
Other
in
ignore (type_term ~use_gmp_opt:true ~ctx t1);
ignore (type_term ~use_gmp_opt:true ~ctx t2);
dup ctx
| TAddrOf tlv
| TStartOf tlv ->
(* it is a pointer, but subterms must be typed. *)
......@@ -681,7 +666,6 @@ let rec type_predicate p =
| Pexists _ -> Error.not_yet "unguarded \\exists quantification"
| Pat(p, _) -> (type_predicate p).ty
| Pfresh _ -> Error.not_yet "\\fresh"
| Psubtype _ -> Error.not_yet "subtyping relation" (* Jessie specific *)
in
coerce ~arith_operand:false ~ctx:c_int ~op c_int
......
Supports Markdown
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