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

Add new IcfgBuilder #690

Open
wants to merge 66 commits into
base: dev
Choose a base branch
from
Open

Add new IcfgBuilder #690

wants to merge 66 commits into from
+13,001 −8,824

Commits on Nov 14, 2024

  1. wip IcfgBuilder Plugin

    @NiklasKult @schuessf
    NiklasKult authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    5a5df01 View commit details
    Browse the repository at this point in the history

  2. wip 2 IcfgBuilder Plugin

    @NiklasKult @schuessf
    NiklasKult authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    e74ea69 View commit details
    Browse the repository at this point in the history

  3. moving of classes into old RCFGBuilder & invariants

    @NiklasKult @schuessf
    NiklasKult authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    a7c19f1 View commit details
    Browse the repository at this point in the history

  4. Backtranslation wip

    @NiklasKult @schuessf
    NiklasKult authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    dfd35b2 View commit details
    Browse the repository at this point in the history

  5. Backtranslation

    @NiklasKult @schuessf
    NiklasKult authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    dcc262b View commit details
    Browse the repository at this point in the history

  6. cleanup

    @NiklasKult @schuessf
    NiklasKult authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    665ebcd View commit details
    Browse the repository at this point in the history

  7. Rename license header

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    1005b9e View commit details
    Browse the repository at this point in the history

  8. comment and delete useless file

    @NiklasKult @schuessf
    NiklasKult authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    3376ae6 View commit details
    Browse the repository at this point in the history

  9. add author info

    @NiklasKult @schuessf
    NiklasKult authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    77f235c View commit details
    Browse the repository at this point in the history

  10. Fix for new ICFG in WitnessPrinter

    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    f64e131 View commit details
    Browse the repository at this point in the history

  11. Bugfix: Do not just reuse ateBuilder 

    Otherwise the StepInfo is reset, since mutable sets are used.
    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    45449d8 View commit details
    Browse the repository at this point in the history

  12. fix label last statement in procedure

    @NiklasKult @schuessf
    NiklasKult authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    818567e View commit details
    Browse the repository at this point in the history

  13. Add IcfgBuilder to feature.xml

    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    da66c24 View commit details
    Browse the repository at this point in the history

  14. fix Label last Statement of While/If

    @NiklasKult @schuessf
    NiklasKult authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    2332261 View commit details
    Browse the repository at this point in the history

  15. Fix plugin name

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    4b83d2c View commit details
    Browse the repository at this point in the history

  16. Require plugin instead of require package

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    7529abc View commit details
    Browse the repository at this point in the history

  17. Add icfgbuilder to UltimateRegressionTest

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    4d3df4d View commit details
    Browse the repository at this point in the history

  18. add icfgbuilder as valid generator for abstract interpretation plugin

    @danieldietsch @schuessf
    danieldietsch authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    500be5c View commit details
    Browse the repository at this point in the history

  19. Adapt to Dominik's move of AtomicBlockInfo

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    ffa4677 View commit details
    Browse the repository at this point in the history

  20. CC fixes

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    7971d04 View commit details
    Browse the repository at this point in the history

  21. Simplify code: more explicit case distinction

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    35560bc View commit details
    Browse the repository at this point in the history

  22. Bugfix: We need the target location, new StatementSequence is startet… 

    … when we build the new block
    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    41a78f8 View commit details
    Browse the repository at this point in the history

  23. Inline method

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    6e7ce6a View commit details
    Browse the repository at this point in the history

  24. Bugfix BooleanLiteral 

    We need that BooleanLiteral have a type.
We now ensure this by using the ExpressionFactory#createBooleanLiteral
    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    2512dd6 View commit details
    Browse the repository at this point in the history

  25. move CfgBuilder.LargeBlockEncoding to own file

    @maul-esel @schuessf
    maul-esel authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    b9566c6 View commit details
    Browse the repository at this point in the history

  26. avoid duplicating CFG LargeBlockEncoding

    @maul-esel @schuessf
    maul-esel authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    b8f9d7a View commit details
    Browse the repository at this point in the history

  27. Fix backtranslation of IfStatement and WhileStatement

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    837c2e2 View commit details
    Browse the repository at this point in the history

  28. Revert "Inline method" 

    This reverts commit f13a388.
    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    26e8a57 View commit details
    Browse the repository at this point in the history

  29. Revert "Bugfix: We need the target location, new StatementSequence is… 

    … startet when we build the new block"

This reverts commit ba104cf.
    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    90be532 View commit details
    Browse the repository at this point in the history

  30. Bugfix atomic blocks in IcfgBuilder 

    Bugfix for cases where atomic blocks end with an IfStatement.
    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    14cb474 View commit details
    Browse the repository at this point in the history

  31. Explicit case distinction, cast to StatementSequence

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    88bea96 View commit details
    Browse the repository at this point in the history

  32. Refactor private method of IcfgBuilder 

    * Rename identifiers
* Add documentation
* Make method void (returned object is an argument of method)
    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    5e83f1d View commit details
    Browse the repository at this point in the history

  33. Refactor private method of IcfgBuilder 

    * Rename identifiers
