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.

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

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

Open
cniddodi opened this issue Dec 16, 2021 · 0 comments
Open

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

cniddodi opened this issue Dec 16, 2021 · 0 comments

Comments

@cniddodi
Copy link

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant