Skip to content

Commit

Permalink
Rename cce to Cce
Browse files Browse the repository at this point in the history
  • Loading branch information
@keyboardDrummer
keyboardDrummer committed Aug 2, 2024
1 parent de1c567 commit c62d13a
Show file tree
Hide file tree
Showing 78 changed files with 1,048 additions and 1,048 deletions.
38 changes: 19 additions & 19 deletions Source/AbstractInterpretation/Traverse.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,44 +18,44 @@ public class WidenPoints
public static void Compute(Program program)
{
Contract.Requires(program != null);
cce.BeginExpose(program);
Cce.BeginExpose(program);

foreach (var impl in program.Implementations)
{
if (impl.Blocks != null && impl.Blocks.Count > 0)
{
Contract.Assume(cce.IsConsistent(impl));
cce.BeginExpose(impl);
Contract.Assume(Cce.IsConsistent(impl));
Cce.BeginExpose(impl);
Block start = impl.Blocks[0];
Contract.Assume(start != null);
Contract.Assume(cce.IsConsistent(start));
Contract.Assume(Cce.IsConsistent(start));
Visit(start);

// We reset the state...
foreach (Block b in impl.Blocks)
{
cce.BeginExpose(b);
Cce.BeginExpose(b);
b.TraversingStatus = Block.VisitState.ToVisit;
cce.EndExpose();
Cce.EndExpose();
}

cce.EndExpose();
Cce.EndExpose();
}
}

cce.EndExpose();
Cce.EndExpose();
}

