NOTES

[reb-ddm]

APRON:
    To get the index of a variable if you have a variable, use:
    Environment.dim_of_var env variable 

    Function naming:
    _with -> in-place changes
    no _with -> make a copy 

    == compares address equality 
    != for unequal addresses

    HOW TO RUN THE REGRESSION TESTS:
    Method 1: ./regtest.sh numberofdirectory(=77) numberoftest -> run a single regression test
    Method 2: ./scripts/update_suite.rb group lin2vareq -> runs only our tests but all at the same time
    Method 3: make test -> run entire test suite
    -> the methods have a different behaviour w.r.t. unreachable code 
    - test with different flags 
    - gobview doesnt work with apron
      -Visualize test:
      ./regtest.sh 63 01
      python3 -m http.server
      open http://localhost:8000/ on a browser
      go to /result folder
      index.xml -> main (printxml uses show)
      click on program points 
      orange nodes: dead code
      state at the beginning of the line
      multiple paths-> line was divided in two parts by the analysis

    TODO:
    12. January or earlier pull request -> all features implemented 
            -> run on svcomp benchmarks -> to check runtime and unsoundness and crashes

    DEBUG:
    1. print stack trace while executing ./goblint:
      -v option for goblint -> prints stack trace
    2. Print the debug information defined with M.tracel:
      https://goblint.readthedocs.io/en/latest/developer-guide/debugging/#tracing
      ./script/trace_on
      --trace name1 --trace name2
    3. Debug OCaml
      gdb debug for OCaml
      or with EarlyBird (apparently it will maybe not work)
      or with ocamldebug

    SUBMODULES:
    To update submodules:
    git submodule update --init --recursive

[alina-weber]

Deadline for final pull request: 12th of January Next meeting with supervisors: 11th of January

[reb-ddm]

TODO add ask for overflow

may signed overflow -> instead of no_overflow in each subexpression -> because top is not always returned if subexpr is top exp -> MayBool.t -> in base analysis -> with query function match query -> or use EvalInt in each subexpression ignores "assume_none" but we don't call that function if it's assume none treat assume_wraparound like assume_none Function calls in expressions get converted to variables OR use no_overflow OR still provide the query but not use it

Base contains interval analysis, add MaySignedOverflow to query that uses evalInt for each subexpression

Or just do it locally?

also ensure that x = y information gets considered, there is no overflow here

in each subexpression

HOW TO USE QUERY: ask function in ctx in assign in relatioinAnalysis.ml

for casts: upcast("is_cast_injective") -> no problem downcast/reinterpreted cast: type1 to type2-> check bounds if gamma(x1) subset range(type2) then ok else if the concrete value is a single constant, then convert (cast with int domain) else don't bother

in texpr_of_cil_expr -> give up if it needs overflow handling

TEST for widening and narrowing -> only works with nested loops? idk

TEST for different integer kinds