Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

TUM Practical Course Summer 2023: Termination Analyses #1093

Merged
merged 419 commits into from
Nov 18, 2023
Merged

TUM Practical Course Summer 2023: Termination Analyses #1093

merged 419 commits into from
Nov 18, 2023
This pull request is big! We’re only showing the most recent 250 commits.

Commits on Jun 20, 2023

  1. Merge branch 'recursion' of https://github.com/serenita/goblint-analyzer 

     into recursion
    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    af61d92 View commit details
    Browse the repository at this point in the history

  2. added weird test case + merging

    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    c6f37b2 View commit details
    Browse the repository at this point in the history

  3. Fix indentation

    Alexander Schlenga committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    566ae50 View commit details
    Browse the repository at this point in the history

  4. Small changes 

    Direct empty list comparison instead of checking length = 0.
Make loop_heads a function with argument ().
    Alexander Schlenga committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    6cf3d12 View commit details
    Browse the repository at this point in the history

  5. added location to recursion Warning

    Isidor Zweckstetter committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    cfaf417 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'recursion' of https://github.com/serenita/goblint-analyzer 

     into recursion
    Isidor Zweckstetter committed Jun 20, 2023
    Configuration menu
    Copy the full SHA
    f309afd View commit details
    Browse the repository at this point in the history

Commits on Jun 21, 2023

  1. Merge branch 'master' into lagemann-dev 

    # Conflicts:
#	src/analyses/termination_new.ml
#	src/util/terminationPreprocessing.ml
    @LageTs
    LageTs committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    b562cac View commit details
    Browse the repository at this point in the history

  2. Merge branch 'recursion' into lagemann-dev 

    # Conflicts:
#	src/framework/analyses.ml
    @LageTs
    LageTs committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    cb8d719 View commit details
    Browse the repository at this point in the history

  3. Adapted update_suite.rb and tests to termination output

    @LageTs
    LageTs committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    a4991e0 View commit details
    Browse the repository at this point in the history

  4. reverted test case

    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    7a6b18c View commit details
    Browse the repository at this point in the history

  5. reverted test case

    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    4a402ca View commit details
    Browse the repository at this point in the history

  6. pulled master

    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    f35c116 View commit details
    Browse the repository at this point in the history

  7. fixed error that for only one function the analysis was not executed:… 

    … pulled check for result of loop analysis outside
    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    79ac4ba View commit details
    Browse the repository at this point in the history

  8. Added SKIP/TODO functionality for loop termination

    @LageTs
    LageTs committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    6a4105d View commit details
    Browse the repository at this point in the history

  9. Merge branch 'recursion' into lagemann-dev 

    # Conflicts:
#	src/framework/analyses.ml
    @LageTs
    LageTs committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    3e6ffcc View commit details
    Browse the repository at this point in the history

  10. Adapted TODO comments to current state

    @LageTs
    LageTs committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    6f39218 View commit details
    Browse the repository at this point in the history

  11. Comment out unused loop_heads function

    Alexander Schlenga committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    0f3dbdc View commit details
    Browse the repository at this point in the history

  12. Answer queries with false when multi-threaded

    Alexander Schlenga committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    1a09057 View commit details
    Browse the repository at this point in the history

  13. Change comments

    Alexander Schlenga committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    524f0cb View commit details
    Browse the repository at this point in the history

  14. Added requested test cases

    @LageTs
    LageTs committed Jun 21, 2023
    Configuration menu
    Copy the full SHA
    72062a6 View commit details
    Browse the repository at this point in the history

Commits on Jun 22, 2023

  1. Merge branch 'master' of https://github.com/serenita/goblint-analyzer

    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    05cb3f7 View commit details
    Browse the repository at this point in the history

  2. Skip crashing tests

    @LageTs
    LageTs committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    2f9f697 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into lagemann-dev

    @LageTs
    LageTs committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    178c1ac View commit details
    Browse the repository at this point in the history

  4. reverted test case 55 01

    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    e250557 View commit details
    Browse the repository at this point in the history

  5. merging

    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    cf96d59 View commit details
    Browse the repository at this point in the history

  6. make recursion analysis optional (depending if loop ana is activated)

    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    4e66fd2 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'master' of https://github.com/serenita/goblint-analyzer … 

    …into recursion
    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    f467bab View commit details
    Browse the repository at this point in the history

  8. Merge branch 'master' of https://github.com/serenita/goblint-analyzer

    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    d2fce9b View commit details
    Browse the repository at this point in the history

  9. work-in-progress on svcomp integration

    Isidor Zweckstetter committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    4b4be5b View commit details
    Browse the repository at this point in the history

  10. handled warnings during make

    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    62d260f View commit details
    Browse the repository at this point in the history

  11. indentation

    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    3707652 View commit details
    Browse the repository at this point in the history

  12. indentation

    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    f7dab71 View commit details
    Browse the repository at this point in the history

  13. Indentation with ocp-indent

    @LageTs
    LageTs committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    5b0d72f View commit details
    Browse the repository at this point in the history

  14. added sv-comp compatability

    Isidor Zweckstetter committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    8a320eb View commit details
    Browse the repository at this point in the history

  15. revert testchanges in option.schema.json

    Isidor Zweckstetter committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    5bb821c View commit details
    Browse the repository at this point in the history

  16. Fix indentation

    Alexander Schlenga committed Jun 22, 2023
    Configuration menu
    Copy the full SHA
    5d3f25c View commit details
    Browse the repository at this point in the history

