Skip to content

Commit

Permalink
fix: References to built-in types in C# (dafny-lang#4285)
Browse files Browse the repository at this point in the history
  • Loading branch information
fabiomadge authored Jul 15, 2023
1 parent abec131 commit e95d4ce
Show file tree
Hide file tree
Showing 4 changed files with 14 additions and 8 deletions.
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/Modules/ModuleDefinition.cs
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,7 @@ public string SanitizedName {
public string GetCompileName(DafnyOptions options) {
if (compileName == null) {
var externArgs = options.DisallowExterns ? null : Attributes.FindExpressions(this.Attributes, "extern");
var nonExternSuffix = (options.Get(CommonOptionBag.AddCompileSuffix) ? "_Compile" : "");
var nonExternSuffix = (options.Get(CommonOptionBag.AddCompileSuffix) && Name != "_module" && Name != "_System" ? "_Compile" : "");
if (externArgs != null && 1 <= externArgs.Count && externArgs[0] is StringLiteralExpr) {
compileName = (string)((StringLiteralExpr)externArgs[0]).Value;
} else if (externArgs != null) {
Expand Down
14 changes: 7 additions & 7 deletions Source/TestDafny/MultiBackendTest.cs
Original file line number Diff line number Diff line change
Expand Up @@ -164,15 +164,15 @@ private int ForEachCompiler(ForEachCompilerOptions options) {
// Ideally we could hook into the general `dafny` options parsing logic
// and `ICommandSpec` commands instead.
private static bool OptionAppliesToVerifyCommand(string option) {
if (option is "--spill-translation") {
return false;
}
var name = option[2..].Split(':')[0];

if (option.StartsWith("--optimize-erasable-datatype-wrapper")) {
return false;
}
var compileOptions = new List<Option> {
CommonOptionBag.SpillTranslation,
CommonOptionBag.OptimizeErasableDatatypeWrapper,
CommonOptionBag.AddCompileSuffix
}.Select(o => o.Name);

return true;
return !compileOptions.Contains(name);
}

private int RunWithCompiler(ForEachCompilerOptions options, IExecutableBackend backend, string expectedOutput, string? checkFile) {
Expand Down
5 changes: 5 additions & 0 deletions Test/git-issues/git-issue-4284.dfy
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
// RUN: %testDafnyForEachCompiler "%s" -- --compile-suffix

method Main() {
print (true, false), "\n";
}
1 change: 1 addition & 0 deletions Test/git-issues/git-issue-4284.dfy.expect
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(true, false)

0 comments on commit e95d4ce

Please sign in to comment.