Skip to content
Snippets Groups Projects
Commit 8eeaed5d authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] Option for default call termination

parent 8dd5dee7
No related branches found
No related tags found
No related merge requests found
......@@ -188,14 +188,19 @@ let get_terminates kf =
(fun p -> WpPropId.mk_terminates_id kf Kglobal p, normalize_terminates p)
(Annotations.funspec kf).spec_terminates
let get_terminates_goal kf =
let get_terminates_call kf =
match (Annotations.funspec kf).spec_terminates with
| Some p ->
normalize_terminates p
| None when Kernel_function.is_definition kf ->
Logic_const.pfalse
if Wp_parameters.TerminatesDefinitions.get ()
then Logic_const.ptrue
else Logic_const.pfalse
| None ->
Logic_const.ptrue
if Wp_parameters.TerminatesDeclarations.get ()
then Logic_const.ptrue
else Logic_const.pfalse
(* -------------------------------------------------------------------------- *)
(* --- Contracts --- *)
......@@ -284,7 +289,7 @@ module CallContract = WpContext.StaticGenerator(Kernel_function)
| WritesAny -> WritesAny
| Writes froms -> Writes (normalize_froms Normal froms)
in
let terminates = get_terminates_goal kf in
let terminates = get_terminates_call kf in
{
contract_cond = List.rev !wcond ;
contract_hpre = List.rev !whpre ;
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/terminates_call_options.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function call_declaration
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_call_options.i, line 19) in 'call_declaration':
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function call_definition
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_call_options.i, line 24) in 'call_definition' (1/2):
Prove: true.
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_call_options.i, line 24) in 'call_definition' (2/2):
Call Effect at line 26
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function definition
------------------------------------------------------------
Goal Assigns nothing in 'definition':
Prove: true.
------------------------------------------------------------
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/terminates_call_options.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function call_declaration
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_call_options.i, line 19) in 'call_declaration' (1/2):
Prove: true.
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_call_options.i, line 19) in 'call_declaration' (2/2):
Call Effect at line 21
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function call_definition
------------------------------------------------------------
Goal Termination-condition (file tests/wp_acsl/terminates_call_options.i, line 24) in 'call_definition':
Prove: true.
------------------------------------------------------------
------------------------------------------------------------
Function definition
------------------------------------------------------------
Goal Assigns nothing in 'definition':
Prove: true.
------------------------------------------------------------
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/terminates_call_options.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_definition_assigns : Valid
[wp] [Qed] Goal typed_call_declaration_terminates : Valid
[wp] [Qed] Goal typed_call_definition_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_call_definition_terminates_part2 : Unsuccess
[wp] Proved goals: 3 / 4
Qed: 3
Alt-Ergo: 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
definition 1 - 1 100%
call_declaration 1 - 1 100%
call_definition 1 - 2 50.0%
------------------------------------------------------------
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/terminates_call_options.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_definition_assigns : Valid
[wp] [Qed] Goal typed_call_declaration_terminates_part1 : Valid
[wp] [Alt-Ergo] Goal typed_call_declaration_terminates_part2 : Unsuccess
[wp] [Qed] Goal typed_call_definition_terminates : Valid
[wp] Proved goals: 3 / 4
Qed: 3
Alt-Ergo: 0 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
definition 1 - 1 100%
call_declaration 1 - 2 50.0%
call_definition 1 - 1 100%
------------------------------------------------------------
/* run.config
OPT:
OPT: -wp-no-declarations-terminate -wp-definitions-terminate
*/
/* run.config_qualif
OPT:
OPT: -wp-no-declarations-terminate -wp-definitions-terminate
*/
// -wp-declaration-terminates <--- default to TRUE
// -wp-definition-terminates <--- default to FALSE
//@ assigns \nothing ;
void declaration(void);
//@ assigns \nothing ;
void definition(void){}
//@ terminates \true ;
void call_declaration(void){
declaration();
}
//@ terminates \true ;
void call_definition(void){
definition();
}
......@@ -478,6 +478,22 @@ module PrecondWeakening =
let help = "Discard pre-conditions of side behaviours (sound but incomplete optimisation)."
end)
let () = Parameter_customize.set_group wp_strategy
module TerminatesDeclarations =
True(struct
let option_name = "-wp-declarations-terminate"
let help = "Function declarations without terminates specification are \
considered to terminate when called."
end)
let () = Parameter_customize.set_group wp_strategy
module TerminatesDefinitions =
False(struct
let option_name = "-wp-definitions-terminate"
let help = "Function definitions without terminates specification are \
considered to terminate when called."
end)
let () = Parameter_customize.set_group wp_strategy
module TerminatesVariantHyp =
False(struct
......
......@@ -101,6 +101,8 @@ module SimplifyForall : Parameter_sig.Bool
module SimplifyType : Parameter_sig.Bool
module CalleePreCond : Parameter_sig.Bool
module PrecondWeakening : Parameter_sig.Bool
module TerminatesDeclarations : Parameter_sig.Bool
module TerminatesDefinitions : Parameter_sig.Bool
module TerminatesVariantHyp : Parameter_sig.Bool
(** {2 Prover Interface} *)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment