[www] r235600 - Added SMACK to the LLVM Projects page.

[John Criswell]

Dear All,

I'd appreciate a quick post-commit review for these small web-site changes.

Regards,

John Criswell

On 4/23/15 10:35 AM, John Criswell wrote:
> Author: criswell
> Date: Thu Apr 23 09:35:54 2015
> New Revision: 235600
>
> URL: http://llvm.org/viewvc/llvm-project?rev=235600&view=rev
> Log:
> Added SMACK to the LLVM Projects page.
> Added SMACK to the list of LLVM Users.
>
> Modified:
>      www/trunk/ProjectsWithLLVM/index.html
>      www/trunk/Users.html
>
> Modified: www/trunk/ProjectsWithLLVM/index.html
> URL: http://llvm.org/viewvc/llvm-project/www/trunk/ProjectsWithLLVM/index.html?rev=235600&r1=235599&r2=235600&view=diff
> ==============================================================================
> --- www/trunk/ProjectsWithLLVM/index.html (original)
> +++ www/trunk/ProjectsWithLLVM/index.html Thu Apr 23 09:35:54 2015
> @@ -36,6 +36,7 @@
>   <div class="www_text">
>   
>   <ul>
> +<li><a href="#smack">SMACK Software Verifier</a></li>
>   <li><a href="#discopop">DiscoPoP: A Parallelism Discovery Tool</a></li>
>   <li><a href="#jade">Just-in-time Adaptive Decoder Engine (Jade)</a></li>
>   <li><a href="#crack">The Crack Programming Language</a></li>
> @@ -75,6 +76,27 @@
>   </div>
>   
>   <!--=========================================================================-->
> +<div class="www_subsection">
> +<a name="smack">SMACK Software Verifier</a>
> +</div>
> +
> +<div class="www_subsubsection">
> +  By <a href="https://github.com/smackers/smack/wiki/Smackers">smackers</a>
> +</div>
> +
> +<div class="www_text">
> +  <p>
> +  <a href="https://github.com/smackers/smack">SMACK</a> is an automated
> +  software verifier, verifying assertions given in its input LLVM
> +  intermediate representation (IR) programs. Under the hood, SMACK is a
> +  translator from the LLVM IR into the Boogie intermediate verification
> +  language (IVL). Targeting Boogie exploits a canonical platform which
> +  simplifies the implementation of algorithms for verification, model
> +  checking, and abstract interpretation.
> +  </p>
> +</div>
> +
> +<!--=========================================================================-->
>   <div class="www_subsection">
>   <a name="discopop">DiscoPoP: A Parallelism Discovery Tool</a>
>   </div>
>
> Modified: www/trunk/Users.html
> URL: http://llvm.org/viewvc/llvm-project/www/trunk/Users.html?rev=235600&r1=235599&r2=235600&view=diff
> ==============================================================================
> --- www/trunk/Users.html (original)
> +++ www/trunk/Users.html Thu Apr 23 09:35:54 2015
> @@ -295,6 +295,11 @@ multi-core code generation to the compil
>     </tr>
>   
>     <tr>
> +    <td><a href="https://github.com/smackers/smack">SMACK Software Verifier</a></td>
> +    <td>Software verifier that converts LLVM IR to Boogie</td>
> +  </tr>
> +
> +  <tr>
>       <td><a href="http://objective.modula2.net">Objective Modula-2 Project</a></td>
>       <td>Modula-2 compiler w/ObjC runtime support. Targets Objective-C and LLVM.</td>
>     </tr>
>
>
> _______________________________________________
> llvm-commits mailing list
> llvm-commits at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvm-commits


-- 
John Criswell
Assistant Professor
Department of Computer Science, University of Rochester
http://www.cs.rochester.edu/u/criswell