-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
- Loading branch information
There are no files selected for viewing
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Large diffs are not rendered by default.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,44 @@ | ||
|
||
|
||
<!DOCTYPE html> | ||
<html lang="en" data-theme="light"> | ||
<head> | ||
<meta charset="UTF-8"> | ||
<meta http-equiv="X-UA-Compatible" content="IE=edge"> | ||
<meta name="viewport" content="width=1024px, initial-scale=1.0"> | ||
<title>#3172 - Translation of bitwise operators</title> | ||
<link rel="stylesheet" href="https://unpkg.com/@picocss/pico@1.*/css/pico.min.css"> | ||
<link rel="stylesheet" href="/artiweb/css/style.css"> | ||
<script type="application/javascript" src="/artiweb/js/main.js"></script> | ||
|
||
|
||
</head> | ||
<body> | ||
<main class="container"> | ||
|
||
<section> | ||
<a href="/artiweb/">Artiweb</a> > <a href="/artiweb/3172">Pull Request #3172</a> > <span>Artifact 752027048</span> | ||
<h1>Translation of bitwise operators <span class="color-muted">#3172</span></h1> | ||
<span>Build time: 15. Jun 2023 13:42</span><br> | ||
<a href="https://github.com/KeYProject/key/actions/runs/5278621906">Github Action</a><br> | ||
</section> | ||
|
||
<section> | ||
<h3>Tests</h3> | ||
<ul><li>✅ <a href="key.core.testgen/build/reports/tests/test">key.core.testgen:test</a> (13 succeeded) | ||
</li><li>✅ key.core:rap [no report files] (1041 succeeded) | ||
</li><li>❌ <a href="key.core/build/reports/tests/test">key.core:test</a> (2948 succeeded, 2 failed, 106 skipped) | ||
</li><li>✅ <a href="key.core/build/reports/tests/testProveRules">key.core:testProveRules</a> (198 succeeded) | ||
</li><li>✅ <a href="key.core/build/reports/tests/testRunAllFunProofs">key.core:testRunAllFunProofs</a> (34 succeeded) | ||
</li><li>✅ <a href="key.core/build/reports/tests/testRunAllInfProofs">key.core:testRunAllInfProofs</a> (29 succeeded) | ||
</li><li>✅ <a href="key.removegenerics/build/reports/tests/test">key.removegenerics:test</a> (45 succeeded) | ||
</li><li>✅ <a href="key.ui/build/reports/tests/test">key.ui:test</a> (5 succeeded) | ||
</li><li>✅ <a href="key.util/build/reports/tests/test">key.util:test</a> (132 succeeded) | ||
</li><li>✅ <a href="keyext.exploration/build/reports/tests/test">keyext.exploration:test</a> (3 succeeded) | ||
</li><li>✅ <a href="keyext.slicing/build/reports/tests/test">keyext.slicing:test</a> (12 succeeded) | ||
</li><li>✅ <a href="recoder/build/reports/tests/test">recoder:test</a> (14 succeeded, 15 skipped) | ||
</li></ul> | ||
</section> | ||
</main> | ||
</body> | ||
</html> |
Large diffs are not rendered by default.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,188 @@ | ||
<!DOCTYPE html> | ||
<html> | ||
<head> | ||
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/> | ||
<meta http-equiv="x-ua-compatible" content="IE=edge"/> | ||
<title>Test results - TestCE</title> | ||
<link href="../css/base-style.css" rel="stylesheet" type="text/css"/> | ||
<link href="../css/style.css" rel="stylesheet" type="text/css"/> | ||
<script src="../js/report.js" type="text/javascript"></script> | ||
</head> | ||
<body> | ||
<div id="content"> | ||
<h1>TestCE</h1> | ||
<div class="breadcrumbs"> | ||
<a href="../index.html">all</a> > | ||
<a href="../packages/de.uka.ilkd.key.testcase.smt.ce.html">de.uka.ilkd.key.testcase.smt.ce</a> > TestCE</div> | ||
<div id="summary"> | ||
<table> | ||
<tr> | ||
<td> | ||
<div class="summaryGroup"> | ||
<table> | ||
<tr> | ||
<td> | ||
<div class="infoBox" id="tests"> | ||
<div class="counter">12</div> | ||
<p>tests</p> | ||
</div> | ||
</td> | ||
<td> | ||
<div class="infoBox" id="failures"> | ||
<div class="counter">0</div> | ||
<p>failures</p> | ||
</div> | ||
</td> | ||
<td> | ||
<div class="infoBox" id="ignored"> | ||
<div class="counter">0</div> | ||
<p>ignored</p> | ||
</div> | ||
</td> | ||
<td> | ||
<div class="infoBox" id="duration"> | ||
<div class="counter">27.298s</div> | ||
<p>duration</p> | ||
</div> | ||
</td> | ||
</tr> | ||
</table> | ||
</div> | ||
</td> | ||
<td> | ||
<div class="infoBox success" id="successRate"> | ||
<div class="percent">100%</div> | ||
<p>successful</p> | ||
</div> | ||
</td> | ||
</tr> | ||
</table> | ||
</div> | ||
<div id="tabs"> | ||
<ul class="tabLinks"> | ||
<li> | ||
<a href="#tab0">Tests</a> | ||
</li> | ||
<li> | ||
<a href="#tab1">Standard output</a> | ||
</li> | ||
</ul> | ||
<div id="tab0" class="tab"> | ||
<h2>Tests</h2> | ||
<table> | ||
<thead> | ||
<tr> | ||
<th>Test</th> | ||
<th>Duration</th> | ||
<th>Result</th> | ||
</tr> | ||
</thead> | ||
<tr> | ||
<td class="success">testMiddle()</td> | ||
<td class="success">25.177s</td> | ||
<td class="success">passed</td> | ||
</tr> | ||
<tr> | ||
<td class="success">testOverFlow1()</td> | ||
<td class="success">1.767s</td> | ||
<td class="success">passed</td> | ||
</tr> | ||
<tr> | ||
<td class="success">testOverFlow2()</td> | ||
<td class="success">0.002s</td> | ||
<td class="success">passed</td> | ||
</tr> | ||
<tr> | ||
<td class="success">testTypes1()</td> | ||
<td class="success">0.002s</td> | ||
<td class="success">passed</td> | ||
</tr> | ||
<tr> | ||
<td class="success">testTypes2()</td> | ||
<td class="success">0.002s</td> | ||
<td class="success">passed</td> | ||
</tr> | ||
<tr> | ||
<td class="success">testTypes3()</td> | ||
<td class="success">0.004s</td> | ||
<td class="success">passed</td> | ||
</tr> | ||
<tr> | ||
<td class="success">testTypes4()</td> | ||
<td class="success">0.004s</td> | ||
<td class="success">passed</td> | ||
</tr> | ||
<tr> | ||
<td class="success">testTypes5()</td> | ||
<td class="success">0.001s</td> | ||
<td class="success">passed</td> | ||
</tr> | ||
<tr> | ||
<td class="success">testTypes6()</td> | ||
<td class="success">0.002s</td> | ||
<td class="success">passed</td> | ||
</tr> | ||
<tr> | ||
<td class="success">testTypes7()</td> | ||
<td class="success">0.004s</td> | ||
<td class="success">passed</td> | ||
</tr> | ||
<tr> | ||
<td class="success">testTypes8()</td> | ||
<td class="success">0.331s</td> | ||
<td class="success">passed</td> | ||
</tr> | ||
<tr> | ||
<td class="success">testTypes9()</td> | ||
<td class="success">0.002s</td> | ||
<td class="success">passed</td> | ||
</tr> | ||
</table> | ||
</div> | ||
<div id="tab1" class="tab"> | ||
<h2>Standard output</h2> | ||
<span class="code"> | ||
<pre>12:46:32,895 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.7 | ||
12:46:32,942 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml] | ||
12:46:32,958 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/D:/a/key/key/key.core.testgen/build/resources/test/logback.xml] | ||
12:46:33,223 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT] | ||
12:46:33,223 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender] | ||
12:46:33,239 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender] | ||
12:46:33,239 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender] | ||
12:46:33,255 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property | ||
12:46:33,335 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to DEBUG | ||
12:46:33,335 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT] | ||
12:46:33,335 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@62dbe64e - End of configuration. | ||
12:46:33,350 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@6cff61fc - Registering current configuration as safe fallback point | ||
|
||
2832 WARN Test worker d.u.i.k.t.s.c.TestCE Warning: Z3_CE is not installed, tests skipped. | ||
2832 WARN Test worker d.u.i.k.t.s.c.TestCE Maybe use JVM system property "z3SolverPath" to define the path to the Z3 command. | ||
3223 WARN Test worker d.u.i.k.s.ProofIndependentSettings The settings in C:\Users\runneradmin\.key\proofIndependentSettings.props are *not* read due to flag 'key.disregardSettings' | ||
3254 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\smt\ce\middle.key | ||
3316 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 13.65ms | ||
4355 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config | ||
4429 WARN Test worker d.u.i.k.s.ProofSettings The settings in C:\Users\runneradmin\.key\proof-settings.props are *not* read. | ||
7154 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta | ||
7154 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta | ||
7154 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta | ||
7170 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for Meta | ||
11254 DEBUG Test worker d.u.i.k.j.TypeConverter No LDT found for JavaBigintExpression | ||
22793 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 18.44s | ||
23142 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Middle[Middle::middle(int,int,int)].JML normal_behavior operation contract.0 | ||
23314 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 83.9ns | ||
</pre> | ||
</span> | ||
</div> | ||
</div> | ||
<div id="footer"> | ||
<p> | ||
<div> | ||
<label class="hidden" id="label-for-line-wrapping-toggle" for="line-wrapping-toggle">Wrap lines | ||
<input id="line-wrapping-toggle" type="checkbox" autocomplete="off"/> | ||
</label> | ||
</div>Generated by | ||
<a href="http://www.gradle.org">Gradle 8.1.1</a> at Jun 15, 2023, 12:47:09 PM</p> | ||
</div> | ||
</div> | ||
</body> | ||
</html> |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,113 @@ | ||
<!DOCTYPE html> | ||
<html> | ||
<head> | ||
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/> | ||
<meta http-equiv="x-ua-compatible" content="IE=edge"/> | ||
<title>Test results - TestTestgen</title> | ||
<link href="../css/base-style.css" rel="stylesheet" type="text/css"/> | ||
<link href="../css/style.css" rel="stylesheet" type="text/css"/> | ||
<script src="../js/report.js" type="text/javascript"></script> | ||
</head> | ||
<body> | ||
<div id="content"> | ||
<h1>TestTestgen</h1> | ||
<div class="breadcrumbs"> | ||
<a href="../index.html">all</a> > | ||
<a href="../packages/de.uka.ilkd.key.testcase.smt.testgen.html">de.uka.ilkd.key.testcase.smt.testgen</a> > TestTestgen</div> | ||
<div id="summary"> | ||
<table> | ||
<tr> | ||
<td> | ||
<div class="summaryGroup"> | ||
<table> | ||
<tr> | ||
<td> | ||
<div class="infoBox" id="tests"> | ||
<div class="counter">1</div> | ||
<p>tests</p> | ||
</div> | ||
</td> | ||
<td> | ||
<div class="infoBox" id="failures"> | ||
<div class="counter">0</div> | ||
<p>failures</p> | ||
</div> | ||
</td> | ||
<td> | ||
<div class="infoBox" id="ignored"> | ||
<div class="counter">0</div> | ||
<p>ignored</p> | ||
</div> | ||
</td> | ||
<td> | ||
<div class="infoBox" id="duration"> | ||
<div class="counter">7.626s</div> | ||
<p>duration</p> | ||
</div> | ||
</td> | ||
</tr> | ||
</table> | ||
</div> | ||
</td> | ||
<td> | ||
<div class="infoBox success" id="successRate"> | ||
<div class="percent">100%</div> | ||
<p>successful</p> | ||
</div> | ||
</td> | ||
</tr> | ||
</table> | ||
</div> | ||
<div id="tabs"> | ||
<ul class="tabLinks"> | ||
<li> | ||
<a href="#tab0">Tests</a> | ||
</li> | ||
<li> | ||
<a href="#tab1">Standard output</a> | ||
</li> | ||
</ul> | ||
<div id="tab0" class="tab"> | ||
<h2>Tests</h2> | ||
<table> | ||
<thead> | ||
<tr> | ||
<th>Test</th> | ||
<th>Duration</th> | ||
<th>Result</th> | ||
</tr> | ||
</thead> | ||
<tr> | ||
<td class="success">testMiddle()</td> | ||
<td class="success">7.626s</td> | ||
<td class="success">passed</td> | ||
</tr> | ||
</table> | ||
</div> | ||
<div id="tab1" class="tab"> | ||
<h2>Standard output</h2> | ||
<span class="code"> | ||
<pre>28441 WARN Test worker d.u.i.k.t.s.t.TestTestgen Warning: Z3_CE is not installed, tests skipped. | ||
28441 WARN Test worker d.u.i.k.t.s.t.TestTestgen Maybe use JVM system property "z3SolverPath" to define the path to the Z3 command. | ||
28441 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\smt\tg\middle.key | ||
28441 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 740.8ns | ||
28457 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config | ||
35058 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 6.61s | ||
35199 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof Middle[Middle::middle(int,int,int)].JML normal_behavior operation contract.0 | ||
35199 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 25.3ns | ||
</pre> | ||
</span> | ||
</div> | ||
</div> | ||
<div id="footer"> | ||
<p> | ||
<div> | ||
<label class="hidden" id="label-for-line-wrapping-toggle" for="line-wrapping-toggle">Wrap lines | ||
<input id="line-wrapping-toggle" type="checkbox" autocomplete="off"/> | ||
</label> | ||
</div>Generated by | ||
<a href="http://www.gradle.org">Gradle 8.1.1</a> at Jun 15, 2023, 12:47:09 PM</p> | ||
</div> | ||
</div> | ||
</body> | ||
</html> |