Changeset 3395


Ignore:
Timestamp:
Nov 1, 2013, 5:29:55 PM (6 years ago)
Author:
fguidi
Message:

scan for redundant includes with new version of matitadep

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Makefile

    r2919 r3395  
    55MATITADEP_OUT = redundant_includes.txt
    66MATITADEP_DIR = $(MATITA_COMPONENTS)binaries/matitadep/
    7 MATITADEP     = $(MATITADEP_DIR)matitadep.native
     7MATITADEP     = $(MATITADEP_DIR)matitadep.native -c
    88
    99all:
     
    1414deps:
    1515        @echo "  MATITADEP > $(MATITADEP_OUT)"
    16         $(H)find -name "*.ma" | xargs grep "^include \"" | sed "s/.\///" | $(MATITADEP) > $(MATITADEP_OUT)
     16        $(H)find -name "*.ma" | xargs grep "^include \"" | $(MATITADEP) > $(MATITADEP_OUT)
  • src/redundant_includes.txt

    r2919 r3395  
    1 utilities/extralib.ma: redundant basics/lists/list.ma
    2 utilities/extralib.ma: redundant basics/types.ma
    3 utilities/monad.ma: redundant basics/relations.ma
    4 utilities/monad.ma: redundant basics/types.ma
    5 utilities/option.ma: redundant basics/types.ma
    6 utilities/extranat.ma: redundant basics/types.ma
    7 ASM/Vector.ma: redundant arithmetics/nat.ma
    8 ASM/Vector.ma: redundant basics/types.ma
    9 ASM/Vector.ma: redundant basics/lists/list.ma
    10 ASM/BitVector.ma: redundant arithmetics/nat.ma
    11 common/PositiveMap.ma: redundant basics/types.ma
    12 common/Errors.ma: redundant utilities/monad.ma
    13 common/Errors.ma: redundant basics/russell.ma
    14 common/Errors.ma: redundant basics/lists/list.ma
    15 common/Errors.ma: redundant basics/logic.ma
    16 common/Errors.ma: redundant basics/types.ma
    17 utilities/lists.ma: redundant utilities/monad.ma
    18 utilities/lists.ma: redundant utilities/option.ma
    19 utilities/lists.ma: redundant basics/lists/list.ma
    20 common/Identifiers.ma: redundant utilities/binary/positive.ma
    21 common/Identifiers.ma: redundant basics/types.ma
    22 common/Integers.ma: redundant ASM/BitVector.ma
    23 common/Integers.ma: redundant utilities/extranat.ma
    24 common/Integers.ma: redundant arithmetics/nat.ma
    25 common/AST.ma: redundant basics/types.ma
    26 ASM/BitVectorZ.ma: redundant ASM/BitVector.ma
    27 ASM/BitVectorZ.ma: redundant utilities/binary/Z.ma
    28 common/Values.ma: redundant common/Errors.ma
    29 utilities/Coqlib.ma: redundant basics/lists/list.ma
    30 utilities/Coqlib.ma: redundant basics/types.ma
    31 common/GenMem.ma: redundant common/Pointers.ma
    32 common/GenMem.ma: redundant utilities/extralib.ma
    33 common/Globalenvs.ma: redundant common/AST.ma
    34 common/Globalenvs.ma: redundant common/Errors.ma
    35 common/extraGlobalenvs.ma: redundant common/AST.ma
    36 common/ExtraMonads.ma: redundant common/Errors.ma
    37 utilities/bind_new.ma: redundant utilities/monad.ma
    38 common/LabelledObjects.ma: redundant utilities/lists.ma
    39 joint/Joint.ma: redundant utilities/lists.ma
    40 common/Graphs.ma: redundant common/Identifiers.ma
    41 ASM/BitVectorTrie.ma: redundant basics/types.ma
    42 common/Graphs.ma: redundant basics/types.ma
    43 ASM/I8051.ma: redundant arithmetics/nat.ma
    44 joint/TranslateUtils.ma: redundant joint/Joint.ma
    45 joint/semanticsUtils.ma: redundant ASM/BitVectorTrie.ma
    46 joint/semanticsUtils.ma: redundant utilities/hide.ma
    47 joint/BEMem.ma: redundant common/ByteValues.ma
    48 common/Events.ma: redundant utilities/extralib.ma
    49 common/Events.ma: redundant basics/lists/list.ma
    50 joint/joint_semantics.ma: redundant common/Globalenvs.ma
    51 common/StructuredTraces.ma: redundant utilities/option.ma
    52 common/StructuredTraces.ma: redundant common/CostLabel.ma
    53 common/StructuredTraces.ma: redundant basics/bool.ma
    54 joint/semantics_blocks.ma: redundant joint/blocks.ma
    55 common/Animation.ma: redundant arithmetics/nat.ma
    56 common/SmallstepExec.ma: redundant common/Integers.ma
    57 common/SmallstepExec.ma: redundant utilities/extralib.ma
    58 Clight/Csyntax.ma: redundant common/Errors.ma
    59 Clight/Csem.ma: redundant Clight/Csyntax.ma
    60 Clight/Cexec.ma: redundant utilities/extralib.ma
    61 ERTLptr/ERTLptr_semantics.ma: redundant joint/semanticsUtils.ma
    62 Clight/frontend_misc.ma: redundant common/IOMonad.ma
    63 Clight/frontend_misc.ma: redundant common/Pointers.ma
    64 Clight/frontend_misc.ma: redundant Clight/TypeComparison.ma
    65 Clight/MemProperties.ma: redundant common/FrontEndMem.ma
    66 Clight/switchRemoval.ma: redundant utilities/extralib.ma
    67 Clight/switchRemoval.ma: redundant common/Identifiers.ma
    68 Clight/switchRemoval.ma: redundant basics/lists/listb.ma
    69 RTLabs/RTLabs_syntax.ma: redundant ASM/Vector.ma
    70 common/FrontEndOps.ma: redundant common/Values.ma
    71 RTLabs/RTLabs_syntax.ma: redundant common/AST.ma
    72 RTLabs/RTLabs_syntax.ma: redundant basics/logic.ma
    73 RTLabs/CostCheck.ma: redundant RTLabs/CostSpec.ma
    74 RTLabs/RTLabs_semantics.ma: redundant common/Errors.ma
    75 RTLabs/RTLabs_semantics.ma: redundant basics/lists/list.ma
    76 Cminor/toRTLabs.ma: redundant Cminor/Cminor_syntax.ma
    77 Cminor/toRTLabs.ma: redundant common/Globalenvs.ma
    78 Cminor/toRTLabs.ma: redundant utilities/lists.ma
    79 Cminor/Cminor_semantics.ma: redundant common/FrontEndMem.ma
    80 Cminor/Cminor_semantics.ma: redundant common/Events.ma
    81 Clight/toCminor.ma: redundant basics/lists/list.ma
    82 Clight/SimplifyCasts.ma: redundant Clight/Cexec.ma
    83 Clight/SimplifyCasts.ma: redundant Clight/TypeComparison.ma
    84 Clight/SimplifyCasts.ma: redundant Clight/Csyntax.ma
    85 ASM/UtilBranch.ma: redundant ASM/Util.ma
    86 ERTL/ERTLToERTLptr.ma: redundant ERTL/ERTL.ma
    87 RTLabs/RTLabs_traces.ma: redundant RTLabs/CostSpec.ma
    88 joint/extra_joint_semantics.ma: redundant joint/joint_semantics.ma
    89 ERTL/ERTLtoERTLptrUtils.ma: redundant common/ExtraMonads.ma
    90 ERTL/ERTLtoERTLptrUtils.ma: redundant joint/Traces.ma
    91 joint/StatusSimulationHelper.ma: redundant joint/Traces.ma
    92 joint/StatusSimulationHelper.ma: redundant joint/semanticsUtils.ma
    93 common/stacksize.ma: redundant basics/lists/list.ma
    94 ASM/Fetch.ma: redundant ASM/Arithmetic.ma
    95 ASM/Assembly.ma: redundant ASM/Arithmetic.ma
    96 ASM/Assembly.ma: redundant ASM/ASM.ma
    97 semantics.ma: redundant ERTL/ERTL_semantics.ma
    98 compiler.ma: redundant ASM/ASMCosts.ma
    99 ASM/PolicyFront.ma: redundant utilities/extralib.ma
    100 ASM/PolicyFront.ma: redundant ASM/Status.ma
    101 ASM/PolicyFront.ma: redundant ASM/Fetch.ma
    102 ASM/PolicyFront.ma: redundant ASM/Arithmetic.ma
    103 ASM/PolicyFront.ma: redundant ASM/ASM.ma
    104 LIN/LINToASM.ma: redundant ASM/Util.ma
    105 ERTLptr/ERTLptrToLTL.ma: redundant ASM/Arithmetic.ma
    106 utilities/adt/set_adt.ma: redundant arithmetics/nat.ma
    107 utilities/adt/set_adt.ma: redundant basics/lists/list.ma
    108 utilities/adt/set_adt.ma: redundant basics/types.ma
    109 ERTLptr/liveness.ma: redundant ASM/Util.ma
    110 RTL/RTLToERTL.ma: redundant common/Identifiers.ma
    111 RTLabs/RTLabsToRTL.ma: redundant common/Graphs.ma
    112 Clight/test/search.test.ma: redundant common/Animation.ma
    113 Clight/toCminorOps.ma: redundant Clight/frontend_misc.ma
    114 Clight/toCminorOps.ma: redundant Clight/Cexec.ma
    115 Clight/toCminorCorrectnessExpr.ma: redundant common/Globalenvs.ma
    116 Clight/toCminorCorrectnessExpr.ma: redundant Clight/toCminor.ma
    117 Clight/toCminorCorrectness.ma: redundant Cminor/Cminor_abstract.ma
    118 Clight/toCminorCorrectness.ma: redundant Clight/Clight_abstract.ma
    119 Clight/toCminorCorrectness.ma: redundant Clight/memoryInjections.ma
    120 Clight/toCminorCorrectness.ma: redundant common/Globalenvs.ma
    121 Clight/toCminorCorrectness.ma: redundant Clight/CexecInd.ma
    122 Clight/toCminorCorrectness.ma: redundant Clight/toCminor.ma
    123 utilities/adt/priority_set_adt.ma: redundant arithmetics/nat.ma
    124 utilities/adt/priority_set_adt.ma: redundant basics/lists/list.ma
    125 utilities/adt/priority_set_adt.ma: redundant basics/types.ma
    126 ASM/Test.ma: redundant ASM/StatusProofs.ma
    127 ASM/Test.ma: redundant ASM/Interpret.ma
    128 ASM/Test.ma: redundant ASM/Assembly.ma
    129 ERTLptr/ERTLptrToLTLProof.ma: redundant common/StatusSimulation.ma
    130 ERTLptr/ERTLptrToLTLProof.ma: redundant joint/Traces.ma
    131 Clight/test/castremoval.test.ma: redundant common/Animation.ma
    132 ASM/WellLabeled.ma: redundant ASM/ASM.ma
    133 ASM/CostsProof.ma: redundant arithmetics/bigops.ma
    134 RTLabs/RTLabs_partial_traces.ma: redundant RTLabs/CostSpec.ma
     1./utilities/lists.ma: redundant utilities/option.ma
     2./utilities/lists.ma: redundant utilities/option.ma
Note: See TracChangeset for help on using the changeset viewer.