reb-ddm / analyzer Goto Github PK

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