* Add documentation
* Make method void (returned object is an argument of method)
    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    2250dd1 View commit details
    Browse the repository at this point in the history

  34. Refactor IcfgBuilder 

    * extract method for building IcfgLocations
* remove method that became obsolete
    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    4217afa View commit details
    Browse the repository at this point in the history

  35. Bugfix and refactoring IcfgBuilder 

    * Bugfix: Do not merge loop entry and location after invariant.
* Rename identifiers
    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    b45bc3c View commit details
    Browse the repository at this point in the history

  36. Add backtranslation for free invariants

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    ae12d66 View commit details
    Browse the repository at this point in the history

  37. Bugfix: Support for backtranslation of loop invariants

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    dcd4fe1 View commit details
    Browse the repository at this point in the history

  38. Update errorpath

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    82df167 View commit details
    Browse the repository at this point in the history

  39. Refactoring IcfgBuilder 

    Do not copy annotations directly from original statements to edges but only to
auxiliary statements. (Because annotations are copied from all
statements to edges anyway.)
    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    c42775f View commit details
    Browse the repository at this point in the history

  40. Refactoring IcfgBuilder 

    Unify code for prepending statements
    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    830ed51 View commit details
    Browse the repository at this point in the history

  41. Remove origin

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    aa2c581 View commit details
    Browse the repository at this point in the history

  42. Add documentation and assert

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    2810c26 View commit details
    Browse the repository at this point in the history

  43. Add auxiliary edges for labels

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    7aa0556 View commit details
    Browse the repository at this point in the history

  44. Refactoring IcfgBacktranslator 

    Use assumption that mapping returns singleton except for calls.
    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    a9ec88c View commit details
    Browse the repository at this point in the history

  45. Omit labels in backtranslation

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    ae2fe35 View commit details
    Browse the repository at this point in the history

  46. Bugfix backtranslation

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    b6725cb View commit details
    Browse the repository at this point in the history

  47. Remove XnfConversionTechnique

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    989489d View commit details
    Browse the repository at this point in the history

  48. make sure nodatarace-LBE is only used for concurrent programs 

    The setting "Only consider context switches at boundaries of atomic blocks"
(aka the nodatarace-LBE) is only meant to affect concurrent programs. It
performs a kind of large-block encoding (LBE) that is usually not desirable
for sequential programs.
    @maul-esel @schuessf
    maul-esel authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    d41dd3b View commit details
    Browse the repository at this point in the history

  49. Use IcfgBuilder in all settings and toolchains

    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    1b2b065 View commit details
    Browse the repository at this point in the history

  50. CC fixes

    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    aad567b View commit details
    Browse the repository at this point in the history

  51. Sync preferences

    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    bbdf1c9 View commit details
    Browse the repository at this point in the history

  52. Remove IcfgBuilder settings and toolchains 

    IcfgBuilder is already the default anyway.
    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    078f261 View commit details
    Browse the repository at this point in the history

  53. Make class public to use in IcfgBuilder

    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    eba3b56 View commit details
    Browse the repository at this point in the history

  54. Sync CfgBuilder classes

    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    34230b1 View commit details
    Browse the repository at this point in the history

  55. Omit UnstructureCode in BoogiePreprocessor

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    506cd1a View commit details
    Browse the repository at this point in the history

  56. Adapt solver check to IcfgBuilder

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    0ec76e3 View commit details
    Browse the repository at this point in the history

  57. Add IcfgBuilder to BuchiProgramProduct

    @Heizmann @schuessf
    Heizmann authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    14e1f52 View commit details
    Browse the repository at this point in the history

  58. Move replacement of array assignment from UnstructureCode to new obse… 

    …rver

The new IcfgBuilder does not use UnstructureCode anymore. To avoid reimplementation there, this was moved to the new oberserver ReplaceArrayAssignments.
    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    b85b9e1 View commit details
    Browse the repository at this point in the history

  59. Add removal of assume true statements 

    This does not seem as useful as in the RCFGBuilder, as most of such assume true statements where introduced in UnstructureCode, but it does not harm to keep it.
    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    3267313 View commit details
    Browse the repository at this point in the history

  60. Fix sonar issues, remove unused code

    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    d52e0c8 View commit details
    Browse the repository at this point in the history

  61. Move side-effect outside of assertion

    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    fbccbf6 View commit details
    Browse the repository at this point in the history

  62. Remove if end location if possible

    @NiklasKult @schuessf
    NiklasKult authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    1812cdd View commit details
    Browse the repository at this point in the history

  63. Adapt to e53bbfe

    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    b09905c View commit details
    Browse the repository at this point in the history

  64. fix reachable but not registered program points

    @NiklasKult @schuessf
    NiklasKult authored and schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    9107825 View commit details
    Browse the repository at this point in the history

  65. Fix missing annotation

    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    bcf6ac4 View commit details
    Browse the repository at this point in the history

  66. Minor simplifications

    @schuessf
    schuessf committed Nov 14, 2024
    Configuration menu
    Copy the full SHA
    c409b0f View commit details
    Browse the repository at this point in the history