Commits on Jun 26, 2023

  1. Merge redefinition of old termination with new loop/recursion termina… 

    …tion
    @LageTs
    LageTs committed Jun 26, 2023
    Configuration menu
    Copy the full SHA
    a6a1526 View commit details
    Browse the repository at this point in the history

Commits on Jun 28, 2023

  1. Merge remote-tracking branch 'upstream/master'

    Alexander Schlenga committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    fa71e4e View commit details
    Browse the repository at this point in the history

  2. Fix indentation

    Alexander Schlenga committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    8603177 View commit details
    Browse the repository at this point in the history

  3. Restore signs analysis tutorial

    Alexander Schlenga committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    d987f1a View commit details
    Browse the repository at this point in the history

  4. Simplify src/framework/analyses.ml 

    Co-authored-by: Julian Erhard <julian.erhard@yahoo.de>
    @serenita @jerhard
    serenita and jerhard committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    b1930ab View commit details
    Browse the repository at this point in the history

  5. Fix indentation

    Alexander Schlenga committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    a3fd8d0 View commit details
    Browse the repository at this point in the history

  6. Remove build_testing.yml

    Alexander Schlenga committed Jun 28, 2023
    Configuration menu
    Copy the full SHA
    ba596d7 View commit details
    Browse the repository at this point in the history

Commits on Jun 29, 2023

  1. No skipping

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    fbef208 View commit details
    Browse the repository at this point in the history

  2. New non terminating for loop

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    13f369a View commit details
    Browse the repository at this point in the history

  3. Folder Renaming

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    d681158 View commit details
    Browse the repository at this point in the history

  4. Enable polyhedra; Removed unnecessary TODOs

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    541e49b View commit details
    Browse the repository at this point in the history

  5. patched loop termination check position to right after the loop head

    Isidor Zweckstetter committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    1b5db9c View commit details
    Browse the repository at this point in the history

  6. removed temporary comment

    Isidor Zweckstetter committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    e6ba559 View commit details
    Browse the repository at this point in the history

  7. Merge branch 'master' into lagemann-dev

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    30ecae7 View commit details
    Browse the repository at this point in the history

  8. removed outdated code

    Isidor Zweckstetter committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    16b8c37 View commit details
    Browse the repository at this point in the history

  9. Removed unnecessary TODOs

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    1cefa96 View commit details
    Browse the repository at this point in the history

  10. Renamed LOCAL_TERM to TERM

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    2430f3f View commit details
    Browse the repository at this point in the history

  11. Merge branch 'master' into lagemann-dev

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    1ec6bd6 View commit details
    Browse the repository at this point in the history

  12. Reformat

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    2c73948 View commit details
    Browse the repository at this point in the history

  13. Skip crashing tests

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    7f484cb View commit details
    Browse the repository at this point in the history

  14. Rename loop termination analysis

    Alexander Schlenga committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    a91e716 View commit details
    Browse the repository at this point in the history

  15. Removed Todos

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    8483cec View commit details
    Browse the repository at this point in the history

  16. Merge branch 'master' into lagemann-dev

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    11122b3 View commit details
    Browse the repository at this point in the history

  17. Adapted tests to current state

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    91f18ef View commit details
    Browse the repository at this point in the history

  18. Adapted tests to current state

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    1c43039 View commit details
    Browse the repository at this point in the history

  19. No skipping

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    c890d5b View commit details
    Browse the repository at this point in the history

  20. New non terminating for loop

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    569fefd View commit details
    Browse the repository at this point in the history

  21. Folder Renaming

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    aca1ec5 View commit details
    Browse the repository at this point in the history

  22. Enable polyhedra; Removed unnecessary TODOs

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    70bad4c View commit details
    Browse the repository at this point in the history

  23. Removed unnecessary TODOs

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    e70761c View commit details
    Browse the repository at this point in the history

  24. Renamed LOCAL_TERM to TERM

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    ee93929 View commit details
    Browse the repository at this point in the history

  25. Reformat

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    d05da3a View commit details
    Browse the repository at this point in the history

  26. Skip crashing tests

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    036dd17 View commit details
    Browse the repository at this point in the history

  27. Removed Todos

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    4cb5da0 View commit details
    Browse the repository at this point in the history

  28. Adapted tests to current state

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    fec0d62 View commit details
    Browse the repository at this point in the history

  29. Adapted tests to current state

    @LageTs
    LageTs committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    68b01af View commit details
    Browse the repository at this point in the history

  30. Merge remote-tracking branch 'upstream/master'

    Alexander Schlenga committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    529d70e View commit details
    Browse the repository at this point in the history

  31. Restore apronAnalysis.apron.ml

    Alexander Schlenga committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    b7c6ec5 View commit details
    Browse the repository at this point in the history

  32. Explicitly use () as the abstract local state

    Alexander Schlenga committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    432e92d View commit details
    Browse the repository at this point in the history

  33. Change let-in clause to sequential statements

    Alexander Schlenga committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    2953242 View commit details
    Browse the repository at this point in the history

  34. Update src/framework/constraints.ml 

    Make comment more precise

Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
    @serenita @michael-schwarz
    serenita and michael-schwarz committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    c2c69cf View commit details
    Browse the repository at this point in the history

  35. Update src/framework/constraints.ml 

    Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
    @serenita @michael-schwarz
    serenita and michael-schwarz committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    d18d8fe View commit details
    Browse the repository at this point in the history

  36. Remove unnecessary semicola 

    Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
    @serenita @michael-schwarz
    serenita and michael-schwarz committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    0d77172 View commit details
    Browse the repository at this point in the history

  37. Restore 01-simple-cases.c from white space change

    Alexander Schlenga committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    76230f4 View commit details
    Browse the repository at this point in the history

  38. Merge branch 'master'

    Alexander Schlenga committed Jun 29, 2023
    Configuration menu
    Copy the full SHA
    7706ac3 View commit details
    Browse the repository at this point in the history

