search

SymbolicPathFinder / jpf-symbc

Symbolic PathFinder
https://github.com/SymbolicPathFinder/jpf-symbc
124 stars 89 forks source link

Some examples don't work out of the box. #67

Open cniddodi opened 2 years ago

cniddodi commented 2 years ago

The following examples don't execute successfully:

         - perthread/PerthreadExample.jpf

        - [SEVERE] JPF configuration error: class not found gov.nasa.jpf.symbc.symexectree.visualizer.SymExecTreeVisualizerListener
            [SEVERE] JPF terminated

    - strings/DelimSearchz.jpf

        - [SEVERE] JPF configuration error: class not found sidechannel.TimingChannelListener
            [SEVERE] JPF terminated 

    - concolic/MathSin.jpf
        - [SEVERE] JPF exception, terminating: exception during instructionExecuted() notification
        java.lang.AssertionError

    - concolic/TestConcreteAnote.jpf
        - [SEVERE] JPF exception, terminating: exception during instructionExecuted() notification
        java.lang.AssertionError

    - coverage/MyDriverForPathAnnotations.jpf
        - java.lang.ClassCastException: Cannot cast coverage.JPF_coverage_CheckCoverage to gov.nasa.jpf.vm.NativePeer

    - fuzz.gram.test/Chars99int2_2_2.jpf
        - [SEVERE] JPF configuration error: class not found Dbg_inst_listener
        [SEVERE] JPF terminated

    - lazyinit.paramAndPoly/TestDriver00.jpf
        - [SEVERE] cannot load application class uberlazy.TestDriver00

    - lazyinit.paramAndPoly/TestDriver01.jpf
        - [SEVERE] cannot load application class uberlazy.TestDriver01

    - lazyinit.paramAndPoly/TestDriver02.jpf
        - [SEVERE] cannot load application class uberlazy.TestDriver02

    - lazyinit.paramAndPoly/TestDriver03.jpf
        -  [SEVERE] cannot load application class uberlazy.TestDriver03

    - lazyinit.paramAndPoly/TestDriver04.jpf
        - [SEVERE] cannot load application class uberlazy.TestDriver04

    - sequences/BankAccountDriverSeqSymCGOptimizationVisualizer.jpf
        - [SEVERE] JPF configuration error: class not found gov.nasa.jpf.symbc.symexectree.visualizer.SymExecTreeVisualizerListener
        [SEVERE] JPF terminated

    - simple/Branches.jpf
        -  [za.ac.sun.cs.green.taskmanager.ParallelTaskManager process][SEVERE] thread execution error

    - strings/HelloWorld.jpf
        - [SEVERE] cannot load application class strings.HelloWorld

    - strings/IndexOfTest.jpf
        - java.lang.UnsatisfiedLinkError: no abc in java.library.path

    - strings/NaivePWCheck.jpf
        - [SEVERE] JPF configuration error: class not found sidechannel.TimingChannelListener
        [SEVERE] JPF terminated

    - strings/NaivePWCheckz.jpf
        - java.lang.UnsatisfiedLinkError: no abc in java.library.path

    - strings/PassCheck01z.jpf
        -  [SEVERE] JPF configuration error: class not found sidechannel.TimingChannelListener
        [SEVERE] JPF terminated

    - strings/PassCheck02.jpf
        -  [SEVERE] JPF configuration error: class not found sidechannel.TimingChannelListener
        [SEVERE] JPF terminated

    - strings/StringSearch01.jpf
        -  [SEVERE] JPF configuration error: class not found sidechannel.TimingChannelListener
        [SEVERE] JPF terminated

    - strings/SubStr.jpf
        -  java.lang.UnsatisfiedLinkError: no abc in java.library.path

    - tsafe/Conflict.jpf
        -  [SEVERE] JPF configuration error: class not found gov.nasa.jpf.reliability.listeners.FloatingPointReliabilityListener
        [SEVERE] JPF terminated

    - tsafe/turnlogic.jpf
        -  [SEVERE] cannot load application class TurnLogic

    - ExampleDReal.jpf
        - java.lang.RuntimeException: ## Error: unknown decision procedure symbolic.dp=dreal 
        (use choco or IAsolver or CVC3)

    - icse13MT.jpf
        - [SEVERE] JPF configuration error: class not found gov.nasa.jpf.symbc.AntoniosListener
        [SEVERE] JPF terminated

    - PronSysmExe.jpf
        -[SEVERE] JPF configuration error: class not found .symbc.probsym.ProbSymListener
        [SEVERE] JPF terminated

    - TestPaths.jpf
        - [SEVERE] JPF configuration error: class not found .symbc.SymbolicListenerCounting
        [SEVERE] JPF terminated