Commit 7162dd60 authored by Heiko Becker's avatar Heiko Becker
Browse files

Merge branch 'stable-certification' into 'certification'

# Conflicts:
#   src/main/scala/daisy/Main.scala
parents f7b47a46 983d6141
......@@ -21,3 +21,4 @@ rawdata/*
.ensime*
/daisy
last.log
output/*.scala
......@@ -5,12 +5,12 @@
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Contributing &mdash; Daisy 0.0 documentation</title>
<link rel="stylesheet" href="_static/alabaster.css" type="text/css" />
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<script type="text/javascript">
var DOCUMENTATION_OPTIONS = {
URL_ROOT: './',
......@@ -27,18 +27,18 @@
<link rel="top" title="Daisy 0.0 documentation" href="index.html" />
<link rel="next" title="Testing" href="testing.html" />
<link rel="prev" title="Navigating the Repository" href="repo_navigation.html" />
<meta name="viewport" content="width=device-width, initial-scale=0.9, maximum-scale=0.9">
</head>
<body role="document">
<body role="document">
<div class="document">
<div class="documentwrapper">
<div class="bodywrapper">
<div class="body" role="main">
<div class="section" id="contributing">
<h1>Contributing<a class="headerlink" href="#contributing" title="Permalink to this headline"></a></h1>
<p>Here is some (random) information that may help you if you want to extend or modify Daisy.</p>
......@@ -60,6 +60,8 @@ with the other immutable &#8216;Seq&#8217;s.</p>
<div class="highlight-python"><div class="highlight"><pre>package daisy
package analysis
// default Seq is mutable
import scala.collection.immutable.Seq
import lang.Trees.Program
/**
......@@ -73,7 +75,7 @@ object TemplatePhase extends DaisyPhase {
override val name = &quot;&quot;
override val description = &quot;&quot;
override val definedOptions: Set[CmdLineOptionDef] = Set()
override val definedOptions: Set[CmdLineOptionDef[Any]] = Set()
implicit val debugSection = ???
......@@ -99,7 +101,7 @@ object TemplatePhase extends DaisyPhase {
</div>
</div>
</div>
<!--div class="sphinxsidebar" role="navigation" aria-label="main navigation">
<div class="sphinxsidebar" role="navigation" aria-label="main navigation">
<div class="sphinxsidebarwrapper">
<h3><a href="index.html">Table Of Contents</a></h3>
<ul>
......@@ -139,23 +141,23 @@ object TemplatePhase extends DaisyPhase {
</div>
<script type="text/javascript">$('#searchbox').show(0);</script>
</div>
</div-->
</div>
<div class="clearer"></div>
</div>
<div class="footer">
&copy;2015, E. Darulova.
|
Powered by <a href="http://sphinx-doc.org/">Sphinx 1.3.1</a>
&amp; <a href="https://github.com/bitprophet/alabaster">Alabaster 0.7.6</a>
|
<a href="_sources/contributing.txt"
rel="nofollow">Page source</a>
</div>
</body>
</html>
\ No newline at end of file
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
......@@ -5,12 +6,12 @@
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Trees &mdash; Daisy 0.0 documentation</title>
<title>Index &mdash; Daisy 0.0 documentation</title>
<link rel="stylesheet" href="_static/alabaster.css" type="text/css" />
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<script type="text/javascript">
var DOCUMENTATION_OPTIONS = {
URL_ROOT: './',
......@@ -25,80 +26,40 @@
<script type="text/javascript" src="_static/doctools.js"></script>
<script type="text/javascript" src="https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
<link rel="top" title="Daisy 0.0 documentation" href="index.html" />
<meta name="viewport" content="width=device-width, initial-scale=0.9, maximum-scale=0.9">
</head>
<body role="document">
<body role="document">
<div class="document">
<div class="documentwrapper">
<div class="bodywrapper">
<div class="body" role="main">
<div class="section" id="trees">
<h1>Trees<a class="headerlink" href="#trees" title="Permalink to this headline"></a></h1>
<p>Daisy&#8217;s AST is defined in lang/Trees. The trees and heir structure is heavily inspired
by Leon (or simply copied in many places). This has been done on purpose so that
Daisy can re-use much of Leon&#8217;s functionality easily.</p>
<p>If you want to add a new AST node, you have to do these steps:</p>
<p>1:
if (real-leon can extract new node)
then</p>
<blockquote>
<div>skip</div></blockquote>
<dl class="docutils">
<dt>else</dt>
<dd>modify real-leon to do the extraction
package real-leon and update the jar files in daisy/lib/</dd>
</dl>
<p>2: add a new node in lang/Trees</p>
<p>3: extract new node from real-leon in frontends/ScalaExtraction</p>
<p>4: update lang/PrettyPrinter</p>
<p>5: update Extractors and check the functions in lang/TreeOps</p>
<p>6: if your tree node is/can be involved in a call to a solver, make sure
it&#8217;s translation o SMTLib is supported (solvers/Solver.scala)</p>
<div class="section" id="modifying-real-leon">
<h2>Modifying real-leon<a class="headerlink" href="#modifying-real-leon" title="Permalink to this headline"></a></h2>
<p>If you want to add a new function to be parsed, say &#8216;asin&#8217;,
then usually you will need to modify
frontends.scalac.ASTExtractors
frontends.scalac.CodeExtraction
purescala.Extractors</p>
<p>Try to search for a tree already present, such as &#8216;Sqrt&#8217;.</p>
<p>To test your modifications:
&gt; run &#8211;real library/annotation/package.scala library/daisy/Real.scala testcases/RealTest.scala</p>
</div>
<h1 id="index">Index</h1>
<div class="genindex-jumpbox">
</div>
</div>
</div>
</div>
<!--div class="sphinxsidebar" role="navigation" aria-label="main navigation">
<div class="sphinxsidebar" role="navigation" aria-label="main navigation">
<div class="sphinxsidebarwrapper">
<h3><a href="index.html">Table Of Contents</a></h3>
<ul>
<li><a class="reference internal" href="#">Trees</a><ul>
<li><a class="reference internal" href="#modifying-real-leon">Modifying real-leon</a></li>
</ul>
</li>
</ul>
<div class="relations">
<div class="relations">
<h3>Related Topics</h3>
<ul>
<li><a href="index.html">Documentation overview</a><ul>
</ul></li>
</ul>
</div>
<div role="note" aria-label="source link">
<h3>This Page</h3>
<ul class="this-page-menu">
<li><a href="_sources/trees.txt"
rel="nofollow">Show Source</a></li>
</ul>
</div>
<div id="searchbox" style="display: none" role="search">
<h3>Quick search</h3>
<form class="search" action="search.html" method="get">
......@@ -113,23 +74,20 @@ purescala.Extractors</p>
</div>
<script type="text/javascript">$('#searchbox').show(0);</script>
</div>
</div-->
</div>
<div class="clearer"></div>
</div>
<div class="footer">
&copy;2015, E. Darulova.
|
Powered by <a href="http://sphinx-doc.org/">Sphinx 1.3.1</a>
&amp; <a href="https://github.com/bitprophet/alabaster">Alabaster 0.7.6</a>
|
<a href="_sources/trees.txt"
rel="nofollow">Page source</a>
</div>
</body>
</html>
\ No newline at end of file
......@@ -5,12 +5,12 @@
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Welcome to Daisy’s documentation! &mdash; Daisy 0.0 documentation</title>
<link rel="stylesheet" href="_static/alabaster.css" type="text/css" />
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<script type="text/javascript">
var DOCUMENTATION_OPTIONS = {
URL_ROOT: './',
......@@ -26,18 +26,18 @@
<script type="text/javascript" src="https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
<link rel="top" title="Daisy 0.0 documentation" href="#" />
<link rel="next" title="Intro" href="intro.html" />
<meta name="viewport" content="width=device-width, initial-scale=0.9, maximum-scale=0.9">
</head>
<body role="document">
<body role="document">
<div class="document">
<div class="documentwrapper">
<div class="bodywrapper">
<div class="body" role="main">
<div class="section" id="welcome-to-daisy-s-documentation">
<h1>Welcome to Daisy&#8217;s documentation!<a class="headerlink" href="#welcome-to-daisy-s-documentation" title="Permalink to this headline"></a></h1>
<p>Contents:</p>
......@@ -76,7 +76,7 @@
</div>
</div>
</div>
<!--div class="sphinxsidebar" role="navigation" aria-label="main navigation">
<div class="sphinxsidebar" role="navigation" aria-label="main navigation">
<div class="sphinxsidebarwrapper"><div class="relations">
<h3>Related Topics</h3>
<ul>
......@@ -106,23 +106,23 @@
</div>
<script type="text/javascript">$('#searchbox').show(0);</script>
</div>
</div-->
</div>
<div class="clearer"></div>
</div>
<div class="footer">
&copy;2015, E. Darulova.
|
Powered by <a href="http://sphinx-doc.org/">Sphinx 1.3.1</a>
&amp; <a href="https://github.com/bitprophet/alabaster">Alabaster 0.7.6</a>
|
<a href="_sources/index.txt"
rel="nofollow">Page source</a>
</div>
</body>
</html>
\ No newline at end of file
......@@ -5,12 +5,12 @@
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Daisy Internals &mdash; Daisy 0.0 documentation</title>
<link rel="stylesheet" href="_static/alabaster.css" type="text/css" />
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<script type="text/javascript">
var DOCUMENTATION_OPTIONS = {
URL_ROOT: './',
......@@ -25,19 +25,20 @@
<script type="text/javascript" src="_static/doctools.js"></script>
<script type="text/javascript" src="https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
<link rel="top" title="Daisy 0.0 documentation" href="index.html" />
<link rel="next" title="Utilities" href="utils.html" />
<link rel="prev" title="Testing" href="testing.html" />
<meta name="viewport" content="width=device-width, initial-scale=0.9, maximum-scale=0.9">
</head>
<body role="document">
<body role="document">
<div class="document">
<div class="documentwrapper">
<div class="bodywrapper">
<div class="body" role="main">
<div class="section" id="daisy-internals">
<h1>Daisy Internals<a class="headerlink" href="#daisy-internals" title="Permalink to this headline"></a></h1>
<div class="section" id="intermediate-representation">
......@@ -62,7 +63,7 @@ the range of values at each intermediate node has to be known.)</p>
</div>
</div>
</div>
<!--div class="sphinxsidebar" role="navigation" aria-label="main navigation">
<div class="sphinxsidebar" role="navigation" aria-label="main navigation">
<div class="sphinxsidebarwrapper">
<h3><a href="index.html">Table Of Contents</a></h3>
<ul>
......@@ -76,6 +77,7 @@ the range of values at each intermediate node has to be known.)</p>
<ul>
<li><a href="index.html">Documentation overview</a><ul>
<li>Previous: <a href="testing.html" title="previous chapter">Testing</a></li>
<li>Next: <a href="utils.html" title="next chapter">Utilities</a></li>
</ul></li>
</ul>
</div>
......@@ -100,23 +102,23 @@ the range of values at each intermediate node has to be known.)</p>
</div>
<script type="text/javascript">$('#searchbox').show(0);</script>
</div>
</div-->
</div>
<div class="clearer"></div>
</div>
<div class="footer">
&copy;2015, E. Darulova.
|
Powered by <a href="http://sphinx-doc.org/">Sphinx 1.3.1</a>
&amp; <a href="https://github.com/bitprophet/alabaster">Alabaster 0.7.6</a>
|
<a href="_sources/internals.txt"
rel="nofollow">Page source</a>
</div>
</body>
</html>
\ No newline at end of file
......@@ -5,12 +5,12 @@
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Intro &mdash; Daisy 0.0 documentation</title>
<link rel="stylesheet" href="_static/alabaster.css" type="text/css" />
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<script type="text/javascript">
var DOCUMENTATION_OPTIONS = {
URL_ROOT: './',
......@@ -27,18 +27,18 @@
<link rel="top" title="Daisy 0.0 documentation" href="index.html" />
<link rel="next" title="Navigating the Repository" href="repo_navigation.html" />
<link rel="prev" title="Welcome to Daisy’s documentation!" href="index.html" />
<meta name="viewport" content="width=device-width, initial-scale=0.9, maximum-scale=0.9">
</head>
<body role="document">
<body role="document">
<div class="document">
<div class="documentwrapper">
<div class="bodywrapper">
<div class="body" role="main">
<div class="section" id="intro">
<h1>Intro<a class="headerlink" href="#intro" title="Permalink to this headline"></a></h1>
<p>Daisy is (or will be) a framework for verifying, approximating and
......@@ -103,7 +103,7 @@ for modularity&#8217;s sake. Currently, working phases are</p>
</div>
</div>
</div>
<!--div class="sphinxsidebar" role="navigation" aria-label="main navigation">
<div class="sphinxsidebar" role="navigation" aria-label="main navigation">
<div class="sphinxsidebarwrapper">
<h3><a href="index.html">Table Of Contents</a></h3>
<ul>
......@@ -144,23 +144,23 @@ for modularity&#8217;s sake. Currently, working phases are</p>
</div>
<script type="text/javascript">$('#searchbox').show(0);</script>
</div>
</div-->
</div>
<div class="clearer"></div>
</div>
<div class="footer">
&copy;2015, E. Darulova.
|
Powered by <a href="http://sphinx-doc.org/">Sphinx 1.3.1</a>
&amp; <a href="https://github.com/bitprophet/alabaster">Alabaster 0.7.6</a>
|
<a href="_sources/intro.txt"
rel="nofollow">Page source</a>
</div>
</body>
</html>
\ No newline at end of file
File added
......@@ -5,12 +5,12 @@
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Navigating the Repository &mdash; Daisy 0.0 documentation</title>
<link rel="stylesheet" href="_static/alabaster.css" type="text/css" />
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<script type="text/javascript">
var DOCUMENTATION_OPTIONS = {
URL_ROOT: './',
......@@ -27,18 +27,18 @@
<link rel="top" title="Daisy 0.0 documentation" href="index.html" />
<link rel="next" title="Contributing" href="contributing.html" />
<link rel="prev" title="Intro" href="intro.html" />
<meta name="viewport" content="width=device-width, initial-scale=0.9, maximum-scale=0.9">
</head>
<body role="document">
<body role="document">
<div class="document">
<div class="documentwrapper">
<div class="bodywrapper">
<div class="body" role="main">
<div class="section" id="navigating-the-repository">
<span id="repo-navigation"></span><h1>Navigating the Repository<a class="headerlink" href="#navigating-the-repository" title="Permalink to this headline"></a></h1>
<p>Some of these are rather empty for now; the most interesting folders for
......@@ -64,7 +64,7 @@ in rawdata/ are not persistent.</p>
</div>
</div>
</div>
<!--div class="sphinxsidebar" role="navigation" aria-label="main navigation">
<div class="sphinxsidebar" role="navigation" aria-label="main navigation">
<div class="sphinxsidebarwrapper"><div class="relations">
<h3>Related Topics</h3>
<ul>
......@@ -95,23 +95,23 @@ in rawdata/ are not persistent.</p>
</div>
<script type="text/javascript">$('#searchbox').show(0);</script>
</div>
</div-->
</div>
<div class="clearer"></div>
</div>
<div class="footer">
&copy;2015, E. Darulova.
|
Powered by <a href="http://sphinx-doc.org/">Sphinx 1.3.1</a>
&amp; <a href="https://github.com/bitprophet/alabaster">Alabaster 0.7.6</a>
|
<a href="_sources/repo_navigation.txt"
rel="nofollow">Page source</a>
</div>
</body>
</html>
\ No newline at end of file
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Search &mdash; Daisy 0.0 documentation</title>
<link rel="stylesheet" href="_static/alabaster.css" type="text/css" />
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
<script type="text/javascript">
var DOCUMENTATION_OPTIONS = {
URL_ROOT: './',
VERSION: '0.0',
COLLAPSE_INDEX: false,
FILE_SUFFIX: '.html',
HAS_SOURCE: true
};
</script>
<script type="text/javascript" src="_static/jquery.js"></script>
<script type="text/javascript" src="_static/underscore.js"></script>
<script type="text/javascript" src="_static/doctools.js"></script>
<script type="text/javascript" src="https://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML"></script>
<script type="text/javascript" src="_static/searchtools.js"></script>
<link rel="top" title="Daisy 0.0 documentation" href="index.html" />
<script type="text/javascript">
jQuery(function() { Search.loadIndex("searchindex.js"); });
</script>
<script type="text/javascript" id="searchindexloader"></script>
<meta name="viewport" content="width=device-width, initial-scale=0.9, maximum-scale=0.9">
</head>
<body role="document">
<div class="document">
<div class="documentwrapper">
<div class="bodywrapper">
<div class="body" role="main">
<h1 id="search-documentation">Search</h1>
<div id="fallback" class="admonition warning">
<script type="text/javascript">$('#fallback').hide();</script>
<p>
Please activate JavaScript to enable the search
functionality.
</p>
</div>
<p>
From here you can search these documents. Enter your search
words into the box below and click "search". Note that the search
function will automatically search for all of the words. Pages
containing fewer words won't appear in the result list.
</p>
<form action="" method="get">
<input type="text" name="q" value="" />
<input type="submit" value="search" />
<span id="search-progress" style="padding-left: 10px"></span>
</form>
<div id="search-results">
</div>
</div>
</div>
</div>
<div class="sphinxsidebar" role="navigation" aria-label="main navigation">
<div class="sphinxsidebarwrapper"><div class="relations">
<h3>Related Topics</h3>
<ul>
<li><a href="index.html">Documentation overview</a><ul>
</ul></li>
</ul>
</div>
</div>
</div>
<div class="clearer"></div>
</div>
<div class="footer">
&copy;2015, E. Darulova.
|
Powered by <a href="http://sphinx-doc.org/">Sphinx 1.3.1</a>