Commits on Jun 30, 2023

  1. adapted changes from pull request: 1. using a module for tuple; 2. de… 

    …leted dublicated method; 3. removed the arg from the arg_termination variable
    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 30, 2023
    Configuration menu
    Copy the full SHA
    6e62041 View commit details
    Browse the repository at this point in the history

  2. changed the order in C_Printable

    Johanna Schinabeck authored and Johanna Schinabeck committed Jun 30, 2023
    Configuration menu
    Copy the full SHA
    9c8d128 View commit details
    Browse the repository at this point in the history

Commits on Jul 1, 2023

  1. changed naming for SV-Comp specification from NoTermination to Termin… 

    …ation, to meet naming conventions
    Isidor Zweckstetter committed Jul 1, 2023
    Configuration menu
    Copy the full SHA
    c776d8c View commit details
    Browse the repository at this point in the history

Commits on Jul 2, 2023

  1. renamed termination in control to termination_enabled; added comment … 

    …for global invariant in RecursionTermLifter
    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 2, 2023
    Configuration menu
    Copy the full SHA
    b1da8e2 View commit details
    Browse the repository at this point in the history

Commits on Jul 3, 2023

  1. Add description to loop/goto termination analysis

    Alexander Schlenga committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    1ace9d6 View commit details
    Browse the repository at this point in the history

  2. Introduce isEverMultiThreaded analysis 

    Does not work properly yet. Need to fix query function.
    Alexander Schlenga committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    30b03ce View commit details
    Browse the repository at this point in the history

  3. Finish and use everMultiThreaded analysis 

    Used by the termination analysis
    Alexander Schlenga committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    e8aec04 View commit details
    Browse the repository at this point in the history

  4. Revert whitespace change

    Alexander Schlenga committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    f8fa8e3 View commit details
    Browse the repository at this point in the history

  5. added missing __goblint_bounded implementations

    Isidor Zweckstetter committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    4f60156 View commit details
    Browse the repository at this point in the history

  6. Temp. revert must_be_single_threaded_since_start

    Alexander Schlenga committed Jul 3, 2023
    Configuration menu
    Copy the full SHA
    21f2f34 View commit details
    Browse the repository at this point in the history

Commits on Jul 5, 2023

  1. Patched inconsistency with nested loops

    Isidor Zweckstetter committed Jul 5, 2023
    Configuration menu
    Copy the full SHA
    048de26 View commit details
    Browse the repository at this point in the history

Commits on Jul 6, 2023

  1. Merge remote-tracking branch 'upstream/master'

    Alexander Schlenga committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    1421775 View commit details
    Browse the repository at this point in the history

  2. Rename loop termation analysis 

    Keep camelCase naming convention
    Alexander Schlenga committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    b67eacd View commit details
    Browse the repository at this point in the history

  3. changed name

    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    22efd12 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' of https://github.com/serenita/goblint-analyzer

    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    4308bdb View commit details
    Browse the repository at this point in the history

  5. Remove unused code

    Alexander Schlenga committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    c5fe485 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'master' into lagemann-dev

    @LageTs
    LageTs committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    094d564 View commit details
    Browse the repository at this point in the history

  7. Tests adapted and new test 74/35

    @LageTs
    LageTs committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    b9a5c36 View commit details
    Browse the repository at this point in the history

  8. Tests is now passing

    @LageTs
    LageTs committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    7e12cb5 View commit details
    Browse the repository at this point in the history

  9. Restrict boundedness checking to postsolving

    Alexander Schlenga committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    bc7bef7 View commit details
    Browse the repository at this point in the history

  10. Revert "Restrict boundedness checking to postsolving" 

    This reverts commit bc7bef7.
    Alexander Schlenga committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    08ad8d0 View commit details
    Browse the repository at this point in the history

  11. Restrict boundedness checking to postsolving (fix)

    Alexander Schlenga committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    2e05e9e View commit details
    Browse the repository at this point in the history

  12. Widen recursion test

    @LageTs
    LageTs committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    0d79d2a View commit details
    Browse the repository at this point in the history

  13. Merge branch 'lagemann-dev'

    @LageTs
    LageTs committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    4459239 View commit details
    Browse the repository at this point in the history

  14. Adapted test parameter

    @LageTs
    LageTs committed Jul 6, 2023
    Configuration menu
    Copy the full SHA
    1190d63 View commit details
    Browse the repository at this point in the history