static void Visit(Block b)
{
Contract.Requires(b != null);
Contract.Assume(cce.IsExposable(b));
Contract.Assume(Cce.IsExposable(b));
if (b.TraversingStatus == Block.VisitState.BeingVisited)
{
cce.BeginExpose(b);
Cce.BeginExpose(b);
// we got here through a back-edge
b.widenBlock = true;
cce.EndExpose();
Cce.EndExpose();
}
else if (b.TraversingStatus == Block.VisitState.AlreadyVisited)
{
Expand All @@ -66,15 +66,15 @@ static void Visit(Block b)
Contract.Assert(b.TraversingStatus == Block.VisitState.ToVisit);

GotoCmd g = (GotoCmd) b.TransferCmd;
cce.BeginExpose(b);
Cce.BeginExpose(b);

cce.BeginExpose(g); //PM: required for the subsequent expose (g.labelTargets)
Cce.BeginExpose(g); //PM: required for the subsequent expose (g.labelTargets)
b.TraversingStatus = Block.VisitState.BeingVisited;

// labelTargets is made non-null by Resolve, which we assume
// has already called in a prior pass.
Contract.Assume(g.labelTargets != null);
cce.BeginExpose(g.labelTargets);
Cce.BeginExpose(g.labelTargets);
foreach (Block succ in g.labelTargets)
// invariant b.currentlyTraversed;
//PM: The following loop invariant will work once properties are axiomatized
Expand All @@ -84,7 +84,7 @@ static void Visit(Block b)
Visit(succ);
}

cce.EndExpose();
Cce.EndExpose();

Contract.Assert(b.TraversingStatus == Block.VisitState.BeingVisited);
// System.Diagnostics.Debug.Assert(b.currentlyTraversed);
Expand All @@ -94,7 +94,7 @@ static void Visit(Block b)
//PM: The folowing assumption is needed because we cannot prove that a simple field update
//PM: leaves the value of a property unchanged.
Contract.Assume(g.labelNames == null || g.labelNames.Count == g.labelTargets.Count);
cce.EndExpose();
Cce.EndExpose();
}
else
{
Expand All @@ -113,7 +113,7 @@ public static List<Block> ComputeLoopBodyFrom(Block block)
{
Contract.Requires(block.widenBlock);
Contract.Requires(block != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
Contract.Ensures(Cce.NonNullElements(Contract.Result<List<Block>>()));

Contract.Assert(rootBlock == null);
rootBlock = block;
Expand Down Expand Up @@ -141,8 +141,8 @@ public static List<Block> ComputeLoopBodyFrom(Block block)
private static void DoDFSVisit(Block block, List<Block> path, List<Block> blocksInPath)
{
Contract.Requires(block != null);
Contract.Requires(cce.NonNullElements(path));
Contract.Requires(cce.NonNullElements(path));
Contract.Requires(Cce.NonNullElements(path));
Contract.Requires(Cce.NonNullElements(path));

#region case 1. We visit the root => We are done, "path" is a path inside the loop

Expand Down
2 changes: 1 addition & 1 deletion Source/BaseTypes/BigNum.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -148,7 +148,7 @@ public override int GetHashCode()
public override string /*!*/ ToString()
{
Contract.Ensures(Contract.Result<string>() != null);
return cce.NonNull(val.ToString());
return Cce.NonNull(val.ToString());
}

//////////////////////////////////////////////////////////////////////////////
Expand Down
4 changes: 2 additions & 2 deletions Source/BaseTypes/Set.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -273,7 +273,7 @@ public virtual int Count
Contract.Ensures(Contract.Result<GSet<T>>() != null);
//Contract.Ensures(Contract.ForAll(result, x => a[x] && b[x] ));
GSet<T> /*!*/
res = (GSet<T> /*!*/) cce.NonNull(a.Clone());
res = (GSet<T> /*!*/) Cce.NonNull(a.Clone());
res.Intersect(b);
return res;
}
Expand All @@ -286,7 +286,7 @@ public virtual int Count
Contract.Ensures(Contract.Result<GSet<T>>() != null);
// Contract.Ensures(Contract.ForAll(result, x => a[x] || b[x] ));
GSet<T> /*!*/
res = (GSet<T> /*!*/) cce.NonNull(a.Clone());
res = (GSet<T> /*!*/) Cce.NonNull(a.Clone());
res.AddRange(b);
return res;
}
Expand Down
2 changes: 1 addition & 1 deletion Source/BoogieDriver/BoogieDriver.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ public class OnlyBoogie
{
public static int Main(string[] args)
{
Contract.Requires(cce.NonNullElements(args));
Contract.Requires(Cce.NonNullElements(args));

var options = new CommandLineOptions(Console.Out, new ConsolePrinter())
{
Expand Down
6 changes: 3 additions & 3 deletions Source/CodeContractsExtender/cce.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
/// <summary>
/// A class containing static methods to extend the functionality of Code Contracts
/// </summary>
public static class cce
public static class Cce
{
//[Pure]
//public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {
Expand All @@ -29,7 +29,7 @@ public static bool NonNullElements<T>(IEnumerable<T> collection) where T : class
[Pure]
public static bool NonNullDictionaryAndValues<TKey, TValue>(IDictionary<TKey, TValue> collection) where TValue : class
{
return collection != null && cce.NonNullElements(collection.Values);
return collection != null && Cce.NonNullElements(collection.Values);
}

//[Pure]
Expand All @@ -46,7 +46,7 @@ public static bool NonNullDictionaryAndValues<TKey, TValue>(IDictionary<TKey, TV
[Pure]
public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) where T : class
{
return (nullability && collection == null) || cce.NonNullElements(collection);
return (nullability && collection == null) || Cce.NonNullElements(collection);
//Should be the same as:
/*if(nullability&&collection==null)
* return true;
Expand Down
4 changes: 2 additions & 2 deletions Source/Concurrency/CivlCoreTypes.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -390,7 +390,7 @@ private List<AssertCmd> HoistAsserts(Implementation impl, ConcurrencyOptions opt
}
else
{
throw new cce.UnreachableException();
throw new Cce.UnreachableException();
}
}
return wlps[impl.Blocks[0]].Select(assertCmd => Forall(impl.LocVars.Union(impl.OutParams), assertCmd)).ToList();
Expand Down Expand Up @@ -435,7 +435,7 @@ private List<AssertCmd> HoistAsserts(List<Cmd> cmds, List<AssertCmd> postconditi
}
else
{
throw new cce.UnreachableException();
throw new Cce.UnreachableException();
}
}
cmds.RemoveAll(cmd => cmd is AssertCmd);
Expand Down
4 changes: 2 additions & 2 deletions Source/Concurrency/CivlUtil.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ public void Compute()
}
else
{
throw new cce.UnreachableException();
throw new Cce.UnreachableException();
}
}
}
Expand Down Expand Up @@ -108,7 +108,7 @@ private HashSet<Variable> Propagate(Cmd cmd, HashSet<Variable> liveVars)
liveVars.ExceptWith(stateCmd.Locals);
return liveVars;
}
throw new cce.UnreachableException();
throw new Cce.UnreachableException();
}
}

Expand Down
32 changes: 16 additions & 16 deletions Source/Core/AST/Absy.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,7 @@ public virtual Absy Clone()
{
Contract.Ensures(Contract.Result<Absy>() != null);
Absy /*!*/
result = cce.NonNull((Absy /*!*/) this.MemberwiseClone());
result = Cce.NonNull((Absy /*!*/) this.MemberwiseClone());
result.UniqueId = System.Threading.Interlocked.Increment(ref CurrentAbsyNodeId); // BUGBUG??

if (InternalNumberedMetadata != null)
Expand Down Expand Up @@ -762,7 +762,7 @@ public NamedDeclaration(IToken tok, string name)
[Pure]
public override string ToString()
{
return cce.NonNull(Name);
return Cce.NonNull(Name);
}

public virtual bool MayRename => true;
Expand Down Expand Up @@ -1128,7 +1128,7 @@ public override void Typecheck(TypecheckingContext tc)

public static void ResolveTypeSynonyms(List<TypeSynonymDecl /*!*/> /*!*/ synonymDecls, ResolutionContext /*!*/ rc)
{
Contract.Requires(cce.NonNullElements(synonymDecls));
Contract.Requires(Cce.NonNullElements(synonymDecls));
Contract.Requires(rc != null);
// then discover all dependencies between type synonyms
IDictionary<TypeSynonymDecl /*!*/, List<TypeSynonymDecl /*!*/> /*!*/> /*!*/
Expand Down Expand Up @@ -1196,7 +1196,7 @@ private static void FindDependencies(Type /*!*/ type, List<TypeSynonymDecl /*!*/
ResolutionContext /*!*/ rc)
{
Contract.Requires(type != null);
Contract.Requires(cce.NonNullElements(deps));
Contract.Requires(Cce.NonNullElements(deps));
Contract.Requires(rc != null);
if (type.IsVariable || type.IsBasic)
{
Expand Down Expand Up @@ -1398,7 +1398,7 @@ public int Compare(object a, object b)
throw new ArgumentException("VariableComparer works only on objects of type Variable");
}

return cce.NonNull(A.Name).CompareTo(B.Name);
return Cce.NonNull(A.Name).CompareTo(B.Name);
}
}

Expand Down Expand Up @@ -1741,12 +1741,12 @@ public DeclWithFormals(IToken tok, string name, List<TypeVariable> typeParams,
}

protected DeclWithFormals(DeclWithFormals that)
: base(that.tok, cce.NonNull(that.Name))
: base(that.tok, Cce.NonNull(that.Name))
{
Contract.Requires(that != null);
this.TypeParameters = that.TypeParameters;
this.inParams = cce.NonNull(that.InParams);
this.outParams = cce.NonNull(that.OutParams);
this.inParams = Cce.NonNull(that.InParams);
this.outParams = Cce.NonNull(that.OutParams);
}

public byte[] MD5Checksum_;
Expand Down Expand Up @@ -1938,7 +1938,7 @@ protected void EmitSignature(TokenTextWriter stream, bool shortRet)
{
Contract.Assert(OutParams.Count == 1);
stream.Write(" : ");
cce.NonNull(OutParams[0]).TypedIdent.Type.Emit(stream);
Cce.NonNull(OutParams[0]).TypedIdent.Type.Emit(stream);
}
else if (OutParams.Count > 0)
{
Expand Down Expand Up @@ -2240,11 +2240,11 @@ public override void Typecheck(TypecheckingContext tc)
{
Contract.Assert(DefinitionBody == null);
Body.Typecheck(tc);
if (!cce.NonNull(Body.Type).Unify(cce.NonNull(OutParams[0]).TypedIdent.Type))
if (!Cce.NonNull(Body.Type).Unify(Cce.NonNull(OutParams[0]).TypedIdent.Type))
{
tc.Error(Body,
"function body with invalid type: {0} (expected: {1})",
Body.Type, cce.NonNull(OutParams[0]).TypedIdent.Type);
Body.Type, Cce.NonNull(OutParams[0]).TypedIdent.Type);
}
}
else if (DefinitionBody != null)
Expand All @@ -2253,11 +2253,11 @@ public override void Typecheck(TypecheckingContext tc)

// We are matching the type of the function body with output param, and not the type
// of DefinitionBody, which is always going to be bool (since it is of the form func_call == func_body)
if (!cce.NonNull(DefinitionBody.Args[1].Type).Unify(cce.NonNull(OutParams[0]).TypedIdent.Type))
if (!Cce.NonNull(DefinitionBody.Args[1].Type).Unify(Cce.NonNull(OutParams[0]).TypedIdent.Type))
{
tc.Error(DefinitionBody.Args[1],
"function body with invalid type: {0} (expected: {1})",
DefinitionBody.Args[1].Type, cce.NonNull(OutParams[0]).TypedIdent.Type);
DefinitionBody.Args[1].Type, Cce.NonNull(OutParams[0]).TypedIdent.Type);
}
}
}
Expand Down Expand Up @@ -3692,7 +3692,7 @@ public static class Emitter
public static void Emit(this List<Declaration /*!*/> /*!*/ decls, TokenTextWriter stream)
{
Contract.Requires(stream != null);
Contract.Requires(cce.NonNullElements(decls));
Contract.Requires(Cce.NonNullElements(decls));
bool first = true;
foreach (Declaration d in decls)
{
Expand Down Expand Up @@ -4041,7 +4041,7 @@ public static RE Transform(Block b)
Contract.Assume(g.labelTargets != null);
if (g.labelTargets.Count == 1)
{
return new Sequential(new AtomicRE(b), Transform(cce.NonNull(g.labelTargets[0])));
return new Sequential(new AtomicRE(b), Transform(Cce.NonNull(g.labelTargets[0])));
}
else
{
Expand All @@ -4060,7 +4060,7 @@ public static RE Transform(Block b)
else
{
Contract.Assume(false);
throw new cce.UnreachableException();
throw new Cce.UnreachableException();
}
}
}
Expand Down
Loading

0 comments on commit c62d13a

Please sign in to comment.