[new release] goblint-cil (2.0.8)

[sim642]

A front-end for the C programming language that facilitates program analysis and transformation

• Project page: https://github.com/goblint/cil

CHANGES:

• Fix 32bit Machdep generation on 64bit host (Separate machdep-config.h for each architecture goblint/cil#195).

[jmid]

Thanks!

CI failures are down to: 2 FreeBSD timeouts and a Windows failure ('.' is not recognized as an internal or external command, operable program or batch file) which looks OK to me 👍

Would you consider adding an x-maintenance-intent entry for goblint?
https://github.com/ocaml/opam-repository/blob/master/governance/policies/archiving.md

[sim642]

Would you consider adding an x-maintenance-intent entry for goblint?
https://github.com/ocaml/opam-repository/blob/master/governance/policies/archiving.md

I will look into it. It would be nice to have this merged, I can open a separate PR to add the intent to goblint.

[jmid]

OK thanks 👍

In CI I see

• conf-gmp.1 issues - this is a separate issue though mark conf-gmp.1 as avoid version #28540
• run-test failures on arm64 (both with 4.14 and 5.3) . Is this expected? These could be silenced by guarding it by, e.g., arch = "x86_64"

[sim642]

• run-test failures on arm64 (both with 4.14 and 5.3) . Is this expected? These could be silenced by guarding it by, e.g., arch = "x86_64"

Hmm, no. I was surprised to see this since this should be unchanged since #28433, where it did pass.

The actual problem is deep in the logs:

# /usr/include/aarch64-linux-gnu/bits/math-vector.h[156:9-22] : syntax error
# Parsing errorFatal error: exception GoblintCil__Frontc.ParseError("Parse error")

Looks like the Debian version update between the two PRs means that there are now new headers which contain funky builtin C types like __Float32x4_t.

I wouldn't want to exclude arch = "arm64" entirely though because this also excludes Apple silicon if I remember correctly. Perhaps x-ci-accept-failures for the Debian arm64 would make sense?

[jmid]

I wouldn't want to exclude arch = "arm64" entirely though because this also excludes Apple silicon if I remember correctly. Perhaps x-ci-accept-failures for the Debian arm64 would make sense?

Makes sense to me 👍
AFAICS, under x-ci-accept-failures we list operating systems from the first list here: https://github.com/ocurrent/opam-repo-ci/blob/master/doc/platforms.md
I don't know how if it is possibly to quantify that to debian-13 only on arm64 though... 🤔

[sim642]

AFAICS, under x-ci-accept-failures we list operating systems from the first list here: https://github.com/ocurrent/opam-repo-ci/blob/master/doc/platforms.md
I don't know how if it is possibly to quantify that to debian-13 only on arm64 though... 🤔

Hmm, that seems to be the case indeed, looking at opam-repo-ci sources.

Oddly enough, I found some packages that have tried looking for other parts of the variant string though (and also has extra brackets!):

opam-repository/packages/echo/echo.0.0.5/opam

Lines 16 to 19 in 5f4fdc0

	x-ci-accept-failures: [
	["x86_32"]
	["arm32"]
	]

opam-repository/packages/frama-c/frama-c.24.0/opam

Lines 139 to 142 in 5f4fdc0

	x-ci-accept-failures: [
	"nnp" "nnpchecker"
	"centos-7" # Too old version of make
	]

And even one which uses a formula there:

opam-repository/packages/conf-rust-llvm/conf-rust-llvm.1/opam

Line 25 in 5f4fdc0

x-ci-accept-failures: os-distribution = "freebsd" | os-family = "fedora"

I suspect that one accidentally even works because opam-repo-ci just greps the value on the shell.

[jmid]

Nice digging! Indeed greping for a distribution
https://github.com/ocurrent/opam-repo-ci/blob/master/opam-ci-check/lib/opam_build.ml#L66-L74
is not going to have much luck matching architectures (or nnp*), so I think the above are mistakes that have flown under the radar.

For Goblint we could of course cast a wider net with x-ci-accept-failures: ["debian-13"] at the risk of silencing later errors surfacing. However it seems like guarding run-test with, e.g., arch = "x86_64 || os != "linux" is the best option. 🤔

[mseri]

Good now. The lower bounds are unrelated

[mseri]

Thanks