Skip to content

Handle sqrt & Some Bodged Solution for computing through abs#1254

Merged
michael-schwarz merged 19 commits intomasterfrom
no-overflow-sqrt-pfusch
Nov 21, 2023
Merged

Handle sqrt & Some Bodged Solution for computing through abs#1254
michael-schwarz merged 19 commits intomasterfrom
no-overflow-sqrt-pfusch

Conversation

@michael-schwarz
Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz commented Nov 18, 2023 •
edited
Loading

This contains @stilscher's useful changes for computing sqrts for floats, plus some bodged together solution for refining through abs library functions we need for SV-COMP.

I propose to merge this for now and then replace it with @stilscher's cleaner solution once she finishes it.

References #1244 (and duplicates the working part of #1253).

@michael-schwarz michael-schwarz added this to the SV-COMP 2024 milestone Nov 18, 2023
@michael-schwarz michael-schwarz changed the title Handle sqrt & Some Botched Solution for computing through abs Handle sqrt & Some Bodged Solution for computing through abs Nov 18, 2023
@michael-schwarz michael-schwarz marked this pull request as ready for review November 18, 2023 11:53
sim642
sim642 reviewed Nov 20, 2023
View reviewed changes
sim642
sim642 reviewed Nov 21, 2023
View reviewed changes
@sim642 sim642 added feature sv-comp SV-COMP (analyses, results), witnesses labels Nov 21, 2023
sim642
sim642 approved these changes Nov 21, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@sim642 sim642 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Conflicts need to be resolved, but otherwise I suppose this seems ready.

@stilscher
Copy link
Copy Markdown
Member

stilscher commented Nov 21, 2023

Based on the latest run, I wanted to take another look at some test cases that use imaxabs. We cannot handle them yet, but simply adding imaxabs to the library functions does also not seem to work since there is a debug warning about an invariant failing.

@sim642
Copy link
Copy Markdown
Member

sim642 commented Nov 21, 2023

Since intmax_t is determined by some headers, maybe we cannot so statically know its ikind (if we can at all). It may be different from long long: https://stackoverflow.com/questions/20459513/is-intmax-t-the-same-as-long-long-int.

@michael-schwarz michael-schwarz merged commit e8b880e into master Nov 21, 2023
@michael-schwarz michael-schwarz deleted the no-overflow-sqrt-pfusch branch November 21, 2023 12:27
This was referenced Nov 21, 2023
Merged
Merged
sim642 added a commit to sim642/opam-repository that referenced this pull request Nov 24, 2023
@sim642
[new release] goblint (2.3.0)
34ad5a7 
CHANGES:

Functionally equivalent to Goblint in SV-COMP 2024.

* Add termination analysis for loops (goblint/analyzer#1093).
* Add memory out-of-bounds analysis (goblint/analyzer#1094, goblint/analyzer#1197).
* Add memory leak analysis (goblint/analyzer#1127, goblint/analyzer#1241, goblint/analyzer#1246).
* Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (goblint/analyzer#1220, goblint/analyzer#1228, goblint/analyzer#1201, goblint/analyzer#1199, goblint/analyzer#1259, goblint/analyzer#1262).
* Add YAML witness version 2.0 support (goblint/analyzer#1238, goblint/analyzer#1240, goblint/analyzer#1217, goblint/analyzer#1226, goblint/analyzer#1225, goblint/analyzer#1248).
* Add final warnings about unsound results (goblint/analyzer#1190, goblint/analyzer#1191).
* Add many library function specifications (goblint/analyzer#1167, goblint/analyzer#1174, goblint/analyzer#1203, goblint/analyzer#1205, goblint/analyzer#1212, goblint/analyzer#1220, goblint/analyzer#1239, goblint/analyzer#1242, goblint/analyzer#1244, goblint/analyzer#1254, goblint/analyzer#1269).
* Adapt automatic configuration tuning (goblint/analyzer#912, goblint/analyzer#921, goblint/analyzer#987, goblint/analyzer#1168, goblint/analyzer#1214, goblint/analyzer#1234).
@sim642 sim642 mentioned this pull request Nov 27, 2023
Merged
nberth pushed a commit to nberth/opam-repository that referenced this pull request Jun 18, 2024
@sim642 @nberth
[new release] goblint (2.3.0)
8f8e773 
CHANGES:

Functionally equivalent to Goblint in SV-COMP 2024.

* Add termination analysis for loops (goblint/analyzer#1093).
* Add memory out-of-bounds analysis (goblint/analyzer#1094, goblint/analyzer#1197).
* Add memory leak analysis (goblint/analyzer#1127, goblint/analyzer#1241, goblint/analyzer#1246).
* Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (goblint/analyzer#1220, goblint/analyzer#1228, goblint/analyzer#1201, goblint/analyzer#1199, goblint/analyzer#1259, goblint/analyzer#1262).
* Add YAML witness version 2.0 support (goblint/analyzer#1238, goblint/analyzer#1240, goblint/analyzer#1217, goblint/analyzer#1226, goblint/analyzer#1225, goblint/analyzer#1248).
* Add final warnings about unsound results (goblint/analyzer#1190, goblint/analyzer#1191).
* Add many library function specifications (goblint/analyzer#1167, goblint/analyzer#1174, goblint/analyzer#1203, goblint/analyzer#1205, goblint/analyzer#1212, goblint/analyzer#1220, goblint/analyzer#1239, goblint/analyzer#1242, goblint/analyzer#1244, goblint/analyzer#1254, goblint/analyzer#1269).
* Adapt automatic configuration tuning (goblint/analyzer#912, goblint/analyzer#921, goblint/analyzer#987, goblint/analyzer#1168, goblint/analyzer#1214, goblint/analyzer#1234).
@sim642 sim642 mentioned this pull request Jun 20, 2024
Merged
1 task
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jerhard jerhard jerhard left review comments

@sim642 sim642 sim642 approved these changes

@stilscher stilscher Awaiting requested review from stilscher

Assignees

No one assigned

Labels

feature precision sv-comp SV-COMP (analyses, results), witnesses

Projects

None yet

Milestone

SV-COMP 2024

Development

Successfully merging this pull request may close these issues.

4 participants

@michael-schwarz @stilscher @sim642 @jerhard