Commit a783ea6d authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch '775-boolean-comparisons-are-unusable-in-wp' into 'master'

Resolve "boolean comparisons are unusable in WP"

Closes #775

See merge request frama-c/frama-c!2490
parents 46ad0e65 151d43ed
......@@ -34,6 +34,11 @@ let option_import = LogicBuiltins.create_option
(fun ~driver_dir:_ x -> x)
"why3" "import"
let option_qual =
LogicBuiltins.create_option
(fun ~driver_dir:_ x -> x)
"why3" "qualifier"
let why3_failure msg =
Pretty_utils.ksfprintf failwith msg
......@@ -227,6 +232,16 @@ let regexp_dot = Str.regexp_string "."
let cut_path s = Str.split_delim regexp_dot s
let wp_why3_lib library =
match LogicBuiltins.get_option option_qual ~library with
| [] -> [library]
| [ lib ] -> Str.split_delim regexp_dot lib
| l ->
let pp_sep fmt () = Format.pp_print_string fmt ", " in
Wp_parameters.fatal
"too many bindings for WP-specific Why3 theory file %s:@\n%a"
library Format.(pp_print_list ~pp_sep pp_print_string) l
(* conversion *)
let rec of_tau ~cnv (t:Lang.F.tau) =
......@@ -364,13 +379,13 @@ let rec of_term ~cnv expected t : Why3.Term.term =
a b
| Leq (a,b), _, Bool ->
int_or_real ~cnv
~fint:["qed"] ~lint:"Qed" ~pint:["zleq"]
~freal:["qed"] ~lreal:"Qed" ~preal:["rleq"]
~fint:(wp_why3_lib "qed") ~lint:"Qed" ~pint:["zleq"]
~freal:(wp_why3_lib "qed") ~lreal:"Qed" ~preal:["rleq"]
a b
| Lt (a,b), _, Bool ->
int_or_real ~cnv
~fint:["qed"] ~lint:"Qed" ~pint:["zlt"]
~freal:["qed"] ~lreal:"Qed" ~preal:["rlt"]
~fint:(wp_why3_lib "qed") ~lint:"Qed" ~pint:["zlt"]
~freal:(wp_why3_lib "qed") ~lreal:"Qed" ~preal:["rlt"]
a b
| And l, _, Bool ->
t_app_fold ~f:["bool"] ~l:"Bool" ~p:["andb"] ~cnv expected l
......@@ -420,9 +435,9 @@ let rec of_term ~cnv expected t : Why3.Term.term =
| _ -> Why3.Term.t_neq (of_term' cnv a) (of_term' cnv b)
end
| Eq (a,b), _, Bool ->
t_app ~cnv ~f:["qed"] ~l:"Qed" ~p:["eqb"] [of_term' cnv a; of_term' cnv b]
t_app ~cnv ~f:(wp_why3_lib "qed") ~l:"Qed" ~p:["eqb"] [of_term' cnv a; of_term' cnv b]
| Neq (a,b), _, Bool ->
t_app ~cnv ~f:["qed"] ~l:"Qed" ~p:["neqb"] [of_term' cnv a; of_term' cnv b]
t_app ~cnv ~f:(wp_why3_lib "qed") ~l:"Qed" ~p:["neqb"] [of_term' cnv a; of_term' cnv b]
| If(a,b,c), _, _ ->
let cnv' = {cnv with polarity = `NoPolarity} in
Why3.Term.t_if (of_term cnv' Prop a) (of_term cnv expected b) (of_term cnv expected c)
......@@ -741,7 +756,7 @@ class visitor (ctx:context) c =
| [ th ] -> self#add_import th
| [ th ; was ] -> self#add_import ~was th
| _ -> why3_failure
"[driver] incorrect why3.file %S for library '%s'"
"[driver] incorrect why3.import %S for library '%s'"
opt thy
) (Str.split regexp_com opt)
in
......
......@@ -38,6 +38,7 @@ coq.file += "coqwp/Qedlib.v";
coq.file += "coqwp/Qed.v";
why3.import += "int.Abs:IAbs";
why3.import += "frama_c_wp.qed.Qed";
why3.qualifier := "frama_c_wp.qed";
altergo.file += "ergo/int.Int.mlw";
altergo.file += "ergo/int.Abs.mlw";
altergo.file += "ergo/int.ComputerDivision.mlw";
......
/* run.config
OPT: -wp-gen -wp-prover why3 -wp-msg-key success-only
*/
/*@
logic boolean u8_continue_f(unsigned char b) =
0x80<=b && 0xC0 > b;
*/
/*@
assigns \nothing;
ensures u8_continue_f(b) == \result;
*/
int u8_is_continue(const unsigned char b)
{
return b >= 0x80 && b <= 0xBF;
}
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/boolean.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_u8_is_continue_assigns_part3 : Valid
[wp] [Qed] Goal typed_u8_is_continue_assigns_part2 : Valid
[wp] [Qed] Goal typed_u8_is_continue_assigns_part1 : Valid
[wp] 4 goals generated
------------------------------------------------------------
Function u8_is_continue
------------------------------------------------------------
Goal Post-condition (file tests/wp_acsl/boolean.i, line 12) in 'u8_is_continue':
Assume {
Type: is_uint8(b) /\ is_sint32(u8_is_continue_0).
If 128 <= b
Then {
If b <= 191
Then { Have: u8_is_continue_0 = 1. }
Else { Have: u8_is_continue_0 = 0. }
}
Else { Have: u8_is_continue_0 = 0. }
}
Prove: (L_u8_continue_f(b)=true) <-> (u8_is_continue_0 != 0).
------------------------------------------------------------
Goal Assigns nothing in 'u8_is_continue' (1/3):
Effect at line 16
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
Goal Assigns nothing in 'u8_is_continue' (2/3):
Effect at line 16
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
Goal Assigns nothing in 'u8_is_continue' (3/3):
Effect at line 16
Prove: true.
Prover Qed returns Valid
------------------------------------------------------------
{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1,
"rank": 10 },
"qed": { "total": 3, "valid": 3 },
"wp:main": { "total": 4, "valid": 4, "rank": 10 } },
"wp:functions": { "u8_is_continue": { "u8_is_continue_assigns": { "qed":
{ "total": 3,
"valid": 3 },
"wp:main":
{ "total": 3,
"valid": 3 } },
"u8_is_continue_ensures": { "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"valid": 1,
"rank": 10 },
"wp:main":
{ "total": 1,
"valid": 1,
"rank": 10 } },
"wp:section": { "why3:Alt-Ergo,2.0.0":
{ "total": 1,
"valid": 1,
"rank": 10 },
"qed": { "total": 3,
"valid": 3 },
"wp:main": { "total": 4,
"valid": 4,
"rank": 10 } } } } }
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/boolean.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Alt-Ergo 2.0.0] Goal typed_u8_is_continue_ensures : Valid
[wp] [Qed] Goal typed_u8_is_continue_assigns_part1 : Valid
[wp] [Qed] Goal typed_u8_is_continue_assigns_part2 : Valid
[wp] [Qed] Goal typed_u8_is_continue_assigns_part3 : Valid
[wp] Proved goals: 4 / 4
Qed: 3
Alt-Ergo 2.0.0: 1
[wp] Report in: 'tests/wp_acsl/oracle_qualif/boolean.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/boolean.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
u8_is_continue 3 1 (36..48) 4 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