helm/software/benchmarks/bugs

   1 ==== CoFix
   2 cic:/Lyon/COINDUCTIVES/STREAMS/Examples/mapS2.con \e[0;31mFAIL\e[0m
   3 cic:/Marseille/CCS/Trans_Sys/refl_strong_eq.con \e[0;31mFAIL\e[0m
   4 cic:/Marseille/CCS/Trans_Sys/sym_strong_eq.con \e[0;31mFAIL\e[0m
   5 cic:/Marseille/CCS/Trans_Sys/trans_strong_eq.con \e[0;31mFAIL\e[0m
   6 cic:/Marseille/CCS/Trans_Sys/refl_weak_eq.con \e[0;31mFAIL\e[0m
   7 cic:/Marseille/CCS/Trans_Sys/strong_weak.con \e[0;31mFAIL\e[0m
   8 cic:/Marseille/CCS/Trans_Sys/sym_weak_eq.con \e[0;31mFAIL\e[0m
   9 cic:/Marseille/CCS/Trans_Sys/weak_eq1_weak_eq.con \e[0;31mFAIL\e[0m
  10
  11 ==== Non positive occurrence
  12 cic:/Suresnes/MiniC/MiniC/State/n_type.ind \e[0;31mFAIL\e[0m
  13 cic:/Suresnes/MiniC/MiniC/CAbstractSyntax/c_type.ind \e[0;31mFAIL\e[0m
  14 cic:/Suresnes/MiniC/MiniC/BasicTypes/c_value.ind \e[0;31mFAIL\e[0m
  15 cic:/Lyon/FIRING-SQUAD/bib/div2.ind \e[0;31mFAIL\e[0m
  16 cic:/Lyon/GRAPHS-BASICS/Trees/Tree.ind \e[0;31mFAIL\e[0m
  17 cic:/Lyon/GRAPHS-BASICS/Graphs/Graph.ind \e[0;31mFAIL\e[0m
  18 cic:/Lyon/GRAPHS-BASICS/Digraphs/Digraph.ind \e[0;31mFAIL\e[0m
  19 cic:/Lyon/GRAPHS-BASICS/Connected/Connected.ind \e[0;31mFAIL\e[0m
  20 cic:/Lyon/GRAPHS-BASICS/Acyclic/Acyclic.ind \e[0;31mFAIL\e[0m
  21 cic:/Rocq/TreeAutomata/pl_path/pl_path_recon.ind \e[0;31mFAIL\e[0m
  22 cic:/Rocq/COMPILER/Mini_ML/compilation.ind \e[0;31mFAIL\e[0m
  23 cic:/Rocq/COMPILER/Mini_ML/compilation_id.ind \e[0;31mFAIL\e[0m
  24 cic:/Rocq/COC/Infer/expln.ind \e[0;31mFAIL\e[0m
  25 cic:/Rocq/COC/Machine/transition.ind \e[0;31mFAIL\e[0m
  26
  27
  28 ==== Convertibilita
  29 cic:/Rocq/TreeAutomata/defs/term_list_term_ind.con \e[0;31mFAIL\e[0m
  30 cic:/Rocq/TreeAutomata/defs/term_list_term_rec.con \e[0;31mFAIL\e[0m
  31 cic:/Rocq/TreeAutomata/defs/term_term_list_ind.con \e[0;31mFAIL\e[0m
  32 cic:/Rocq/TreeAutomata/defs/term_term_list_rec.con \e[0;31mFAIL\e[0m
  33 cic:/Rocq/TreeAutomata/semantics/mlrec_ind.con \e[0;31mFAIL\e[0m
  34 cic:/Rocq/TreeAutomata/semantics/mreconnaissance_ind.con \e[0;31mFAIL\e[0m
  35 cic:/Rocq/TreeAutomata/semantics/mstrec_ind.con \e[0;31mFAIL\e[0m
  36 cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/Fairness.con \e[0;31mFAIL\e[0m
  37 cic:/Rocq/TreeAutomata/non_coacc_kill/mlrec_co_ind.con \e[0;31mFAIL\e[0m
  38 cic:/Rocq/TreeAutomata/non_coacc_kill/mreconnaissance_co_ind.con \e[0;31mFAIL\e[0m
  39 cic:/Rocq/TreeAutomata/non_coacc_kill/mstrec_co_ind.con \e[0;31mFAIL\e[0m
  40 cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/Equity.con \e[0;31mFAIL\e[0m
  41 cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/InTrace.con \e[0;31mFAIL\e[0m
  42 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state1.con \e[0;31mFAIL\e[0m
  43 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state2.con \e[0;31mFAIL\e[0m
  44 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state3.con \e[0;31mFAIL\e[0m
  45 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state5.con \e[0;31mFAIL\e[0m
  46 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Correctness/state4.con \e[0;31mFAIL\e[0m
  47 cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique3.con \e[0;31mFAIL\e[0m
  48 cic:/Suresnes/BDD/canonicite/Boolean_functions/Assign_k_finite.con \e[0;31mFAIL\e[0m
  49 cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique2.con \e[0;31mFAIL\e[0m
  50 cic:/Suresnes/BDD/canonicite/Vars/Var_k_finite.con \e[0;31mFAIL\e[0m
  51 cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique1.con \e[0;31mFAIL\e[0m
  52 cic:/Lyon/PROCESSES/ABP/TRACES/Unique/Unique45.con \e[0;31mFAIL\e[0m
  53 cic:/Rocq/HIGMAN/Higman/higman.con \e[0;31mFAIL\e[0m
  54
  55
  56 === Unknown constant
  57 cic:/Sophia-Antipolis/Huffman/Permutation/permutation_map_ex.con \e[0;31mFAIL\e[0m
  58
  59 === Caso non implementato
  60 cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/ACK.con \e[0;31mFAIL\e[0m
  61 cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/ACKING.con \e[0;31mFAIL\e[0m
  62 cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/OUT.con \e[0;31mFAIL\e[0m
  63 cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/REPEAT.con \e[0;31mFAIL\e[0m
  64 cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/SEND.con \e[0;31mFAIL\e[0m
  65 cic:/Lyon/PROCESSES/ABP/TRACES/Protocol/SENDING.con \e[0;31mFAIL\e[0m
  66 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/ACK.con \e[0;31mFAIL\e[0m
  67 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/ACKING.con \e[0;31mFAIL\e[0m
  68 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/OUT.con \e[0;31mFAIL\e[0m
  69 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/REPEAT.con \e[0;31mFAIL\e[0m
  70 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/SEND.con \e[0;31mFAIL\e[0m
  71 cic:/Lyon/PROCESSES/ABP/BISIMULATION/Protocol/SENDING.con \e[0;31mFAIL\e[0m
  72 cic:/Rocq/MUTUAL-EXCLUSION/binary/version2/Correctness/correct.con \e[0;31mFAIL\e[0m
  73 cic:/Rocq/MUTUAL-EXCLUSION/binary/version1/Correctness/correct.con \e[0;31mFAIL\e[0m
  74
  75 === Wrong branch type (Nel primo caso: esportato male (argomenti permutati
  76     nel tipo di Disc!)
  77 cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/IsClear.con \e[0;31mFAIL\e[0m
  78 cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/OneDel.con \e[0;31mFAIL\e[0m
  79 cic:/Lyon/PROCESSES/ABP/TRACES/Hypotheses/Rtalks.con \e[0;31mFAIL\e[0m
  80
  81 === check_is_really_smaller su un const o mutind?
  82 cic:/Nijmegen/QArith/positive_fraction_encoding/encoding_algorithm.con \e[0;31mFAIL\e[0m
  83 cic:/Nijmegen/QArith/positive_fraction_encoding/encoding_algorithm_ind.con \e[0;31mFAIL\e[0m