diff --git a/headers/header_spec.txt b/headers/header_spec.txt index 7525ffd94ff089e588e678bbcb250096423b14b5..7698e1df5e9ccfcfd40900f56fa4c7fa14afc0ec 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -1680,6 +1680,8 @@ src/plugins/wp/cfgCalculus.ml: CEA_WP src/plugins/wp/cfgCalculus.mli: CEA_WP src/plugins/wp/cfgDump.ml: CEA_WP src/plugins/wp/cfgDump.mli: CEA_WP +src/plugins/wp/cfgGenerator.ml: CEA_WP +src/plugins/wp/cfgGenerator.mli: CEA_WP src/plugins/wp/cfgInit.ml: CEA_WP src/plugins/wp/cfgInit.mli: CEA_WP src/plugins/wp/cfgWP.ml: CEA_WP diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml index e9cd98fec7e2c36d29c04d2dab0398eaf81ece32..2fe63d14871b2d38c4ca43c621ab2780ede0b418 100644 --- a/src/plugins/wp/cfgGenerator.ml +++ b/src/plugins/wp/cfgGenerator.ml @@ -141,8 +141,8 @@ struct begin fun () -> LogicUsage.iter_lemmas VCG.register_lemma ; List.iter (fun l -> - let wpo = VCG.compile_lemma l in - collection := Bag.add wpo !collection + let wpo = VCG.compile_lemma l in + collection := Bag.add wpo !collection ) task.lemmas ; end () ; List.iter