]> matita.cs.unibo.it Git - helm.git/blobdiff - benchmarks/bugs
moved benchmnarks/ dir outside of components/
[helm.git] / benchmarks / bugs
diff --git a/benchmarks/bugs b/benchmarks/bugs
new file mode 100644 (file)
index 0000000..00ac8bf
--- /dev/null
@@ -0,0 +1,83 @@
+==== CoFix
+cic:/Lyon/COINDUCTIVES/STREAMS/Examples/mapS2.con \e[0;31mFAIL\e[0m
+cic:/Marseille/CCS/Trans_Sys/refl_strong_eq.con \e[0;31mFAIL\e[0m
+cic:/Marseille/CCS/Trans_Sys/sym_strong_eq.con \e[0;31mFAIL\e[0m
+cic:/Marseille/CCS/Trans_Sys/trans_strong_eq.con \e[0;31mFAIL\e[0m
+cic:/Marseille/CCS/Trans_Sys/refl_weak_eq.con \e[0;31mFAIL\e[0m
+cic:/Marseille/CCS/Trans_Sys/strong_weak.con \e[0;31mFAIL\e[0m
+cic:/Marseille/CCS/Trans_Sys/sym_weak_eq.con \e[0;31mFAIL\e[0m
+cic:/Marseille/CCS/Trans_Sys/weak_eq1_weak_eq.con \e[0;31mFAIL\e[0m
+
+==== Non positive occurrence
+cic:/Suresnes/MiniC/MiniC/State/n_type.ind \e[0;31mFAIL\e[0m
+cic:/Suresnes/MiniC/MiniC/CAbstractSyntax/c_type.ind \e[0;31mFAIL\e[0m
+cic:/Suresnes/MiniC/MiniC/BasicTypes/c_value.ind \e[0;31mFAIL\e[0m
+cic:/Lyon/FIRING-SQUAD/bib/div2.ind \e[0;31mFAIL\e[0m
+cic:/Lyon/GRAPHS-BASICS/Trees/Tree.ind \e[0;31mFAIL\e[0m
+cic:/Lyon/GRAPHS-BASICS/Graphs/Graph.ind \e[0;31mFAIL\e[0m
+cic:/Lyon/GRAPHS-BASICS/Digraphs/Digraph.ind \e[0;31mFAIL\e[0m
+cic:/Lyon/GRAPHS-BASICS/Connected/Connected.ind \e[0;31mFAIL\e[0m
+cic:/Lyon/GRAPHS-BASICS/Acyclic/Acyclic.ind \e[0;31mFAIL\e[0m
+cic:/Rocq/TreeAutomata/pl_path/pl_path_recon.ind \e[0;31mFAIL\e[0m
+cic:/Rocq/COMPILER/Mini_ML/compilation.ind \e[0;31mFAIL\e[0m
+cic:/Rocq/COMPILER/Mini_ML/compilation_id.ind \e[0;31mFAIL\e[0m
+cic:/Rocq/COC/Infer/expln.ind \e[0;31mFAIL\e[0m
+cic:/Rocq/COC/Machine/transition.ind \e[0;31mFAIL\e[0m
+
+
+==== Convertibilita
+cic:/Rocq/TreeAutomata/defs/term_list_term_ind.con \e[0;31mFAIL\e[0m
+cic:/Rocq/TreeAutomata/defs/term_list_term_rec.con \e[0;31mFAIL\e[0m
+cic:/Rocq/TreeAutomata/defs/term_term_list_ind.con \e[0;31mFAIL\e[0m
+cic:/Rocq/TreeAutomata/defs/term_term_list_rec.con \e[0;31mFAIL\e[0m
+cic:/Rocq/TreeAutomata/semantics/mlrec_ind.con \e[0;31mFAIL\e[0m
+cic:/Rocq/TreeAutomata/semantics/mreconnaissance_ind.con \e[0;31mFAIL\e[0m
+cic:/Rocq/TreeAutomata/semantics/mstrec_ind.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/Fairness.con \e[0;31mFAIL\e[0m
+cic:/Rocq/TreeAutomata/non_coacc_kill/mlrec_co_ind.con \e[0;31mFAIL\e[0m
+cic:/Rocq/TreeAutomata/non_coacc_kill/mreconnaissance_co_ind.con \e[0;31mFAIL\e[0m
+cic:/Rocq/TreeAutomata/non_coacc_kill/mstrec_co_ind.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/Equity.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/InTrace.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state1.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state2.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state3.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state5.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state4.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique3.con \e[0;31mFAIL\e[0m
+cic:/Suresnes/BDD/canonicite/Boolean_functions/Assign_k_finite.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique2.con \e[0;31mFAIL\e[0m
+cic:/Suresnes/BDD/canonicite/Vars/Var_k_finite.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique1.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique45.con \e[0;31mFAIL\e[0m
+cic:/Rocq/HIGMAN/Higman/higman.con \e[0;31mFAIL\e[0m
+
+
+=== Unknown constant
+cic:/Sophia-Antipolis/Huffman/Permutation/permutation_map_ex.con \e[0;31mFAIL\e[0m
+
+=== Caso non implementato
+cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/ACK.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/ACKING.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/OUT.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/REPEAT.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/SEND.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/SENDING.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/ACK.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/ACKING.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/OUT.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/REPEAT.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/SEND.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/SENDING.con \e[0;31mFAIL\e[0m
+cic:/Rocq/MUTUAL-EXCLUSION/binary/version2/Correctness/correct.con \e[0;31mFAIL\e[0m
+cic:/Rocq/MUTUAL-EXCLUSION/binary/version1/Correctness/correct.con \e[0;31mFAIL\e[0m
+
+=== Wrong branch type (Nel primo caso: esportato male (argomenti permutati
+    nel tipo di Disc!)
+cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/IsClear.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/OneDel.con \e[0;31mFAIL\e[0m
+cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/Rtalks.con \e[0;31mFAIL\e[0m
+
+=== check_is_really_smaller su un const o mutind?
+cic:/Nijmegen/QArith/positive_fraction_encoding/encoding_algorithm.con \e[0;31mFAIL\e[0m
+cic:/Nijmegen/QArith/positive_fraction_encoding/encoding_algorithm_ind.con \e[0;31mFAIL\e[0m