Josh Berdine, Nikolaj Bjorner, Samin Ishtiaq, Christoph M. Diagnosing Abstraction Failure for Separation Logic-based Analyses. Josh Berdine, Arlen Cox, Samin Ishtiaq, Christoph M. SLAyer: Memory Safety for Systems-level Code. Once we have received the signed CLA, we'll review the request. Please submit a Contributor License Agreement (CLA) before submitting a pull request.Īlternatively, download the agreement Microsoft Contribution License Agreement.docx or Microsoft Contribution License Agreement.pdf), sign, scan, and email it back to sure to include your github user name along with the agreement. To contribute, you will need to complete a Contributor License Agreement (CLA).īriefly, this agreement testifies that you are granting us permission to use the submitted change according to the terms of the project's license,Īnd that the work being submitted is under appropriate copyright.
See test/README for additional testing instructions. $ cd sll $ slayer -vSE 3 -vAbs 2 traverse.c When slayer runs on tests, it needs to run the WDK compiler.) New shell is that SLAyer is built using the usual VS compiler, but Start a new VS2010+bash shell, and cd to here.
See src/README for additional building instructions. The slayer.exe will be left in the bin directory. To set this up, start in a VS 201x shell. Setupīuilding and testing SLAyer has some dependencies on the environment. SLAyer is licensed under the MIT licence included in the LICENSE file. SLAyer is an automatic formal verification tool that uses separation logic to verify memory safety of C programs.
0 kommentar(er)
