[wp] fix duplicated block in

src/plugins/wp/calculus.ml

@@ -571,11 +571,8 @@ module Cfg (W : Mcfg.S) = struct
           let obj = get_only_succ env cfg v in
           let obj = wp_scope wenv b.blocals Mcfg.SC_Block_out obj in
           obj
-      | Cil2cfg.VblkOut _ ->
+      | Cil2cfg.VblkOut _ | Cil2cfg.VblkIn _ ->
           get_only_succ env cfg v
-      | Cil2cfg.VblkIn (_, b) ->
-          let obj = get_only_succ env cfg v in
-          wp_scope wenv b.blocals Mcfg.SC_Block_in obj
       | Cil2cfg.Vstmt s ->
           let obj = get_only_succ env cfg v in
           wp_stmt wenv s obj

src/plugins/wp/cil2cfg.ml

@@ -653,7 +653,11 @@ let block_scope_for_edge cfg e =
             | None -> no_scope
             | Some s' -> block_scope s s'
       end
-  | _ -> (* TODO ? *) no_scope
+  | VblkIn(Bstmt _,b) -> { b_opened=[b] ; b_closed=[] }
+  | Vcall _
+  | VblkIn _ | VblkOut _ | Vtest(false,_,_)
+  | VfctIn | VfctOut | Vstart | Vend | Vexit | Vloop2 _ ->
+      no_scope
 
 let has_exit cfg =
   try