Commits on Jul 9, 2023

  1. inlined Groupable C to Map

    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    dbe3684 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' of https://github.com/serenita/goblint-analyzer

    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    73b4f89 View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'upstream/master'

    Alexander Schlenga committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    5f11a50 View commit details
    Browse the repository at this point in the history

  4. Rename query MustTermProg to MustTermAllLoops 

    I find the name MustTermProg confusing because it does not consider
recursion.
    Alexander Schlenga committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    68bf103 View commit details
    Browse the repository at this point in the history

  5. Test moved and renamed

    @LageTs
    LageTs committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    fbc2966 View commit details
    Browse the repository at this point in the history

  6. added comments to explain why test 74/28 does fail and why 30 and 35 … 

    …might behave differently; also restructured module G in the recursionTermLifter
    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    4a6714c View commit details
    Browse the repository at this point in the history

  7. Merge branch 'master' of https://github.com/serenita/goblint-analyzer

    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    852d065 View commit details
    Browse the repository at this point in the history

  8. Tests moved

    @LageTs
    LageTs committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    cb13d14 View commit details
    Browse the repository at this point in the history

  9. cleaned module G from an unnecessary function; addded missing comment… 

    … to analysisState
    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    c6e36e4 View commit details
    Browse the repository at this point in the history

  10. Merge branch 'lagemann-dev'

    @LageTs
    LageTs committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    ff42a19 View commit details
    Browse the repository at this point in the history

  11. Complex test adapted

    @LageTs
    LageTs committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    9d66846 View commit details
    Browse the repository at this point in the history

  12. Merge branch 'master' into lagemann-dev

    @LageTs
    LageTs committed Jul 9, 2023
    Configuration menu
    Copy the full SHA
    ed01412 View commit details
    Browse the repository at this point in the history

Commits on Jul 10, 2023

  1. moved warnings to loop analysis

    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    09ee872 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' of https://github.com/serenita/goblint-analyzer

    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    83e31fc View commit details
    Browse the repository at this point in the history

  3. Test refactoring & parameter correction

    @LageTs
    LageTs committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    d6c11b6 View commit details
    Browse the repository at this point in the history

  4. added autoTune for termination analysis in mainGoblint.ml

    Isidor Zweckstetter committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    1faf729 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' of https://github.com/serenita/goblint-analyzer

    Isidor Zweckstetter committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    d58f6c7 View commit details
    Browse the repository at this point in the history

  6. temporarly removed sem.int.signed_overflow assume_none autotuning

    Isidor Zweckstetter committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    43bf64d View commit details
    Browse the repository at this point in the history

  7. Test indentation

    @LageTs
    LageTs committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    5ef2664 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'master' into lagemann-dev

    @LageTs
    LageTs committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    d394d95 View commit details
    Browse the repository at this point in the history

  9. Execute termination tests in CI even if skipped.

    @LageTs
    LageTs committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    71b1eb2 View commit details
    Browse the repository at this point in the history

  10. added warning for multithreaded case

    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    472a76c View commit details
    Browse the repository at this point in the history

  11. Revert "added warning for multithreaded case" 

    This reverts commit 472a76c.
    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    4af911a View commit details
    Browse the repository at this point in the history

  12. addedd the possibly non-terminating warning for multi threaded programs

    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 10, 2023
    Configuration menu
    Copy the full SHA
    32a654b View commit details
    Browse the repository at this point in the history

Commits on Jul 12, 2023

  1. Merge remote-tracking branch 'upstream/master'

    Alexander Schlenga committed Jul 12, 2023
    Configuration menu
    Copy the full SHA
    d0fc53f View commit details
    Browse the repository at this point in the history

  2. Enable use of everMultiThreaded analysis

    Alexander Schlenga committed Jul 12, 2023
    Configuration menu
    Copy the full SHA
    53c3c1c View commit details
    Browse the repository at this point in the history

  3. Make struct for V anonymous

    Alexander Schlenga committed Jul 12, 2023
    Configuration menu
    Copy the full SHA
    76486c9 View commit details
    Browse the repository at this point in the history

