Open
Description
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.
Metadata
Metadata
Assignees
Labels
No labels