From cadc449121429760e223456a01585e27850931e3 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 18 Feb 2022 08:26:57 +0100 Subject: [PATCH 1/2] Bump goblint-cil to universal character names --- goblint.opam | 2 +- goblint.opam.locked | 2 +- goblint.opam.template | 2 +- src/analyses/base.ml | 10 +++++----- src/analyses/fileUse.ml | 4 ++-- src/analyses/spec.ml | 2 +- src/analyses/varEq.ml | 4 ++-- src/cdomains/exp.ml | 4 ++-- src/util/cilfacade.ml | 4 ++-- 9 files changed, 17 insertions(+), 17 deletions(-) diff --git a/goblint.opam b/goblint.opam index 63601820b4..84241e1ca6 100644 --- 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#0f2cd44f5473716f8025c870155a25bf0360dbe9" ] # 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 index 756cfce5e5..a7366e0625 100644 --- 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#0f2cd44f5473716f8025c870155a25bf0360dbe9" ] [ "apron.v0.9.13" diff --git a/goblint.opam.template b/goblint.opam.template index 0d3da642bb..72412c805d 100644 --- 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#0f2cd44f5473716f8025c870155a25bf0360dbe9" ] # 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 index 2ef2348e79..2e846da692 100644 --- 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 index e6faee1ff1..f542cb02e9 100644 --- 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 index 304ec90fb2..38be505f5d 100644 --- 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 index 67015cff6f..38016b688d 100644 --- 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 index 7e1c762481..73c521cc14 100644 --- 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 index 9a47f88649..c11839ed97 100644 --- 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, []) From 9e4e34788b8b0ab5f8ab81376d161b255660c45c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 18 Feb 2022 11:55:06 +0100 Subject: [PATCH 2/2] Bump goblint-cil --- goblint.opam | 2 +- goblint.opam.locked | 2 +- goblint.opam.template | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/goblint.opam b/goblint.opam index 84241e1ca6..4e6b9c71c5 100644 --- 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#0f2cd44f5473716f8025c870155a25bf0360dbe9" ] + [ "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 index a7366e0625..01d58bb918 100644 --- 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#0f2cd44f5473716f8025c870155a25bf0360dbe9" + "git+https://github.com/goblint/cil.git#c47bbbdb442b4d50dac5a0879404ab3b5592170a" ] [ "apron.v0.9.13" diff --git a/goblint.opam.template b/goblint.opam.template index 72412c805d..0ec90fb965 100644 --- 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#0f2cd44f5473716f8025c870155a25bf0360dbe9" ] + [ "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