Commits on Jul 13, 2023

  1. indentation

    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    ba9d35a View commit details
    Browse the repository at this point in the history

  2. Test goal and comments changed

    @LageTs
    LageTs committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    a98f503 View commit details
    Browse the repository at this point in the history

  3. Test indentation

    @LageTs
    LageTs committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    98c062a View commit details
    Browse the repository at this point in the history

  4. Execute termination tests in CI even if skipped.

    @LageTs
    LageTs committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    4dd330c View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/lagemann-dev' into lagemann-dev

    @LageTs
    LageTs committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    7e6ac43 View commit details
    Browse the repository at this point in the history

  6. Merge remote-tracking branch 'upstream/master'

    @LageTs
    LageTs committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    12ce13d View commit details
    Browse the repository at this point in the history

  7. Merge branch 'master' into lagemann-dev

    @LageTs
    LageTs committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    6c8152d View commit details
    Browse the repository at this point in the history

  8. Test explanation && new test case termination 43

    @LageTs
    LageTs committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    5f98417 View commit details
    Browse the repository at this point in the history

  9. Test explanation && new test case termination 43

    @LageTs
    LageTs committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    76f540f View commit details
    Browse the repository at this point in the history

  10. Added special function --Still work in progress

    Isidor Zweckstetter committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    40ea15c View commit details
    Browse the repository at this point in the history

  11. Merge branch 'master' of https://github.com/serenita/goblint-analyzer

    Isidor Zweckstetter committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    392c919 View commit details
    Browse the repository at this point in the history

  12. Test for code line detection

    @LageTs
    LageTs committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    30692fc View commit details
    Browse the repository at this point in the history

  13. changed __goblint_bounded constructor from Assert to Bounded

    Isidor Zweckstetter committed Jul 13, 2023
    Configuration menu
    Copy the full SHA
    dc0a284 View commit details
    Browse the repository at this point in the history

Commits on Jul 14, 2023

  1. Merge remote-tracking branch 'upstream/master'

    Alexander Schlenga committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    c1153f7 View commit details
    Browse the repository at this point in the history

  2. Use special function instead of variable indicator 

    We now use __goblint_bounded to mark the place where the value of the
loop counter variable shall be checked for being bounded. Before, we
used a variable called loop exit indicator for that.
    Alexander Schlenga committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    1f499e9 View commit details
    Browse the repository at this point in the history

  3. Clean up, make things look nicer

    Alexander Schlenga committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    b9a5b3f View commit details
    Browse the repository at this point in the history

  4. Wrap always_single_threaded in let-in clause

    Alexander Schlenga committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    6146c76 View commit details
    Browse the repository at this point in the history

  5. Remove PreProcessing exception

    Alexander Schlenga committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    847ea36 View commit details
    Browse the repository at this point in the history

  6. removed the trick to make C groupable due to goblint#1112; deleted pr… 

    …intXML functions, since they don't make much of a difference for displaying
    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    4087dfb View commit details
    Browse the repository at this point in the history

  7. Merge remote-tracking branch 'upstream/master'

    Alexander Schlenga committed Jul 14, 2023
    Configuration menu
    Copy the full SHA
    bd58dc5 View commit details
    Browse the repository at this point in the history

Commits on Jul 15, 2023

  1. Merge remote-tracking branch 'upstream/master'

    Alexander Schlenga committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    2f31211 View commit details
    Browse the repository at this point in the history

  2. Fix indentation

    Alexander Schlenga committed Jul 15, 2023
    Configuration menu
    Copy the full SHA
    0a9c5d4 View commit details
    Browse the repository at this point in the history

Commits on Jul 16, 2023

  1. Added more recursive tests

    @LageTs
    LageTs committed Jul 16, 2023
    Configuration menu
    Copy the full SHA
    10260bd View commit details
    Browse the repository at this point in the history

  2. Merge branch 'lagemann-dev' 

    # Conflicts:
#	src/analyses/loopTermination.ml
    @LageTs
    LageTs committed Jul 16, 2023
    Configuration menu
    Copy the full SHA
    f8a2e53 View commit details
    Browse the repository at this point in the history

  3. removed exit-indikator variable

    Isidor Zweckstetter committed Jul 16, 2023
    Configuration menu
    Copy the full SHA
    4e36511 View commit details
    Browse the repository at this point in the history

Commits on Jul 17, 2023

  1. removed debug print; Might solve cram tests

    Isidor Zweckstetter committed Jul 17, 2023
    Configuration menu
    Copy the full SHA
    d47e88e View commit details
    Browse the repository at this point in the history

  2. Remove debug output

    Alexander Schlenga committed Jul 17, 2023
    Configuration menu
    Copy the full SHA
    021ddad View commit details
    Browse the repository at this point in the history

  3. Code style optimization

    @LageTs
    LageTs committed Jul 17, 2023
    Configuration menu
    Copy the full SHA
    47440a3 View commit details
    Browse the repository at this point in the history

  4. Indentation

    @LageTs
    LageTs committed Jul 17, 2023
    Configuration menu
    Copy the full SHA
    91d331d View commit details
    Browse the repository at this point in the history

  5. Fix indentation

    Alexander Schlenga committed Jul 17, 2023
    Configuration menu
    Copy the full SHA
    fc427bc View commit details
    Browse the repository at this point in the history

  6. Test case 48

    @LageTs
    LageTs committed Jul 17, 2023
    Configuration menu
    Copy the full SHA
    3fb5d14 View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2023

  1. Merge branch 'master' of https://github.com/serenita/goblint-analyzer

    Isidor Zweckstetter committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    97d9c80 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/master'

    Alexander Schlenga committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    8c2b4e0 View commit details
    Browse the repository at this point in the history

  3. Remove unused code; introduce basic error-handling

    Alexander Schlenga committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    601698f View commit details
    Browse the repository at this point in the history

  4. Merge branch 'lagemann-dev' 

    # Conflicts:
