# User Details

- User Since
- May 17 2021, 1:21 PM (11 w, 1 d)

# Yesterday

I have updated the proof for Add: https://gist.github.com/weirdsmiley/ad6a9dbf3370e96d29f9e90068931d25

Fix unrelated commits mess up!

Fix test comments

# Mon, Aug 2

Fixing another broken dependency packages error.

upgrade cmake-3.21.0 to cmake-3.21.1

# Tue, Jul 20

Here is the proof using Z3: https://gist.github.com/weirdsmiley/8a35a0e1f55f310e3566cbd47555491a

Here is the proof of correctness of the algorithm using Z3: https://gist.github.com/weirdsmiley/ad6a9dbf3370e96d29f9e90068931d25

# Fri, Jul 16

# Thu, Jul 15

# Tue, Jul 6

Pass commands through settings instead of rest

# Mon, Jul 5

Edit summary

Restore global cmake command

# Jul 2 2021

Rebase

Replace literal-value 0 with APSInt Zero

Remove redundant getAPSIntType calls

Replace literal-value 0 with APSInt Zero

Merge conditionals with similar block and add test for one overflow on Tmax-side

Thanks Valeriy.

# Jul 1 2021

Reformat comments

# Jun 25 2021

# Jun 24 2021

Add tests for overflows on both ends

Fix issues involving usage of `uadd_ov` and family of functions

Rebase

# Jun 23 2021

Fix issues involving cases for unsigned type and add tests

I am working on debugging those 3 cases.

# Jun 22 2021

Regarding the tweakings in `constant-folding.c`, I have refrained from using cases which were resulting in `UNKNOWN` assertions as they were the primary reason for constraints being propagated.

Added updated logic for reasoning using number of overflows. Also, changed a couple of tests which were leading to unwanted constriants being propagated further.

# Jun 21 2021

# Jun 18 2021

The diff fixes all invalid assertion issues and also reasons about the cases where Min > Max.

Reason about cases where Min > Max

# Jun 16 2021

# Jun 15 2021

Add logic for computing rangeset for an expression containing BO_Add.

# Jun 5 2021

# Jun 4 2021

Fix for cases involving residual paths and add case for overflowing range near extremum of a type

# Jun 3 2021

Added tests for residual paths and negation of certain values, and fixed expected warnings for UNKNOWN cases.

I also would like to see tests where the ranges are not going all the way to either INT_MIN or INT_MAX (if we talk about int), but overflow still might happen, and cases where overflow might happen, but we still can identify the overflowing results precisely (e.g. the result is

[INT_MIN, INT_MIN + 10] and [INT_MAX - 5, INT_MAX])

# Jun 2 2021

Fixed test cases expecting wrong assertions and added few more test cases.

# Jun 1 2021

@NoQ I figured out the tests but while testing against Z3, I mixed up constraints. I am changing those.