Skip to content
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.

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

Single constant propagation only #64

Open
wants to merge 22 commits into
base: master
Choose a base branch
from
12 changes: 10 additions & 2 deletions .travis.yml
Original file line number Diff line number Diff line change
@@ -1,5 +1,13 @@
sudo: required

language: java

services:
- docker

before_install:
- docker build -t francois .

script:
- ant;
- ant test;
- docker run francois sh -c "ant; ant test;"

2 changes: 1 addition & 1 deletion Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ RUN apt install patchelf -y
RUN apt install libgomp1

# Clone down the GreenSolver repository
RUN git clone https://github.com/wvisser/green
RUN git clone https://github.com/FrancoisVGit/green

# Download and extract Z3
RUN mkdir z3
Expand Down
3 changes: 2 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
[![Build Status](https://travis-ci.org/wvisser/green.svg?branch=master)](https://travis-ci.org/wvisser/green.svg?branch=master)
[![Build
Status](https://travis-ci.org/FrancoisVGit/green.svg?branch=master)](https://travis-ci.org/FrancoisVGit/green?branch=master)

Notes:

Expand Down
17 changes: 17 additions & 0 deletions bin/build.properties
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
# Build properties for green.
#
# It is OK to to change these properties if they do not agree with your
# setup, but do not commit it to the repository.

#target = 1.7
#source = 1.7
#bootpath = /Library/Java/JavaVirtualMachines/jdk1.7.0_75.jdk/Contents/Home/jre/lib/rt.jar

target = 1.8
source = 1.8
bootpath = /Library/Java/JavaVirtualMachines/jdk1.8.0_45.jdk/Contents/Home/jre/lib/rt.jar

cvc3lib = /Users/jaco/Documents/RESEARCH/SYMEXE/cvc3-2.4.1/java/lib
lattepath = /Users/jaco/Documents/RESEARCH/latte-integrale-1.7.3/latte-int-1.7.3/code/latte/count
z3path = /Users/jaco/Documents/RESEARCH/SYMEXE/Z3/build/z3
z3lib = ${basedir}/lib
2 changes: 2 additions & 0 deletions bin/junit/TESTS-TestSuites.xml
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
<?xml version="1.0" encoding="UTF-8" ?>
<testsuites />
22 changes: 22 additions & 0 deletions bin/junit/all-tests.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
<html xmlns:string="xalan://java.lang.String" xmlns:lxslt="http://xml.apache.org/xslt">
<head>
<META http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title>Unit Test Results: All Tests</title>
<link rel="stylesheet" type="text/css" title="Style" href="stylesheet.css">
</head>
<body onload="open('allclasses-frame.html','classListFrame')">
<h1>Unit Test Results.</h1>
<table width="100%">
<tr>
<td align="left"></td><td align="right">Designed for use with <a href="http://www.junit.org/">JUnit</a> and <a href="http://ant.apache.org/">Ant</a>.</td>
</tr>
</table>
<hr size="1">
<h2>All Tests</h2>
<table class="details" border="0" cellpadding="5" cellspacing="2" width="95%">
<tr valign="top">
<th>Class</th><th>Name</th><th>Status</th><th width="80%">Type</th><th nowrap>Time(s)</th>
</tr>
</table>
</body>
</html>
11 changes: 11 additions & 0 deletions bin/junit/allclasses-frame.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
<html xmlns:string="xalan://java.lang.String" xmlns:lxslt="http://xml.apache.org/xslt">
<head>
<META http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title>All Unit Test Classes</title>
<link rel="stylesheet" type="text/css" title="Style" href="stylesheet.css">
</head>
<body>
<h2>Classes</h2>
<table width="100%"></table>
</body>
</html>
22 changes: 22 additions & 0 deletions bin/junit/alltests-errors.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
<html xmlns:string="xalan://java.lang.String" xmlns:lxslt="http://xml.apache.org/xslt">
<head>
<META http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title>Unit Test Results: All Errors</title>
<link rel="stylesheet" type="text/css" title="Style" href="stylesheet.css">
</head>
<body onload="open('allclasses-frame.html','classListFrame')">
<h1>Unit Test Results.</h1>
<table width="100%">
<tr>
<td align="left"></td><td align="right">Designed for use with <a href="http://www.junit.org/">JUnit</a> and <a href="http://ant.apache.org/">Ant</a>.</td>
</tr>
</table>
<hr size="1">
<h2>All Errors</h2>
<table class="details" border="0" cellpadding="5" cellspacing="2" width="95%">
<tr valign="top">
<th>Class</th><th>Name</th><th>Status</th><th width="80%">Type</th><th nowrap>Time(s)</th>
</tr>
</table>
</body>
</html>
22 changes: 22 additions & 0 deletions bin/junit/alltests-fails.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
<html xmlns:string="xalan://java.lang.String" xmlns:lxslt="http://xml.apache.org/xslt">
<head>
<META http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title>Unit Test Results: All Failures</title>
<link rel="stylesheet" type="text/css" title="Style" href="stylesheet.css">
</head>
<body onload="open('allclasses-frame.html','classListFrame')">
<h1>Unit Test Results.</h1>
<table width="100%">
<tr>
<td align="left"></td><td align="right">Designed for use with <a href="http://www.junit.org/">JUnit</a> and <a href="http://ant.apache.org/">Ant</a>.</td>
</tr>
</table>
<hr size="1">
<h2>All Failures</h2>
<table class="details" border="0" cellpadding="5" cellspacing="2" width="95%">
<tr valign="top">
<th>Class</th><th>Name</th><th>Status</th><th width="80%">Type</th><th nowrap>Time(s)</th>
</tr>
</table>
</body>
</html>
22 changes: 22 additions & 0 deletions bin/junit/alltests-skipped.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
<html xmlns:string="xalan://java.lang.String" xmlns:lxslt="http://xml.apache.org/xslt">
<head>
<META http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title>Unit Test Results: All Skipped</title>
<link rel="stylesheet" type="text/css" title="Style" href="stylesheet.css">
</head>
<body onload="open('allclasses-frame.html','classListFrame')">
<h1>Unit Test Results.</h1>
<table width="100%">
<tr>
<td align="left"></td><td align="right">Designed for use with <a href="http://www.junit.org/">JUnit</a> and <a href="http://ant.apache.org/">Ant</a>.</td>
</tr>
</table>
<hr size="1">
<h2>All Skipped</h2>
<table class="details" border="0" cellpadding="5" cellspacing="2" width="95%">
<tr valign="top">
<th>Class</th><th>Name</th><th>Status</th><th width="80%">Type</th><th nowrap>Time(s)</th>
</tr>
</table>
</body>
</html>
19 changes: 19 additions & 0 deletions bin/junit/index.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
<html xmlns:string="xalan://java.lang.String" xmlns:lxslt="http://xml.apache.org/xslt">
<head>
<META http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title>Unit Test Results.</title>
</head>
<frameset cols="20%,80%">
<frameset rows="30%,70%">
<frame src="overview-frame.html" name="packageListFrame">
<frame src="allclasses-frame.html" name="classListFrame">
</frameset>
<frame src="overview-summary.html" name="classFrame">
<noframes>
<h2>Frame Alert</h2>
<p>
This document is designed to be viewed using the frames feature. If you see this message, you are using a non-frame-capable web client.
</p>
</noframes>
</frameset>
</html>
14 changes: 14 additions & 0 deletions bin/junit/overview-frame.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
<html xmlns:string="xalan://java.lang.String" xmlns:lxslt="http://xml.apache.org/xslt">
<head>
<META http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title>All Unit Test Packages</title>
<link rel="stylesheet" type="text/css" title="Style" href="stylesheet.css">
</head>
<body>
<h2>
<a href="overview-summary.html" target="classFrame">Home</a>
</h2>
<h2>Packages</h2>
<table width="100%"></table>
</body>
</html>
38 changes: 38 additions & 0 deletions bin/junit/overview-summary.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
<html xmlns:string="xalan://java.lang.String" xmlns:lxslt="http://xml.apache.org/xslt">
<head>
<META http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title>Unit Test Results: Summary</title>
<link rel="stylesheet" type="text/css" title="Style" href="stylesheet.css">
</head>
<body onload="open('allclasses-frame.html','classListFrame')">
<h1>Unit Test Results.</h1>
<table width="100%">
<tr>
<td align="left"></td><td align="right">Designed for use with <a href="http://www.junit.org/">JUnit</a> and <a href="http://ant.apache.org/">Ant</a>.</td>
</tr>
</table>
<hr size="1">
<h2>Summary</h2>
<table class="details" border="0" cellpadding="5" cellspacing="2" width="95%">
<tr valign="top">
<th>Tests</th><th>Failures</th><th>Errors</th><th>Skipped</th><th>Success rate</th><th>Time</th>
</tr>
<tr valign="top" class="Pass">
<td><a title="Display all tests" href="all-tests.html">0</a></td><td><a title="Display all failures" href="alltests-fails.html">0</a></td><td><a title="Display all errors" href="alltests-errors.html">0</a></td><td><a title="Display all skipped test" href="alltests-skipped.html">0</a></td><td>NaN</td><td>0.000</td>
</tr>
</table>
<table border="0" width="95%">
<tr>
<td style="text-align: justify;">
Note: <em>failures</em> are anticipated and checked for with assertions while <em>errors</em> are unanticipated.
</td>
</tr>
</table>
<h2>Packages</h2>
<table class="details" border="0" cellpadding="5" cellspacing="2" width="95%">
<tr valign="top">
<th width="80%">Name</th><th>Tests</th><th>Errors</th><th>Failures</th><th>Skipped</th><th nowrap>Time(s)</th><th nowrap>Time Stamp</th><th>Host</th>
</tr>
</table>
</body>
</html>
48 changes: 48 additions & 0 deletions bin/junit/stylesheet.css
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@

body {
font:normal 68% verdana,arial,helvetica;
color:#000000;
}
table tr td, table tr th {
font-size: 68%;
}
table.details tr th{
font-weight: bold;
text-align:left;
background:#a6caf0;
}
table.details tr td{
background:#eeeee0;
}

p {
line-height:1.5em;
margin-top:0.5em; margin-bottom:1.0em;
}
h1 {
margin: 0px 0px 5px; font: 165% verdana,arial,helvetica
}
h2 {
margin-top: 1em; margin-bottom: 0.5em; font: bold 125% verdana,arial,helvetica
}
h3 {
margin-bottom: 0.5em; font: bold 115% verdana,arial,helvetica
}
h4 {
margin-bottom: 0.5em; font: bold 100% verdana,arial,helvetica
}
h5 {
margin-bottom: 0.5em; font: bold 100% verdana,arial,helvetica
}
h6 {
margin-bottom: 0.5em; font: bold 100% verdana,arial,helvetica
}
.Error {
font-weight:bold; color:red;
}
.Failure {
font-weight:bold; color:purple;
}
.Properties {
text-align:right;
}
Binary file added bin/za/ac/sun/cs/green/EntireSuite.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/Green$1.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/Green.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/Instance.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/Service.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/Constant.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/Expression.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/IntConstant.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/IntVariable.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/Operation$1$1.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/Operation$1.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/Operation$2.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/Operation$Fix.class
Binary file not shown.
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/Operation.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/RealConstant.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/RealVariable.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/StringConstant.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/StringVariable.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/Variable.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/Visitor.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/expr/VisitorException.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/log/GreenFormatter.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/log/GreenHandler.class
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/parser/klee/Parser$1.class
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/parser/klee/Parser.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/parser/klee/Scanner.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/parser/klee/Token.class
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/service/CountService.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/service/ModelService.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/service/SATService.class
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/service/z3/SATZ3Test.class
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/store/BasicStore.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/store/NullStore.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/store/Store.class
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/taskmanager/TaskManager.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/util/Base64.class
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/util/Configuration.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/util/DummyTaskManager.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/util/Misc.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/util/NullLogger.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/util/ParallelSATTest.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/util/Reporter.class
Binary file not shown.
Binary file added bin/za/ac/sun/cs/green/util/SetServiceTest.class
Binary file not shown.
Binary file not shown.
5 changes: 3 additions & 2 deletions build.xml
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@
<pathelement location="test"/>
</path>
<property name="green.srcpath" refid="green.srcpath"/>
<property name="reports.dir" value="reports" />

<!--
Initialization
Expand Down Expand Up @@ -95,8 +96,8 @@
<target name="test">
<echo message="java.library.path = ${z3lib};${cvc3lib}"/>
<mkdir dir="${junit.dir}"/>
<junit fork="yes" printsummary="withOutAndErr" haltonfailure = "yes">
<formatter type="xml"/>
<junit fork="yes" printsummary="yes" haltonfailure = "no" failureproperty="junit.failed">
<formatter type="plain" usefile="no"/>
<test name="za.ac.sun.cs.green.EntireSuite" todir="${junit.dir}"/>
<env key="DYLD_LIBRARY_PATH" value="lib"/>
<env key="LD_LIBRARY_PATH" value="lib"/>
Expand Down
Loading