#	src/framework/constraints.ml
    @LageTs
    LageTs committed Jul 18, 2023
    Configuration menu
    Copy the full SHA
    ed58098 View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2023

  1. Annotate tests with skip as Apron ist used

    @LageTs
    LageTs committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    66115b1 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/master'

    Alexander Schlenga committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    ed97494 View commit details
    Browse the repository at this point in the history

  3. Revert src/analyses/termination.ml

    @LageTs
    LageTs committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    3c31cb7 View commit details
    Browse the repository at this point in the history

Commits on Jul 25, 2023

  1. Merge remote-tracking branch 'upstream/master'

    Alexander Schlenga committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    912431d View commit details
    Browse the repository at this point in the history

  2. changed initial value of lcv to min int; swaped sequence of increment… 

    … and special function call, to retain top of intdomain at special function call
    Isidor Zweckstetter committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    a9c9c7d View commit details
    Browse the repository at this point in the history

  3. Fix indentation

    Alexander Schlenga committed Jul 25, 2023
    Configuration menu
    Copy the full SHA
    782b21c View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2023

  1. Polish comments

    Alexander Schlenga committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    c53f0b8 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'upstream/master'

    Alexander Schlenga committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    cd8fae0 View commit details
    Browse the repository at this point in the history

  3. Remove runningGob.sh

    Alexander Schlenga committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    c52cf47 View commit details
    Browse the repository at this point in the history

  4. Restore indentation; remove unused include Printf 

    NOTE: This commit makes the indendation of several files wrong again on
purpose!
    Alexander Schlenga committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    867e6ca View commit details
    Browse the repository at this point in the history

  5. More indentation restoring

    Alexander Schlenga committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    0f94aaa View commit details
    Browse the repository at this point in the history

  6. Fix a typo

    Alexander Schlenga committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    f4fd0c2 View commit details
    Browse the repository at this point in the history

  7. Remove goto stuff from loopTermination analysis

    Alexander Schlenga committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    1be8c9c View commit details
    Browse the repository at this point in the history

  8. Add goto-fundec list in cilfacade.ml

    Alexander Schlenga committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    cf594b6 View commit details
    Browse the repository at this point in the history

  9. add gotos with their respective function to new list in Cilfacade

    Isidor Zweckstetter committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    eabf6b7 View commit details
    Browse the repository at this point in the history

  10. added code for control to only print upjumping goto message when goto… 

    … is not in dead code function
    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    19addab View commit details
    Browse the repository at this point in the history

  11. Merge branch 'master' of https://github.com/serenita/goblint-analyzer

    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    7444dc9 View commit details
    Browse the repository at this point in the history

  12. now everything should work :), now iterating over live_lines

    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    72e2e22 View commit details
    Browse the repository at this point in the history

  13. now without prints :)))

    Johanna Schinabeck authored and Johanna Schinabeck committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    6090c62 View commit details
    Browse the repository at this point in the history

  14. Handle skipped (NON-)TERM-Tests other than TODO

    @LageTs
    LageTs committed Jul 26, 2023
    Configuration menu
    Copy the full SHA
    e96433b View commit details
    Browse the repository at this point in the history

Commits on Aug 30, 2023

  1. Set sv-comp flag for upjumping gotos

    @michael-schwarz
    michael-schwarz committed Aug 30, 2023
    Configuration menu
    Copy the full SHA
    e1f8319 View commit details
    Browse the repository at this point in the history

Commits on Sep 1, 2023

  1. Increase indentation in switch-case in update_suite.rb.

    @jerhard
    jerhard committed Sep 1, 2023
    Configuration menu
    Copy the full SHA
    b832f31 View commit details
    Browse the repository at this point in the history

  2. Rename must_be_single_threaded_since_start to must_always_be_single_t… 

    …hreaded
    @jerhard
    jerhard committed Sep 1, 2023
    Configuration menu
    Copy the full SHA
    a6e4af4 View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2023

  1. Merge branch 'master' into term

    @michael-schwarz
    michael-schwarz committed Oct 3, 2023
    Configuration menu
    Copy the full SHA
    7ba0fd3 View commit details
    Browse the repository at this point in the history

