USI & SUPSI Source Code Management (SCM): Issueshttps://scm.ti-edu.ch/https://scm.ti-edu.ch/favicon.ico?15601711372019-10-06T22:15:21ZUSI & SUPSI Source Code Management (SCM)
Redmine hifrog - Bug #13577 (New): prop incorrect resulthttps://scm.ti-edu.ch/issues/135772019-10-06T22:15:21ZSepideh Asadisepideh.a65@gmail.com
<p>Benchmark: ex21-upg2.c (attached)</p>
<p>How to run:<br />./hifrog --logic prop ex21-upg2.</p>
<p>Error:<br />reported as Successful but I think a= 1 and b=1 is a CEX. Surprisingly CBMC also agrees as Successful!</p> hifrog - Bug #13356 (Resolved): Bug in Hifrog LRA encoding - resulting assertion violation for a ...https://scm.ti-edu.ch/issues/133562019-09-26T11:54:36ZSepideh Asadisepideh.a65@gmail.com
<p><strong>Benchmark</strong>: ex13-change-orig.c (attached)</p>
<p><strong>How to run:</strong><br />./hifrog --logic qflra ex13-change-orig.c</p>
<p><strong>Error:</strong><br />LRA reports the bench as unsafe, while prop reports it as safe. The result of dump-query is SAT in OpenSMT and Z3, so the bug is in the encoding.</p> OpenSMT 2 - Bug #10647 (New): UF benchmark crashhttps://scm.ti-edu.ch/issues/106472019-04-11T09:18:00ZMartin Blichablicha@d3s.mff.cuni.czhifrog - Bug #7805 (New): UFInterpolator.Chttps://scm.ti-edu.ch/issues/78052018-08-29T11:04:47ZSepideh Asadisepideh.a65@gmail.com
<p><strong>File</strong>: sumth60.c (attached)</p>
<p><strong>How to run:</strong><br />--logic qfuf --claim 2</p>
<p><strong>Error message:</strong><br />RESULT: UNSAT - it holds!<br />Start generating interpolants...<br />Assertion failed: (!sorted_edges.empty( ) || tmp.back( )->target == x), function getSortedEdges, file /Users/sepidehasadi/2phd/dev/opensmt2/src/tsolvers/egraph/UFInterpolator.C, line 2451.</p> hifrog - Bug #7795 (New): Type constraints option for LA theorieshttps://scm.ti-edu.ch/issues/77952018-08-29T08:08:26ZKarine Even Mendozakarine.even_mendoza@kcl.ac.uk
<p>Following Grigory answer, this code is a test for the assertion ordering than for the type constraints: assuming a >= 0 and b >= 0 we can easily derive that c >= 0.</p>
<p>The original code, suppose to run with type_constraints 1 and results in UNSAT. We can run the loop till 10 (no need for so many iterations). To prove claim 1 and 2 we need type-constraints 1, and using claim 1+2 we can prove claim 3 (I think via claims-opt option).</p>
<p>Older version of type-constraints use to work well. I think not all the added type-constraints are in the end added to the SMT query (can be the remove of incrementality).</p>
<p>=========================<br />The code:</p>
<pre>
int sum ()
{
int s=0;
unsigned n;
for (int i = 0; i <10; i++)
{
n = nondetUInt();
s=s+n;
}
return s;
}
int main()
{
int a,b,c;
a=sum();
assert(a>=0);
b=sum();
assert(b>=0);
c=a+b;
assert(c>=0);
}
</pre><br />Please add this test in the end to the regression test with reference to TACAS17 paper. hifrog - Bug #7760 (New): Infinite loop in theory refinementhttps://scm.ti-edu.ch/issues/77602018-08-24T14:05:23ZMartin Blichablicha@d3s.mff.cuni.cz
<p>In current version (e.g. f4aaed49) there is bug in theory refinement algorithm. In cases 6 and 7 there is an infinite loop.<br />The variable in the condition (last) is not modified inside the loop.</p>
<p>case 7 :<br /> // backward with multiple refinement & dependencies<br /> last = exprs.size()-1;
{<br /> while (last >= 0){<br /> smtcheck_opensmt2t_cuf decider2(bw,<br /> options.get_unsigned_int_option("type-byte-constraints"),<br /> "backward with multiple refinement & dependencies" <br /> );<br /> decider2.check_ce(exprs, model, refined, weak, last, -1, -1, 1);<br /> }<br /> }<br /> break;</p> hifrog - Bug #7414 (In Progress): seg fault in reading non-linear elf summary in lra - sum-theorefhttps://scm.ti-edu.ch/issues/74142018-05-24T12:40:01ZSepideh Asadisepideh.a65@gmail.com
<p>How to run: ./hifrog --sum-theoref sumth73.c (c file in attachement)</p>
<p>Error msg:<br />---EUF was not enough, lets change the encoding to LRA---</p>
<p>; Warning: disabling SATElite preprocessing to track proof</p>
<p>--Reading LRA and UF summary files: _<em>summaries_uf,</em>_summaries_lra<br />Non linear operation encounter. Ignoring 10 expressions in the file.</p>
<p>----Reading summary file: __summaries_uf<br />Non linear operation encounter in file __summaries_uf. Ignoring this file.</p>
<p>----Reading summary file: __summaries_lra</p>
<p>----Reading summary file: __summaries_linear_temp<br />; lra checker query time so far: 0.000000<br />zsh: segmentation fault ./hifrog --sum-theoref sumth73.c</p> hifrog - Bug #7397 (New): seg fault in interpoatinghttps://scm.ti-edu.ch/issues/73972018-05-24T00:10:23ZSepideh Asadisepideh.a65@gmail.com
<p>how to run<br />./hifrog --sum-theoref file.c</p>
<p>int func1(int n)</p>
<p>{</p>
<pre><code>int i, t1 = 0, t2 = 1, nextTerm=1;<br />if(n>0){<br /> for (i = 1; i <= 2; ++i)
{<br /> nextTerm =nextTerm + n* t1 + t2;<br /> t1 = t2;<br /> t2 = nextTerm + t2;<br /> }<br /> return nextTerm % n;<br />}<br />else return n%2;<br />}</code></pre>
<pre><code>int main()
{<br /> unsigned int a = nondet();<br /> unsigned int b = nondet();<br /> int c = a;<br /> int d = b;<br /> int p = func1( a)+func1( b);<br /> assert (p*p >= 0);<br /> int q = func1(c)+func1(d);<br /> assert(p q);<br /> assert(p % q 0);<br /> return 0;<br /> }</code></pre> hifrog - Bug #7391 (New): LRA reading non-linear operationshttps://scm.ti-edu.ch/issues/73912018-05-22T17:27:54ZSepideh Asadisepideh.a65@gmail.com
<p>How to run: /hifrog --sum-theoref sumth31.c</p>
<p>Error: --Reading LRA summary file: __summaries_lra<br />Non linear operation encounter in file __summaries_uf. Ignoring this file.<br />terminate called after throwing an instance of 'std::logic_error'<br /> what(): During refinement we lost summaries for func<br />Command terminated by signal 6</p>
<p>Benchmark is attached.</p> hifrog - Bug #7280 (New): crash in solver in VTT (3)https://scm.ti-edu.ch/issues/72802018-05-07T17:49:28ZSepideh Asadisepideh.a65@gmail.com
<p>File is: /cprover/regression/funfrog/P2P_Joints_TG3_rec_1.c<br />Verification not successful; here is the last few lines: ...</p>
<ul>
<li>INLINING function: simpleDiv</li>
<li>INLINING function: sqrt_<br />Processing a deferred function: fabs_<br />Processing a deferred function: fabs_<br />Processing a deferred function: getNum<br />Processing a deferred function: simpleDiv<br />Processing a deferred function: sqrt_<br />Processing a deferred function: getNum<br />Processing a deferred function: simpleDiv<br />Processing a deferred function: sqrt_<br />SYMEX TIME: 0.348<br />All SSA steps: 16542<br />Ignored SSA steps after slice: 2925<br />SLICER TIME: 0.077<br />Incrementally adding partitions to the SMT solver<br />; uf_solver query time so far: 0.000029</li>
</ul>
<p>Command terminated by signal 6<br />real 162.77</p> hifrog - Bug #7279 (Resolved): crash in VTT (2)https://scm.ti-edu.ch/issues/72792018-05-07T17:38:50ZSepideh Asadisepideh.a65@gmail.com
<p>File is:.../cprover/regression/funfrog/VTT/P2P_Joints_TG3_e.c<br />File is:.../cprover/regression/funfrog/VTT/VTT1.c<br />File: /cprover/regression/funfrog/VTT/P2P_Joints_TG3_e_BUG.c<br />File /cprover/regression/funfrog/VTT/VTT.c<br />File /cprover/regression/funfrog/VTT/P2P_Joints_TG3_e.c</p>
<p>Claim number # 1 is SAFE</p>
<p>Caught exception: identifier tag-#anon#ST[S32'a1'|S32'a2'|S32'v'|S32't1'|S32't2'|S32't3'|S32'delta'|S32'initPos'|S32'initVel'] not found<br />time 108.58</p>
<hr /> hifrog - Bug #7278 (Resolved): crash in VTT (1)https://scm.ti-edu.ch/issues/72782018-05-07T15:10:45ZSepideh Asadisepideh.a65@gmail.com
<p><strong>File</strong>: /cprover/regression/funfrog/VTT/P2P_Joints_TG3_e_num_4.c</p>
<p><strong>how to run</strong>: ./hifrog --unwind 10 --sum-theoref</p>
<p><strong>Error log:</strong> <p>Verification not successful, here is the last few lines: ...</p>
</p>
<p>Processing a deferred function: sqrt_<br />Processing a deferred function: sqrt_<br />SYMEX TIME: 0.708<br />All SSA steps: 672<br />Ignored SSA steps after slice: 214<br />SLICER TIME: 0.007<br />; uf_solver query time so far: 0.000000<br />; 0 | 0 0 | 84.680 s | 871.938 MB</p>
<p>---trying to locally refine the summary in UF---</p>
<p>---EUF was not enough, lets change the encoding to LRA---</p>
<p>; Warning: disabling SATElite preprocessing to track proof<br />hifrog: ~/cprover/src/funfrog/solvers/smtcheck_opensmt2.cpp:1090: PTRef smtcheck_opensmt2t::substitute(smt_itpt&, const std::vector<symbol_exprt>&): Assertion `symbols.size() == static_cast<std::size_t>(args.size())' failed.<br />Command terminated by signal 6<br />time 85.37</p> hifrog - Bug #7277 (New): timeout in ssh categories; several examples stop in early stageshttps://scm.ti-edu.ch/issues/72772018-05-07T10:17:28ZSepideh Asadisepideh.a65@gmail.com
<p>File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/c/ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c<br />File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c<br />File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c</p>
<pre><code>Verification not successful, here is the last few lines: ...</code></pre>
<p>Converting<br />Type-checking s3_srvr.blast.08_false-unreach-call.i.cil<br />Generating GOTO Program<br />Ignoring CPROVER library<br />Removal of function pointers and virtual functions<br />Generic Property Instrumentation<br /> LOAD Time: 2.419 sec.<br />Total number of claims in program...(1)<br />A specific claim is not set, nor any other claim specification is set.<br />Warrning: --claim is set to 1.<br />; Warning: disabling SATElite preprocessing to track proof<br />Use QF_UF logic.</p>
<pre><code>---------checking claim # 1 ---------</code></pre>
<p>; Warning: disabling SATElite preprocessing to track proof<br />Command terminated by signal 24<br />timeout 200 (s)</p> hifrog - Bug #7276 (Resolved): crash on busybox categories; Ideally we should return UNSUPPORTED!https://scm.ti-edu.ch/issues/72762018-05-07T09:52:23ZSepideh Asadisepideh.a65@gmail.com
<p>File is: /home/asadis/hi-bench/challenge-bench/sv-comp17/c/busybox-1.22.0/touch_false-unreach-call_true-no-overflow_true-valid-memsafety.c</p>
<pre><code>Verification was not successful, here is the last few lines: ...</code></pre>
<p>Total number of claims in program...(1).<br />; Warning: disabling SATElite preprocessing to track proof<br />Use QF_UF logic.</p>
<pre><code>---------checking claim # 1 ---------</code></pre>
; Warning: disabling SATElite preprocessing to track proof<br />hifrog: /home/asadis/new-hifrog/hifrog/trunk/cprover/src/funfrog/symex_assertion_sum.cpp:1695: ssa_exprt symex_assertion_sumt::get_next_version(const symbolt&): Assertion `state.level2.current_names.find(ssa_l1_identifier) != state.level2.current_names.end()' failed.
<ul>
<li>INLINING function: __CPROVER_initialize</li>
<li>INLINING function: main<br />Processing a deferred function: __CPROVER_initialize<br />Processing a deferred function: main<br />Command terminated by signal 6<br />real 4.12</li>
</ul>
<p>Note: Busybox is full of pointer, heap manipulation,...as sated in the svcomp webpage this category aims to represent verification tasks from real software systems.</p>
<p>Note2: This crash happens in 9 benchmarks out of 40.</p> hifrog - Bug #7275 (New): supposed be UNSAT, but it is SAThttps://scm.ti-edu.ch/issues/72752018-05-06T00:42:38ZSepideh Asadisepideh.a65@gmail.com
<p>file:<br />/c/ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.</p>
<p>how to run? <br />./hifrog --logic prop --unwind 10<br />or --sum-theoref</p>