-
Notifications
You must be signed in to change notification settings - Fork 122
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
tamarin-prover can't run oracle #629
Comments
Hi, please have a look at #577 and see if that solves your problem. |
Hi,I have tried to modify the Python version and checked the executable permissions of the file, but the issue has not been resolved yet. The problem I encountered is somewhat different from #577
|
Is the file set to be executable? That is, what does a |
Thanks. But the issue has not been resolved yet. |
I'm wondering if it's related to this function |
Can you run the oracle file directly? I.e., Also, please check in your |
Yes, it can successfully run the myoracle file. |
When I run the following command,
tamarin-prover --prove --heuristic=O --oraclename=myoracle oracle_test.spthy
I get the following problem
tamarin-prover: ./myoracle: readCreateProcess: posix_spawnp: does not exist (No such file or directory)
myoracle is in the current folder.
Thanks.
Command line output
ubuntu@ubuntu-KVM:
/Tamarin$ ls/Tamarin$ tamarin-prover --prove=uniqueness --heuristic=O --oraclename=myoracle oracle_test.spthyclient_session_key.aes DH.spthy myoracle oracle_test.spthy
ubuntu@ubuntu-KVM:
maude tool: 'maude'
checking version: 2.7.1. OK.
checking installation: OK.
[Saturating Sources] Step 1/5
[Saturating Sources] Step 2/5
[Saturating Sources] Step 1/5
[Saturating Sources] Step 2/5
[Saturating Sources] Step 1/5
[Saturating Sources] Step 2/5
tamarin-prover: ./myoracle: readCreateProcess: posix_spawnp: does not exist (No such file or directory)
The text was updated successfully, but these errors were encountered: