Merge pull request #464 from goblint/rm_cil_msvc_support

Adapt to CIL without MSVC support

Author: michael-schwarz

goblint.opam

@@ -58,7 +58,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#a3c91aa6e8f946fec9a9a13361b051a73b12a65c" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#83835348d20b3f51f1e8e505480b773c9fa5f96b" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

goblint.opam.locked

@@ -94,7 +94,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#a3c91aa6e8f946fec9a9a13361b051a73b12a65c"
+    "git+https://github.com/goblint/cil.git#83835348d20b3f51f1e8e505480b773c9fa5f96b"
   ]
   [
     "apron.v0.9.13"

goblint.opam.template

@@ -1,7 +1,7 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#a3c91aa6e8f946fec9a9a13361b051a73b12a65c" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#83835348d20b3f51f1e8e505480b773c9fa5f96b" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

src/framework/cfgTools.ml

@@ -219,9 +219,7 @@ let createCFG (file: file) =
           (* Should be removed by Cil.prepareCFG. *)
           failwith "MyCFG.createCFG: unprepared stmt"
 
-        | ComputedGoto _
-        | TryExcept _
-        | TryFinally _ ->
+        | ComputedGoto _->
           failwith "MyCFG.createCFG: unsupported stmt"
     in
     try
@@ -379,9 +377,7 @@ let createCFG (file: file) =
             (* Should be removed by Cil.prepareCFG. *)
             failwith "MyCFG.createCFG: unprepared stmt"
 
-          | ComputedGoto _
-          | TryExcept _
-          | TryFinally _ ->
+          | ComputedGoto _ ->
             failwith "MyCFG.createCFG: unsupported stmt"
         in
         List.iter handle fd.sallstmts;

src/incremental/compareAST.ml

@@ -209,8 +209,6 @@ let rec eq_stmtkind ?(cfg_comp = false) ((a, af): stmtkind * fundec) ((b, bf): s
   | Switch (exp1, block1, stmts1, _l1, _el1), Switch (exp2, block2, stmts2, _l2, _el2) -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else eq_exp exp1 exp2 && eq_block' block1 block2 && eq_list (fun a b -> eq_stmt (a,af) (b,bf)) stmts1 stmts2
   | Loop (block1, _l1, _el1, _con1, _br1), Loop (block2, _l2, _el2, _con2, _br2) -> eq_block' block1 block2
   | Block block1, Block block2 -> eq_block' block1 block2
-  | TryFinally (tryBlock1, finallyBlock1, _l1), TryFinally (tryBlock2, finallyBlock2, _l2) -> eq_block' tryBlock1 tryBlock2 && eq_block' finallyBlock1 finallyBlock2
-  | TryExcept (tryBlock1, exn1, exceptBlock1, _l1), TryExcept (tryBlock2, exn2, exceptBlock2, _l2) -> eq_block' tryBlock1 tryBlock2 && eq_block' exceptBlock1 exceptBlock2
   | _, _ -> false
 
 and eq_stmt ?(cfg_comp = false) ((a, af): stmt * fundec) ((b, bf): stmt * fundec) =

src/util/cilfacade.ml

@@ -340,7 +340,7 @@ and typeOfLval = function
 and typeOffset basetyp =
   let blendAttributes baseAttrs =
     let (_, _, contageous) =
-      partitionAttributes ~default:(AttrName false) baseAttrs in
+      partitionAttributes ~default:AttrName baseAttrs in
     typeAddAttributes contageous
   in
   function
@@ -379,8 +379,6 @@ class countFnVisitor = object
       | If (_,_,_,loc,_)
       | Switch (_,_,_,loc,_)
       | Loop (_,loc,_,_,_)
-      | TryFinally (_,_,loc)
-      | TryExcept (_,_,_,loc)
         -> Hashtbl.replace locs loc.line (); DoChildren
       | _ ->
         DoChildren