Commit af482dc9 authored by Patrick Baudin's avatar Patrick Baudin

Merge branch '771-wp-multiple-instances-of-the-generic-list-type' into 'master'

Resolve "[wp]: multiple instances of the generic \list type"

Closes #771

See merge request frama-c/frama-c!2485
parents 23248802 80cd98c6
......@@ -231,6 +231,13 @@ struct
| _ ->
assert (hash_head a <> hash_head b) ; false
let equal_tau t1 t2 =
match t1, t2 with
| None, None -> true
| None, Some _ | Some _ , None -> false
| Some (Bool|Prop) , Some(Bool|Prop) -> true
| Some t1, Some t2 -> Tau.equal t1 t2
let sort x = x.sort
let vars x = x.vars
let bvars x = x.bind
......@@ -673,7 +680,9 @@ struct
(struct
type t = term
let hash t = t.hash
let equal t1 t2 = equal_repr t1.repr t2.repr
let equal t1 t2 =
equal_tau t1.tau t2.tau &&
equal_repr t1.repr t2.repr
end)
(* -------------------------------------------------------------------------- *)
......
......@@ -110,7 +110,9 @@ let () = let open LogicBuiltins in add_builtin "\\bit_test" [Z;Z] f_bit_positive
let f_bits = [ f_bit_stdlib ; f_bit_positive ; f_bit_export ]
let bit_test e k =
F.e_fun (if k <= 0 then f_bit_positive else f_bit_stdlib) [e ; e_int k]
let r = F.e_fun ~result:Logic.Bool
(if k <= 0 then f_bit_positive else f_bit_stdlib) [e ; e_int k]
in assert (is_prop r) ; r
(* -------------------------------------------------------------------------- *)
(* --- Matching utilities for simplifications --- *)
......@@ -483,7 +485,7 @@ let smp2 f zf = (* f(c1,c2) ~> zf(c1,c2), f(c1,c2,...) ~> f(zf(c1,c2),...) *)
end
| _ -> raise Not_found
let bitk_positive k e = F.e_fun f_bit_positive [e;k]
let bitk_positive k e = F.e_fun ~result:Logic.Bool f_bit_positive [e;k]
let smp_mk_bit_stdlib = function
| [ a ; k ] when is_positive_or_null k ->
(* No need to expand the logic definition of the ACSL stdlib symbol when
......@@ -767,12 +769,13 @@ let smp_leq_with_lsr a0 b0 =
smp_cmp_with_lsr e_leq a0 b0
(* Rewritting at export *)
let bitk_export k e = F.e_fun ~result:Logic.Bool f_bit_export [e;k]
let export_eq_with_land a b =
let es = match_fun f_land a in
if b == e_zero then
let k,_,es = match_binop_one_extraction f_lsl es in
(* e1 & ... & en & (1 << k) = 0 <==> !bit_test(e1 & ... & en, k) *)
e_not (e_fun f_bit_export [e_fun f_land es ; k ])
e_not (bitk_export k (e_fun f_land es))
else raise Not_found
(* ACSL Semantics *)
......
/*@
axiomatic LISTS {
type ta;
type tb;
logic \list<ta> EmptyA = \Nil;
logic \list<tb> EmptyB = \Nil;
lemma A: \length(EmptyA) == \length(EmptyB) ;
}
*/
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_711.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
------------------------------------------------------------
Axiomatic 'LISTS'
------------------------------------------------------------
Lemma A:
Prove: (length L_EmptyB)=(length L_EmptyA)
------------------------------------------------------------
{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1, "rank": 1 },
"wp:main": { "total": 1, "valid": 1, "rank": 1 } },
"wp:axiomatics": { "LISTS": { "lemma_A": { "why3:Alt-Ergo,2.0.0": { "total": 1,
"valid": 1,
"rank": 1 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 1 } },
"wp:section": { "why3:Alt-Ergo,2.0.0":
{ "total": 1, "valid": 1,
"rank": 1 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 1 } } } } }
# frama-c -wp [...]
[kernel] Parsing tests/wp_bts/issue_711.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] 1 goal scheduled
[wp] [Alt-Ergo 2.0.0] Goal typed_lemma_A : Valid
[wp] Proved goals: 1 / 1
Qed: 0
Alt-Ergo 2.0.0: 1
[wp] Report in: 'tests/wp_bts/oracle_qualif/issue_711.0.report.json'
[wp] Report out: 'tests/wp_bts/result_qualif/issue_711.0.report.json'
-------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic LISTS - 1 (1..12) 1 100%
-------------------------------------------------------------
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