Simmo Saan
Simmo Saan
GobCon decision: use `#ifdef` to disable the test on OSX/arm64.
This has somehow gotten a lot worse. Now in our CI all non-M1 MacOS tests seem to be failing: https://github.com/goblint/cil/actions/runs/10073492596.
There are 50 occurrences of this in one of the logs: ``` /Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/stdio.h[47:80-86] : syntax error ``` Is this the same as #168 but also on OSX 13, not 15?
Extracting the file from CI, it is ```c int renameat(int, const char *, int, const char *) __OSX_AVAILABLE_STARTING(__MAC_10_10, __IPHONE_8_0); ``` which indeed preprocesses to the same availability crap.
Apparently we have some special logic for this that allows these constants, but only in the non-default C90 mode: https://github.com/goblint/cil/blob/4ef5a0865ce81c740c93da73e20a4f26daab3f1b/src/cil.ml#L64-L73 That's confusing because with GCC it's fine with C11, etc...
Concrat benchmarks have been merged with Goblint CIL 1.8.2 and that has, for example, parsed `0x8000000000000000ULL` and printed `9223372036854775808` into the merged file. Goblint CIL 2.0.0 no longer does that,...
For `Environment` at least a total order should be possible: they seem to be normalized such that variables (which are totally ordered) are sorted in the underlying array. `Environment.equal` also...
Turns out this is a problem with configuration under emscripten: https://github.com/Z3Prover/z3/issues/1298#issuecomment-400999214.
> Looks good to me now and can be merged once the branch name is changed in the workflow. That's now done as well. After merged, GitHub Pages needs to...
There's another problem regarding `loop_invariant` and its positioning in the code that got discussed during some SV-COMP community meeting a while ago AFAIK, but I don't recall any solution. Namely,...