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> cow - Feature #12972 (New): Implementazione header e footer del CERDDhttps://scm.ti-edu.ch/issues/129722019-08-21T15:17:23ZAndrea Massimini
<p>Per avere uno standard nei vari siti e una corporate identity si vuole implementare un header e un footer per tutti i siti che sia anche facilmente modificabile. <br />Questo è stato reso possibile tramite un implementazione in JS.</p>
<p>in allegato (codice.docx) ho evidenziato il codice necessario per il funzionamento.<br />Ho inserito già per il comando "createHeader" i colori per la vostra piattaforma.</p>
<p>Il risultato dovrebbe essere come allegato ("Pescu3-withCERDD.png" e "Pescu2-withCERDD_01.png" con il problema di conflitto di bootstrap e "Pescu3-withCERDD_02.png" senza)</p>
<p>questo crea un tempo di loading dato che deve scaricare i vari file come anche eseguire i comandi. Noi abbiamo internamente sviluppato dei semplici controlli per evitare una fase di caricamento che visualizza gli elementi che vengono disposti. Eventualmente si può discutere su come implementarlo ma richiede poche linee di codice quindi sarebbe interessante avere lo stesso sistema.</p> OpenSMT 2 - Bug #10647 (New): UF benchmark crashhttps://scm.ti-edu.ch/issues/106472019-04-11T09:18:00ZMartin Blichablicha@d3s.mff.cuni.czhifrog - To do #7863 (New): report system in HiFroghttps://scm.ti-edu.ch/issues/78632018-09-08T18:19:17ZSepideh Asadisepideh.a65@gmail.com
<p>Design a separate class as a report class in HiFrog (storing in the Buffer beforehand) - (due to performance)</p> hifrog - To do #7861 (New): A minimal necessary unwinding boundhttps://scm.ti-edu.ch/issues/78612018-09-07T20:19:13ZSepideh Asadisepideh.a65@gmail.com
<p>A minimal necessary unwinding bound<br />A lazy enumeration of unrollings, it is something that CBMC is doing in SVCOMP.</p> hifrog - To do #7859 (New): checks for uninitialized locals in CBMChttps://scm.ti-edu.ch/issues/78592018-09-07T20:01:30ZSepideh Asadisepideh.a65@gmail.com
<p>CBMC in the goto-instrument program supports --uninitialized-check.<br />Since we updated cprover to version 5.10, it is well worth investigating.</p> 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 - To do #7728 (New): Refactor theory refinement codehttps://scm.ti-edu.ch/issues/77282018-08-21T11:36:10ZMartin Blichablicha@d3s.mff.cuni.cz
<p>Code related to theory refinement should be refactored/simplfied.<br />Karine should have some version prepared.</p> OpenSMT 2 - To do #7717 (New): Implement theory propagation also for PRODUCE_PROOF versionhttps://scm.ti-edu.ch/issues/77172018-08-16T13:00:25ZMartin Blichablicha@d3s.mff.cuni.cz
<p>Theory propagation is now disabled for PRODUCE_PROOF version (see beginning of CoreSMTSolver::search method).<br />The reason is that literals derived by theory propagation do not have reason set at the moment, but this is expected by the proof logging.</p> hifrog - To do #7601 (New): Fixing User-defined summarieshttps://scm.ti-edu.ch/issues/76012018-07-09T21:19:52ZMartin Blichablicha@d3s.mff.cuni.cz
<p>User-defined summaries were disabled during refactoring.<br />Re-enable the functionality.</p> hifrog - To do #7600 (Resolved): Cleaning check_sum_theoref_singlehttps://scm.ti-edu.ch/issues/76002018-07-09T21:16:52ZMartin Blichablicha@d3s.mff.cuni.cz
<p>Hack was used to go around OpenSMT problem in LRA incrementality.<br />This should be fixed now, so a new LRA solver does not need to be created in each iteration.</p>
<p>Rewrite the method so a single OpenSMT instance is used on LRA level.<br />Write tests for checking correctness.</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 #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 />