Commits on Oct 12, 2023

  1. Merge branch 'master' into term

    @michael-schwarz
    michael-schwarz committed Oct 12, 2023
    Configuration menu
    Copy the full SHA
    8be0343 View commit details
    Browse the repository at this point in the history

  2. Issue non-termination warning for longjmp calls

    @michael-schwarz
    michael-schwarz committed Oct 12, 2023
    Configuration menu
    Copy the full SHA
    44b4492 View commit details
    Browse the repository at this point in the history

  3. Include termination tests into coverage and unlocked

    @michael-schwarz
    michael-schwarz committed Oct 12, 2023
    Configuration menu
    Copy the full SHA
    ea38918 View commit details
    Browse the repository at this point in the history

  4. Simplify global invariant 

    Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
    @michael-schwarz @sim642
    michael-schwarz and sim642 committed Oct 12, 2023
    Configuration menu
    Copy the full SHA
    e284953 View commit details
    Browse the repository at this point in the history

  5. Adapt comments to simplified global invariant

    @michael-schwarz
    michael-schwarz committed Oct 12, 2023
    Configuration menu
    Copy the full SHA
    7f3cadf View commit details
    Browse the repository at this point in the history

  6. Simplify cycle detection

    @michael-schwarz
    michael-schwarz committed Oct 12, 2023
    Configuration menu
    Copy the full SHA
    515a8bd View commit details
    Browse the repository at this point in the history

  7. Failwith meaningful message for invaliud calls to __goblint_bounded

    @michael-schwarz
    michael-schwarz committed Oct 12, 2023
    Configuration menu
    Copy the full SHA
    b3016ff View commit details
    Browse the repository at this point in the history

Commits on Oct 14, 2023

  1. Merge branch 'master' into term

    @michael-schwarz
    michael-schwarz committed Oct 14, 2023
    Configuration menu
    Copy the full SHA
    14c3ead View commit details
    Browse the repository at this point in the history

  2. Cleanup termination property

    @michael-schwarz
    michael-schwarz committed Oct 14, 2023
    Configuration menu
    Copy the full SHA
    5844552 View commit details
    Browse the repository at this point in the history

  3. LTL for termination is F end

    @michael-schwarz
    michael-schwarz committed Oct 14, 2023
    Configuration menu
    Copy the full SHA
    7cca2cf View commit details
    Browse the repository at this point in the history

Commits on Nov 1, 2023

  1. Merge branch 'master' into term

    @michael-schwarz
    michael-schwarz committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    268d86d View commit details
    Browse the repository at this point in the history

  2. Simplify warning

    @michael-schwarz
    michael-schwarz committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    a7d02c4 View commit details
    Browse the repository at this point in the history

  3. Delete old termination analysis

    @michael-schwarz
    michael-schwarz committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    cf22550 View commit details
    Browse the repository at this point in the history

  4. Rm old Termination also from goblint_lib.ml

    @michael-schwarz
    michael-schwarz committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    67cc037 View commit details
    Browse the repository at this point in the history

  5. Make do_preprocess_cil more efficient

    @michael-schwarz
    michael-schwarz committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    dff7be0 View commit details
    Browse the repository at this point in the history

  6. Remove outdated TODO

    @michael-schwarz
    michael-schwarz committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    2d8fe09 View commit details
    Browse the repository at this point in the history

Commits on Nov 2, 2023

  1. Prioritze termination warnings in update_suite.rb

    @michael-schwarz
    michael-schwarz committed Nov 2, 2023
    Configuration menu
    Copy the full SHA
    e690d9a View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into term

    @michael-schwarz
    michael-schwarz committed Nov 2, 2023
    Configuration menu
    Copy the full SHA
    f024fd9 View commit details
    Browse the repository at this point in the history

Commits on Nov 10, 2023

  1. Rename NonTerminating -> Termination

    @michael-schwarz
    michael-schwarz committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    fb92abc View commit details
    Browse the repository at this point in the history

  2. Autotune for Termination

    @michael-schwarz
    michael-schwarz committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    aad465c View commit details
    Browse the repository at this point in the history

  3. Simplify variable names

    @michael-schwarz
    michael-schwarz committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    2ff979b View commit details
    Browse the repository at this point in the history

  4. Deduplicate preprocessing

    @michael-schwarz
    michael-schwarz committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    b49356c View commit details
    Browse the repository at this point in the history

  5. Move everMultiThreaded to threadflag

    @michael-schwarz
    michael-schwarz committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    490203d View commit details
    Browse the repository at this point in the history

  6. Simplify loopTermination

    @michael-schwarz
    michael-schwarz committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    e25b708 View commit details
    Browse the repository at this point in the history

  7. Fail when termination is active and incremental analysis is enabled

    @michael-schwarz
    michael-schwarz committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    d4ab699 View commit details
    Browse the repository at this point in the history

  8. Termination: set is_write_only

    @michael-schwarz
    michael-schwarz committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    47d0f5d View commit details
    Browse the repository at this point in the history

  9. Reset upjumping_gotos

    @michael-schwarz
    michael-schwarz committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    4417b9c View commit details
    Browse the repository at this point in the history

  10. Cleanup upjumping_gotos

    @michael-schwarz
    michael-schwarz committed Nov 10, 2023
    Configuration menu
    Copy the full SHA
    de416ee View commit details
    Browse the repository at this point in the history

Commits on Nov 13, 2023

  1. Make type of variables used for loop termination analysis more easily… 

    … exchangable.
    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    e66cf56 View commit details
    Browse the repository at this point in the history

  2. Remove redundant code for setting todo variable

    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    e02801a View commit details
    Browse the repository at this point in the history

  3. Add define min_int_exp depending on the signedness of the counter var… 

    …iable introduced.

