001package daikon.inv; 002 003import org.checkerframework.checker.lock.qual.GuardSatisfied; 004import org.checkerframework.dataflow.qual.Pure; 005import org.checkerframework.dataflow.qual.SideEffectFree; 006 007/** Enumeration type for output style. (Should this be somewhere else?) */ 008public enum OutputFormat { 009 010 /** The standard, concise Daikon output format. Intended to be read by humans. */ 011 DAIKON("Daikon"), 012 /** Design-By-Contract for Java (used by Parasoft JContract) */ 013 DBCJAVA("DBC") { 014 @Override 015 public String ensures_tag() { 016 return "@post"; 017 } 018 019 @Override 020 public String requires_tag() { 021 return "@pre"; 022 } 023 }, 024 /** ESC/Java's annotation language -- a variant of JML. */ 025 ESCJAVA("ESC/Java"), 026 /** Java boolean expression. */ 027 JAVA("Java"), 028 /** Java Modeling Language. */ 029 JML("JML"), 030 /** Simplify theorem prover. First order logical expressions, expressed in Lisp-style parens. */ 031 SIMPLIFY("Simplify"), 032 /** C# Code Contract. */ 033 CSHARPCONTRACT("CSharpContract"); 034 035 final String name; 036 037 OutputFormat(String name) { 038 this.name = name; 039 } 040 041 @SideEffectFree 042 @Override 043 public String toString(@GuardSatisfied OutputFormat this) { 044 return "OutputFormat:" + name; 045 } 046 047 @Pure 048 public boolean isJavaFamily() { 049 return (this == DBCJAVA || this == JML || this == JAVA); 050 } 051 052 // We define the get() method instead of using valueOf() because get() 053 // can be case-sensitive, can permit alternative names, etc. An enum 054 // cannot override valueOf(). 055 /** 056 * Return the appropriate OutputFormat for the given name, or throw an error if no such 057 * OutputFormat exists. 058 */ 059 public static OutputFormat get(String name) { 060 // if (name == null) { return null; } 061 if (name.compareToIgnoreCase(DAIKON.name) == 0) { 062 return DAIKON; 063 } 064 if (name.compareToIgnoreCase(DBCJAVA.name) == 0) { 065 return DBCJAVA; 066 } 067 if (name.compareToIgnoreCase(ESCJAVA.name) == 0) { 068 return ESCJAVA; 069 } 070 if (name.compareToIgnoreCase("ESC") == 0) { 071 return ESCJAVA; 072 } 073 if (name.compareToIgnoreCase(JAVA.name) == 0) { 074 return JAVA; 075 } 076 if (name.compareToIgnoreCase(JML.name) == 0) { 077 return JML; 078 } 079 if (name.compareToIgnoreCase(SIMPLIFY.name) == 0) { 080 return SIMPLIFY; 081 } 082 if (name.compareToIgnoreCase(CSHARPCONTRACT.name) == 0) { 083 return CSHARPCONTRACT; 084 } 085 // return null; 086 throw new Error("Unknown OutputFormat " + name); 087 } 088 089 public String ensures_tag() { 090 return "ensures"; 091 } 092 093 public String requires_tag() { 094 return "requires"; 095 } 096}