Skip to content

Commit d64a5a3

Browse files
RobotechnicRobotechnic
authored
Merge branch 'goblint:master' into master
2 parents 4382ecb + ff6f52c commit d64a5a3

File tree

13 files changed

+461
-33
lines changed

13 files changed

+461
-33
lines changed

‎dune-project‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
4040
(goblint-cil (>= 2.0.5)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
4141
(batteries (>= 3.5.1))
4242
(zarith (>= 1.10))
43-
(yojson (>= 2.0.0))
43+
(yojson (and (>= 2.0.0) (< 3))) ; json-data-encoding has incompatible yojson representation for yojson 3
4444
(qcheck-core (>= 0.19))
4545
(ppx_deriving (>= 6.0.2))
4646
(ppx_deriving_hash (>= 0.1.2))
@@ -72,6 +72,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
7272
)
7373
(depopts
7474
(apron (>= v0.9.15))
75+
(camlidl (>= 1.13)) ; for stability (https://github.com/goblint/analyzer/issues/1520)
7576
z3
7677
domainslib
7778
)

‎goblint.opam‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,7 +40,7 @@ depends: [
4040
"goblint-cil" {>= "2.0.5"}
4141
"batteries" {>= "3.5.1"}
4242
"zarith" {>= "1.10"}
43-
"yojson" {>= "2.0.0"}
43+
"yojson" {>= "2.0.0" & < "3"}
4444
"qcheck-core" {>= "0.19"}
4545
"ppx_deriving" {>= "6.0.2"}
4646
"ppx_deriving_hash" {>= "0.1.2"}
@@ -72,6 +72,7 @@ depends: [
7272
]
7373
depopts: [
7474
"apron" {>= "v0.9.15"}
75+
"camlidl" {>= "1.13"}
7576
"z3"
7677
"domainslib"
7778
]
@@ -102,8 +103,6 @@ available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" |
102103
pin-depends: [
103104
# published goblint-cil 2.0.6 is currently up-to-date, but pinned for reproducibility
104105
[ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#8385ab315bc7461f6801af57673c64731bfa036a" ]
105-
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
106-
[ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
107106
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
108107
[ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
109108
]

‎goblint.opam.locked‎

Lines changed: 18 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ depends: [
3535
"bigarray-compat" {= "1.1.0"}
3636
"bigstringaf" {= "0.9.1"}
3737
"bos" {= "0.2.1"}
38-
"camlidl" {= "1.12"}
38+
"camlidl" {= "1.13"}
3939
"camlp-streams" {= "5.0.1"}
4040
"catapult" {= "0.2"}
4141
"catapult-file" {= "0.2"}
@@ -50,18 +50,18 @@ depends: [
5050
"conf-ruby" {= "1.0.0" & with-test}
5151
"cppo" {= "1.6.9"}
5252
"cpu" {= "2.0.0"}
53-
"crunch" {= "3.3.1" & with-doc}
53+
"crunch" {= "4.0.0" & with-doc}
5454
"csexp" {= "1.5.2"}
5555
"cstruct" {= "6.2.0"}
5656
"ctypes" {= "0.22.0"}
5757
"domain-local-await" {= "1.0.1"}
5858
"domain_shims" {= "0.1.0"}
59-
"dune" {= "3.16.0"}
60-
"dune-build-info" {= "3.16.0"}
61-
"dune-configurator" {= "3.16.0"}
62-
"dune-private-libs" {= "3.16.0"}
63-
"dune-site" {= "3.16.0"}
64-
"dyn" {= "3.16.0"}
59+
"dune" {= "3.19.1"}
60+
"dune-build-info" {= "3.19.1"}
61+
"dune-configurator" {= "3.19.1"}
62+
"dune-private-libs" {= "3.19.1"}
63+
"dune-site" {= "3.19.1"}
64+
"dyn" {= "3.19.1"}
6565
"ez-conf-lib" {= "2"}
6666
"fileutils" {= "0.6.4"}
6767
"fmt" {= "0.9.0"}
@@ -82,31 +82,31 @@ depends: [
8282
"ocaml-variants" {= "4.14.2+options"}
8383
"ocamlbuild" {= "0.14.3"}
8484
"ocamlfind" {= "1.9.8"}
85-
"odoc" {= "2.4.2" & with-doc}
86-
"odoc-parser" {= "2.4.2" & with-doc}
87-
"ordering" {= "3.16.0"}
85+
"odoc" {= "3.0.0" & with-doc}
86+
"odoc-parser" {= "3.0.0" & with-doc}
87+
"ordering" {= "3.19.1"}
8888
"ounit2" {= "2.2.7" & with-test}
89-
"pp" {= "1.2.0"}
89+
"pp" {= "2.0.0"}
9090
"ppx_blob" {= "0.9.0"}
9191
"ppx_derivers" {= "1.2.1"}
9292
"ppx_deriving" {= "6.0.2"}
9393
"ppx_deriving_hash" {= "0.1.2"}
9494
"ppx_deriving_yojson" {= "3.8.0"}
95-
"ppxlib" {= "0.32.1"}
96-
"ptime" {= "1.1.0" & with-doc}
97-
"qcheck-core" {= "0.21.3"}
98-
"qcheck-ounit" {= "0.21.3" & with-test}
95+
"ppxlib" {= "0.35.0"}
96+
"ptime" {= "1.2.0" & with-doc}
97+
"qcheck-core" {= "0.25"}
98+
"qcheck-ounit" {= "0.25" & with-test}
9999
"re" {= "1.11.0" & with-doc}
100100
"result" {= "1.5" & with-doc}
101101
"rresult" {= "0.7.0"}
102102
"seq" {= "base"}
103103
"sexplib0" {= "v0.16.0"}
104104
"sha" {= "1.15.4"}
105105
"stdlib-shims" {= "0.3.0"}
106-
"stdune" {= "3.16.0"}
106+
"stdune" {= "3.19.1"}
107107
"stringext" {= "1.6.0"}
108108
"thread-table" {= "1.0.0"}
109-
"topkg" {= "1.0.7"}
109+
"topkg" {= "1.0.8"}
110110
"tyxml" {= "4.6.0" & with-doc}
111111
"uri" {= "4.4.0"}
112112
"uuidm" {= "0.9.8"}
@@ -145,10 +145,6 @@ pin-depends: [
145145
"goblint-cil.2.0.6"
146146
"git+https://github.com/goblint/cil.git#8385ab315bc7461f6801af57673c64731bfa036a"
147147
]
148-
[
149-
"camlidl.1.12"
150-
"git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0"
151-
]
152148
[
153149
"apron.v0.9.15"
154150
"git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a"

‎goblint.opam.template‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,6 @@ available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" |
44
pin-depends: [
55
# published goblint-cil 2.0.6 is currently up-to-date, but pinned for reproducibility
66
[ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#8385ab315bc7461f6801af57673c64731bfa036a" ]
7-
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
8-
[ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
97
# pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
108
[ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
119
]

‎gobview‎

‎src/analyses/base.ml‎

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -200,8 +200,24 @@ struct
200200
| PlusA -> ID.add
201201
| MinusA -> ID.sub
202202
| Mult -> ID.mul
203-
| Div -> ID.div
204-
| Mod -> ID.rem
203+
| Div ->
204+
fun x y ->
205+
(match ID.equal_to Z.zero y with
206+
| `Eq ->
207+
M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division is zero"
208+
| `Top ->
209+
M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of division might be zero"
210+
| `Neq -> ());
211+
ID.div x y
212+
| Mod ->
213+
fun x y ->
214+
(match ID.equal_to Z.zero y with
215+
| `Eq ->
216+
M.error ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo is zero"
217+
| `Top ->
218+
M.warn ~category:M.Category.Integer.div_by_zero ~tags:[CWE 369] "Second argument of modulo might be zero"
219+
| `Neq -> ());
220+
ID.rem x y
205221
| Lt -> ID.lt
206222
| Gt -> ID.gt
207223
| Le -> ID.le

‎src/cdomain/value/cdomains/int/intervalDomain.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -296,7 +296,7 @@ struct
296296
begin
297297
let is_zero v = Ints_t.compare v Ints_t.zero = 0 in
298298
match y1, y2 with
299-
| l, u when is_zero l && is_zero u -> (top_of ik,{underflow=false; overflow=false}) (* TODO warn about undefined behavior *)
299+
| l, u when is_zero l && is_zero u -> (top_of ik,{underflow=false; overflow=false})
300300
| l, _ when is_zero l -> div ik (Some (x1,x2)) (Some (Ints_t.one,y2))
301301
| _, u when is_zero u -> div ik (Some (x1,x2)) (Some (y1, Ints_t.(neg one)))
302302
| _ when leq (of_int ik (Ints_t.zero) |> fst) (Some (y1,y2)) -> (top_of ik,{underflow=false; overflow=false})

‎src/cdomain/value/cdomains/int/intervalSetDomain.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -362,7 +362,7 @@ struct
362362
let top_of ik = top_of ik |> List.hd in
363363
let is_zero v = v =. Ints_t.zero in
364364
match y1, y2 with
365-
| l, u when is_zero l && is_zero u -> top_of ik (* TODO warn about undefined behavior *)
365+
| l, u when is_zero l && is_zero u -> top_of ik
366366
| l, _ when is_zero l -> interval_div x (Ints_t.one,y2)
367367
| _, u when is_zero u -> interval_div x (y1, Ints_t.(neg one))
368368
| _ when leq (of_int ik (Ints_t.zero) |> fst) ([(y1,y2)]) -> top_of ik

‎tests/regression/01-cpa/77-def_exc-starting-ending.c‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// PARAM: --enable ana.int.def_exc --disable ana.int.interval
2+
#include <goblint.h>
3+
4+
int main() {
5+
int x;
6+
7+
if (-10 <= x) {
8+
__goblint_check(-128 <= x);
9+
}
10+
11+
if (x <= 10) {
12+
__goblint_check(x <= 127); // TODO
13+
}
14+
return 0;
15+
}

‎tests/regression/01-cpa/78-divbyzero.c‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
// PARAM: --enable ana.int.interval
2+
3+
int main(void) {
4+
5+
int a = 0;
6+
for (int i = 0; i < 5; i++) {
7+
a += 100/i; //WARN
8+
}
9+
a = 5;
10+
a /= 0; //WARN
11+
12+
return 0;
13+
}

0 commit comments

Comments
 (0)