8000 make error for SGX folder and AbstractPlatform folder · Issue #2 · 0tcb/TAP · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

make error for SGX folder and AbstractPlatform folder #2

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.

Sign up for GitHub

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

Jump to bottom
Open
YueWang1996 opened this issue Jul 10, 2020 · 1 comment
Open

make error for SGX folder and AbstractPlatform folder #2

YueWang1996 opened this issue Jul 10, 2020 · 1 comment

Comments

@YueWang1996
Copy link
YueWang1996 commented Jul 10, 2020 •
edited
Loading

Hello, I am trying to execute makefile in SGX folder, but I meet this error:

yue@ubuntu:~/TAP$ cd SGX
yue@ubuntu:~/TAP/SGX$ export BOOGIE="mono ~/boogie/Binaries/Boogie.exe"
yue@ubuntu:~/TAP/SGX$ ls
Hardware Makefile Proof.bpl
yue@ubuntu:~/TAP/SGX$ make

mono ~/boogie/Binaries/Boogie.exe /xml:build/SGXProof.xml /z3opt:smt.RELEVANCY=0 /z3opt:smt.CASE_SPLIT=0 /errorLimit:1 Hardware/sgx.bpl Proof.bpl
[ERROR] FATAL UNHANDLED EXCEPTION: System.IO.DirectoryNotFoundException: Could not find a part of the path "/home/yue/TAP/SGX/build/SGXProof.xml".
  at System.IO.FileStream..ctor (System.String path, System.IO.FileMode mode, System.IO.FileAccess access, System.IO.FileShare share, System.Int32 bufferSize, System.Boolean anonymous, System.IO.FileOptions options) [0x00164] in <a17fa1457c5d44f2885ac746c1764ea5>:0 
  at System.IO.FileStream..ctor (System.String path, System.IO.FileMode mode, System.IO.FileAccess access, System.IO.FileShare share, System.Int32 bufferSize, System.IO.FileOptions options) [0x00000] in <a17fa1457c5d44f2885ac746c1764ea5>:0 
  at System.IO.FileStream..ctor (System.String path, System.IO.FileMode mode, System.IO.FileAccess access, System.IO.FileShare share, System.Int32 bufferSize, System.Boolean useAsync) [0x00000] in <a17fa1457c5d44f2885ac746c1764ea5>:0 
  at (wrapper remoting-invoke-with-check) System.IO.FileStream..ctor(string,System.IO.FileMode,System.IO.FileAccess,System.IO.FileShare,int,bool)
  at System.Xml.XmlWriterSettings.CreateWriter (System.String outputFileName) [0x00051] in <4a776760e559455ead15edf260db6599>:0 
  at System.Xml.XmlWriter.Create (System.String outputFileName, System.Xml.XmlWriterSettings settings) [0x0000a] in <4a776760e559455ead15edf260db6599>:0 
  at Microsoft.Boogie.XmlSink.Open () [0x0002d] in <b8387f4c32184b3fb265854e480fe328>:0 
  at Microsoft.Boogie.OnlyBoogie.Main (System.String[] args) [0x00081] in <eedaca8a21cb4887bb5e5eb3b461f942>:0 
Makefile:8: recipe for target 'build/SGXProof.xml' failed
make: *** [build/SGXProof.xml] Error 1
yue@ubuntu:~/TAP/SGX$ mono ~/boogie/Binaries/Boogie.exe
*** Error: No input files were specified.

Similarly, I get an error when I try to execute makefile in AbstractPlatform folder, which shows as below:

yue@ubuntu:~/TAP/AbstractPlatform$ make

mono ~/boogie/Binaries/Boogie.exe /z3opt:smt.RELEVANCY=0 /z3opt:smt.CASE_SPLIT=0 /errorLimit:1  /xml:build/CacheConfidentialityProof.xml Types.bpl ../Common/Types.bpl ../Common/Common.bpl ../Common/Cache.bpl CPU.bpl ConfidentialityProof.bpl ProofCommon.bpl CacheConfidentialityProof.bpl
Boogie program verifier version 2.4.1.10503, Copyright (c) 2003-2014, Microsoft.
*** Error: '/z3opt:smt.RELEVANCY=0': Filename extension '.relevancy=0' is not supported. Input files must be BoogiePL programs (.bpl).
Makefile:48: recipe for target 'build/CacheConfidentialityProof.xml' failed
make: *** [build/CacheConfidentialityProof.xml] Error

I would appreciate it if you could give me any hints about the solutions to these bugs.
Thanks for your attention.
@arxgy
Copy link
arxgy commented Dec 2, 2022

You can replace the /z3opt to /proverOpt:O: like this:
BOOGIEOPT:=/proverOpt:O:smt.RELEVANCY=0 /proverOpt:O:smt.CASE_SPLIT=0 /errorLimit:1
Hope this be useful.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None ye 381D t
Milestone
No milestone
Development

No branches or pull requests
2 participants
@YueWang1996 @arxgy
0