USI & SUPSI Source Code Management (SCM): Issueshttps://scm.ti-edu.ch/https://scm.ti-edu.ch/favicon.ico?15601711372019-09-26T11:54:36ZUSI & SUPSI Source Code Management (SCM)
Redmine 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 #10434 (New): Automatically detect the bound in HiFrog for the sake of completenesshttps://scm.ti-edu.ch/issues/104342019-03-29T13:52:40ZSepideh Asadisepideh.a65@gmail.com
<p>Developing a preprocessing mechanism to detect the necessary depth of unrolling the program.(completeness threshold)<br />Then we can claim on verification of those instances, not just falsification.</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 - 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. 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 - 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 #7116 (New): Segmentation fault in summary reuse in LRAhttps://scm.ti-edu.ch/issues/71162018-04-18T23:56:30ZSepideh Asadisepideh.a65@gmail.com
<p>How to run:<br />./hifrog /hifrog/trunk/cprover/regression/funfrog/03_simple/no_grouping.c --claim 1 --logic qflra // First generate summary<br />./hifrog /hifrog/trunk/cprover/regression/funfrog/03_simple/no_grouping.c --claim 2 --logic qflra // Reuse the previous summary</p>
<p>-------------------------------------<br />Error:<br />; lra checker query time so far: 0.000002</p>
<p>Thread 3 received signal SIGSEGV, Segmentation fault.<br />0x0000000101328af0 in ?? ()<br />Segmentation fault: 11</p> hifrog - Bug #5720 (Resolved): Regression Test : reusing LRA summary abortedhttps://scm.ti-edu.ch/issues/57202017-10-20T00:50:03ZSepideh Asadisepideh.a65@gmail.com
<p>When verifying the attached C code with LRA, the summary is generated successfully, but cannot be reused in the second run.</p>
<p><strong>How to run:</strong></p>
<blockquote>
<p>./hifrog --claim 1 --logic qflra getchar1.c</p>
</blockquote>
<p><strong>Error message:</strong></p>
<blockquote>
<p><em>Assertion failed: ("Error: Not all arguments of a summary of a function was instantiated." && symbols.size() == args_instantiated), function substitute, file solvers/smt_itp.cpp, line 326.<br />Abort trap: 6</em></p>
</blockquote>
<p>P.S. with the logic prop it works fine.(summary is generated and can be reused successfully).</p> hifrog - Bug #5519 (Resolved): Function summary + UF/LRA does not workhttps://scm.ti-edu.ch/issues/55192017-08-13T19:47:15ZSepideh Asadisepideh.a65@gmail.com
<p>It seems in UF/LRA Interpolants are generated but cannot be reused.</p>
<p>./hifrog --logic qfuf --claim 1 --unwind 10 token.c</p>
<p>hifrog: solvers/smt_itp.cpp:273: void smt_itpt::substitute(smtcheck_opensmt2t&, const std::vector<symbol_exprt>&, bool) const: Assertion `aname == unidx_aname || aname.find("::#return_value!0") != string::npos' failed.<br />Aborted (core dumped)</p>
<p>----------<br />QF-Bool works fine.</p> hifrog - Bug #5355 (New): /regression/hifrog/benchmarks/06_main5.chttps://scm.ti-edu.ch/issues/53552017-06-25T20:31:49ZSepideh Asadisepideh.a65@gmail.com
<p>/hifrog --claim 1 --theoref --no-itp --unwind 10 --bitwidth 32 --heuristic 4 /regression/hifrog/benchmarks/06_main5.c ---> SAT</p>
<p>Obtained counter-examples are refined<br />(15 / 26 expressions bit-blasted)<br />ASSERTION DOES NOT HOLD</p>
<p>VERIFICATION FAILED<br />TOTAL TIME FOR CHECKING THIS CLAIM: 16.787</p>
<p>------------------------------------------------<br />CBMC reports as SUCCESSFUL</p> hifrog - Bug #4998 (Feedback): bug in QF_BOOL: wrong result for prop in benchs in directrory ntdr...https://scm.ti-edu.ch/issues/49982017-04-12T15:03:35ZSepideh Asadisepideh.a65@gmail.com
<p>/hifrog --claim 1 --logic prop --bitwidth 8 --unwind 1 ~/hi-bench/challenge-bench/sv-comp16/c/ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c</p>
<p>VERIFICATION FAILED</p>
<p>wrong result! because claim 1 should hold</p> cow - Bug #862 (New): Cow doesn't compile for Moose Build 43 (PULL REQUEST)https://scm.ti-edu.ch/issues/8622015-07-06T13:00:51ZErich Fostererich.foster@usi.ch
<p>The master branch still doesn't compile for the latest version of Moose. The problem is _f in include/materials/GuccioneCostaRot.h this should be a constant.</p>