Merge pull request #604 from goblint/cil_universial_character_names

Bump CIL to support Universal Character Names, `char16_t`, and `char32_t` (part of C99/C11)
goblint · Feb 21, 2022 · f365ae5 · f365ae5
2 parents c39905c + 9e4e347
commit f365ae5
Show file tree

Hide file tree

Showing 9 changed files with 17 additions and 17 deletions.
diff --git a/goblint.opam b/goblint.opam
@@ -63,7 +63,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#4356eb39fd9ea5192fc96f7b8e135586c65c3a19" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#c47bbbdb442b4d50dac5a0879404ab3b5592170a" ]
   # 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

diff --git a/goblint.opam.locked b/goblint.opam.locked
@@ -110,7 +110,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#4356eb39fd9ea5192fc96f7b8e135586c65c3a19"
+    "git+https://github.com/goblint/cil.git#c47bbbdb442b4d50dac5a0879404ab3b5592170a"
   ]
   [
     "apron.v0.9.13"

diff --git a/goblint.opam.template b/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#4356eb39fd9ea5192fc96f7b8e135586c65c3a19" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#c47bbbdb442b4d50dac5a0879404ab3b5592170a" ]
   # 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

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -499,7 +499,7 @@ struct
       let toInt i =
         match IdxDom.to_int @@ ID.cast_to ik i with
         | Some x -> Const (CInt (x,ik, None))
-        | _ -> mkCast ~e:(Const (CStr "unknown")) ~newt:intType
+        | _ -> mkCast ~e:(Const (CStr ("unknown",No_encoding))) ~newt:intType
 
       in
       match o with
@@ -681,8 +681,8 @@ struct
         (match str with Some x -> M.tracel "casto" "CInt (%s, %a, %s)\n" (Cilint.string_of_cilint num) d_ikind ikind x | None -> ());
         `Int (ID.cast_to ikind (IntDomain.of_const (num,ikind,str)))
       (* String literals *)
-      | Const (CStr x) -> `Address (AD.from_string x) (* normal 8-bit strings, type: char* *)
-      | Const (CWStr xs as c) -> (* wide character strings, type: wchar_t* *)
+      | Const (CStr (x,_)) -> `Address (AD.from_string x) (* normal 8-bit strings, type: char* *)
+      | Const (CWStr (xs,_) as c) -> (* wide character strings, type: wchar_t* *)
         let x = Pretty.sprint ~width:80 (d_const () c) in (* escapes, see impl. of d_const in cil.ml *)
         let x = String.sub x 2 (String.length x - 3) in (* remove surrounding quotes: L"foo" -> foo *)
         `Address (AD.from_string x) (* `Address (AD.str_ptr ()) *)
@@ -773,7 +773,7 @@ struct
           | None -> ad
         in
         `Address (AD.map array_start (eval_lv a gs st lval))
-      | CastE (t, Const (CStr x)) -> (* VD.top () *) eval_rv a gs st (Const (CStr x)) (* TODO safe? *)
+      | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv a gs st (Const (CStr (x,e))) (* TODO safe? *)
       | CastE  (t, exp) ->
         let v = eval_rv a gs st exp in
         VD.cast ~torg:(Cilfacade.typeOf exp) t v
@@ -2172,7 +2172,7 @@ struct
       end
     | `Unknown "__builtin" ->
       begin match args with
-        | Const (CStr "invariant") :: ((_ :: _) as args) ->
+        | Const (CStr ("invariant",_)) :: ((_ :: _) as args) ->
           List.fold_left (fun d e -> invariant ctx (Analyses.ask_of_ctx ctx) ctx.global d e true) ctx.local args
         | _ -> failwith "Unknown __builtin."
       end

diff --git a/src/analyses/fileUse.ml b/src/analyses/fileUse.ml
@@ -247,10 +247,10 @@ struct
       let f k m w =
         let m = check_overwrite_open k m in
         (match arglist with
-         | Const(CStr(filename))::Const(CStr(mode))::[] ->
+         | Const(CStr(filename,_))::Const(CStr(mode,_))::[] ->
            (* M.debug @@ "fopen(\""^filename^"\", \""^mode^"\")"; *)
            D.fopen k loc filename mode m |> split_err_branch lval (* TODO k instead of lval? *)
-         | e::Const(CStr(mode))::[] ->
+         | e::Const(CStr(mode,_))::[] ->
            (* ignore(printf "CIL: %a\n" d_plainexp e); *)
            (match ctx.ask (Queries.EvalStr e) with
             | `Lifted filename -> D.fopen k loc filename mode m

diff --git a/src/analyses/spec.ml b/src/analyses/spec.ml
@@ -62,7 +62,7 @@ struct
 
     let equal_exp ctx spec_exp cil_exp = match spec_exp, cil_exp with
       (* TODO match constants right away to avoid queries? *)
-      | `String a, Const(CStr b) -> M.debug "EQUAL String Const: %s = %s" a b; a=b
+      | `String a, Const(CStr (b,_)) -> M.debug "EQUAL String Const: %s = %s" a b; a=b
       (* | `String a, Const(CWStr xs as c) -> failwith "not implemented" *)
       (* CWStr is done in base.ml, query only returns `Str if it's safe *)
       | `String a, e -> (match ctx.ask (Queries.EvalStr e) with

diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
@@ -49,8 +49,8 @@ struct
 
   let const_equal c1 c2 =
     match c1, c2 with
-    |	CStr s1  , CStr s2	 -> s1 = s2
-    |	CWStr is1, CWStr is2 -> is1 = is2
+    |	CStr (s1,_)  , CStr (s2,_)	 -> s1 = s2
+    |	CWStr (is1,_), CWStr (is2,_) -> is1 = is2
     |	CChr c1  , CChr c2   -> c1 = c2
     |	CInt (v1,k1,_), CInt (v2,k2,_) -> Cilint.compare_cilint v1 v2 = 0 && k1 = k2
     |	CReal (f1,k1,_) , CReal (f2,k2,_)  -> f1 = f2 && k1 = k2

diff --git a/src/cdomains/exp.ml b/src/cdomains/exp.ml
@@ -110,8 +110,8 @@ struct
   let eq_const c1 c2 =
     match c1, c2 with
     | CInt (i1,_,_), CInt (i2,_,_)     -> Cilint.compare_cilint i1 i2 = 0
-    |	CStr s1        , CStr s2         -> s1=s2
-    |	CWStr s1       , CWStr s2        -> s1=s2
+    |	CStr (s1,_)        , CStr (s2,_)         -> s1=s2
+    |	CWStr (s1,_)       , CWStr (s2,_)        -> s1=s2
     |	CChr c1        , CChr c2         -> c1=c2
     |	CReal (f1,_,_) , CReal (f2,_,_)  -> f1=f2
     |	CEnum (_,n1,_) , CEnum (_,n2,_)  -> n1=n2

diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
@@ -277,9 +277,9 @@ let rec typeOf (e: exp) : typ =
   (* The type of a string is a pointer to characters ! The only case when
    * you would want it to be an array is as an argument to sizeof, but we
    * have SizeOfStr for that *)
-  | Const(CStr s) -> !stringLiteralType
+  | Const(CStr (s,_)) -> !stringLiteralType
 
-  | Const(CWStr s) -> TPtr(!wcharType,[])
+  | Const(CWStr (s,_)) -> TPtr(!wcharType,[])
 
   | Const(CReal (_, fk, _)) -> TFloat(fk, [])