Also remove custom definition for incrementing expression by one.
    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    3d3c069 View commit details
    Browse the repository at this point in the history

  4. Change indentation in update_suite.rb back to reduce number of lines … 

    …changed.
    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    46b0f67 View commit details
    Browse the repository at this point in the history

  5. Change indentatation back.

    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    21d405d View commit details
    Browse the repository at this point in the history

  6. Fix indentation of line.

    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    bc126fa View commit details
    Browse the repository at this point in the history

  7. Use Z instead of Cilint

    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    0e0986a View commit details
    Browse the repository at this point in the history

  8. Change - to _ in name of variable introduced in terminationPreprocess… 

    …ing.

- is not a legal part of a variable.
    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    f18fe58 View commit details
    Browse the repository at this point in the history

  9. Add LoopTermination and TerminationPreprocessing to goblint_lib

    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    aef46ce View commit details
    Browse the repository at this point in the history

  10. Extract function find_loop, given a loop_counter.

    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    72c14e2 View commit details
    Browse the repository at this point in the history

  11. Rename x to loop_counter.

    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    ddfcaea View commit details
    Browse the repository at this point in the history

  12. Use increment_expression that takes the ikind of the counter variable… 

    … into account.
    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    7241324 View commit details
    Browse the repository at this point in the history

  13. Termination analysis: Insert only one increment statement, do not set… 

    … assume no overflow.
    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    76751d4 View commit details
    Browse the repository at this point in the history

  14. Set regresion tests to todo that are now imprecise.

    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    5d54827 View commit details
    Browse the repository at this point in the history

  15. Termination: Use unsigned long long for counter variables; reactivate… 

    … assume no overflow when termination analysis is activated.
    @jerhard
    jerhard committed Nov 13, 2023
    Configuration menu
    Copy the full SHA
    f81ca2c View commit details
    Browse the repository at this point in the history

Commits on Nov 14, 2023

  1. Termination: Update verdict to TODO for 78/35. 

    Case can no longer be handled when no longer using signed integers and assuming no-overflow.
    @jerhard
    jerhard committed Nov 14, 2023
    Configuration menu
    Copy the full SHA
    2728c2a View commit details
    Browse the repository at this point in the history

  2. Autotuner: Activate termination analysis in autotuner.

    @jerhard
    jerhard committed Nov 14, 2023
    Configuration menu
    Copy the full SHA
    8934a21 View commit details
    Browse the repository at this point in the history

Commits on Nov 15, 2023

  1. Indicate that termination analysis is activated.

    @jerhard
    jerhard committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    d5662c5 View commit details
    Browse the repository at this point in the history

  2. Change wording from enabling to enabled for consistency.

    @jerhard
    jerhard committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    245b438 View commit details
    Browse the repository at this point in the history

  3. Add termination to autotune for svcomp.json, but remove it from svcom… 

    …p23.json.
    @jerhard
    jerhard committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    cbe4ad0 View commit details
    Browse the repository at this point in the history

  4. Move LoopTermination in Goblint_lib to analyses/other section.

    @jerhard
    jerhard committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    a466650 View commit details
    Browse the repository at this point in the history

  5. Extract some loops into functions; this reduces runtime of analysis.

    @jerhard
    jerhard committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    b57b9e4 View commit details
    Browse the repository at this point in the history

  6. RelationalAnalysis: Assert type-bounds also for signed types when no-… 

    …overflow is assumed.
    @jerhard
    jerhard committed Nov 15, 2023
    Configuration menu
    Copy the full SHA
    70ef2d2 View commit details
    Browse the repository at this point in the history

Commits on Nov 16, 2023

  1. Termination distribute loops into multiple functions to make analysis… 

    … terminate faster.
    @jerhard
    jerhard committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    8141869 View commit details
    Browse the repository at this point in the history

  2. Add test case that did not work when not asserting the type bounds fo… 

    …r signed types when sem.int.signed_overflow was set to assume_none.
    @jerhard
    jerhard committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    1ef011c View commit details
    Browse the repository at this point in the history

  3. Remove outdated comment.

    @jerhard
    jerhard committed Nov 16, 2023
    Configuration menu
    Copy the full SHA
    d9f3910 View commit details
    Browse the repository at this point in the history

Commits on Nov 17, 2023

  1. Autotuner: Remove activateTerminationAnalysis, as there is already ot… 

    …her code for it.
    @jerhard
    jerhard committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    26d8012 View commit details
    Browse the repository at this point in the history

  2. Add specification to activated settings for autotuner.

    @jerhard
    jerhard committed Nov 17, 2023
    3 Configuration menu
    Copy the full SHA
    28dca49 View commit details
    Browse the repository at this point in the history

  3. Call Autotune.focusOnSpecification before preprocessing, as terminati… 

    …no analysis needs to be activated before preprocessing to work.
    @jerhard
    jerhard committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    a4adabd View commit details
    Browse the repository at this point in the history

  4. Do loop unrolling for loops with boundedness check.

    @jerhard
    jerhard committed Nov 17, 2023
    Configuration menu
    Copy the full SHA
    41ee060 View commit details
    Browse the repository at this point in the history