From 2fa11c88354a6791ac1f2536d345ee1a63f97b02 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 28 Jan 2021 17:57:04 +0100
Subject: [PATCH] [wp] Fix modes collection
---
src/plugins/wp/cfgGenerator.ml | 72 ++++++++++++++++++++--------------
1 file changed, 43 insertions(+), 29 deletions(-)
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index a08bedfa008..89109971805 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -31,7 +31,7 @@ module KFmap = Kernel_function.Map
type task = {
mutable lemmas: LogicUsage.logic_lemma list ;
- mutable modes: CfgCalculus.mode KFmap.t ; (** TODO: when New CFG is validated, use list *)
+ mutable modes: CfgCalculus.mode list KFmap.t ; (** TODO: when New CFG is validated, use list *)
mutable props: CfgCalculus.props ;
}
@@ -81,9 +81,15 @@ let apply task ~kf ?bhvs ?prop () =
match Annotations.behaviors kf with
| [] -> [empty_default_behavior]
| bhvs -> bhvs in
- List.iter (fun bhv ->
- task.modes <- KFmap.add kf { CfgCalculus.kf ; bhv } task.modes
- ) bhvs ;
+ let add_mode kf m =
+ let modes =
+ match KFmap.find_opt kf task.modes with
+ | None -> []
+ | Some modes -> modes
+ in
+ task.modes <- KFmap.add kf (m :: modes) task.modes
+ in
+ List.iter (fun bhv -> add_mode kf { CfgCalculus.kf ; bhv }) bhvs ;
Option.iter (fun ip -> task.props <- `PropId ip) prop ;
end
@@ -183,20 +189,24 @@ struct
) task.lemmas ;
end () ;
KFmap.iter
- (fun _ (mode : CfgCalculus.mode) ->
- WpContext.on_context (model,WpContext.Kf mode.kf)
- begin fun () ->
- LogicUsage.iter_lemmas VCG.register_lemma ;
- if WpRTE.missing_guards model mode.kf then
- warning ~current:false ~once:true "Missing RTE guards" ;
- let bhv =
- if Cil.is_default_behavior mode.bhv then None
- else Some mode.bhv.b_name in
- let index = Wpo.Function(mode.kf,bhv) in
- let wp = snd @@ WP.compute ~mode ~props:task.props in
- let wcs = VCG.compile_wp index wp in
- collection := Bag.concat !collection wcs
- end ()
+ (fun _ modes ->
+ List.iter
+ begin fun (mode: CfgCalculus.mode) ->
+ WpContext.on_context (model,WpContext.Kf mode.kf)
+ begin fun () ->
+ LogicUsage.iter_lemmas VCG.register_lemma ;
+ if WpRTE.missing_guards model mode.kf then
+ warning ~current:false ~once:true "Missing RTE guards" ;
+ let bhv =
+ if Cil.is_default_behavior mode.bhv then None
+ else Some mode.bhv.b_name in
+ let index = Wpo.Function(mode.kf,bhv) in
+ let wp = snd @@ WP.compute ~mode ~props:task.props in
+ let wcs = VCG.compile_wp index wp in
+ collection := Bag.concat !collection wcs
+ end ()
+ end
+ (List.rev modes)
) task.modes ;
!collection
end
@@ -248,17 +258,21 @@ let dump task =
let module WP = CfgCalculus.Make(CfgDump) in
let props = task.props in
KFmap.iter
- (fun _ (mode : CfgCalculus.mode) ->
- let bhv =
- if Cil.is_default_behavior mode.bhv
- then None else Some mode.bhv.b_name in
- try
- CfgDump.fopen mode.kf bhv ;
- ignore (WP.compute ~mode ~props) ;
- CfgDump.flush () ;
- with err ->
- CfgDump.flush () ;
- raise err
+ (fun _ modes ->
+ List.iter
+ begin fun (mode : CfgCalculus.mode) ->
+ let bhv =
+ if Cil.is_default_behavior mode.bhv
+ then None else Some mode.bhv.b_name in
+ try
+ CfgDump.fopen mode.kf bhv ;
+ ignore (WP.compute ~mode ~props) ;
+ CfgDump.flush () ;
+ with err ->
+ CfgDump.flush () ;
+ raise err
+ end
+ (List.rev modes)
) task.modes
let dumper setup driver =
--
GitLab