Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Upgrade to dotnet8.0 #928

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Upgrade to dotnet8.0 #928

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
de1c567
Upgrade to dotnet8.0
keyboardDrummer Aug 2, 2024
f3d17bb
Rename cce to Cce
keyboardDrummer Aug 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
38 changes: 19 additions & 19 deletions Source/AbstractInterpretation/Traverse.cs
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading